From d0d3e124cd8576b274b477c3c5ac848967cb2dc2 Mon Sep 17 00:00:00 2001
From: Jonathan Chan <jonathanhwchan@gmail.com>
Date: Wed, 9 Aug 2023 13:21:58 -0400
Subject: [PATCH] Fix Hurkens' paradox to type check all the way to M; improve
 error messages somewhat.

---
 pi/Hurkens.pi    | 13 ++++++-------
 pi/HurkensEx.pi  | 40 ++++++++++++++++------------------------
 src/Equal.hs     |  3 ++-
 src/TypeCheck.hs |  2 +-
 4 files changed, 25 insertions(+), 33 deletions(-)

diff --git a/pi/Hurkens.pi b/pi/Hurkens.pi
index e8d149e..39840b3 100644
--- a/pi/Hurkens.pi
+++ b/pi/Hurkens.pi
@@ -17,23 +17,22 @@ tau = \t. \x. \f. \p. t (\s. p (f (s x f)))
 sigma : U -> P (P U)
 sigma = \s. s U tau
 
-Delta : P U
-Delta = \y. neg ((p : P U) -> sigma y p -> p (tau (sigma y)))
+Delta : Type -> P U
+Delta = \b. \y. ((p : P U) -> sigma y p -> p (tau (sigma y))) -> b
 
 Omega : U
 Omega = tau (\p. (x : U) -> sigma x p -> p (\y. x y))
 
-M : (x : U) -> sigma x Delta -> Delta x
-M = \x. \two. \three. three Delta two (\p. three (\y. p (tau (sigma y))))
-
--- can't type check
+M : (x : U) -> sigma x (Delta Void) -> (Delta Void) x
+M = \x. \two. \three. three (Delta Void) two (\p. three (\y. p (tau (sigma y))))
 
 {-
 R : (p : P U) -> ((x : U) -> sigma x p -> p x) -> p Omega
 R = \zero. \one. one Omega (\x. one (tau (sigma x)))
 
 L : neg ((p : P U) -> ((x : U) -> sigma x p -> p x) -> p Omega)
-L = \zero. zero Delta M (\p. zero (\y. p (tau (sigma y))))
+L = \zero. zero (Delta Void) M (\p. zero (\y. p (tau (sigma y))))
+
 false : Void
 false = L R
 -}
\ No newline at end of file
diff --git a/pi/HurkensEx.pi b/pi/HurkensEx.pi
index 2013bdf..c9e1188 100644
--- a/pi/HurkensEx.pi
+++ b/pi/HurkensEx.pi
@@ -3,23 +3,19 @@ module HurkensEx where
 
 data Void : Type where {}
 
-neg : Type -> Type @ 0
-neg = \X. X -> Void
-
 P : Type -> Type @ 0
 P = \S. S -> Type
 
 U : Type @ 1
-U = (x : Type @ 0) -> (((P^0) ((P^0) x)) -> x) -> (P^0) ((P^0) x)
+U = (x : Type @ 0) -> (P^0 (P^0 x) -> x) -> P^0 (P^0 x)
 
-tau : ((P^0) ((P^0) (U^0))) -> (U^0) @ 1
+tau : P^0 (P^0 U^0) -> U^0 @ 1
 tau = \t. \x. \f. \p. t (\s. p (f (s x f)))
 
-sigma : U -> (P^0) ((P^0) (U^0)) @ 2
-sigma = \s. s (U^0) (tau^0)
+sigma : U^1 -> P^0 (P^0 U^0) @ 2
+sigma = \s. s U^0 tau^0
 
 {-
-
 s : U^1
 s : (x:*1) -> (P1 (P1 x) -> x) -> P1 (P1 x)
 
@@ -31,28 +27,24 @@ NOTE:
    P1 (P1 U0) = P0 (P0 U0)
    but *only* after expanding terms
    so we should keep track of which definitions are freely displaceable
-
 -}
 
+Delta : Type -> P^0 U^1 @ 2
+Delta = \b. \y. ((p : P^0 U^0 @ 1) -> sigma^0 y p -> p (tau^0 (sigma^0 y))) -> b
 
+Omega : U^0 @ 3
+Omega = tau^0 (\p. (x : U^1 @ 2) -> sigma^0 x p -> p (\y. x y))
 
-Delta : (P^0) U^1 @ 2
-Delta = \y. neg ((p : (P^0) (U^0) @ 1) -> (sigma^0) y p -> p ((tau^0) ((sigma^0) y)))
+M : (x : U^2 @ 3) -> sigma^1 x (Delta^0 Void^0) -> Delta^1 Void^0 x @ 4
+M = \x. \two. \three. three (Delta^0 Void^0) two (\p. three (\y. p (tau^0 (sigma^0 y))))
 
--- warning: parser is not good enough for U^1 @ 2, need to have parens around displaced term
-
-Omega : (U^0) @ 3
-Omega = (tau^0) (\p. (x : (U^1) @ 2) -> (sigma^0) x p -> p (\y. x y))
-
-M : (x : (U^2) @ 3) -> sigma^1 x Delta^0 -> Delta^1 x @ 4
-M = \x. \two. \three. three Delta^0 two (\p. three (\y. p ((tau^0) ((sigma^0) y))))
+{-
+R : (p : P^0 U^0) -> ((x : U^0) -> sigma^0 x p -> p x) -> p Omega^0
+R = \zero. \one. one Omega^0 (\x. one (tau^0 (sigma^0 x)))
 
+L : ((p : P^0 U^0) -> ((x : U^0) -> sigma^0 x p -> p x) -> p Omega^0) -> Void^0
+L = \zero. zero (Delta^0 Void^0) M (\p. zero (\y. p (tau^0 (sigma^0 y))))
 
-{-  -- can't type check
-R : (p : (P^0) (U^0)) -> ((x : (U^0)) -> (sigma^0) x p -> p x) -> p (Omega^0)
-R = \zero. \one. one (Omega^0) (\x. one ((tau^0) ((sigma^0) x)))
-L : neg ((p : (P^0) (U^0)) -> ((x : (U^0)) -> (sigma^0) x p -> p x) -> p (Omega^0))
-L = \zero. zero Delta M (\p. zero (\y. p ((tau^0) ((sigma^0) y))))
-false : Void
+false : Void^0
 false = L R
 -}
diff --git a/src/Equal.hs b/src/Equal.hs
index 5a5f229..e86be7d 100644
--- a/src/Equal.hs
+++ b/src/Equal.hs
@@ -83,7 +83,8 @@ equate' d t1 t2 = do
       (_, tyB1, _, tyB2) <- Unbound.unbind2Plus bnd1 bnd2
       unless (r1 == r2) $
           tyErr n2 n1
-      cs1 <- equateMaybeLevel l1 l2
+      cs1 <- Env.extendErr (equateMaybeLevel l1 l2) $
+        disp [DS "when equating", DD n1, DS "and", DD n2]
       cs2 <- equate' Shallow tyA1 tyA2
       cs3 <- equate' Shallow tyB1 tyB2
       return (cs1 <> cs2 <> cs3)
diff --git a/src/TypeCheck.hs b/src/TypeCheck.hs
index 52b8669..7e85747 100644
--- a/src/TypeCheck.hs
+++ b/src/TypeCheck.hs
@@ -334,7 +334,7 @@ tcTerm PrintMe (Just ty) mk = do
   cs <- Env.dumpConstraints
   let dcs = displayConstraints (Env.simplify cs)
   Env.warn $ [DS "Unmet obligation.\nContext:", DD gamma,
-        DS "\nGoal:", DD ty,
+        DS "\nGoal:", DD ty, DS " @ ", DD mk,
         DS "\nConstraints:"] ++ dcs
   ty' <- tcType ty mk
   return (ty', PrintMe)