Re: [Haskell-cafe] Eta Reduction

Also, with -XImpredicativeTypes: > (seq :: (forall x. Show x => x) -> b -> b) undefined () () On Wed, Apr 2, 2014 at 9:18 PM, Dan Doel wrote:

On Wed, Apr 2, 2014 at 8:40 PM, Niklas Haas wrote:

...

Oh, fair point; this particular F apparently doesn't break it but if you remove the Show x constraint, it does.

Actually, is that a bug in GHC?

...

λ newtype F = F (forall x. Show x => x -> String) λ F undefined `seq` () () λ undefined `seq` () *** Exception: Prelude.undefined

I'm not sure how to interpret this output.

This is pretty weird, but here's what I think is going on:

F requires an argument of type forall x. Show x => x -> String. This requires abstracting over a dictionary for Show x. So at the core level, this gets expanded to something like:

\showd -> undefined

which is non-bottom.

Even if you annotate undefined with the above type, You'll probably end up with:

(\showd -> undefined) defaultd `seq` ()

after GHC reinstantiates the polymorphic type and then defaults, which will be undefined. So you can only observe this by wrapping the polymorphic expression in a newtype, to keep it abstracted.

I don't know that this qualifies as a bug, but it's definitely pretty subtle behavior.

-- Dan