introduce motive in the syntax for cases

The only unsolved meta is in the context extension of conversion checker
for the *sort* of the scrutinee. Which shouldn't matter because we
never use sorts of the variables from the context. Nevertheless, have
to find a way to fill it in in a way that makes sense.

src/Agda/Core/Conversion.agda

@@ -99,9 +99,13 @@ data Conv {α} Γ where
 data ConvElim {α} Γ where
   CEArg  : Γ ⊢ v ≅ v'
          → Γ ⊢ EArg v ≃ EArg v'
-  CECase : (bs bp : Branches α cs)
+  CECase : {@0 r : Rezz _ α}
+           (bs bp : Branches α cs)
+           (ms : Type (x ◃ α)) (mp : Type (y ◃ α))
+         --TODO: enforce that a is the type of the scrutinee
+         → Γ , x ∶ a ⊢ renameTop r (unType ms) ≅ renameTop r (unType mp)
          → ConvBranches Γ bs bp
-         → Γ ⊢ ECase bs ≃ ECase bp
+         → Γ ⊢ ECase bs ms ≃ ECase bp mp
   -- TODO: CEProj : {!   !}
 
 data ConvBranch {α} Γ where

src/Agda/Core/Converter.agda

@@ -234,9 +234,7 @@ convertElims fl ctx t           u (EArg w) (EArg w') = do
   let ksort = piSort (typeSort a) (typeSort b)
   cw ← convertCheck fl ctx (unType a) w w'
   return $ substTop r w (unType b) Σ, CEArg cw
-convertElims fl ctx t u (ECase ws) (ECase ws') = do
-  let rt : Term ({!!} ◃ α)
-      rt = {!!}
+convertElims fl ctx t u (ECase ws m) (ECase ws' m') = do
   let r = rezzScope ctx
   rezz sig  ← tcmSignature
   (TDef d dp , els) ⟨ rp ⟩  ← reduceElimView _ _ <$> reduceTo r sig t fl
@@ -252,8 +250,12 @@ convertElims fl ctx t u (ECase ws) (ECase ws') = do
   (Erased refl) ← liftMaybe
     (allInScope {γ = conScope} (allBranches ws) (allBranches ws'))
     "couldn't verify that branches cover the same constructors"
-  cbs ← convertBranches fl ctx df psubst rt ws ws'
-  return (substTop r u rt Σ, CECase ws ws' cbs)
+  cm ← convertCheck fl (ctx , _ ∶ El {!!} t)
+                       (TSort (typeSort m))
+                       (renameTop r (unType m))
+                       (renameTop r (unType m'))
+  cbs ← convertBranches fl ctx df psubst (unType m) ws ws'
+  return (substTop r u (unType m) Σ, CECase ws ws' m m' cm cbs)
 convertElims fl ctx s u (EProj _ _) (EProj _ _) = tcError "not implemented yet"
 convertElims fl ctx s u _           _ = tcError "two elims aren't the same shape"
 

src/Agda/Core/Reduce.agda

@@ -132,7 +132,7 @@ step sig (MkState e (TLet x v w) s) =
 step sig (MkState e (TDef d q) s) = case getBody sig d q of λ where
   (Just v) → Just (MkState e (weaken subEmpty v) s)
   Nothing  → Nothing
-step sig (MkState e (TCon c q vs) (ECase bs ∷ s)) =
+step sig (MkState e (TCon c q vs) (ECase bs _ ∷ s)) =
   case lookupBranch bs c q of λ where
     (Just (r , v)) → Just (MkState
       (extendEnvironment (revSubst vs) e)

src/Agda/Core/Substitute.agda

@@ -45,9 +45,10 @@ substTerm f (TLet x u v)      = TLet x (substTerm f u) (substTerm (liftBindSubst
 substTerm f (TAnn u t)        = TAnn (substTerm f u) (substType f t)
 {-# COMPILE AGDA2HS substTerm #-}
 
-substElim f (EArg u)    = EArg (substTerm f u)
-substElim f (EProj p k) = EProj p k
-substElim f (ECase bs)  = ECase (substBranches f bs)
+substElim f (EArg u)             = EArg (substTerm f u)
+substElim f (EProj p k)          = EProj p k
+substElim f (ECase {x = x} bs m) = ECase (substBranches f bs)
+                                         (substType (liftBindSubst {y = x} f) m)
 {-# COMPILE AGDA2HS substElim #-}
 
 substElims f = map (substElim f)

src/Agda/Core/Syntax.agda

@@ -91,7 +91,7 @@ sortType s = El (sucSort s) (TSort s)
 data Elim α where
   EArg  : Term α → Elim α
   EProj : (@0 x : name) → x ∈ defScope → Elim α
-  ECase : (bs : Branches α cs) → Elim α
+  ECase : (bs : Branches α cs) (m : Type (x ◃ α)) → Elim α
   -- TODO: do we need a type annotation for the return type of case?
 {-# COMPILE AGDA2HS Elim deriving Show #-}
 
@@ -230,7 +230,7 @@ weakenType p (El st t) = El (weakenSort p st) (weaken p t)
 
 weakenElim p (EArg x)    = EArg (weaken p x)
 weakenElim p (EProj x k) = EProj x k
-weakenElim p (ECase bs)  = ECase (weakenBranches p bs)
+weakenElim p (ECase bs m)  = ECase (weakenBranches p bs) (weakenType (subBindKeep p) m)
 {-# COMPILE AGDA2HS weakenElim #-}
 
 weakenElims p = map (weakenElim p)
@@ -348,7 +348,7 @@ strengthenType p (El st t) = El <$> strengthenSort p st <*> strengthen p t
 
 strengthenElim p (EArg v) = EArg <$> strengthen p v
 strengthenElim p (EProj f q) = Just (EProj f q)
-strengthenElim p (ECase bs) = ECase <$> strengthenBranches p bs
+strengthenElim p (ECase bs m) = ECase <$> strengthenBranches p bs <*> strengthenType (subBindKeep p) m
 
 strengthenElims p = traverse (strengthenElim p)
 

src/Agda/Core/Typechecker.agda

@@ -73,9 +73,7 @@ inferElim ctx u (Syntax.EArg v) tu = do
       tytype = substTopType r v rt
   return $ tytype , TyArg gc gtv
 
-inferElim {α = α} ctx u (Syntax.ECase bs) (El s ty) = do
-  let rt : Type ({!!} ◃ α)
-      rt = El (weakenSort (subWeaken subRefl) s) {!!}
+inferElim {α = α} ctx u (Syntax.ECase bs m) (El s ty) = do
   let r = rezzScope ctx
   fuel      ← tcmFuel
   rezz sig  ← tcmSignature
@@ -96,11 +94,11 @@ inferElim {α = α} ctx u (Syntax.ECase bs) (El s ty) = do
   (Erased refl) ← liftMaybe
     (allInScope {γ = conScope} (allBranches bs) (mapAll fst $ dataConstructors df))
     "couldn't verify that branches cover all constructors"
-  cb ← checkBranches ctx (rezzBranches bs) bs df psubst rt
+  cb ← checkBranches ctx (rezzBranches bs) bs df psubst m
   let ds = substSort psubst (dataSort df)
   cc ← convert ctx (TSort s) ty (unType $ dataType d dp ds psubst isubst)
-  let tj = TyCase {k = ds} {r = r} dp df dep {is = isubst} bs rt cc cb
-  return (substTopType r u rt , tj)
+  let tj = TyCase {k = ds} {r = r} dp df dep {is = isubst} bs m cc cb
+  return (substTopType r u m , tj)
 
 inferElim ctx u (Syntax.EProj _ _) ty = tcError "not implemented"
 

src/Agda/Core/Typing.agda

@@ -148,7 +148,7 @@ data TyElim {α} Γ where
              (rt : Type (x ◃ α))
            → Γ ⊢ (unType c) ≅ (unType $ dataType d dp k ps is)
            → TyBranches Γ dt ps rt bs
-           → TyElim Γ u (ECase bs) c (substTopType r u rt)
+           → TyElim Γ u (ECase bs rt) c (substTopType r u rt)
     -- TODO: proj
 
 {-# COMPILE AGDA2HS TyElim #-}