[GHC] #10381: Type-checking failure with RankNTypes and RebindableSyntax

4 May 2015

      #10381: Type-checking failure with RankNTypes and RebindableSyntax
-------------------------------------+-------------------------------------
              Reporter:  goldfire    |             Owner:
                  Type:  bug         |            Status:  new
              Priority:  normal      |         Milestone:
             Component:  Compiler    |           Version:  7.10.1
              Keywords:              |  Operating System:  Unknown/Multiple
          Architecture:              |   Type of failure:  None/Unknown
  Unknown/Multiple                   |        Blocked By:
             Test Case:              |   Related Tickets:
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
 When I say

 {{{
 {-# LANGUAGE RebindableSyntax, RankNTypes #-}

 module Bug where

 import Prelude ( String, undefined )

 newtype Cont r a = Cont { runCont :: (forall i. a i -> r) -> r }

 (>>=) :: Cont r a -> (forall i. a i -> Cont r b) -> Cont r b
 ma >>= fmb
   = Cont (\k -> runCont ma (\a -> runCont (fmb a) k))

 fail :: String -> Cont r a
 fail = undefined

 return :: a i -> Cont r a
 return x = Cont (\k -> k x)

 foo :: Cont r []
 foo = do
   bar <- foo
   return bar
 }}}

 I get

 {{{
 Bug.hs:21:3:
     Couldn't match type ‘i0’ with ‘i’
       because type variable ‘i’ would escape its scope
     This (rigid, skolem) type variable is bound by
       a type expected by the context: [i] -> Cont r []
       at Bug.hs:21:3-12
     Expected type: Cont r [] -> ([i0] -> Cont r []) -> Cont r []
       Actual type: Cont r []
                    -> (forall i. [i] -> Cont r []) -> Cont r []
     In a stmt of a 'do' block: bar <- foo
     In the expression:
       do { bar <- foo;
            return bar }
     In an equation for ‘foo’:
         foo
           = do { bar <- foo;
                  return bar }
 }}}

 Yet,

 {{{
 baz :: Cont r []
 baz = baz >>= \bar -> return bar
 }}}

 at the end of this file compiles just fine. I had thought that `foo` and
 `baz` are entirely equivalent.

 Note that, with normal `do` notation, it ''is'' possible to do a GADT-like
 pattern-match with `<-`, without anyone's brain exploding.

 Some background: I'm attempting to write a type-checker for a simply-typed
 lambda calculus that uses GADTs to help me write the evaluation functions.
 The actual lambda-calculus bit has gone swimmingly; you can see it
 [https://github.com/goldfirere/glambda/blob/master/Language/Glambda/Exp.hs
 here]. But now I'm writing a type-checker, which has to take a possibly-
 ill-typed expression of type `UExp` and convert it to an `Exp ctx ty`,
 which is guaranteed to have type `ty` in context (a list of types) `ctx`.
 I can't just write

 {{{
 check :: UExp -> Maybe (Exp '[] ty)
 }}}

 because the type has to be an ''output''. I could use existentials, but I
 find continuation-passing style to be easier to work with. But then the
 syntax goes all terrible. So, I want the `Cont` monad. Except that doesn't
 deal with these existentially-bound type variables at all. And, without
 doing any category theory, I have a very strong hunch that my CPS-with-
 extra-type-variables does not form a Monad. But, no matter, I'll just use
 `RebindableSyntax` and define my enhanced `Cont` not-a-monad with
 appropriate operators, and get my nice syntax back.

 But it doesn't work, as we see with this ticket. :(

 Clearly, this isn't really blocking me, but it makes me a touch sad not to
 use the nice syntax.

 `foo` fails to type-check in both 7.8 and 7.10, although the error
 messages are quite different (7.10 is an improvement). `baz` type-checks
 in both.

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