[project @ 1997-09-03 23:31:30 by sof]

new test

diff --git a/ghc/tests/typecheck/should_fail/tcfail076.hs b/ghc/tests/typecheck/should_fail/tcfail076.hs
new file mode 100644 (file)
index 0000000..7e0b45a
--- /dev/null
+++ b/ghc/tests/typecheck/should_fail/tcfail076.hs
@@ -0,0 +1,33 @@
+{- 
+       From: Ralf Hinze <ralf@uran.informatik.uni-bonn.de>
+       Date: Fri, 15 Aug 1997 15:20:51 +0200 (MET DST)
+
+I *suppose* that there is a bug in GHC's type checker. The following
+program, which I think is ill-typed, passes silently the type checker.
+Needless to say that it uses some of GHC's arcane type extensions.
+-}
+
+{-# OPTIONS -fglasgow-exts #-}
+
+module Test                    (  module Test  )
+where
+
+import GlaExts
+
+data ContT m a         =  KContT ((All res) => (a -> m res) -> m res)
+unKContT (KContT x)    =  x
+
+callcc                 :: ((a -> ContT m b) -> ContT m a) -> ContT m a
+callcc f               =  KContT (\cont -> unKContT (f (\a -> KContT (\cont' -> cont a))) cont)
+
+{-
+`ContT' is a continuation monad transformer. Note that we locally
+qualify over the result type `res' (sometimes called answer or
+output).  IMHO this make it impossible to define control constructs
+like `callcc'. Let's have a closer look: the code of `callcc' contains
+the subexpression `KContT (\cont' -> cont a)'. To be well-typed the
+argument of `KContT' must have the type `(All res) => (a -> m res) -> m
+res'. Quantification is not possible, however, since the type variable
+in `cont's type cannot be forall'd, since it also appears at an outer
+level.  Right? Or wrong?
+-}