properly compile type elims

Author: flupe

src/Agda2Lambox/Compile/Type.hs

@@ -13,22 +13,23 @@ import Control.Monad ( mapM )
 import Data.List ( foldl' )
 import Data.Function ( (&) )
 import Data.Bifunctor ( second )
-import Data.Maybe ( isJust )
+import Data.Maybe ( isJust, mapMaybe )
 import Data.Function ( applyWhen )
 
 import Agda.Syntax.Common ( unArg, Arg (Arg) )
 import Agda.Syntax.Internal
+import Agda.TypeChecking.Substitute ( absBody, TelV (theCore), absApp )
+import Agda.TypeChecking.Telescope (telView)
 import Agda.TypeChecking.Monad.Base ( TCM, MonadTCM (liftTCM), Definition(..))
-import Agda.Utils.Monad (ifM)
+import Agda.TypeChecking.Monad.Signature ( canonicalName )
+import Agda.TypeChecking.Telescope ( mustBePi )
+import Agda.Utils.Monad ( ifM )
 
 import qualified LambdaBox as LBox
 import Agda2Lambox.Compile.Utils
 import Agda2Lambox.Compile.Monad
 import Agda.Compiler.Backend (HasConstInfo(getConstInfo), Definition(Defn), AddContext (addContext))
 import Agda.Utils (isDataOrRecDef, getInductiveParams, isArity, maybeUnfoldCopy)
-import Agda.TypeChecking.Substitute (absBody, TelV (theCore))
-import Agda.TypeChecking.Telescope (telView)
-import Agda.TypeChecking.Monad.Signature ( canonicalName )
 
 
 -- | The kind of variables that are locally bound
@@ -113,11 +114,15 @@ compileType tvars = runC tvars . compileTypeC
 compileTypeC :: Type -> C LBox.Type
 compileTypeC = local (\e -> e { insertVars = False }) . fmap snd . compileTopLevelTypeC
 
-compileElims :: Elims -> C [LBox.Type]
-compileElims = mapM \case
-  Apply a  -> fmap snd $ compileTypeTerm $ unArg a
-  Proj{}   -> genericError "type-level projection elim not supported."
-  IApply{} -> genericError "type-level cubical path application not supported."
+compileElims :: Type -> Args -> C [LBox.Type]
+compileElims _ [] = pure []
+compileElims ty (x:xs) = do
+  (a, b) <- mustBePi ty
+  rest   <- compileElims (absApp b $ unArg x) xs
+  first  <- ifM (liftTCM $ isLogical a)
+              (pure LBox.TBox)
+              (fmap snd $ compileTypeTerm $ unArg x)
+  pure (first : rest)
 
 getTypeVarInfo :: Dom Type -> TCM LBox.TypeVarInfo
 getTypeVarInfo typ = do
@@ -164,8 +169,9 @@ compileTypeTerm = \case
     else if isDataOrRecDef def then do
       lift $ requireDef q
       ind <- liftTCM $ toInductive q
+      let args = mapMaybe isApplyElim es
       ([],) . foldl' LBox.TApp (LBox.TInd ind)
-        <$> compileElims (take (getInductiveParams def) es)
+        <$> compileElims defType (take (getInductiveParams def) args)
 
     -- otherwise, it must have been compiled as a type scheme,
     -- and therefore is kept with all arguments.
@@ -175,9 +181,11 @@ compileTypeTerm = \case
     -- TODO(flupe): possibly merge the logic with the above for datatypes
     else do
       q <- liftTCM $ canonicalName q
+      lift $ requireDef q
       let ts = qnameToKName q
+      let args = mapMaybe isApplyElim es
       ([],) . foldl' LBox.TApp (LBox.TConst ts)
-        <$> compileElims es
+        <$> compileElims defType args
 
   Pi dom codom -> do
     let domType   = unDom dom

src/Agda2Lambox/Compile/TypeScheme.hs

@@ -51,30 +51,24 @@ compileTypeScheme Defn{..} = do
   TelV tyargs _ <- telView defType
   let Function{..} = theDef
   case funClauses of
-    [cl] | onlyVarsPat (namedClausePats cl)
-         , isJust (clauseBody cl) -> do
-      cl <- etaExpandClause cl
-      addContext (KeepNames $ clauseTel cl) do
-        -- retrieve the telescope of arguments that have not been introduced yet
-        let
-          -- number of parameters introduced in the clause
-          nvars = length $ namedClausePats cl
-          args = drop nvars $ telToList tyargs
+    [cl]
+      | onlyVarsPat (namedClausePats cl)
+      , isJust (clauseBody cl) -> do
 
-          -- we traverse explicit lambdas
-          underLams :: Term -> [Dom (ArgName, Type)] -> CompileM LBox.Type
-          underLams (Lam ai t) (dom:rest) =
-            underAbstraction (snd <$> dom) t \body ->
-              underLams body rest
-          underLams t args =
-            fmap snd $ runCNoVars nvars $ compileTypeTerm t
+      -- We eta-expand the clause to maximal arity by inserting variable patterns
+      -- and applying the body to variables.
+      -- This also lifts all lambdas from the body to variable patterns.
+      cl <- etaExpandClause cl
 
-          Just body = clauseBody cl
+      let
+        -- number of parameters introduced in the clause
+        nvars     = length $ namedClausePats cl
+        Just body = clauseBody cl
 
-        res      <- underLams body args
-        tvarInfo <- compileTele tyargs
+      (_, res) <- addContext (KeepNames $ clauseTel cl) $ runCNoVars nvars $ compileTypeTerm body
+      tvarInfo <- compileTele tyargs
 
-        pure $ TypeAliasDecl $ Just (tvarInfo, res)
+      pure $ TypeAliasDecl $ Just (tvarInfo, res)
 
     -- if there isn't exactly one clause, we give up
     -- compiling the type alias and return TAny

test/Scheme.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --erasure #-}
+{-# OPTIONS --erasure --prop #-}
 -- compilation of λ□ type schemes
 module Scheme where
 
@@ -11,23 +11,26 @@ length : {A : Set} → List A → Nat
 length [] = 0
 length (_ ∷ xs) = suc (length xs)
 
-record Σ (A : Set) (B : A → Set) : Set where
+data Eq {A : Set} (x : A) : A -> Prop where
+  rfl : Eq x x
+
+record Σ (A : Set) (B : A → Prop) : Set where
   constructor _,_
   field
-    fst    : A
+    fst : A
     snd : B fst
-Σ-syntax : (A : Set) (B : A → Set) → Set
+Σ-syntax : (A : Set) (B : A → Prop) → Set
 Σ-syntax = Σ
 
 syntax Σ-syntax A (λ x → B) = [ x ∈ A ∣ B ]
 
 -- NOTE: this doesn't compile properly?
 -- the snd projection is compiled while it shouldn't be?
-record Σ0 (A : Set) (@0 B : A → Set) : Set where
-  constructor _,_
-  field
-    fst    : A
-    @0 snd : B fst
+-- record Σ0 (A : Set) (@0 B : A → Set) : Set where
+--   constructor _,_
+--   field
+--     fst    : A
+--     @0 snd : B fst
 
 -- expected: type scheme
 -- ­ vars: [a, b]
@@ -50,7 +53,7 @@ ListAlias' A = List A
 -- - vars: [a, n]
 -- - type: Σ (List a) □
 Vec : (A : Set) → Nat → Set
-Vec A n = [ xs ∈ List A ∣ length xs ≡ n ]
+Vec A n = [ xs ∈ List A ∣ Eq (length xs) n ]
 
 Bad : Bool → Set
 Bad false = Nat