[GHC] #10646: Adding GADTs extension makes RankNTypes code fail to compile.

16 Jul 2015

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

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10646
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler