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