Closes #309: Ensures we compile pattern variables correctly by relying

on the existing compileTypeArgs.

Author: VictorCMiraldo

src/Agda2Hs/Compile/TypeDefinition.hs

@@ -10,25 +10,28 @@ 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 ()]
 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

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
 #-}

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 #-}

test/golden/AllTests.hs

@@ -78,4 +78,5 @@ import Issue264
 import Issue301
 import Issue305
 import Issue302
+import Issue309
 

test/golden/Issue309.hs

@@ -0,0 +1,4 @@
+module Issue309 where
+
+type Ap p = p
+