ghc/tests/typecheck/should_fail/tcfail076.hs

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