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