"Simon Marlow"
Nope. You can't return something without evaluating it to head normal form in Haskell. Every value that is "returned" is a value, never a thunk. If you want to return something unevaluated, you have to wrap it in a constructor.
Actually, there are two possible strategies for who evaluates a thunk to head normal form. The caller or the callee. GHC says that the callee always evaluates to HNF before returning the value. But the language does not force this implementation choice. It is equally possible for an implementation of the function to return a thunk and for the caller to evaluate it if necessary. Both strategies give the same result semantically, since if the value in question is demanded, it gets evaluated.
If there's a Haskell implementation that compiles addHeight in such a way that addHeight _|_ e /= _|_, then I'd say it was wrong
So would we all! Regards, Malcolm