Adding GADTs extension makes RankNTypes code fail to compile.
The failing example:
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
data I a = I a
example :: String -> I a -> String
example str x = withContext x s
where
s i = "Foo" ++ str
withContext :: I a -> (forall b. I b -> c) -> c
withContext x f = f x
Without GADTs
, this compiles and works fine:
λ *Main > example "bar" (P 'a' "quux")
"Foobar"
With GADTs
the code fails to compile with an error:
ex.hs:7:31:
Couldn't match type ‘t0’ with ‘I b’
because type variable ‘b’ would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context: I b -> String
at ex.hs:7:17-31
Expected type: I b -> String
Actual type: t0 -> [Char]
Relevant bindings include s :: t0 -> [Char] (bound at ex.hs:9:5)
In the second argument of ‘withContext’, namely ‘s’
In the expression: withContext x s
Failed, modules loaded: none.
Yet, if I add type annotation for s
, everything seems to be fine:
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
data I a = I a
example :: String -> I a -> String
example str x = withContext x s
where
s :: I a -> String
s i = "Foo" ++ str
withContext :: I a -> (forall b. I b -> c) -> c
withContext x f = f x
I tried to make the failing example smaller, but seems that every bit participates. The use of str
inside s
especially.
Is there some bug hiding inside GADTs related stuff?
Tried with 7.8.4 and 7.10.1