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