Impredicative types and forall regression in 8.0 ?

[Adam Gundry]

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/