fix several quantity issues

- contents of box intro
- definition of let
- non-recursive ℕ case
- also make a few var names more consistent

lib/Quox/Typechecker.idr

@@ -208,16 +208,17 @@ mutual
 
   check' ctx sg (Box val loc) ty = do
     (q, ty) <- expectBOX !(askAt DEFS) ctx SZero ty.loc ty
-    -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
+    -- if Ψ | Γ ⊢ σ ⨴ π · s ⇐ A ⊳ Σ
-    valout <- checkC ctx sg val ty
+    valout <- checkC ctx (subjMult sg q) val ty
     -- then Ψ | Γ ⊢ σ · [s] ⇐ [π.A] ⊳ πΣ
     pure $ q * valout
 
   check' ctx sg (Let qty rhs body loc) ty = do
     eres <- inferC ctx (subjMult sg qty) rhs
-    qout <- checkC (extendTyLet (qty * sg.qty) body.name eres.type (E rhs) ctx)
+    let sqty = sg.qty * qty
+    qout <- checkC (extendTyLet sqty body.name eres.type (E rhs) ctx)
               sg body.term (weakT 1 ty)
-        >>= popQ loc qty
+        >>= popQ loc sqty
     pure $ qty * eres.qout + qout
 
   check' ctx sg (E e) ty = do
@@ -432,8 +433,8 @@ mutual
     checkTypeC (extendTy Zero ret.name nat ctx) ret.term Nothing
     -- if Ψ | Γ ⊢ σ · zer ⇐ A[0 ∷ ℕ/n] ⊳ Σz
     zerout <- checkC ctx sg zer $ sub1 ret $ Ann (Zero zer.loc) nat zer.loc
-    -- if Ψ | Γ, n : ℕ, ih : A ⊢ σ · suc ⇐ A[succ p ∷ ℕ/n] ⊳ Σs, ρ₁.p, ρ₂.ih
+    -- if Ψ | Γ, n : ℕ, ih : A ⊢ σ · suc ⇐ A[succ p ∷ ℕ/n] ⊳ Σs, ρ.p, ς.ih
-    -- with ρ₂ ≤ π'σ, (ρ₁ + ρ₂) ≤ πσ
+    -- with ς ≤ π'σ, (ρ + ς) ≤ πσ
     let [< p, ih] = suc.names
         pisg      = pi * sg.qty
         sucCtx    = extendTyN [< (pisg, p, NAT p.loc), (pi', ih, ret.term)] ctx
@@ -442,24 +443,28 @@ mutual
     expectCompatQ loc qih (pi' * sg.qty)
     -- [fixme] better error here
     expectCompatQ loc (qp + qih) pisg
-    -- then Ψ | Γ ⊢ caseπ ⋯ ⇒ A[n] ⊳ πΣn + Σz + ωΣs
+    -- if ς = 0, then Σb = lubs(Σz, Σs), otherwise Σb = Σz + ωςΣs
+    let bodyout = case qih of
+          Zero => lubs ctx [zerout, sucout]
+          _    => zerout + Any * sucout
+    -- then Ψ | Γ ⊢ caseπ ⋯ ⇒ A[n] ⊳ πΣn + Σb
     pure $ InfRes {
       type = sub1 ret n,
-      qout = pi * nres.qout + zerout + Any * sucout
+      qout = pi * nres.qout + bodyout
     }
 
   infer' ctx sg (CaseBox pi box ret body loc) = do
     -- if Ψ | Γ ⊢ σ · b ⇒ [ρ.A] ⊳ Σ₁
     boxres <- inferC ctx sg box
-    (q, ty) <- expectBOX !(askAt DEFS) ctx SZero box.loc boxres.type
+    (rh, ty) <- expectBOX !(askAt DEFS) ctx SZero box.loc boxres.type
     -- if Ψ | Γ, x : [ρ.A] ⊢₀ R ⇐ Type
     checkTypeC (extendTy Zero ret.name boxres.type ctx) ret.term Nothing
-    -- if Ψ | Γ, x : A ⊢ t ⇐ R[[x] ∷ [ρ.A/x]] ⊳ Σ₂, ς·x
+    -- if Ψ | Γ, x : A ⊢ σ · t ⇐ R[[x] ∷ [ρ.A/x]] ⊳ Σ₂, ς·x
     --   with ς ≤ ρπσ
-    let qpisg    = q * pi * sg.qty
+    let rhpisg   = rh * pi * sg.qty
-        bodyCtx  = extendTy qpisg body.name ty ctx
+        bodyCtx  = extendTy rhpisg body.name ty ctx
         bodyType = substCaseBoxRet body.name ty ret
-    bodyout <- checkC bodyCtx sg body.term bodyType >>= popQ loc qpisg
+    bodyout <- checkC bodyCtx sg body.term bodyType >>= popQ loc rhpisg
     -- then Ψ | Γ ⊢ caseπ ⋯ ⇒ R[b/x] ⊳ Σ₁ + Σ₂
     pure $ InfRes {
       type = sub1 ret box,