13 files changed, 349 insertions, 0 deletions
diff --git a/testsuite/tests/boxy/Base1.hs b/testsuite/tests/boxy/Base1.hs
new file mode 100644
index 0000000000..88e7e80f17
--- /dev/null
+++ b/testsuite/tests/boxy/Base1.hs
@@ -0,0 +1,30 @@
+{-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags #-}
+
+module Base1 where 
+-- basic examples of impredicative instantiation of variables 
+
+data MEither a b = MLeft a 
+                 | MRight b 
+                 | MEmpty
+
+type Sid = forall a. a -> a 
+
+-- no need for impredicativity 
+test0 = MRight id 
+
+-- requires impredicativity 
+test1 :: Sid -> MEither Sid b
+test1 fid = MLeft fid 
+
+test2 :: MEither b Sid -> Maybe (Sid,Sid) 
+test2 m = case (test1 id) of 
+             MLeft x -> case m of 
+                          MRight y -> Just (x,y) 
+                          _ -> Nothing 
+             _ -> Nothing
+
+test3 :: MEither a b -> b
+test3 (MRight x) = x 
+
+test4 = test3 (test1 id) 
+
diff --git a/testsuite/tests/boxy/Church1.hs b/testsuite/tests/boxy/Church1.hs
new file mode 100644
index 0000000000..fccaac7d8c
--- /dev/null
+++ b/testsuite/tests/boxy/Church1.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE RankNTypes #-}
+
+module Church1 where 
+-- Church numerals w/o extra type constructors 
+
+type CNat = forall a. (a->a) -> a -> a 
+
+n0 :: CNat 
+n0 = \f z -> z
+
+n1 :: CNat 
+n1 = \f z -> f z 
+
+nsucc :: CNat -> CNat 
+nsucc n = \f z -> f (n f z)
+
+add, mul :: CNat -> CNat -> CNat
+add m n = \f -> \a -> m f (n f a)
+mul m n = \f -> \a -> m (n f) a
+
+-- already works with GHC 6.4 
+exp0 :: CNat -> CNat -> CNat 
+exp0 m n = n m
+
+
+exp1 :: CNat -> CNat -> CNat 
+exp1 m n = (n::((CNat -> CNat) -> CNat -> CNat)) (mul m) n1  -- checks with app rule 
+
diff --git a/testsuite/tests/boxy/Church2.hs b/testsuite/tests/boxy/Church2.hs
new file mode 100644
index 0000000000..c360bb3a8b
--- /dev/null
+++ b/testsuite/tests/boxy/Church2.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE RankNTypes #-}
+
+module Church2 where 
+-- Church numerals w/o extra type constructors: Should fail
+
+type CNat = forall a. (a->a) -> a -> a 
+
+n0 :: CNat 
+n0 = \f z -> z
+
+n1 :: CNat 
+n1 = \f z -> f z 
+
+nsucc :: CNat -> CNat 
+nsucc n = \f z -> f (n f z)
+
+add, mul :: CNat -> CNat -> CNat
+add m n = \f -> \a -> m f (n f a)
+mul m n = \f -> \a -> m (n f) a
+
+-- already works with GHC 6.4 
+exp0 :: CNat -> CNat -> CNat 
+exp0 m n = n m
+
+-- should fail! 
+exp2 :: CNat -> CNat -> CNat 
+exp2 m n = n (mul m) n1 
diff --git a/testsuite/tests/boxy/Church2.stderr b/testsuite/tests/boxy/Church2.stderr
new file mode 100644
index 0000000000..ea7613733b
--- /dev/null
+++ b/testsuite/tests/boxy/Church2.stderr
@@ -0,0 +1,12 @@
+
+Church2.hs:27:14:
+    Couldn't match expected type `CNat'
+	   against inferred type `(a -> a) -> a -> a'
+    In the first argument of `n', namely `(mul m)'
+    In the expression: n (mul m) n1
+    In the definition of `exp2': exp2 m n = n (mul m) n1
+
+*** This error message is not helpful,
+*** and the test should fail, not pass
+*** These comments are here to make sure the output
+*** doesn't match!
diff --git a/testsuite/tests/boxy/Compose.hs b/testsuite/tests/boxy/Compose.hs
new file mode 100644
index 0000000000..0caa84cbe1
--- /dev/null
+++ b/testsuite/tests/boxy/Compose.hs
@@ -0,0 +1,26 @@
+{-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags -XEmptyDataDecls -XGADTs #-}
+
+-- Trac #1118
+
+module Compose where
+
+data Z
+data S n
+
+data List n a where
+    Nil :: List Z a
+    (:-) :: a -> List n a -> List (S n) a
+
+data Hold a = Hold (forall m . a m -> a (S m))
+
+compose' :: List n (Hold a) -> a (S Z) -> a (S n)
+compose' Nil x = x
+compose' ((Hold f) :- fs) x = f (compose' fs x)
+
+compose :: List n (forall m . a m -> a (S m)) -> a (S Z) -> a (S n)
+compose Nil x = x
+compose (f :- fs) x = f (compose fs x)
+
+composeS :: [forall m . a m -> a m] -> a n -> a n
+composeS [] x = x
+composeS (f:fs) x = f (composeS fs x)
diff --git a/testsuite/tests/boxy/Makefile b/testsuite/tests/boxy/Makefile
new file mode 100644
index 0000000000..9a36a1c5fe
--- /dev/null
+++ b/testsuite/tests/boxy/Makefile
@@ -0,0 +1,3 @@
+TOP=../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/boxy/PList1.hs b/testsuite/tests/boxy/PList1.hs
new file mode 100644
index 0000000000..80fac96d9f
--- /dev/null
+++ b/testsuite/tests/boxy/PList1.hs
@@ -0,0 +1,26 @@
+{-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags #-}
+
+module PList1 where 
+-- Polymorphic lists 1: requires smart-app-res  
+
+type Sid = forall a . a -> a
+
+ids :: [Sid] 
+ids = [] 
+
+-- requires smart-app-res 
+test0 :: [Sid] 
+test0 = (\x->x) : ids 
+
+test1 :: [Sid]	-- SLPJ added
+test1 = ids ++ test0 
+
+test2 :: [Sid] 
+test2 = tail test1 
+
+
+test3 :: [Sid]	-- SLPJ added
+test3 = reverse test2 
+test4 = (tail::([Sid]->[Sid])) test2 
+
+test5 = (head::([Sid]->Sid)) test2 
+\ No newline at end of file
diff --git a/testsuite/tests/boxy/PList2.hs b/testsuite/tests/boxy/PList2.hs
new file mode 100644
index 0000000000..581ce086a9
--- /dev/null
+++ b/testsuite/tests/boxy/PList2.hs
@@ -0,0 +1,27 @@
+{-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags #-}
+
+module PList2 where 
+-- Polymorphic lists 2: require smart-app-arg & smart-app-res: Should fail w/o smart-app-arg
+
+type Sid = forall a. a -> a 
+
+ids :: [Sid] 
+ids = [] 
+
+test0 :: [Sid] 
+test0 = (\x -> x):ids  -- requires smart-app-res
+
+test1 :: [Sid]	-- Added SLPJ
+test1 = ids ++ test0 
+
+test2 :: [Sid]
+test2 = tail test1 -- requires smart-app-arg 
+
+test3 :: [Sid] 	-- Added SLPJ 
+test3 = reverse test2 
+
+test4 :: Sid
+test4 = head ids  --requires smart-app-arg
+
+test5 :: Sid
+test5 = head ids  -- still requires smart-app-arg 
diff --git a/testsuite/tests/boxy/SystemF.hs b/testsuite/tests/boxy/SystemF.hs
new file mode 100644
index 0000000000..3f5b4b957a
--- /dev/null
+++ b/testsuite/tests/boxy/SystemF.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE Rank2Types #-}
+
+module SystemF where 
+-- System-F examples 
+
+
+type Sid = forall a. a -> a 
+
+apply :: forall a b . (a -> b) -> a -> b 
+apply f g = f g 
+
+hr :: (forall a. a -> a) -> (Int,Bool)
+hr f = (f 3,f True)
+
+test0 = apply hr id   -- requires smart-app-arg 
+
+selfApp :: Sid -> Sid 
+selfApp x = (x::(Sid -> Sid)) x 
+
+
+
diff --git a/testsuite/tests/boxy/T2193.hs b/testsuite/tests/boxy/T2193.hs
new file mode 100644
index 0000000000..904a13721c
--- /dev/null
+++ b/testsuite/tests/boxy/T2193.hs
@@ -0,0 +1,13 @@
+{-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags #-}
+
+module Main where
+
+data Foo x y = Foo {foo1 :: x, foo2 :: y}
+instance Functor (Foo x) where
+    fmap f (Foo x y) = Foo x (f y)
+
+bar :: a -> Foo (forall s. s) a
+bar a = Foo undefined a
+
+main = print (foo2 (fmap (*2) (bar 2)))
+
diff --git a/testsuite/tests/boxy/T2193.stdout b/testsuite/tests/boxy/T2193.stdout
new file mode 100644
index 0000000000..b8626c4cff
--- /dev/null
+++ b/testsuite/tests/boxy/T2193.stdout
@@ -0,0 +1 @@
+4
diff --git a/testsuite/tests/boxy/all.T b/testsuite/tests/boxy/all.T
new file mode 100644
index 0000000000..0294d01629
--- /dev/null
+++ b/testsuite/tests/boxy/all.T
@@ -0,0 +1,11 @@
+# Boxy-type tests
+
+test('Base1',    expect_broken(4295), compile, [''])
+test('Church1',  expect_broken(4295), compile, [''])
+test('Church2',  expect_broken(1330), compile_fail, [''])
+test('PList1',   expect_broken(4295), compile, [''])
+test('PList2',   expect_broken(4295), compile, [''])
+test('SystemF',  expect_broken(4295), compile, [''])
+test('boxy',     expect_broken(4295), compile, [''])
+test('Compose',  normal, compile, [''])
+test('T2193',    normal, compile_and_run, [''])
diff --git a/testsuite/tests/boxy/boxy.hs b/testsuite/tests/boxy/boxy.hs
new file mode 100644
index 0000000000..4d2bd029b1
--- /dev/null
+++ b/testsuite/tests/boxy/boxy.hs
@@ -0,0 +1,124 @@
+{-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags -XScopedTypeVariables #-}
+
+module ShouldCompile where
+
+
+{-------- Examples from the paper ---------}
+
+f :: (forall a. [a] -> a) -> (Int, Char)
+f get = (get [1,2], get ['a', 'b', 'c'])
+
+g :: Maybe (forall a. [a] -> a) -> (Int, Char)
+g Nothing = (0, '0')
+g (Just get) = (get [1,2], get ['a','b','c'])
+
+sing x = [x] 
+
+id1 :: forall a. a -> a
+id1 = id
+
+{-
+ids :: [forall a. a -> a]  
+ids = [id1,id1] 
+
+t1 :: [forall a. a -> a]
+t1 = tail ids
+
+t2 :: [forall a. a -> a]
+t2 = sing id
+
+t3 :: forall a. a -> a
+t3 = head ids
+-}
+
+{--------------- Examples from QMLF paper -------------------}
+
+qF :: (forall a. a -> a -> a) -> (Bool, Char)
+qF choose = (choose True False, choose 'a' 'b')
+
+qG :: (forall a. a -> a -> a) -> (forall a. a -> a) -> (forall g. (g -> g) -> (g -> g))
+qG choose id = choose id
+
+qH :: (forall a. a -> a -> a) -> (forall a. a -> a) -> (forall b. b -> b) -> (forall b. b -> b)
+qH choose id = choose id
+   
+choose :: forall a. a -> a -> a
+choose x y = x
+
+{-
+impred1 :: (Bool, Char)
+impred1 = qF $ choose  --- impredicative instantiation for $
+
+impred2 :: (forall a. a -> a -> a) -> (Bool, Char)
+impred2 = id qF
+-}
+
+{------ Examples for Garrique/Remy paper -------}
+
+--- all of these currently work in GHC with higher-rank types
+
+self1 :: (forall a. a -> a) -> (forall a. a -> a)
+self1 f = f f 
+
+self2 :: (forall a. a -> a) -> b -> b
+self2 f = f f 
+
+gr1 = self1 id
+
+gr2 = self2 id
+
+gr3 = (\(u :: (forall a. a -> a) -> (forall a. a -> a)) -> u id) self1
+
+{------------ Church numerals ----------}
+
+type Church = forall a. a -> (a -> a) -> a
+
+z :: Church
+z = \z -> \f -> z
+
+s :: Church -> Church
+s = \n -> \z -> \f -> f (n z f)
+
+fold :: Church -> a -> (a -> a) -> a
+fold n f z = n f z
+
+{-
+mul :: Church -> Church -> Church
+mul m n = \f -> \a -> m (n f) a
+
+exp :: Church -> Church -> Church
+exp m n = n (mul m) (s z)
+
+idC :: Church -> Church
+idC x = fold x s z
+
+inc :: Church -> Church
+inc x = fold x s (s z)
+-}
+
+{------- fix for higher rank types ---------}
+
+data Tree a = Branch a (Tree (a,a)) | Leaf
+
+type MapTree = forall a b. (a -> b) -> Tree a -> Tree b
+cross f (a,b) = (f a,f b)
+
+-- I think this should work in GHC now, but it doesn't
+-- fix specialized to higher-rank type
+fixMT :: (MapTree -> MapTree) -> MapTree
+fixMT f = f (fixMT f)
+
+mapTree' = fixMT (\ (mapTree :: MapTree) -> \f tree -> case tree of
+ 			    Branch a t -> Branch (f a) (mapTree (cross f) t)
+ 			    Leaf -> Leaf)
+
+-- polymorphic fix
+fix :: (a -> a) -> a
+fix f = f (fix f)
+
+
+-- mapTree'' :: MapTree
+mapTree'' = (fix :: (MapTree -> MapTree) -> MapTree)
+	       (\ mapTree -> \f tree -> case tree of
+ 			    Branch a t -> Branch (f a) (mapTree (cross f) t)
+ 			    Leaf -> Leaf)