From d5039ed963b1139ec73bd4fe616fd1f101e77677 Mon Sep 17 00:00:00 2001 From: sof Date: Wed, 3 Sep 1997 23:31:30 +0000 Subject: [PATCH] [project @ 1997-09-03 23:31:30 by sof] new test --- ghc/tests/typecheck/should_fail/tcfail076.hs | 33 ++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 ghc/tests/typecheck/should_fail/tcfail076.hs diff --git a/ghc/tests/typecheck/should_fail/tcfail076.hs b/ghc/tests/typecheck/should_fail/tcfail076.hs new file mode 100644 index 0000000..7e0b45a --- /dev/null +++ b/ghc/tests/typecheck/should_fail/tcfail076.hs @@ -0,0 +1,33 @@ +{- + From: Ralf Hinze + 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? +-} -- 1.7.10.4