Support generating RankN haskell types. Fixes #352

src/Agda2Hs/Compile.hs

@@ -35,6 +35,7 @@ initCompileEnv :: TopLevelModuleName -> SpecialRules -> CompileEnv
 initCompileEnv tlm rewrites = CompileEnv
   { currModule        = tlm
   , minRecordName     = Nothing
+  , isNestedInType    = False
   , locals            = []
   , compilingLocal    = False
   , whereModules      = []

src/Agda2Hs/Compile/Type.hs

@@ -93,6 +93,8 @@ compileType t = do
 
   instantiate t >>= \case
     Pi a b -> do
+      reportSDoc "agda2hs.compile.type" 13 $ text "Compiling pi type (" <+> prettyTCM (absName b)
+        <+> text ":" <+> prettyTCM a <+> text ") -> " <+> prettyTCM (unAbs b)
       let compileB = underAbstraction a b (compileType . unEl)
       compileDomType (absName b) a >>= \case
         DomType _ hsA -> Hs.TyFun () hsA <$> compileB
@@ -248,15 +250,21 @@ compileDomType x a =
     DOInstance -> DomConstraint . Hs.TypeA () <$> compileType (unEl $ unDom a)
     DOType     -> do
       -- We compile (non-erased) type parameters to an explicit forall if they
-      -- come from a module parameter.
+      -- come from a module parameter or if we are in a nested position inside the type.
+      reportSDoc "agda2hs.compile.type" 15 $ text "Compiling forall type:" <+> prettyTCM a
+      isNested <- asks isNestedInType
       ctx <- getContextSize
       npars <- size <$> (lookupSection =<< currentModule)
-      if ctx < npars
-        then do
+      if
+        | isNested -> do
+          tellExtension Hs.RankNTypes
+          -- tellExtension Hs.ExistentialQuantification
+          return $ DomForall $ Hs.UnkindedVar () $ Hs.Ident () x
+        | ctx < npars -> do
           tellExtension Hs.ScopedTypeVariables
           return $ DomForall $ Hs.UnkindedVar () $ Hs.Ident () x
-        else return $ DomDropped
-    DOTerm     -> uncurry DomType <$> compileTypeWithStrictness (unEl $ unDom a)
+        | otherwise -> return DomDropped
+    DOTerm     -> fmap (uncurry DomType) . withNestedType . compileTypeWithStrictness . unEl $ unDom a
 
 compileTeleBinds :: Telescope -> C [Hs.TyVarBind ()]
 compileTeleBinds EmptyTel = return []

src/Agda2Hs/Compile/Types.hs

@@ -78,6 +78,8 @@ data CompileEnv = CompileEnv
   -- ^ the current module we are compiling
   , minRecordName :: Maybe ModuleName
   -- ^ keeps track of the current minimal record we are compiling
+  , isNestedInType :: Bool
+  -- ^ if we're inside an argument of a type and need an explicit forall
   , locals :: LocalDecls
   -- ^ keeps track of the current clause's where declarations
   , compilingLocal :: Bool

src/Agda2Hs/Compile/Utils.hs

@@ -275,6 +275,9 @@ checkInstance u = do
     checkInstanceElim (Proj _ f) =
       unlessM (isInstance . defArgInfo <$> getConstInfo f) illegalInstance
 
+withNestedType :: C a -> C a
+withNestedType = local $ \e -> e { isNestedInType = True }
+
 compileLocal :: C a -> C a
 compileLocal = local $ \e -> e { compilingLocal = True }
 

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
+