From 036e2bd4a57df618e1711474c7b1fe4d9b7882ed Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 1 Apr 2023 16:01:29 +0200
Subject: [PATCH] fix case-box typing

---
 lib/Quox/Typechecker.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index 76aa585..824a442 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -407,7 +407,7 @@ parameters {auto _ : IsQty q}
     -- if Ψ | Γ, x : A ⊢ t ⇐ R[[x] ∷ [ρ.A/x]] ⊳ Σ₂, ς·x
     --   with ς ≤ ρπσ
     let qpisg    = q * pi * sg.fst
-        bodyCtx  = extendTy qpisg body.name boxres.type ctx
+        bodyCtx  = extendTy qpisg body.name ty ctx
         bodyType = substCaseBoxRet ty ret
     bodyout <- checkC bodyCtx sg body.term bodyType >>= popQ qpisg
     -- then Ψ | Γ ⊢ case ⋯ ⇒ R[b/x] ⊳ Σ₁ + Σ₂