Impredicative types and forall regression in 8.0 ?

Vincent Hanquez tab at snarc.org
Mon Feb 15 09:44:45 UTC 2016


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


More information about the ghc-devs mailing list