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 |