[Haskell-cafe] Enabling GADTs breaks Rank2Types code compilation - Why?

[austin seipp]

Hi David,

It seems to be a result of the new typechecker and more specifically
the new behavior for GADTs in GHC 7.

The short story is thus: when you turn on GADTs, it also now turns on
another extension implicitly (MonoLocalBinds) which restricts let
generalization. More specifically, it causes GHC to not generalize the
inferred type of polymorphic let bindings (and where clauses too.)
This results in the error you see. GHC telling you that the type of
the argument to mkUnit (in this case mkConst_r) is not polymorphic
enough.

The correct fix is to simply give an explicit type to any polymorphic
let binding. This will let GHC happily compile your program with GADTs
with otherwise no changes needed for correctness. The reasoning for
this behavior is because SPJ et al found it a lot more difficult to
build a robust type inference engine, when faced with non-monomorphic
local bindings. Luckily the overall impact of such a change was
measured to be relatively small, but indeed, it will break some
existing programs. The changes aren't huge though - this program
successfully typechecks with GHC 7.0.3:

-----------
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GADTs #-}

module Main where

mkUnit :: (forall t. t -> m t) -> m ()
mkUnit f = f ()

data Const b a = Const { unConst :: b }

sillyId :: forall r. r -> r
sillyId r = unConst (mkUnit mkConst_r) -- This line can't compile with GADTs
  where mkConst_r :: t -> Const r t
        mkConst_r t = mkConst r t
        mkConst :: b -> t -> Const b t
        mkConst b _ = Const b

main :: IO ()
main = return ()
-----------

There is also another 'fix' that may work, which Simon talks about
himself: you can enable GADTs, but turn off enforced monomorphic local
bindings by giving the extension 'NoMonoLocalBinds'. This will merely
tell GHC to try anyway, but it'd be better to just update your
program, as you can't give as many guarantees about the type
inferencer when you give it such code.

You can find a little more info about the change here:

http://hackage.haskell.org/trac/ghc/blog/LetGeneralisationInGhc7

And in Simon's paper ("Let should not be generalized.")

Hope it helps,

On Tue, May 31, 2011 at 6:42 PM,  <dm-list-haskell-cafe at scs.stanford.edu> wrote:
> I'm using GHC 7.0.2 and running into a compiler error that I cannot
> understand.  Can anyone shed light on the issue for me?  The code does
> not make use of GADTs and compiles just fine without them.  But when I
> add a {-# LANGUAGE GADTs #-} pragma, it fails to compile.
>
> Here is the code:
>
> ====
>
> {-# LANGUAGE Rank2Types #-}
> {-# LANGUAGE GADTs #-}
>
> mkUnit :: (forall t. t -> m t) -> m ()
> mkUnit f = f ()
>
> data Const b a = Const { unConst :: b }
>
> sillyId :: r -> r
> sillyId r = unConst (mkUnit mkConst_r) -- This line can't compile with GADTs
>    where mkConst_r t = mkConst r t
>          mkConst :: b -> t -> Const b t
>          mkConst b _ = Const b
>
> ====
>
> And the error I get is:
>
>    Couldn't match type `t0' with `t'
>      because type variable `t' would escape its scope
>    This (rigid, skolem) type variable is bound by
>      a type expected by the context: t -> Const r t
>    The following variables have types that mention t0
>      mkConst_r :: t0 -> Const r t0
>        (bound at /u/dm/hack/hs/gadt.hs:11:11)
>    In the first argument of `mkUnit', namely `mkConst_r'
>    In the first argument of `unConst', namely `(mkUnit mkConst_r)'
>    In the expression: unConst (mkUnit mkConst_r)
>
> I've found several workarounds for the issue, but I'd like to
> understand what the error message means and why it is caused by GADTs.
>
> Thanks in advance for any help.
>
> David
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



-- 
Regards,
Austin