From 4b814d7502c225ae69d8da7630e378f3cd2bfe30 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Thu, 23 Feb 2023 10:04:00 +0100
Subject: [PATCH] fix quantity in CasePair typing

---
 lib/Quox/Typechecker.idr | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index 1d272c3..2d9c493 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -235,10 +235,11 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     (tfst, tsnd) <- expectSig !ask pairres.type
     -- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐
     --    ret[(x, y) ∷ (x : A) × B/p] ⊳ Σ₂, ρ₁·x, ρ₂·y
-    -- with ρ₁, ρ₂ ≤ π
+    -- with ρ₁, ρ₂ ≤ πσ
     let bodyctx = extendTyN [< tfst, tsnd.term] ctx
         bodyty  = substCasePairRet pairres.type ret
-    bodyout <- popQs [< pi, pi] !(checkC bodyctx sg body.term bodyty)
+        pisg    = pi * sg.fst
+    bodyout <- popQs [< pisg, pisg] !(checkC bodyctx sg body.term bodyty)
     -- then Ψ | Γ ⊢ σ · case ⋯ ⇒ ret[pair/p] ⊳ πΣ₁ + Σ₂
     pure $ InfRes {
       type = sub1 ret pair,