From 3fe9b96f05893cf9e9d2881a6497070691b058a1 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 17 Sep 2023 20:09:33 +0200
Subject: [PATCH] make function types with an empty domain subsingletons

this is useful for the base cases of W types when i try those again

closes #23
---
 examples/eta.quox  |  7 ++++++
 lib/Quox/Equal.idr | 53 ++++++++++++++++++++++++++++++++++++++++------
 2 files changed, 54 insertions(+), 6 deletions(-)

diff --git a/examples/eta.quox b/examples/eta.quox
index 1e9dadd..452a4d4 100644
--- a/examples/eta.quox
+++ b/examples/eta.quox
@@ -1,3 +1,5 @@
+load "misc.quox"
+
 namespace eta {
 
 def0 Π : (A : ★) → (A → ★) → ★ = λ A B ⇒ (x : A) → B x
@@ -10,4 +12,9 @@ def0 box : (A : ★) → (P : [ω.A] → ★) → (e : [ω.A]) →
            P [case1 e return A of {[x] ⇒ x}] → P e =
   λ A P e p ⇒ p
 
+-- not exactly η, but kinda related
+def0 from-false : (A : ★) → (P : (False → A) → ★) → (f : False → A) →
+                  P (λ x ⇒ void A x) → P f =
+  λ A P f p ⇒ p
+
 }
diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index d220039..d847cf2 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -63,11 +63,44 @@ sameTyCon (E    {}) (E    {}) = True
 sameTyCon (E    {}) _         = False
 
 
+||| true if a type is known to be empty.
+|||
+||| * a pair is empty if either element is.
+||| * `{}` is empty.
+||| * `[π.A]` is empty if `A` is.
+||| * that's it.
+public export covering
+isEmpty : {n : Nat} -> Definitions -> EqContext n -> Term 0 n ->
+          Eff EqualInner Bool
+isEmpty defs ctx ty0 = do
+  Element ty0 nc <- whnf defs ctx ty0.loc ty0
+  case ty0 of
+    TYPE {} => pure False
+    Pi {arg, res, _} => pure False
+    Sig {fst, snd, _} =>
+      isEmpty defs ctx fst `orM`
+      isEmpty defs (extendTy0 snd.name fst ctx) snd.term
+    Enum {cases, _} =>
+      pure $ null cases
+    Eq {} => pure False
+    Nat {} => pure False
+    BOX {ty, _} => isEmpty defs ctx ty
+    E (Ann {tm, _}) => isEmpty defs ctx tm
+    E _ => pure False
+    Lam  {} => pure False
+    Pair {} => pure False
+    Tag  {} => pure False
+    DLam {} => pure False
+    Zero {} => pure False
+    Succ {} => pure False
+    Box  {} => pure False
+
 ||| true if a type is known to be a subsingleton purely by its form.
 ||| a subsingleton is a type with only zero or one possible values.
 ||| equality/subtyping accepts immediately on values of subsingleton types.
 |||
-||| * a function type is a subsingleton if its codomain is.
+||| * a function type is a subsingleton if its codomain is,
+|||   or if its domain is empty.
 ||| * a pair type is a subsingleton if both its elements are.
 ||| * equality types are subsingletons because of uip.
 ||| * an enum type is a subsingleton if it has zero or one tags.
@@ -80,6 +113,7 @@ isSubSing defs ctx ty0 = do
   case ty0 of
     TYPE {} => pure False
     Pi {arg, res, _} =>
+      isEmpty defs ctx arg `orM`
       isSubSing defs (extendTy0 res.name arg ctx) res.term
     Sig {fst, snd, _} =>
       isSubSing defs ctx fst `andM`
@@ -143,13 +177,17 @@ compareType : Definitions -> EqContext n -> (s, t : Term 0 n) ->
 namespace Term
   private covering
   compare0' : (defs : Definitions) -> EqContext n ->
-               (ty, s, t : Term 0 n) ->
-               (0 _ : NotRedex defs ty) => (0 _ : So (isTyConE ty)) =>
-               (0 _ : NotRedex defs s)  => (0 _ : NotRedex defs t) =>
-               Eff EqualInner ()
+              (ty, s, t : Term 0 n) ->
+              (0 _ : NotRedex defs ty) => (0 _ : So (isTyConE ty)) =>
+              (0 _ : NotRedex defs s)  => (0 _ : NotRedex defs t) =>
+              Eff EqualInner ()
   compare0' defs ctx (TYPE {}) s t = compareType defs ctx s t
 
-  compare0' defs ctx ty@(Pi {qty, arg, res, _}) s t {n} = local_ Equal $
+  compare0' defs ctx ty@(Pi {qty, arg, res, _}) s t = local_ Equal $
+    --              Γ ⊢ A empty
+    -- -------------------------------------------
+    --  Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) : (π·x : A) → B
+    if !(isEmpty' arg) then pure () else
     case (s, t) of
       --           Γ, x : A ⊢ s = t : B
       -- -------------------------------------------
@@ -169,6 +207,9 @@ namespace Term
       (E _,    t) => wrongType t.loc ctx ty t
       (s,      _) => wrongType s.loc ctx ty s
   where
+    isEmpty' : Term 0 n -> Eff EqualInner Bool
+    isEmpty' t = let Val n = ctx.termLen in isEmpty defs ctx arg
+
     ctx' : EqContext (S n)
     ctx' = extendTy qty res.name arg ctx