Enabling GADTs breaks Rank2Types code compilation - Why?
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
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,
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- Regards, Austin
At Tue, 31 May 2011 21:30:01 -0500, austin seipp wrote:
The short story is thus: when you turn on GADTs, it also now turns on another extension implicitly (MonoLocalBinds) which restricts let generalization...
You can find a little more info about the change here:
http://hackage.haskell.org/trac/ghc/blog/LetGeneralisationInGhc7
Thanks for the precise response I needed. It definitely felt like I was running up against something like the monomorphism restriction, but my bindings were function and not pattern bindings, so I couldn't understand what was going on. I had even gone and re-read the GHC documentation (http://www.haskell.org/ghc/docs/7.0-latest/html/users_guide/data-type-extens...), which says that -XGADTs enables -XRelaxedPolyRec, but makes no mention of -XMonoLocalBinds. It might save users some frustration if the GHC manual and/or the error message mentioned something about let bindings being monomorphic by default. On a related note, I already started fixing this in my code by enabling ScopedTypeVariables, as it's too much of a pain to do this without that extension. I usually try to use the minimum number of extensions possible to future-proof my code. However, is it reasonable to conclude that if I'm going to use GADTs anyway, then additionally enabling ScopedTypeVariables doesn't really make my code any less future-proof? Thanks, David
On Tue, May 31, 2011 at 11:13 PM,
It definitely felt like I was running up against something like the monomorphism restriction, but my bindings were function and not pattern bindings, so I couldn't understand what was going on. I had even gone and re-read the GHC documentation (http://www.haskell.org/ghc/docs/7.0-latest/html/users_guide/data-type-extens...), which says that -XGADTs enables -XRelaxedPolyRec, but makes no mention of -XMonoLocalBinds.
It might save users some frustration if the GHC manual and/or the error message mentioned something about let bindings being monomorphic by default.
I'd agree it should be documented behavior and put somewhere in the users guide. It's bitten a few people before, but Simon's blog post is the only reference I've really seen on the matter I think.
However, is it reasonable to conclude that if I'm going to use GADTs anyway, then additionally enabling ScopedTypeVariables doesn't really make my code any less future-proof?
I'd say so. For nontrivial extensions like this, I'd wager you're likely to rely on GHC inadvertently in some form anyway - a result of all this new typechecking stuff for example, is that GHC can correctly infer types for more programs involving these complex extensions. You may end up relying on such inference in the future, as we've already seen happen here, which could break things down the road. ScopedTypeVariables seems much more simple and future proof in this regard, IMO. -- Regards, Austin
participants (2)
-
austin seipp -
dm-list-haskell-cafe＠scs.stanford.edu