From b2eb7610f424c2de8960cdf1843f5bcc3dc4af2e Mon Sep 17 00:00:00 2001
From: Victor Taelin <victor.taelin@gmail.com>
Date: Fri, 1 Mar 2024 23:31:05 -0300
Subject: [PATCH] fix type error, re-add qbool matchers

---
 book/QBool.match.kind2  | 42 +++++++++++++++++++++++++++++++++++++++++
 book/QBool2.match.kind2 | 27 ++++++++++++++++++++++++++
 src/kind2.hvm1          |  6 +++---
 3 files changed, 72 insertions(+), 3 deletions(-)
 create mode 100644 book/QBool.match.kind2
 create mode 100644 book/QBool2.match.kind2

diff --git a/book/QBool.match.kind2 b/book/QBool.match.kind2
new file mode 100644
index 00000000..1da6ede6
--- /dev/null
+++ b/book/QBool.match.kind2
@@ -0,0 +1,42 @@
+QBool.match
+: ∀(a: QBool)
+  ∀(P: ∀(x: QBool) *)
+  ∀(t: (P QBool.true))
+  ∀(f: (P QBool.false))
+  (P a)
+= λa λP λt λf
+  (~(~a P)
+    λx (P a)
+    λtag
+    #match tag = tag {
+      #0: λx (x t)
+      #+: λx
+      (#match tag_1 = tag-1 {
+        #0: λx (x f)
+        #+: λx (x λe (Empty.absurd e *)) 
+      }: ∀(x: 
+        ∀(x: 
+          #match tag_1 = tag_1 {
+            #0: (P QBool.false)
+            #+: ∀(x: Empty) * 
+          }: *
+        )
+        (P a)
+      )
+      (P a)
+        x
+      ) 
+    }: ∀(x: 
+      ∀(x: 
+        #match tag = tag {
+          #0: (P QBool.true)
+          #+: #match tag_1 = tag-1 {
+            #0: (P QBool.false)
+            #+: ∀(x: Empty) * 
+          }: * 
+        }: *
+      )
+      (P a)
+    )
+    (P a)
+  )
\ No newline at end of file
diff --git a/book/QBool2.match.kind2 b/book/QBool2.match.kind2
new file mode 100644
index 00000000..70ad05d3
--- /dev/null
+++ b/book/QBool2.match.kind2
@@ -0,0 +1,27 @@
+QBool2.match
+: ∀(a: QBool2)
+  ∀(P: ∀(x: QBool2) *)
+  ∀(t: (P QBool2.true))
+  ∀(f: (P QBool2.false))
+  (P a)
+= λa λP λt λf
+  (~a
+    P
+    λtag
+    #match tag = tag {
+      #0: t
+      #+: #match tag_1 = tag-1 {
+        #0: f
+        #+: λe (~e λx *) 
+      }: #match tag_1 = tag_1 {
+        #0: (P QBool2.false)
+        #+: ∀(e: Empty) * 
+      }: * 
+    }: #match tag = tag {
+      #0: (P QBool2.true)
+      #+: #match tag_1 = tag-1 {
+        #0: (P QBool2.false)
+        #+: ∀(e: Empty) * 
+      }: * 
+    }: *
+  )
\ No newline at end of file
diff --git a/src/kind2.hvm1 b/src/kind2.hvm1
index 7cc753a3..8687c451 100644
--- a/src/kind2.hvm1
+++ b/src/kind2.hvm1
@@ -320,13 +320,13 @@
 (Similar (Op2 a.opr a.fst a.snd) (Op2 b.opr b.fst b.snd) dep) =
   (Checker.bind (Equal a.fst b.fst dep) λe.fst
   (Checker.bind (Equal a.snd b.snd dep) λe.snd
-  (Checker.pure (Same e.fst e.snd))))
+  (Checker.pure (& e.fst e.snd))))
 (Similar (Mat a.nam a.x a.z a.s a.p) (Mat b.nam b.x b.z b.s b.p) dep) =
   (Checker.bind (Equal a.x b.x dep) λe.x
   (Checker.bind (Equal a.z b.z dep) λe.z
   (Checker.bind (Equal (a.s (Var (String.concat a.nam "-1") dep)) (b.s (Var (String.concat b.nam "-1") dep)) dep) λe.s
   (Checker.bind (Equal (a.p (Var a.nam dep)) (b.p (Var b.nam dep)) dep) λe.p
-  (& e.x (& e.z (& e.s e.p)))))))
+  (Checker.pure (& e.x (& e.z (& e.s e.p))))))))
 (Similar a b dep) =
   (Checker.pure 0)
 
@@ -384,7 +384,7 @@
   (Checker.bind (Identical a.z b.z dep) λi.z
   (Checker.bind (Identical (a.s (Var (String.concat a.nam "-1") dep)) (b.s (Var (String.concat b.nam "-1") dep)) dep) λi.s
   (Checker.bind (Identical (a.p (Var a.nam dep)) (b.p (Var b.nam dep)) dep) λi.p
-  (& i.x (& i.z (& i.s i.p)))))))
+  (Checker.pure (& i.x (& i.z (& i.s i.p))))))))
 (Identical.go (Txt a.txt) (Txt b.txt) dep) =
   (Checker.pure (Same a.txt b.txt))
 (Identical.go (Src a.src a.val) b dep) =