Fix incorrectly bound type variables

SystemF/check.hs

@@ -4,7 +4,7 @@ import Control.Monad
 import SystemFImpl
 import HaskellOutput
 
-data Abs = Term | Type
+data Abs = Term | Type deriving Show
 
 
 ----
@@ -29,12 +29,13 @@ nonvarterm var n = oneof [liftM2 TmAbs  (genterm (Term:var) (2*(n `div` 3))) nex
 -- Types
 ----
 gentype :: [Abs] -> Int -> Gen Type
+gentype []  0 = return TyBase
 gentype var 0 = oneof [return TyBase,
                        liftM  TyVar $ gentypevar var]
 gentype var n = 
         frequency [(n^3 - n^2,
                           oneof [ liftM2 TyArr nextTy nextTy,
-                                  liftM  TyAll nextTy
+                                  liftM  TyAll $ gentype (Type:var) (2*(n `div` 3))
                                   ]),
                    (n^2,
                           gentype var 0)]
@@ -59,14 +60,17 @@ gentermvar' (Term:as) = frequency [(prob, return $ mkvar $ reverse $ Term:as),
                                       prob = 1000 `div` (length (Term:as))
 
 gentypevar :: [Abs] -> Gen HNat
-gentypevar []        = gentypevar' []
-gentypevar (Type:as) = gentypevar' $ reverse as -- First abstraction is a Type => skip it
-gentypevar (Term:as) = gentypevar' $ reverse (Type:as)
+gentypevar (_:as) = gentypevar' . stripTerms $ as
+
+stripTerms :: [Abs] -> [Abs]
+stripTerms (Term:as) = stripTerms as
+stripTerms (Type:as) = Type:(stripTerms as)
+stripTerms []        = []
 
 gentypevar' :: [Abs] -> Gen HNat
 gentypevar' []        = return $ mkvar []
 gentypevar' (Term:as) = gentypevar' as
-gentypevar' (Type:as) = frequency [(prob, return $ mkvar $ reverse $ Term:as),
+gentypevar' (Type:as) = frequency [(prob, return $ mkvar $ reverse $ Type:as),
                                    (1000-prob, gentypevar' as)]
                                  where 
                                      prob = 1000 `div` (length (Type:as))