Add test case for RankNTypes #352

test/AllTests.agda

@@ -86,6 +86,7 @@ import Issue302
 import Issue309
 import Issue317
 import Issue353
+import RankNTypes
 import ErasedPatternLambda
 import CustomTuples
 import ProjectionLike
@@ -173,6 +174,7 @@ import Issue302
 import Issue309
 import Issue317
 import Issue353
+import RankNTypes
 import ErasedPatternLambda
 import CustomTuples
 import ProjectionLike

test/RankNTypes.agda

@@ -0,0 +1,22 @@
+{-# FOREIGN AGDA2HS
+{-# LANGUAGE Haskell98 #-}
+#-}
+
+data MyBool : Set where
+    MyTrue : MyBool
+    MyFalse : MyBool
+{-# COMPILE AGDA2HS MyBool #-}
+
+rank2ForallUse : (∀ (a : Set) → a → a) → MyBool
+rank2ForallUse f = f MyBool MyTrue
+{-# COMPILE AGDA2HS rank2ForallUse #-}
+
+module _  (f : ∀ (a : Set) → a → a) where
+    rank2Module : MyBool
+    rank2Module = f MyBool MyTrue
+    {-# COMPILE AGDA2HS rank2Module #-}
+
+-- ExistentialQuantification: Not supported yet, but also no error message yet
+-- data Exist : Set₁ where
+--     MkExist : ∀ (a : Set) → a → Exist
+-- {-# COMPILE AGDA2HS Exist #-}

test/golden/AllTests.hs

@@ -81,6 +81,7 @@ import Issue302
 import Issue309
 import Issue317
 import Issue353
+import RankNTypes
 import ErasedPatternLambda
 import CustomTuples
 import ProjectionLike

test/golden/RankNTypes.hs

@@ -0,0 +1,14 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE Haskell98 #-}
+
+module RankNTypes where
+
+data MyBool = MyTrue
+            | MyFalse
+
+rank2ForallUse :: (forall a . a -> a) -> MyBool
+rank2ForallUse f = f MyTrue
+
+rank2Module :: (forall a . a -> a) -> MyBool
+rank2Module f = f MyTrue
+