Impredicative types and forall regression in 8.0 ?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Impredicative types and forall regression in 8.0 ?

Vincent Hanquez
Hi GHC-Devs,

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.
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

Any idea why this is triggering this issue in GHC 8.0 ? Is this
something that need fixing maybe ?

Cheers,
--
Vincent
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Impredicative types and forall regression in 8.0 ?

Adam Gundry-2
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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Impredicative types and forall regression in 8.0 ?

Richard Eisenberg-2
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 <[hidden email]> 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
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Impredicative types and forall regression in 8.0 ?

Vincent Hanquez
In reply to this post by Adam Gundry-2


On 15/02/2016 10:49, Adam Gundry 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
Ok, make sense; After reading what ImpredicativeTypes are, I can see the
difference in the construct.

Thanks,
--
Vincent
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs