Impredicative types and forall regression in 8.0 ?

[Richard Eisenberg]

More generally, ImpredicativeTypes is utterly broken and has been for several release cycles. Sometimes, when you're lucky, it allows you to do something pretty neat. However, you need to hope that your luck remains strong between minor releases. It is an unsupported feature.

I should note that TypeApplications required fairly serious surgery to the way type checking works. Given the general brokenness of ImpredicativeTypes, I didn't spend effort in trying to retain behavior with ImpredicativeTypes on. (I didn't actively try to make it worse, either.) It does not surprise me in the slightest that 8.0's ImpredicativeTypes is quite different from previous versions'.

Richard

On Feb 15, 2016, at 5:49 AM, Adam Gundry <adam at well-typed.com> wrote:

> Hi Vincent,
> 
> On 15/02/16 09:44, Vincent Hanquez wrote:
>> I recently came across a compilation problem on 8.0 that do not trigger
>> on < 8.0. I've reduced the issue to this snippet with Rank2Types:
>> 
>>    type Action = (forall a . Show a => a) -> Int
>>    data Command = Command (Maybe Action)
>> 
>>    com1 = Command Nothing
>> 
>> With GHC 7.0 to 7.10, this compile and works.
> 
> This shouldn't be accepted without ImpredicativeTypes[*], but GHC
> versions prior to 8.0 failed to look through the type synonym. Note that
> if you say
> 
>    data Command = Command (Maybe ((forall a . Show a => a) -> Int))
> 
> then earlier versions report an error. Take a look at GHC ticket #10194
> for more details: https://ghc.haskell.org/trac/ghc/ticket/10194
> 
>> However on GHC 8.0, I now have:
>> 
>> Test.hs:19:16: error:
>>    • Cannot instantiate unification variable ‘a0’
>>      with a type involving foralls: Action
>>        GHC doesn't yet support impredicative polymorphism
>>    • In the first argument of ‘Command’, namely ‘Nothing’
>>      In the expression: Command Nothing
>>      In an equation for ‘com1’: com1 = Command Nothing
>> 
>> I workarounded it by "inlining" the maybe and creating a proper wrapping
>> type:
>> 
>>    data Action2 = Action2 ((forall a . Show a => a) -> Int) | NoAction2
>>    data Command2 = Command2 Action2
>> 
>>    com2 = Command2 NoAction2
> 
> This looks like a reasonable alternative.
> 
> Hope this helps,
> 
> Adam
> 
> [*] And if you turn on ImpredicativeTypes, GHC may or may not do the
> right thing.
> 
> 
> -- 
> Adam Gundry, Haskell Consultant
> Well-Typed LLP, http://www.well-typed.com/
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>