Merge branch 'master' of https://github.com/ghc/testsuite
[ghc.git] / testsuite / tests / typecheck / should_fail / tcfail076.hs
1 {-# LANGUAGE RankNTypes #-}
2
3 {-
4 From: Ralf Hinze <ralf@uran.informatik.uni-bonn.de>
5 Date: Fri, 15 Aug 1997 15:20:51 +0200 (MET DST)
6
7 I *suppose* that there is a bug in GHC's type checker. The following
8 program, which I think is ill-typed, passes silently the type checker.
9 Needless to say that it uses some of GHC's arcane type extensions.
10 -}
11
12 module ShouldFail where
13
14 data ContT m a = KContT (forall res. (a -> m res) -> m res)
15 unKContT (KContT x) = x
16
17 callcc :: ((a -> ContT m b) -> ContT m a) -> ContT m a
18 callcc f = KContT (\cont -> unKContT (f (\a -> KContT (\cont' -> cont a))) cont)
19
20 {-
21 `ContT' is a continuation monad transformer. Note that we locally
22 qualify over the result type `res' (sometimes called answer or
23 output). IMHO this make it impossible to define control constructs
24 like `callcc'. Let's have a closer look: the code of `callcc' contains
25 the subexpression `KContT (\cont' -> cont a)'. To be well-typed the
26 argument of `KContT' must have the type `(All res) => (a -> m res) -> m
27 res'. Quantification is not possible, however, since the type variable
28 in `cont's type cannot be forall'd, since it also appears at an outer
29 level. Right? Or wrong?
30 -}