check for 0=1 in typechecker

2023-02-19 17:51:44 +01:00 · 2023-02-19 17:51:44 +01:00 · 858b5db530
commit 858b5db530
parent 195791e158
5 changed files with 95 additions and 55 deletions
--- 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 [<]
--- 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}
--- 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
--- 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)
--- 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" :- [