Allow motive of case statement to depend on the datatype indices, plu…

…s actually enforce its well-typedness

src/Agda/Core/Conversion.agda

@@ -74,13 +74,16 @@ data Conv {α} where
   CApp   : u ≅ u'
          → w ≅ w'
          → TApp u w ≅ TApp u' w'
-  CCase  : {@0 r : Rezz α}
+  CCase  : ∀ {@0 x y z cs} {u u' : Term α} {@0 r : Rezz α}
+           (d : NameIn dataScope)
+           (r1 r2 : Rezz (dataIxScope d))
            (bs bp : Branches α cs)
-           (ms : Type (x ◃ α)) (mp : Type (y ◃ α))
+           (ms : Type _) (mp : Type _)
          → u ≅ u'
-         → renameTop {y = z} r (unType ms) ≅ renameTop {y = z} r (unType mp)
+         →   renameTop {y = z} (rezzCong2 _<>_ r1 r) (unType ms)
+           ≅ renameTop {y = z} (rezzCong2 _<>_ r2 r) (unType mp)
          → ConvBranches bs bp
-         → TCase u bs ms ≅ TCase u' bp mp
+         → TCase {x = x} d r1 u bs ms ≅ TCase {x = y} d r2 u' bp mp
   -- TODO: CProj : {!   !}
   CData  : (@0 d : NameIn dataScope)
            {@0 ps qs : dataParScope d ⇒ α}

src/Agda/Core/Converter.agda

@@ -74,12 +74,17 @@ reduceToSort r v err = reduceTo r v >>= λ where
   _ → tcError err
 {-# COMPILE AGDA2HS reduceToSort #-}
 
+convNamesIn : (x y : NameIn α) → TCM (x ≡ y)
+convNamesIn x y =
+  ifEqualNamesIn x y
+    (λ where {{refl}} → return refl)
+    (tcError "names not equal")
+
 convVars : (x y : NameIn α)
          → TCM (Conv (TVar x) (TVar y))
-convVars x y =
-  ifEqualNamesIn x y
-    (λ where {{refl}} → return CRefl)
-    (tcError "variables not convertible")
+convVars x y = do
+  refl ← convNamesIn x y
+  return CRefl
 {-# COMPILE AGDA2HS convVars #-}
 
 convDefs : (f g : NameIn defScope)
@@ -161,19 +166,23 @@ convApps r u u' w w' = do
 
 convertCase : {{fl : Fuel}}
             → Rezz α
+            → (d d' : NameIn dataScope)
+            → (r : Rezz (dataIxScope d)) (r' : Rezz (dataIxScope d'))
             → (u u' : Term α)
             → ∀ {@0 cs cs'} (ws : Branches α cs) (ws' : Branches α cs')
-            → (rt : Type (x ◃ α)) (rt' : Type (y ◃ α))
-            → TCM (Conv (TCase u ws rt) (TCase u' ws' rt'))
-convertCase {x = x} r u u' ws ws' rt rt' = do
-  cu ← convertCheck r u u'
+            → (rt : Type (x ◃ _)) (rt' : Type (y ◃ _))
+            → TCM (Conv (TCase d r u ws rt) (TCase d' r' u' ws' rt'))
+convertCase {x = x} rα d d' ri ri' u u' ws ws' rt rt' = do
+  refl ← convNamesIn d d'
+  cu ← convertCheck rα u u'
+  let r = rezzCong2 _<>_ ri rα
   cm ← convertCheck (rezzBind {x = x} r)
                        (renameTop r (unType rt))
-                       (renameTop r (unType rt'))
+                       (renameTop _ (unType rt'))
   Erased refl ← liftMaybe (allInScope (allBranches ws) (allBranches ws'))
     "comparing case statements with different branches"
-  cbs ← convertBranches r ws ws'
-  return (CCase ws ws' rt rt' cu cm cbs)
+  cbs ← convertBranches rα ws ws'
+  return (CCase d ri ri' ws ws' rt rt' cu cm cbs)
 
 {-# COMPILE AGDA2HS convertCase #-}
 
@@ -209,7 +218,7 @@ convertBranch r (BBranch (⟨ c1 ⟩ cp1) rz1 rhs1) (BBranch (⟨ c2 ⟩ cp2) rz
   ifDec (decIn cp1 cp2)
     (λ where {{refl}} → do
       CBBranch (⟨ c1 ⟩ cp1) rz1 rz2 rhs1 rhs2 <$>
-        convertCheck (rezzCong2 _<>_ (rezzCong revScope rz1) r) rhs1 rhs2)
+        convertCheck (rezzCong2 _<>_ (rezzCong revScope rz2) r) rhs1 rhs2)
     (tcError "can't convert two branches that match on different constructors")
 
 {-# COMPILE AGDA2HS convertBranch #-}
@@ -229,8 +238,8 @@ convertWhnf r (TCon c lc) (TCon d ld) = convCons r c d lc ld
 convertWhnf r (TLam x u) (TLam y v) = convLams r x y u v
 convertWhnf r (TApp u e) (TApp v f) = convApps r u v e f
 convertWhnf r (TProj u f) (TProj v g) = tcError "not implemented: conversion of projections"
-convertWhnf r (TCase {cs = cs} u bs rt) (TCase {cs = cs'} u' bs' rt') =
-  convertCase r u u' {cs} {cs'} bs bs' rt rt'
+convertWhnf r (TCase {cs = cs} d ri u bs rt) (TCase {cs = cs'} d' ri' u' bs' rt') =
+  convertCase r d d' ri ri' u u' {cs} {cs'} bs bs' rt rt'
 convertWhnf r (TPi x tu tv) (TPi y tw tz) = convPis r x y tu tw tv tz
 convertWhnf r (TSort s) (TSort t) = convSorts s t
 --let and ann shoudln't appear here since they get reduced away

src/Agda/Core/Reduce.agda

@@ -59,21 +59,25 @@ envToSubst r (env , x ↦ v) =
 data Frame (@0 α : Scope Name) : Set where
   FApp  : (u : Term α) → Frame α
   FProj : (x : NameIn defScope) → Frame α
-  FCase : (bs : Branches α cs) (m : Type (x ◃ α)) → Frame α
+  FCase : (d : NameIn dataScope) (r : Rezz (dataIxScope d))
+          (bs : Branches α cs) (m : Type (x ◃ (dataIxScope d <> α))) → Frame α
 
 {-# COMPILE AGDA2HS Frame #-}
 
 unFrame : Frame α → Term α → Term α
 unFrame (FApp v) u = TApp u v
 unFrame (FProj f) u = TProj u f
-unFrame (FCase bs m) u = TCase u bs m
+unFrame (FCase d r bs m) u = TCase d r u bs m
 
 {-# COMPILE AGDA2HS unFrame #-}
 
 weakenFrame : α ⊆ β → Frame α → Frame β
 weakenFrame s (FApp u) = FApp (weaken s u)
 weakenFrame s (FProj f) = FProj f
-weakenFrame s (FCase bs m) = FCase (weakenBranches s bs) (weakenType (subBindKeep s) m)
+weakenFrame s (FCase d r bs m) =
+  FCase d r
+    (weakenBranches s bs)
+    (weakenType (subBindKeep (subJoinKeep r s)) m)
 
 {-# COMPILE AGDA2HS weakenFrame #-}
 
@@ -160,7 +164,7 @@ step rsig (MkState e (TVar (⟨ x ⟩ p)) s) =
     (Right v) → Just (MkState e v s)
 step rsig (MkState e (TApp v w) s) = Just (MkState e v (FApp w ∷ s))
 step rsig (MkState e (TProj v f) s) = Just (MkState e v (FProj f ∷ s))
-step rsig (MkState e (TCase v bs m) s) = Just (MkState e v (FCase bs m ∷ s))
+step rsig (MkState e (TCase d r v bs m) s) = Just (MkState e v (FCase d r bs m ∷ s))
 step rsig (MkState e (TLam x v) (FApp w ∷ s)) =
   Just (MkState
     (e , x ↦ w)
@@ -174,7 +178,7 @@ step rsig (MkState e (TLet x v w) s) =
 step (rezz sig) (MkState e (TDef d) s) =
   case getBody sig d of λ where
     v → Just (MkState e (weaken subEmpty v) s)
-step rsig (MkState e (TCon c vs) (FCase bs _ ∷ s)) =
+step rsig (MkState e (TCon c vs) (FCase d r bs _ ∷ s)) =
   case lookupBranch bs c of λ where
     (Just (r , v)) → Just (MkState
       (extendEnvironment (revSubst vs) e)

src/Agda/Core/Signature.agda

@@ -60,7 +60,7 @@ record Datatype (@0 pars : Scope Name) (@0 ixs : Scope Name) : Set where
     dataParameterTel     : Telescope mempty pars
     dataIndexTel         : Telescope pars ixs
     dataConstructors     : ((⟨ c ⟩ cp) : NameIn  dataConstructorScope)
-                         → Σ (c ∈ conScope) (λ p → Constructor pars ixs (⟨ _ ⟩ p))
+                         → Σ (c ∈ conScope) (λ p → Constructor pars ixs (⟨ c ⟩ p))
 open Datatype public
 
 {-# COMPILE AGDA2HS Datatype #-}
@@ -106,7 +106,7 @@ getBody sig x = case getDefinition sig x of λ where
 getConstructor : ((⟨ c ⟩ cp) : NameIn conScope)
                → ∀ {@0 pars ixs} (d : Datatype pars ixs)
                → Maybe (∃[ cd ∈ (c ∈ dataConstructorScope d) ]
-                         fst (dataConstructors d (⟨ _ ⟩ cd)) ≡ cp)
+                         fst (dataConstructors d (⟨ c ⟩ cd)) ≡ cp)
 getConstructor c d =
   findAll (tabulateAll (rezz (dataConstructorScope d)) (λ _ → tt))
       λ _ p → ifEqualNamesIn (⟨ _ ⟩ fst (dataConstructors d (⟨ _ ⟩ p))) c

src/Agda/Core/Substitute.agda

@@ -39,8 +39,11 @@ substTerm f (TCon c vs)       = TCon c (substSubst f vs)
 substTerm f (TLam x v)        = TLam x (substTerm (liftBindSubst f) v)
 substTerm f (TApp u v)        = TApp (substTerm f u) (substTerm f v)
 substTerm f (TProj u p)       = TProj (substTerm f u) p
-substTerm f (TCase {x = x} u bs m) =
-  TCase (substTerm f u) (substBranches f bs) (substType (liftBindSubst {y = x} f) m)
+substTerm f (TCase {x = x} d r u bs m) =
+  TCase {x = x} d r
+    (substTerm f u)
+    (substBranches f bs)
+    (substType (liftBindSubst (liftSubst r f)) m)
 substTerm f (TPi x a b)       = TPi x (substType f a) (substType (liftBindSubst f) b)
 substTerm f (TSort s)         = TSort (substSort f s)
 substTerm f (TLet x u v)      = TLet x (substTerm f u) (substTerm (liftBindSubst f) v)

src/Agda/Core/Syntax.agda

@@ -65,7 +65,11 @@ data Term α where
   TLam  : (@0 x : Name) (v : Term (x ◃ α)) → Term α
   TApp  : (u : Term α) (v : Term α) → Term α
   TProj : (u : Term α) (x : NameIn defScope) → Term α
-  TCase : (u : Term α) (bs : Branches α cs) (m : Type (x ◃ α)) → Term α
+  TCase : (d : NameIn dataScope)
+        → Rezz (dataIxScope d)
+        → (u : Term α) (bs : Branches α cs)
+        → (m : Type (x ◃ (dataIxScope d <> α)))
+        → Term α
   TPi   : (@0 x : Name) (u : Type α) (v : Type (x ◃ α)) → Term α
   TSort : Sort α → Term α
   TLet  : (@0 x : Name) (u : Term α) (v : Term (x ◃ α)) → Term α
@@ -181,7 +185,7 @@ unAppsView (TDef _) = refl
 unAppsView (TData _ _ _) = refl
 unAppsView (TCon _ _) = refl
 unAppsView (TProj _ _) = refl
-unAppsView (TCase _ _ _) = refl
+unAppsView (TCase _ _ _ _ _) = refl
 unAppsView (TLam _ _) = refl
 unAppsView (TPi _ _ _) = refl
 unAppsView (TSort _) = refl
@@ -221,7 +225,7 @@ weaken p (TCon c vs)       = TCon c (weakenSubst p vs)
 weaken p (TLam x v)        = TLam x (weaken (subBindKeep p) v)
 weaken p (TApp u e)        = TApp (weaken p u) (weaken p e)
 weaken p (TProj u x)       = TProj (weaken p u) x
-weaken p (TCase u bs m)    = TCase (weaken p u) (weakenBranches p bs) (weakenType (subBindKeep p) m)
+weaken p (TCase d r u bs m) = TCase d r (weaken p u) (weakenBranches p bs) (weakenType (subBindKeep (subJoinKeep r p)) m)
 weaken p (TPi x a b)       = TPi x (weakenType p a) (weakenType (subBindKeep p) b)
 weaken p (TSort α)         = TSort (weakenSort p α)
 weaken p (TLet x v t)      = TLet x (weaken p v) (weaken (subBindKeep p) t)
@@ -339,8 +343,10 @@ strengthen p (TCon c vs) = TCon c <$> strengthenSubst p vs
 strengthen p (TLam x v) = TLam x <$> strengthen (subBindKeep p) v
 strengthen p (TApp v e) = TApp <$> strengthen p v <*> strengthen p e
 strengthen p (TProj u f) = (λ v → TProj v f) <$> strengthen p u
-strengthen p (TCase u bs m) =
-  TCase <$> strengthen p u <*> strengthenBranches p bs <*> strengthenType (subBindKeep p) m
+strengthen p (TCase d r u bs m) =
+  TCase d r <$> strengthen p u
+            <*> strengthenBranches p bs
+            <*> strengthenType (subBindKeep (subJoinKeep r p)) m
 strengthen p (TPi x a b) =
   TPi x <$> strengthenType p a <*> strengthenType (subBindKeep p) b
 strengthen p (TSort s) = TSort <$> strengthenSort p s

src/Agda/Core/Tests.agda

@@ -48,10 +48,10 @@ instance
     ; fieldScope = λ _ → mempty
     }
 
-boolcons : (c : NameIn cons)
-         → Σ (proj₁ c ∈ cons) (λ cp → Constructor mempty mempty (⟨ _ ⟩ cp))
+boolcons : ((⟨ c ⟩ cp) : NameIn cons)
+         → Σ (c ∈ cons) (λ cp → Constructor mempty mempty (⟨ c ⟩ cp))
 boolcons (⟨ c ⟩ cp) = lookupAll
-  {p = λ c → Σ (c ∈ cons) (λ cp → Constructor mempty mempty (⟨ _ ⟩ cp))}
+  {p = λ c → Σ (c ∈ cons) (λ cp → Constructor mempty mempty (⟨ c ⟩ cp))}
   (allJoin (allSingl (inHere
                      , record { conTelescope = EmptyTel
                               ; conIndices = SNil } )) $
@@ -101,7 +101,7 @@ module TestReduce (@0 x y z : Name) where
     test₁ = refl
 
     testTerm₂ : Term α
-    testTerm₂ = TCase {x = "condition"} `true
+    testTerm₂ = TCase {x = "condition"} (⟨ "Bool" ⟩ inHere) (rezz _) `true
                                   (BsCons (BBranch (⟨ "true" ⟩ inHere) (rezz _) `false)
                                   (BsCons (BBranch (⟨ "false" ⟩ inThere inHere) (rezz _) `true)
                                    BsNil))

src/Agda/Core/Typechecker.agda

@@ -91,7 +91,7 @@ checkBranches : ∀ {@0 pars ixs cons : Scope Name}
                   (bs : Branches α cons)
                   (dt : Datatype pars ixs)
                   (ps : pars ⇒ α)
-                  (rt : Type (x ◃ α))
+                  (rt : Type (x ◃ (ixs <> α)))
                 → TCM (TyBranches Γ dt ps rt bs)
 
 inferApp : ∀ Γ u v → TCM (Σ[ t ∈ Type α ] Γ ⊢ TApp u v ∶ t)
@@ -107,18 +107,19 @@ inferApp ctx u v = do
   return (tytype , TyApp gtu gc gtv)
 {-# COMPILE AGDA2HS inferApp #-}
 
-inferCase : ∀ {@0 cs} Γ u bs rt → TCM (Σ[ t ∈ Type α ] Γ ⊢ TCase {x = x} u bs rt ∶ t)
-inferCase ctx u bs rt = do
+inferCase : ∀ {@0 cs} Γ d r u bs rt → TCM (Σ[ t ∈ Type α ] Γ ⊢ TCase {x = x} d r u bs rt ∶ t)
+inferCase ctx d rixs u bs rt = do
   let r = rezzScope ctx
   El s tu , gtu ← inferType ctx u
-  d , (params , ixs) ⟨ rp ⟩ ← reduceToData r tu
+  d' , (params , ixs) ⟨ rp ⟩ ← reduceToData r tu
     "can't typecheck a constrctor with a type that isn't a def application"
+  refl ← convNamesIn d d'
   df ⟨ deq ⟩ ← tcmGetDatatype d
   Erased refl ← checkCoverage df bs
   cb ← checkBranches ctx (rezzBranches bs) bs df params rt
   let ds = substSort params (dataSort df)
   cc ← convert r tu (unType $ dataType d ds params ixs)
-  return (substTopType r u rt , TyCase {k = ds} d df deq {is = ixs} bs rt gtu cc cb)
+  return (_ , TyCase {k = ds} {r = r} d df deq rixs bs rt gtu cc cb)
 
 {-# COMPILE AGDA2HS inferCase #-}
 
@@ -175,20 +176,13 @@ checkBranch : ∀ {@0 con : Name} (Γ : Context α)
                 (bs : Branch α con)
                 {@0 pars ixs} (dt : Datatype pars ixs)
                 (ps : pars ⇒ α)
-                (rt : Type (x ◃ α))
+                (rt : Type (x ◃ ixs <> _))
             → TCM (TyBranch Γ dt ps rt bs)
 checkBranch ctx (BBranch c r rhs) dt ps rt = do
   let ra = rezzScope ctx
   cid ⟨ refl ⟩  ← liftMaybe (getConstructor c dt)
     "can't find a constructor with such a name"
-  let (c∈conScope , con) = dataConstructors dt (⟨ _ ⟩ cid)
-      ctel = substTelescope ps (conTelescope con)
-      cargs = weakenSubst (subJoinHere (rezzCong revScope r) subRefl)
-                          (revIdSubst r)
-      idsubst = weakenSubst (subJoinDrop (rezzCong revScope r) subRefl)
-                            (idSubst ra)
-      bsubst = SCons (TCon (⟨ _ ⟩ c∈conScope) cargs) idsubst
-  crhs ← checkType (addContextTel ctel ctx) rhs (substType bsubst rt)
+  crhs ← checkType _ _ _
   return (TyBBranch (⟨ _ ⟩ cid) {rα = ra} rhs crhs)
 {-# COMPILE AGDA2HS checkBranch #-}
 
@@ -264,9 +258,9 @@ checkType ctx (TLam x te) ty = checkLambda ctx x te ty
 checkType ctx (TApp u e) ty = do
   tapp ← inferApp ctx u e
   checkCoerce ctx (TApp u e) tapp ty
-checkType ctx (TCase {cs = cs} u bs rt) ty = do
-  tapp ← inferCase {cs = cs} ctx u bs rt
-  checkCoerce ctx (TCase u bs rt) tapp ty
+checkType ctx (TCase {cs = cs} d r u bs rt) ty = do
+  tapp ← inferCase {cs = cs} ctx d r u bs rt
+  checkCoerce ctx (TCase d r u bs rt) tapp ty
 checkType ctx (TProj u f) ty = tcError "not implemented: projections"
 checkType ctx (TPi x tu tv) ty = do
   tpi ← inferPi ctx x tu tv
@@ -287,7 +281,7 @@ inferType ctx (TData d ps is) = inferData ctx d ps is
 inferType ctx (TCon c x) = tcError "non inferrable: can't infer the type of a constructor"
 inferType ctx (TLam x te) = tcError "non inferrable: can't infer the type of a lambda"
 inferType ctx (TApp u e) = inferApp ctx u e
-inferType ctx (TCase u bs rt) = inferCase ctx u bs rt
+inferType ctx (TCase d r u bs rt) = inferCase ctx d r u bs rt
 inferType ctx (TProj u f) = tcError "not implemented: projections"
 inferType ctx (TPi x a b) = inferPi ctx x a b
 inferType ctx (TSort s) = inferTySort ctx s