make typechecker NotClo args implicit

lib/Quox/Typechecker.idr

@@ -79,7 +79,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
   checkC ctx sg subj ty =
     wrapErr (WhileChecking ctx sg.fst subj ty) $
       let Element subj nc = pushSubsts subj in
-      check' ctx sg subj nc ty
+      check' ctx sg subj ty
 
 
   ||| "Ψ | Γ ⊢ σ · e ⇒ A ⊳ Σ"
@@ -101,22 +101,22 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
   inferC ctx sg subj =
     wrapErr (WhileInferring ctx sg.fst subj) $
       let Element subj nc = pushSubsts subj in
-      infer' ctx sg subj nc
+      infer' ctx sg subj
 
 
   private covering
   check' : TyContext q d n -> SQty q ->
-           (subj : Term q d n) -> (0 nc : NotClo subj) -> Term q d n ->
+           (subj : Term q d n) -> (0 nc : NotClo subj) => Term q d n ->
            m (CheckResult' q n)
 
-  check' ctx sg (TYPE k) _ ty = do
+  check' ctx sg (TYPE k) ty = do
     -- if 𝓀 < ℓ then Ψ | Γ ⊢₀ Type 𝓀 ⇐ Type ℓ
     l <- expectTYPE !ask ty
     expectEqualQ zero sg.fst
     unless (k < l) $ throwError $ BadUniverse k l
     pure $ zeroFor ctx
 
-  check' ctx sg (Pi qty _ arg res) _ ty = do
+  check' ctx sg (Pi qty _ arg res) ty = do
     l <- expectTYPE !ask ty
     expectEqualQ zero sg.fst
     -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
@@ -128,7 +128,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- then Ψ | Γ ⊢₀ (π·x : A) → B ⇐ Type ℓ
     pure $ zeroFor ctx
 
-  check' ctx sg (Lam _ body) _ ty = do
+  check' ctx sg (Lam _ body) ty = do
     (qty, arg, res) <- expectPi !ask ty
     -- if Ψ | Γ, x : A ⊢ σ · t ⇐ B ⊳ Σ, ρ·x
     -- with ρ ≤ σπ
@@ -137,7 +137,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- then Ψ | Γ ⊢ σ · (λx ⇒ t) ⇐ (π·x : A) → B ⊳ Σ
     popQ qty' qout
 
-  check' ctx sg (Sig _ fst snd) _ ty = do
+  check' ctx sg (Sig _ fst snd) ty = do
     l <- expectTYPE !ask ty
     expectEqualQ zero sg.fst
     -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
@@ -149,7 +149,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- then Ψ | Γ ⊢₀ (x : A) × B ⇐ Type ℓ
     pure $ zeroFor ctx
 
-  check' ctx sg (Pair fst snd) _ ty = do
+  check' ctx sg (Pair fst snd) ty = do
     (tfst, tsnd) <- expectSig !ask ty
     -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ₁
     qfst <- checkC ctx sg fst tfst
@@ -159,7 +159,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- then Ψ | Γ ⊢ σ · (s, t) ⇐ (x : A) × B ⊳ Σ₁ + Σ₂
     pure $ qfst + qsnd
 
-  check' ctx sg (Eq i t l r) _ ty = do
+  check' ctx sg (Eq _ t l r) ty = do
     u <- expectTYPE !ask ty
     expectEqualQ zero sg.fst
     -- if Ψ, i | Γ ⊢₀ A ⇐ Type ℓ
@@ -173,7 +173,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- then Ψ | Γ ⊢₀ Eq [i ⇒ A] l r ⇐ Type ℓ
     pure $ zeroFor ctx
 
-  check' ctx sg (DLam i body) _ ty = do
+  check' ctx sg (DLam _ body) ty = do
     (ty, l, r) <- expectEq !ask ty
     -- if Ψ, i | Γ ⊢ σ · t ⇐ A ⊳ Σ
     qout <- checkC (extendDim ctx) sg body.term ty.term
@@ -184,7 +184,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- then Ψ | Γ ⊢ σ · (λᴰi ⇒ t) ⇐ Eq [i ⇒ A] l r ⊳ Σ
     pure qout
 
-  check' ctx sg (E e) _ ty = do
+  check' ctx sg (E e) ty = do
     -- if Ψ | Γ ⊢ σ · e ⇒ A' ⊳ Σ
     infres <- inferC ctx sg e
     -- if Ψ | Γ ⊢ A' <: A
@@ -194,10 +194,10 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
 
   private covering
   infer' : TyContext q d n -> SQty q ->
-           (subj : Elim q d n) -> (0 nc : NotClo subj) ->
+           (subj : Elim q d n) -> (0 nc : NotClo subj) =>
            m (InferResult' q d n)
 
-  infer' ctx sg (F x) _ = do
+  infer' ctx sg (F x) = do
     -- if π·x : A {≔ s} in global context
     g <- lookupFree x
     -- if σ ≤ π
@@ -205,12 +205,12 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ 𝟎
     pure $ InfRes {type = g.type.get, qout = zeroFor ctx}
 
-  infer' ctx sg (B i) _ =
+  infer' ctx sg (B i) =
     -- if x : A ∈ Γ
     -- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ (𝟎, σ·x, 𝟎)
     pure $ lookupBound sg.fst i ctx.tctx
 
-  infer' ctx sg (fun :@ arg) _ = do
+  infer' ctx sg (fun :@ arg) = do
     -- if Ψ | Γ ⊢ σ · f ⇒ (π·x : A) → B ⊳ Σ₁
     funres <- inferC ctx sg fun
     (qty, argty, res) <- expectPi !ask funres.type
@@ -222,7 +222,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
       qout = funres.qout + argout
     }
 
-  infer' ctx sg (CasePair pi pair _ ret _ _ body) _ = do
+  infer' ctx sg (CasePair pi pair _ ret _ _ body) = do
     -- if 1 ≤ π
     expectCompatQ one pi
     -- if Ψ | Γ ⊢ 1 · pair ⇒ (x : A) × B ⊳ Σ₁
@@ -233,21 +233,21 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- with ρ₁, ρ₂ ≤ π
     let bodyctx = extendTyN [< tfst, tsnd.term] ctx
         bodyty  = substCasePairRet pairres.type ret
-    bodyout <- checkC bodyctx sg body.term bodyty >>= popQs [< pi, pi]
+    bodyout <- popQs [< pi, pi] !(checkC bodyctx sg body.term bodyty)
     -- then Ψ | Γ ⊢ σ · case ⋯ ⇒ ret[pair] ⊳ πΣ₁ + Σ₂
     pure $ InfRes {
       type = sub1 ret pair,
       qout = pi * pairres.qout + bodyout
     }
 
-  infer' ctx sg (fun :% dim) _ = do
+  infer' ctx sg (fun :% dim) = do
     -- if Ψ | Γ ⊢ σ · f ⇒ Eq [i ⇒ A] l r ⊳ Σ
     InfRes {type, qout} <- inferC ctx sg fun
-    (ty, _, _) <- expectEq !ask type
+    ty <- fst <$> expectEq !ask type
     -- then Ψ | Γ ⊢ σ · f p ⇒ A‹p› ⊳ Σ
     pure $ InfRes {type = dsub1 ty dim, qout}
 
-  infer' ctx sg (term :# type) _ = do
+  infer' ctx sg (term :# type) = do
     -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
     check0 ctx type (TYPE UAny)
     -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ