#10646: Adding GADTs extension makes RankNTypes code fail to compile. -------------------------------------+------------------------------------- Reporter: phadej | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Old description:

The failing example:

{{{#!hs {-# 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:

{{{#!hs {-# 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?

New description: The failing example: {{{#!hs {-# 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: {{{#!hs {-# 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 -- Comment (by phadej): Happens -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10646#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10646: Adding GADTs extension makes RankNTypes code fail to compile. -------------------------------------+------------------------------------- Reporter: phadej | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1 checker) | Keywords: Resolution: invalid | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by phadej): Thanks to you for the explanation! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10646#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler