>>3
The types of elements popped by word have to follow some rule. Of course you could probably make a word where the most simple way to describe that rule would be the word itself, and I don't know how a type system would handle that. Checking all possible inputs would quickly break down, so I'd assume it would be similar to proving the theorem that the wrong types could never be passed in given the rest of the program. Maybe someone smarter than me could think of something.