From f9e63feb98e5cf0fb5dcd166a4d785b7edb93152 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= <anka.213@gmail.com>
Date: Fri, 20 Sep 2024 12:56:37 +0200
Subject: [PATCH] Add test case for RankNTypes #352

---
 test/AllTests.agda        |  2 ++
 test/RankNTypes.agda      | 22 ++++++++++++++++++++++
 test/golden/AllTests.hs   |  1 +
 test/golden/RankNTypes.hs | 14 ++++++++++++++
 4 files changed, 39 insertions(+)
 create mode 100644 test/RankNTypes.agda
 create mode 100644 test/golden/RankNTypes.hs

diff --git a/test/AllTests.agda b/test/AllTests.agda
index 3bad8422..c62f9f24 100644
--- a/test/AllTests.agda
+++ b/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
diff --git a/test/RankNTypes.agda b/test/RankNTypes.agda
new file mode 100644
index 00000000..4cd0987d
--- /dev/null
+++ b/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 #-}
diff --git a/test/golden/AllTests.hs b/test/golden/AllTests.hs
index 1f5d6f57..f970e50c 100644
--- a/test/golden/AllTests.hs
+++ b/test/golden/AllTests.hs
@@ -81,6 +81,7 @@ import Issue302
 import Issue309
 import Issue317
 import Issue353
+import RankNTypes
 import ErasedPatternLambda
 import CustomTuples
 import ProjectionLike
diff --git a/test/golden/RankNTypes.hs b/test/golden/RankNTypes.hs
new file mode 100644
index 00000000..4ed6d3ad
--- /dev/null
+++ b/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
+