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 +