1 files changed, 124 insertions, 0 deletions
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)