Type-checking failure with RankNTypes and RebindableSyntax

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 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.

Trac metadata

Trac field	Value
Version	7.10.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture