From fdbebb664feb229514ba5cc0a5f817f80e790219 Mon Sep 17 00:00:00 2001
From: Victor Cacciari Miraldo <victor.miraldo@channable.com>
Date: Sat, 8 Jun 2024 17:03:11 +0200
Subject: [PATCH] Closes #309: Ensures we compile pattern variables correctly
 by relying on the existing compileTypeArgs.

---
 src/Agda2Hs/Compile/TypeDefinition.hs | 27 ++++++++++++++-------------
 test/AllTests.agda                    |  2 ++
 test/Issue309.agda                    |  7 +++++++
 test/golden/AllTests.hs               |  1 +
 test/golden/Issue309.hs               |  4 ++++
 5 files changed, 28 insertions(+), 13 deletions(-)
 create mode 100644 test/Issue309.agda
 create mode 100644 test/golden/Issue309.hs

diff --git a/src/Agda2Hs/Compile/TypeDefinition.hs b/src/Agda2Hs/Compile/TypeDefinition.hs
index 3c126ff9..3f064b74 100644
--- a/src/Agda2Hs/Compile/TypeDefinition.hs
+++ b/src/Agda2Hs/Compile/TypeDefinition.hs
@@ -10,17 +10,20 @@ import Agda.Compiler.Backend
 
 import Agda.Syntax.Common ( namedArg )
 import Agda.Syntax.Internal
+import Agda.Syntax.Internal.Pattern
 
 import Agda.TypeChecking.Telescope ( mustBePi )
 
 import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
 import Agda.Utils.Monad
 
-import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..) )
+import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..), compileTypeArgs )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 import Agda2Hs.Compile.Var ( compileDBVar )
 import Agda2Hs.HsUtils
+import Agda.Syntax.Common.Pretty (prettyShow)
+import Agda.TypeChecking.Substitute
 
 
 compileTypeDef :: Hs.Name () -> Definition -> C [Hs.Decl ()]
@@ -28,7 +31,7 @@ compileTypeDef name (Defn {..}) = do
   unlessM (isTransparentFunction defName) $ checkValidTypeName name
   Clause{..} <- singleClause funClauses
   addContext (KeepNames clauseTel) $ do
-    as <- compileTypeArgs defType namedClausePats
+    as <- compileTypePatternArgs defType namedClausePats
     let hd = foldl (Hs.DHApp ()) (Hs.DHead () name) as
     rhs <- compileType $ fromMaybe __IMPOSSIBLE__ clauseBody
     return [Hs.TypeDecl () hd rhs]
@@ -38,17 +41,15 @@ compileTypeDef name (Defn {..}) = do
       [cl] -> return cl
       _    -> genericError "Not supported: type definition with several clauses"
 
-
-compileTypeArgs :: Type -> NAPs -> C [Hs.TyVarBind ()]
-compileTypeArgs ty [] = return []
-compileTypeArgs ty (p:ps) = do
-  (a,b) <- mustBePi ty
-  let rest = underAbstraction a b $ \ty' -> compileTypeArgs ty' ps
-  compileDom a >>= \case
-    DODropped -> rest
-    DOType -> (:) <$> compileTypeArg (namedArg p) <*> rest
-    DOTerm -> genericError "Not supported: type definition with term arguments"
-    DOInstance -> genericError "Not supported: type definition with instance arguments"
+compileTypePatternArgs :: Type -> NAPs -> C [Hs.TyVarBind ()]
+compileTypePatternArgs ty naps = do
+  aux <- compileTypeArgs ty $ fromMaybe __IMPOSSIBLE__ $ allApplyElims $ patternsToElims naps
+  mapM assertIsTyVarBind aux
+  where
+    assertIsTyVarBind :: Hs.Type () -> C (Hs.TyVarBind ())
+    assertIsTyVarBind = \case
+      Hs.TyVar _ n -> pure $ Hs.UnkindedVar () n
+      _ -> genericError "Not supported: type definition by pattern matching"
 
 compileTypeArg :: DeBruijnPattern -> C (Hs.TyVarBind ())
 compileTypeArg p@(VarP o i) = do
diff --git a/test/AllTests.agda b/test/AllTests.agda
index c0ceb099..d2459f9d 100644
--- a/test/AllTests.agda
+++ b/test/AllTests.agda
@@ -83,6 +83,7 @@ import Issue264
 import Issue301
 import Issue305
 import Issue302
+import Issue309
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -163,4 +164,5 @@ import Issue264
 import Issue301
 import Issue305
 import Issue302
+import Issue309
 #-}
diff --git a/test/Issue309.agda b/test/Issue309.agda
new file mode 100644
index 00000000..9c4e5317
--- /dev/null
+++ b/test/Issue309.agda
@@ -0,0 +1,7 @@
+module Issue309 where
+
+private variable @0 a : Set
+
+Ap : (p : @0 a → Set) → @0 a → Set
+Ap p x = p x
+{-# COMPILE AGDA2HS Ap #-}
diff --git a/test/golden/AllTests.hs b/test/golden/AllTests.hs
index c1603dff..35450b76 100644
--- a/test/golden/AllTests.hs
+++ b/test/golden/AllTests.hs
@@ -78,4 +78,5 @@ import Issue264
 import Issue301
 import Issue305
 import Issue302
+import Issue309
 
diff --git a/test/golden/Issue309.hs b/test/golden/Issue309.hs
new file mode 100644
index 00000000..f9dd5e19
--- /dev/null
+++ b/test/golden/Issue309.hs
@@ -0,0 +1,4 @@
+module Issue309 where
+
+type Ap p = p
+