#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