[Haskell-cafe] Eta Reduction

[Dan Doel]

Also, with -XImpredicativeTypes:

    > (seq :: (forall x. Show x => x) -> b -> b) undefined ()
    ()



On Wed, Apr 2, 2014 at 9:18 PM, Dan Doel <dan.doel at gmail.com> wrote:

> On Wed, Apr 2, 2014 at 8:40 PM, Niklas Haas <haskell at nand.wakku.to> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140402/78ca4e01/attachment.html>