From a4ffd746254e8eaa537b3fea4bf690a93752d41b Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Thu, 20 Apr 2023 19:29:57 +0200
Subject: [PATCH] fix the most embarrassing quantity mistake ever

---
 lib/Quox/Typechecker.idr    |  6 +++---
 tests/Tests/Typechecker.idr | 35 +++++++++++++++++++++++++++++++++++
 2 files changed, 38 insertions(+), 3 deletions(-)

diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index 6a1a418..8e077ef 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -26,7 +26,7 @@ runTC defs =
 
 
 export
-popQs : Has ErrorEff fs => QOutput s -> QOutput (s + n) -> Eff fs (QOutput n)
+popQs : Has ErrorEff fs => QContext s -> QOutput (s + n) -> Eff fs (QOutput n)
 popQs [<]         qout         = pure qout
 popQs (pis :< pi) (qout :< rh) = do expectCompatQ rh pi; popQs pis qout
 
@@ -363,10 +363,10 @@ mutual
     (qty, argty, res) <- expectPi !defs ctx funres.type
     -- if Ψ | Γ ⊢ σ ⨴ π · s ⇐ A ⊳ Σ₂
     argout <- checkC ctx (subjMult sg qty) arg argty
-    -- then Ψ | Γ ⊢ σ · f s ⇒ B[s] ⊳ Σ₁ + Σ₂
+    -- then Ψ | Γ ⊢ σ · f s ⇒ B[s] ⊳ Σ₁ + πΣ₂
     pure $ InfRes {
       type = sub1 res $ arg :# argty,
-      qout = funres.qout + argout
+      qout = funres.qout + qty * argout
     }
 
   infer' ctx sg (CasePair pi pair ret body) = do
diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr
index 9894b1f..370862d 100644
--- a/tests/Tests/Typechecker.idr
+++ b/tests/Tests/Typechecker.idr
@@ -78,6 +78,7 @@ defGlobals = fromList
    ("a'", mkPostulate gany  $ FT "A"),
    ("b",  mkPostulate gany  $ FT "B"),
    ("f",  mkPostulate gany  $ Arr One (FT "A") (FT "A")),
+   ("fω", mkPostulate gany  $ Arr Any (FT "A") (FT "A")),
    ("g",  mkPostulate gany  $ Arr One (FT "A") (FT "B")),
    ("f2", mkPostulate gany  $ Arr One (FT "A") $ Arr One (FT "A") (FT "B")),
    ("p",  mkPostulate gany  $ PiY One "x" (FT "A") $ E $ F "P" :@ BVT 0),
@@ -236,6 +237,40 @@ tests = "typechecker" :- [
     note "(fail) runtime-relevant type",
     testTCFail "1 · A ⇏ ★₀" $
       infer_ empty sone (F "A"),
+    testTC "1 . f ⇒ 1.A → A" $
+      inferAs empty sone (F "f") (Arr One (FT "A") (FT "A")),
+    testTC "1 . f ⇐ 1.A → A" $
+      check_ empty sone (FT "f") (Arr One (FT "A") (FT "A")),
+    testTCFail "1 . f ⇍ 0.A → A" $
+      check_ empty sone (FT "f") (Arr Zero (FT "A") (FT "A")),
+    testTCFail "1 . f ⇍ ω.A → A" $
+      check_ empty sone (FT "f") (Arr Any (FT "A") (FT "A")),
+    testTC "1 . (λ x ⇒ f x) ⇐ 1.A → A" $
+      check_ empty sone
+        ([< "x"] :\\ E (F "f" :@ BVT 0))
+        (Arr One (FT "A") (FT "A")),
+    testTC "1 . (λ x ⇒ f x) ⇐ ω.A → A" $
+      check_ empty sone
+        ([< "x"] :\\ E (F "f" :@ BVT 0))
+        (Arr Any (FT "A") (FT "A")),
+    testTCFail "1 . (λ x ⇒ f x) ⇍ 0.A → A" $
+      check_ empty sone
+        ([< "x"] :\\ E (F "f" :@ BVT 0))
+        (Arr Zero (FT "A") (FT "A")),
+    testTC "1 . fω ⇒ ω.A → A" $
+      inferAs empty sone (F "fω") (Arr Any (FT "A") (FT "A")),
+    testTC "1 . (λ x ⇒ fω x) ⇐ ω.A → A" $
+      check_ empty sone
+        ([< "x"] :\\ E (F "fω" :@ BVT 0))
+        (Arr Any (FT "A") (FT "A")),
+    testTCFail "1 . (λ x ⇒ fω x) ⇍ 0.A → A" $
+      check_ empty sone
+        ([< "x"] :\\ E (F "fω" :@ BVT 0))
+        (Arr Zero (FT "A") (FT "A")),
+    testTCFail "1 . (λ x ⇒ fω x) ⇍ 1.A → A" $
+      check_ empty sone
+        ([< "x"] :\\ E (F "fω" :@ BVT 0))
+        (Arr One (FT "A") (FT "A")),
     note "refl : (0·A : ★₀) → (1·x : A) → (x ≡ x : A) ≔ (λ A x ⇒ δ _ ⇒ x)",
     testTC "1 · refl ⇒ ⋯" $ inferAs empty sone (F "refl") reflTy,
     testTC "1 · [refl] ⇐ ⋯" $ check_ empty sone (FT "refl") reflTy