From 858b5db530f27cc438b6684cfc576fc1451a3b51 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 19 Feb 2023 17:51:44 +0100
Subject: [PATCH] check for 0=1 in typechecker

---
 lib/Quox/Syntax/DimEq.idr   |  6 +++
 lib/Quox/Typechecker.idr    | 95 ++++++++++++++++++++++---------------
 lib/Quox/Typing.idr         | 14 ++++--
 tests/Tests/Equal.idr       |  2 +-
 tests/Tests/Typechecker.idr | 33 ++++++++-----
 5 files changed, 95 insertions(+), 55 deletions(-)

diff --git a/lib/Quox/Syntax/DimEq.idr b/lib/Quox/Syntax/DimEq.idr
index d761bcb..1ee5d39 100644
--- a/lib/Quox/Syntax/DimEq.idr
+++ b/lib/Quox/Syntax/DimEq.idr
@@ -28,6 +28,12 @@ data DimEq : Nat -> Type where
 %name DimEq eqs
 
 
+public export
+data IfConsistent : DimEq d -> a -> Type where
+  Nothing :      IfConsistent ZeroIsOne a
+  Just    : a -> IfConsistent (C eqs)   a
+
+
 export %inline
 zeroEq : DimEq 0
 zeroEq = C [<]
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index 436023e..1056e14 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -1,11 +1,7 @@
 module Quox.Typechecker
 
-import public Quox.Syntax
 import public Quox.Typing
 import public Quox.Equal
-import public Control.Monad.Either
-import Decidable.Decidable
-import Data.SnocVect
 
 %default total
 
@@ -22,7 +18,7 @@ CanTC q = CanTC' q IsGlobal
 
 private
 popQs : HasErr q m => IsQty q =>
-        SnocVect s q -> QOutput q (s + n) -> m (QOutput q n)
+        QOutput q s -> QOutput q (s + n) -> m (QOutput q n)
 popQs [<]         qout         = pure qout
 popQs (pis :< pi) (qout :< rh) = do expectCompatQ rh pi; popQs pis qout
 
@@ -33,20 +29,15 @@ popQ pi = popQs [< pi]
 
 
 private %inline
-tail : TyContext q d (S n) -> TyContext q d n
-tail = {tctx $= tail}
-
-
-private %inline
-weakI : IsQty q => InferResult q d n -> InferResult q d (S n)
+weakI : IsQty q => InferResult' q d n -> InferResult' q d (S n)
 weakI = {type $= weakT, qout $= (:< zero)}
 
 private
-lookupBound : IsQty q => q -> Var n -> TyContext q d n -> InferResult q d n
-lookupBound pi VZ (MkTyContext {tctx = tctx :< ty, _}) =
-  InfRes {type = weakT ty, qout = (zero <$ tctx) :< pi}
-lookupBound pi (VS i) ctx =
-  weakI $ lookupBound pi i (tail ctx)
+lookupBound : IsQty q => q -> Var n -> TContext q d n -> InferResult' q d n
+lookupBound pi VZ (ctx :< ty) =
+  InfRes {type = weakT ty, qout = (zero <$ ctx) :< pi}
+lookupBound pi (VS i) (ctx :< _) =
+  weakI $ lookupBound pi i ctx
 
 private %inline
 lookupFree : CanTC' q g m => Name -> m (Definition' q g)
@@ -65,12 +56,16 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
   ||| `check ctx sg subj ty` checks that in the context `ctx`, the term
   ||| `subj` has the type `ty`, with quantity `sg`. if so, returns the
   ||| quantities of all bound variables that it used.
+  |||
+  ||| if the dimension context is inconsistent, then return `Nothing`, without
+  ||| doing any further work.
   export covering %inline
-  check : TyContext q d n -> SQty q -> Term q d n -> Term q d n ->
-          m (CheckResult q n)
-  check ctx sg subj ty =
-    let Element subj nc = pushSubsts subj in
-    check' ctx sg subj nc ty
+  check : (ctx : TyContext q d n) -> SQty q -> Term q d n -> Term q d n ->
+          m (CheckResult ctx.dctx q n)
+  check ctx@(MkTyContext {dctx, _}) sg subj ty =
+    case dctx of
+      ZeroIsOne => pure Nothing
+      C _       => Just <$> checkC ctx sg subj ty
 
   ||| "Ψ | Γ ⊢₀ s ⇐ A"
   |||
@@ -80,21 +75,43 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
   check0 ctx tm ty = ignore $ check ctx szero tm ty
     -- the output will always be 𝟎 because the subject quantity is 0
 
+  ||| `check`, assuming the dimension context is consistent
+  export covering %inline
+  checkC : (ctx : TyContext q d n) -> SQty q -> Term q d n -> Term q d n ->
+           m (CheckResult' q n)
+  checkC ctx sg subj ty =
+    let Element subj nc = pushSubsts subj in
+    check' ctx sg subj nc ty
+
+
   ||| "Ψ | Γ ⊢ σ · e ⇒ A ⊳ Σ"
   |||
   ||| `infer ctx sg subj` infers the type of `subj` in the context `ctx`,
   ||| and returns its type and the bound variables it used.
+  |||
+  ||| if the dimension context is inconsistent, then return `Nothing`, without
+  ||| doing any further work.
   export covering %inline
-  infer : TyContext q d n -> SQty q -> Elim q d n -> m (InferResult q d n)
-  infer ctx sg subj =
+  infer : (ctx : TyContext q d n) -> SQty q -> Elim q d n ->
+          m (InferResult ctx.dctx q d n)
+  infer ctx@(MkTyContext {dctx, _}) sg subj =
+    case dctx of
+      ZeroIsOne => pure Nothing
+      C _       => Just <$> inferC ctx sg subj
+
+  ||| `infer`, assuming the dimension context is consistent
+  export covering %inline
+  inferC : (ctx : TyContext q d n) -> SQty q -> Elim q d n ->
+           m (InferResult' q d n)
+  inferC ctx sg subj =
     let Element subj nc = pushSubsts subj in
     infer' ctx sg subj nc
 
 
-  export covering
+  private covering
   check' : TyContext q d n -> SQty q ->
            (subj : Term q d n) -> (0 nc : NotClo subj) -> Term q d n ->
-           m (CheckResult q n)
+           m (CheckResult' q n)
 
   check' ctx sg (TYPE k) _ ty = do
     -- if 𝓀 < ℓ then Ψ | Γ ⊢₀ Type 𝓀 ⇐ Type ℓ
@@ -120,7 +137,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- if Ψ | Γ, x : A ⊢ σ · t ⇐ B ⊳ Σ, ρ·x
     -- with ρ ≤ σπ
     let qty' = sg.fst * qty
-    qout <- check (extendTy arg ctx) sg body.term res.term
+    qout <- checkC (extendTy arg ctx) sg body.term res.term
     -- then Ψ | Γ ⊢ σ · (λx ⇒ t) ⇐ (π·x : A) → B ⊳ Σ
     popQ qty' qout
 
@@ -139,10 +156,10 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
   check' ctx sg (Pair fst snd) _ ty = do
     (tfst, tsnd) <- expectSig !ask ty
     -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ₁
-    qfst <- check ctx sg fst tfst
+    qfst <- checkC ctx sg fst tfst
     let tsnd = sub1 tsnd (fst :# tfst)
     -- if Ψ | Γ ⊢ σ · t ⇐ B[s] ⊳ Σ₂
-    qsnd <- check ctx sg snd tsnd
+    qsnd <- checkC ctx sg snd tsnd
     -- then Ψ | Γ ⊢ σ · (s, t) ⇐ (x : A) × B ⊳ Σ₁ + Σ₂
     pure $ qfst + qsnd
 
@@ -163,7 +180,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
   check' ctx sg (DLam i body) _ ty = do
     (ty, l, r) <- expectEq !ask ty
     -- if Ψ, i | Γ ⊢ σ · t ⇐ A ⊳ Σ
-    qout <- check (extendDim ctx) sg body.term ty.term
+    qout <- checkC (extendDim ctx) sg body.term ty.term
     -- if Ψ | Γ ⊢ t‹0› = l : A‹0›
     equal ctx ty.zero body.zero l
     -- if Ψ | Γ ⊢ t‹1› = r : A‹1›
@@ -173,16 +190,16 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
 
   check' ctx sg (E e) _ ty = do
     -- if Ψ | Γ ⊢ σ · e ⇒ A' ⊳ Σ
-    infres <- infer ctx sg e
+    infres <- inferC ctx sg e
     -- if Ψ | Γ ⊢ A' <: A
     subtype ctx infres.type ty
     -- then Ψ | Γ ⊢ σ · e ⇐ A ⊳ Σ
     pure infres.qout
 
-  export covering
+  private covering
   infer' : TyContext q d n -> SQty q ->
            (subj : Elim q d n) -> (0 nc : NotClo subj) ->
-           m (InferResult q d n)
+           m (InferResult' q d n)
 
   infer' ctx sg (F x) _ = do
     -- if π·x : A {≔ s} in global context
@@ -195,14 +212,14 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
   infer' ctx sg (B i) _ =
     -- if x : A ∈ Γ
     -- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ (𝟎, σ·x, 𝟎)
-    pure $ lookupBound sg.fst i ctx
+    pure $ lookupBound sg.fst i ctx.tctx
 
   infer' ctx sg (fun :@ arg) _ = do
     -- if Ψ | Γ ⊢ σ · f ⇒ (π·x : A) → B ⊳ Σ₁
-    funres <- infer ctx sg fun
+    funres <- inferC ctx sg fun
     (qty, argty, res) <- expectPi !ask funres.type
     -- if Ψ | Γ ⊢ σ ⨴ π · s ⇐ A ⊳ Σ₂
-    argout <- check ctx (subjMult sg qty) arg argty
+    argout <- checkC ctx (subjMult sg qty) arg argty
     -- then Ψ | Γ ⊢ σ · f s ⇒ B[s] ⊳ Σ₁ + Σ₂
     pure $ InfRes {
       type = sub1 res $ arg :# argty,
@@ -213,14 +230,14 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- if 1 ≤ π
     expectCompatQ one pi
     -- if Ψ | Γ ⊢ 1 · pair ⇒ (x : A) × B ⊳ Σ₁
-    pairres <- infer ctx sone pair
+    pairres <- inferC ctx sone pair
     check0 (extendTy pairres.type ctx) ret.term (TYPE UAny)
     (tfst, tsnd) <- expectSig !ask pairres.type
     -- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐ ret[(x, y)] ⊳ Σ₂, ρ₁·x, ρ₂·y
     -- with ρ₁, ρ₂ ≤ π
     let bodyctx = extendTyN [< tfst, tsnd.term] ctx
         bodyty  = substCasePairRet pairres.type ret
-    bodyout <- check bodyctx sg body.term bodyty >>= popQs [< pi, pi]
+    bodyout <- checkC bodyctx sg body.term bodyty >>= popQs [< pi, pi]
     -- then Ψ | Γ ⊢ σ · case ⋯ ⇒ ret[pair] ⊳ πΣ₁ + Σ₂
     pure $ InfRes {
       type = sub1 ret pair,
@@ -229,7 +246,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
 
   infer' ctx sg (fun :% dim) _ = do
     -- if Ψ | Γ ⊢ σ · f ⇒ Eq [i ⇒ A] l r ⊳ Σ
-    InfRes {type, qout} <- infer ctx sg fun
+    InfRes {type, qout} <- inferC ctx sg fun
     (ty, _, _) <- expectEq !ask type
     -- then Ψ | Γ ⊢ σ · f p ⇒ A‹p› ⊳ Σ
     pure $ InfRes {type = dsub1 ty dim, qout}
@@ -238,6 +255,6 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
     check0 ctx type (TYPE UAny)
     -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
-    qout <- check ctx sg term type
+    qout <- checkC ctx sg term type
     -- then Ψ | Γ ⊢ σ · (s ∷ A) ⇒ A ⊳ Σ
     pure $ InfRes {type, qout}
diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr
index af3afb9..9407953 100644
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@@ -82,15 +82,23 @@ namespace QOutput
 
 
 public export
-CheckResult : Type -> Nat -> Type
-CheckResult = QOutput
+CheckResult' : Type -> Nat -> Type
+CheckResult' = QOutput
 
 public export
-record InferResult q d n where
+CheckResult : DimEq d -> Type -> Nat -> Type
+CheckResult eqs q n = IfConsistent eqs $ CheckResult' q n
+
+public export
+record InferResult' q d n where
   constructor InfRes
   type : Term q d n
   qout : QOutput q n
 
+public export
+InferResult : DimEq d -> TermLike
+InferResult eqs q d n = IfConsistent eqs $ InferResult' q d n
+
 
 public export
 data EqMode = Equal | Sub | Super
diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr
index 73f9b38..32e27b2 100644
--- a/tests/Tests/Equal.idr
+++ b/tests/Tests/Equal.idr
@@ -384,7 +384,7 @@ tests = "equality & subtyping" :- [
     testEq "a‹𝟎› = a" $
       equalED 1 empty (DCloE (F "a") (K Zero ::: id)) (F "a"),
     testEq "(f [a])‹𝟎› = f‹𝟎› [a]‹𝟎›" $
-      let th = (K Zero ::: id) in
+      let th = K Zero ::: id in
       equalED 1 empty
         (DCloE (F "f" :@ FT "a") th)
         (DCloE (F "f") th :@ DCloT (FT "a") th)
diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr
index 6d8f931..cb3633b 100644
--- a/tests/Tests/Typechecker.idr
+++ b/tests/Tests/Typechecker.idr
@@ -83,25 +83,29 @@ qoutEq qout res = unless (qout == res) $ throwError $ WrongQOut qout res
 
 inferAs : TyContext Three d n -> (sg : SQty Three) ->
           Elim Three d n -> Term Three d n -> M ()
-inferAs ctx sg e ty = do
-  res <- inj $ infer ctx sg e
-  inferredTypeEq ctx ty res.type
+inferAs ctx@(MkTyContext {dctx, _}) sg e ty = do
+  case !(inj $ infer ctx sg e) of
+    Just res => inferredTypeEq ctx ty res.type
+    Nothing  => pure ()
 
 inferAsQ : TyContext Three d n -> (sg : SQty Three) ->
            Elim Three d n -> Term Three d n -> QOutput Three n -> M ()
-inferAsQ ctx sg e ty qout = do
-  res <- inj $ infer ctx sg e
-  inferredTypeEq ctx ty res.type
-  qoutEq qout res.qout
+inferAsQ ctx@(MkTyContext {dctx, _}) sg e ty qout = do
+  case !(inj $ infer ctx sg e) of
+    Just res => do
+      inferredTypeEq ctx ty res.type
+      qoutEq qout res.qout
+    Nothing => pure ()
 
 infer_ : TyContext Three d n -> (sg : SQty Three) -> Elim Three d n -> M ()
 infer_ ctx sg e = ignore $ inj $ infer ctx sg e
 
 checkQ : TyContext Three d n -> SQty Three ->
          Term Three d n -> Term Three d n -> QOutput Three n -> M ()
-checkQ ctx sg s ty qout = do
-  res <- inj $ check ctx sg s ty
-  qoutEq qout res
+checkQ ctx@(MkTyContext {dctx, _}) sg s ty qout = do
+  case !(inj $ check ctx sg s ty) of
+    Just res => qoutEq qout res
+    Nothing  => pure ()
 
 check_ : TyContext Three d n -> SQty Three ->
          Term Three d n -> Term Three d n -> M ()
@@ -117,7 +121,9 @@ tests = "typechecker" :- [
     testTCFail "0 · ★₁ ⇍ ★₀" $ check_ (ctx [<]) szero (TYPE 1) (TYPE 0),
     testTCFail "0 · ★₀ ⇍ ★₀" $ check_ (ctx [<]) szero (TYPE 0) (TYPE 0),
     testTCFail "0 · ★_ ⇍ ★_" $ check_ (ctx [<]) szero (TYPE UAny) (TYPE UAny),
-    testTCFail "1 · ★₀ ⇍ ★₁" $ check_ (ctx [<]) sone (TYPE 0) (TYPE 1)
+    testTCFail "1 · ★₀ ⇍ ★₁" $ check_ (ctx [<]) sone (TYPE 0) (TYPE 1),
+    testTC "0=1 ⊢ 0 · ★₁ ⇐ ★₀" $
+      check_ (MkTyContext (ZeroIsOne {d = 0}) [<]) szero (TYPE 1) (TYPE 0)
   ],
 
   "function types" :- [
@@ -136,7 +142,10 @@ tests = "typechecker" :- [
         (Pi One "x" (FT "A") $ TUsed $ E $ F "P" :@ BVT 0)
         (TYPE 0),
     testTCFail "0 · A ⊸ P ⇍ ★₀" $
-      check_ (ctx [<]) szero (Arr One (FT "A") $ FT "P") (TYPE 0)
+      check_ (ctx [<]) szero (Arr One (FT "A") $ FT "P") (TYPE 0),
+    testTC "0=1 ⊢ 0 · A ⊸ P ⇐ ★₀" $
+      check_ (MkTyContext (ZeroIsOne {d = 0}) [<]) szero
+        (Arr One (FT "A") $ FT "P") (TYPE 0)
   ],
 
   "pair types" :- [