fix: changed checker.hvm construtor from Term.u60 to Term.U60 and Term.num to Term.u60

Cargo.lock

@@ -461,8 +461,8 @@ checksum = "809e18805660d7b6b2e2b9f316a5099521b5998d5cba4dda11b5157a21aaef03"
 
 [[package]]
 name = "hvm"
-version = "1.0.5-beta"
-source = "git+https://github.com/Kindelia/HVM.git#0b191cdb5f8997a7e9c257d709c522e06d331b73"
+version = "1.0.7-beta"
+source = "git+https://github.com/Kindelia/HVM.git?rev=5599e0c8504bee976b7870b51f0c2d4b57e3bf82#5599e0c8504bee976b7870b51f0c2d4b57e3bf82"
 dependencies = [
  "clap 3.2.23",
  "crossbeam",
@@ -1372,9 +1372,9 @@ checksum = "73473c0e59e6d5812c5dfe2a064a6444949f089e20eec9a2e5506596494e4623"
 
 [[package]]
 name = "syn"
-version = "1.0.104"
+version = "1.0.105"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4ae548ec36cf198c0ef7710d3c230987c2d6d7bd98ad6edc0274462724c585ce"
+checksum = "60b9b43d45702de4c839cb9b51d9f529c5dd26a4aff255b42b1ebc03e88ee908"
 dependencies = [
  "proc-macro2",
  "quote",

crates/kind-checker/Cargo.toml

@@ -10,7 +10,7 @@ kind-tree = { path = "../kind-tree" }
 kind-span = { path = "../kind-span" }
 kind-report = { path = "../kind-report" }
 
-hvm = { git = "https://github.com/Kindelia/HVM.git" }
+hvm = { git = "https://github.com/Kindelia/HVM.git", rev="5599e0c8504bee976b7870b51f0c2d4b57e3bf82" }
 
 fxhash = "0.2.1"
 im-rc = "15.1.0"

crates/kind-checker/src/checker.hvm

@@ -1,51 +1,4 @@
 (Main) = let imports = [(Dynamic.new λa λb (Kind.Term.set_origin a b)), (Dynamic.new (Kind.API.check_all)), (Dynamic.new (Kind.API.eval_main))]; (Kind.API.check_all)
-(Kind.Term.set_origin new_origin (Kind.Term.typ old_orig)) = (Kind.Term.typ new_origin)
-(Kind.Term.set_origin new_origin (Kind.Term.var old_orig name idx)) = (Kind.Term.var new_origin name idx)
-(Kind.Term.set_origin new_origin (Kind.Term.hol old_orig numb)) = (Kind.Term.hol new_origin numb)
-(Kind.Term.set_origin new_origin (Kind.Term.all old_orig name typ body)) = (Kind.Term.all new_origin name typ body)
-(Kind.Term.set_origin new_origin (Kind.Term.lam old_orig name body)) = (Kind.Term.lam new_origin name body)
-(Kind.Term.set_origin new_origin (Kind.Term.let old_orig name expr body)) = (Kind.Term.let new_origin name expr body)
-(Kind.Term.set_origin new_origin (Kind.Term.ann old_orig expr typ)) = (Kind.Term.ann new_origin expr typ)
-(Kind.Term.set_origin new_origin (Kind.Term.sub old_orig name indx redx expr)) = (Kind.Term.sub new_origin name indx redx expr)
-(Kind.Term.set_origin new_origin (Kind.Term.app old_orig func arg)) = (Kind.Term.app new_origin func arg)
-(Kind.Term.set_origin new_origin (Kind.Term.hlp old_orig)) = (Kind.Term.hlp new_origin)
-(Kind.Term.set_origin new_origin (Kind.Term.u60 old_orig)) = (Kind.Term.u60 new_origin)
-(Kind.Term.set_origin new_origin (Kind.Term.num old_orig num)) = (Kind.Term.num new_origin num)
-(Kind.Term.set_origin new_origin (Kind.Term.op2 old_orig op left right)) = (Kind.Term.op2 new_origin op left right)
-(Kind.Term.set_origin new_origin (Kind.Term.ct0 ctid old_orig)) = (Kind.Term.ct0 ctid new_origin)
-(Kind.Term.set_origin new_origin (Kind.Term.ct1 ctid old_orig x0)) = (Kind.Term.ct1 ctid new_origin x0)
-(Kind.Term.set_origin new_origin (Kind.Term.ct2 ctid old_orig x0 x1)) = (Kind.Term.ct2 ctid new_origin x0 x1)
-(Kind.Term.set_origin new_origin (Kind.Term.ct3 ctid old_orig x0 x1 x2)) = (Kind.Term.ct3 ctid new_origin x0 x1 x2)
-(Kind.Term.set_origin new_origin (Kind.Term.ct4 ctid old_orig x0 x1 x2 x3)) = (Kind.Term.ct4 ctid new_origin x0 x1 x2 x3)
-(Kind.Term.set_origin new_origin (Kind.Term.ct5 ctid old_orig x0 x1 x2 x3 x4)) = (Kind.Term.ct5 ctid new_origin x0 x1 x2 x3 x4)
-(Kind.Term.set_origin new_origin (Kind.Term.ct6 ctid old_orig x0 x1 x2 x3 x4 x5)) = (Kind.Term.ct6 ctid new_origin x0 x1 x2 x3 x4 x5)
-(Kind.Term.set_origin new_origin (Kind.Term.ct7 ctid old_orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Term.ct7 ctid new_origin x0 x1 x2 x3 x4 x5 x6)
-(Kind.Term.set_origin new_origin (Kind.Term.ct8 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Term.ct8 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7)
-(Kind.Term.set_origin new_origin (Kind.Term.ct9 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Term.ct9 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8)
-(Kind.Term.set_origin new_origin (Kind.Term.ct10 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Term.ct10 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)
-(Kind.Term.set_origin new_origin (Kind.Term.ct11 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Term.ct11 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)
-(Kind.Term.set_origin new_origin (Kind.Term.ct12 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Term.ct12 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)
-(Kind.Term.set_origin new_origin (Kind.Term.ct13 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Term.ct13 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)
-(Kind.Term.set_origin new_origin (Kind.Term.ct14 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Term.ct14 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)
-(Kind.Term.set_origin new_origin (Kind.Term.ct15 ctid old_orig args)) = (Kind.Term.ct15 ctid new_origin args)
-(Kind.Term.set_origin new_origin (Kind.Term.ct16 ctid old_orig args)) = (Kind.Term.ct16 ctid new_origin args)
-(Kind.Term.set_origin new_origin (Kind.Term.fn0 fnid old_orig)) = (Kind.Term.fn0 fnid new_origin)
-(Kind.Term.set_origin new_origin (Kind.Term.fn1 fnid old_orig x0)) = (Kind.Term.fn1 fnid new_origin x0)
-(Kind.Term.set_origin new_origin (Kind.Term.fn2 fnid old_orig x0 x1)) = (Kind.Term.fn2 fnid new_origin x0 x1)
-(Kind.Term.set_origin new_origin (Kind.Term.fn3 fnid old_orig x0 x1 x2)) = (Kind.Term.fn3 fnid new_origin x0 x1 x2)
-(Kind.Term.set_origin new_origin (Kind.Term.fn4 fnid old_orig x0 x1 x2 x3)) = (Kind.Term.fn4 fnid new_origin x0 x1 x2 x3)
-(Kind.Term.set_origin new_origin (Kind.Term.fn5 fnid old_orig x0 x1 x2 x3 x4)) = (Kind.Term.fn5 fnid new_origin x0 x1 x2 x3 x4)
-(Kind.Term.set_origin new_origin (Kind.Term.fn6 fnid old_orig x0 x1 x2 x3 x4 x5)) = (Kind.Term.fn6 fnid new_origin x0 x1 x2 x3 x4 x5)
-(Kind.Term.set_origin new_origin (Kind.Term.fn7 fnid old_orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Term.fn7 fnid new_origin x0 x1 x2 x3 x4 x5 x6)
-(Kind.Term.set_origin new_origin (Kind.Term.fn8 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Term.fn8 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7)
-(Kind.Term.set_origin new_origin (Kind.Term.fn9 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Term.fn9 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8)
-(Kind.Term.set_origin new_origin (Kind.Term.fn10 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Term.fn10 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)
-(Kind.Term.set_origin new_origin (Kind.Term.fn11 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Term.fn11 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)
-(Kind.Term.set_origin new_origin (Kind.Term.fn12 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Term.fn12 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)
-(Kind.Term.set_origin new_origin (Kind.Term.fn13 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Term.fn13 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)
-(Kind.Term.set_origin new_origin (Kind.Term.fn14 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Term.fn14 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)
-(Kind.Term.set_origin new_origin (Kind.Term.fn15 ctid old_orig args)) = (Kind.Term.fn15 ctid new_origin args)
-(Kind.Term.set_origin new_origin (Kind.Term.fn16 ctid old_orig args)) = (Kind.Term.fn16 ctid new_origin args)
 (Kind.API.eval_main) = (Kind.Printer.text [(Kind.Term.show (Kind.Term.FN0 (Main.) 0)), (String.new_line), (String.new_line)])
 (String.new_line) = (String.pure (Char.newline))
 (String.pure x) = (String.cons x "")
@@ -55,6 +8,25 @@
 (String.concat (String.cons x xs) ys) = (String.cons x (String.concat xs ys))
 (String.concat "" ys) = ys
 (Kind.Term.show term) = let sugars = [(Kind.Term.show.sugar.string term), (Kind.Term.show.sugar.list term), (Kind.Term.show.sugar.sigma term)]; (Maybe.try sugars (Kind.Term.show.go term))
+(Kind.Term.show.sugar.list term) = (Maybe.bind (Kind.Term.show.sugar.list.go term) λres (Maybe.pure (Kind.Printer.text ["[", (String.join " " res), "]"])))
+(Kind.Term.show.sugar.list.go (Kind.Term.ct0 (List.nil.) orig)) = (Maybe.some [])
+(Kind.Term.show.sugar.list.go (Kind.Term.ct2 (List.cons.) orig x0 x1)) = (Maybe.bind (Kind.Term.show.sugar.list.go x1) λtail (Maybe.pure (List.cons (Kind.Term.show x0) tail)))
+(Kind.Term.show.sugar.list.go other) = (Maybe.none)
+(Maybe.pure x) = (Maybe.some x)
+(Maybe.bind (Maybe.none) mb) = (Maybe.none)
+(Maybe.bind (Maybe.some val) mb) = (mb val)
+(String.join sep list) = (String.intercalate sep list)
+(String.intercalate sep xs) = (String.flatten (List.intersperse sep xs))
+(List.intersperse sep []) = []
+(List.intersperse sep [xh]) = (List.pure xh)
+(List.intersperse sep (List.cons xh xt)) = (List.cons xh (List.cons sep (List.intersperse sep xt)))
+(List.pure x) = [x]
+(String.flatten []) = ""
+(String.flatten (List.cons head tail)) = (String.concat head (String.flatten tail))
+(Kind.Term.show.sugar.string term) = (Maybe.bind (Kind.Term.show.sugar.string.go term) λres let quot = "'"; (Maybe.pure (Kind.Printer.text [quot, res, quot])))
+(Kind.Term.show.sugar.string.go (Kind.Term.ct0 (String.nil.) orig)) = (Maybe.some "")
+(Kind.Term.show.sugar.string.go (Kind.Term.ct2 (String.cons.) orig (Kind.Term.u60 orig1 x0) x1)) = (Maybe.bind (Kind.Term.show.sugar.string.go x1) λtail (Maybe.pure (String.cons x0 tail)))
+(Kind.Term.show.sugar.string.go other) = (Maybe.none)
 (Kind.Term.show.sugar.sigma (Kind.Term.ct2 (Sigma.) orig typ (Kind.Term.lam orig_ name body))) = (Maybe.some (Kind.Printer.text ["([", (Kind.Name.show name), ": ", (Kind.Term.show typ), "] -> ", (Kind.Term.show (body (Kind.Term.var orig_ name 0))), ")"]))
 (Kind.Term.show.sugar.sigma term) = (Maybe.none)
 (Kind.Name.show name) = (Kind.Name.show.go name "")
@@ -65,25 +37,6 @@
 (Maybe.try (List.cons maybe xs) alt) = (Maybe.match maybe (Maybe.try xs alt) λvalue value)
 (Maybe.match (Maybe.none) none some) = none
 (Maybe.match (Maybe.some value_) none some) = (some value_)
-(Kind.Term.show.sugar.list term) = (Maybe.bind (Kind.Term.show.sugar.list.go term) λres (Maybe.pure (Kind.Printer.text ["[", (String.join " " res), "]"])))
-(Kind.Term.show.sugar.list.go (Kind.Term.ct0 (List.nil.) orig)) = (Maybe.some [])
-(Kind.Term.show.sugar.list.go (Kind.Term.ct2 (List.cons.) orig x0 x1)) = (Maybe.bind (Kind.Term.show.sugar.list.go x1) λtail (Maybe.pure (List.cons (Kind.Term.show x0) tail)))
-(Kind.Term.show.sugar.list.go other) = (Maybe.none)
-(Maybe.pure x) = (Maybe.some x)
-(Maybe.bind (Maybe.none) mb) = (Maybe.none)
-(Maybe.bind (Maybe.some val) mb) = (mb val)
-(String.join sep list) = (String.intercalate sep list)
-(String.intercalate sep xs) = (String.flatten (List.intersperse sep xs))
-(String.flatten []) = ""
-(String.flatten (List.cons head tail)) = (String.concat head (String.flatten tail))
-(List.intersperse sep []) = []
-(List.intersperse sep [xh]) = (List.pure xh)
-(List.intersperse sep (List.cons xh xt)) = (List.cons xh (List.cons sep (List.intersperse sep xt)))
-(List.pure x) = [x]
-(Kind.Term.show.sugar.string term) = (Maybe.bind (Kind.Term.show.sugar.string.go term) λres let quot = "'"; (Maybe.pure (Kind.Printer.text [quot, res, quot])))
-(Kind.Term.show.sugar.string.go (Kind.Term.ct0 (String.nil.) orig)) = (Maybe.some "")
-(Kind.Term.show.sugar.string.go (Kind.Term.ct2 (String.cons.) orig (Kind.Term.num orig1 x0) x1)) = (Maybe.bind (Kind.Term.show.sugar.string.go x1) λtail (Maybe.pure (String.cons x0 tail)))
-(Kind.Term.show.sugar.string.go other) = (Maybe.none)
 (Kind.Term.show.go (Kind.Term.typ orig)) = "Type"
 (Kind.Term.show.go (Kind.Term.var orig name index)) = (Kind.Printer.text [(Kind.Name.show name)])
 (Kind.Term.show.go (Kind.Term.hol orig numb)) = (Kind.Printer.text ["_"])
@@ -130,8 +83,8 @@
 (Kind.Term.show.go (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)) = (Kind.Printer.text [(Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), " ", (Kind.Term.show x13), " ", (Kind.Term.show x14)])
 (Kind.Term.show.go (Kind.Term.args16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)) = (Kind.Printer.text [(Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), " ", (Kind.Term.show x13), " ", (Kind.Term.show x14), " ", (Kind.Term.show x15)])
 (Kind.Term.show.go (Kind.Term.hlp orig)) = "?"
-(Kind.Term.show.go (Kind.Term.u60 orig)) = "U60"
-(Kind.Term.show.go (Kind.Term.num orig numb)) = (Show.to_string (U60.show numb))
+(Kind.Term.show.go (Kind.Term.U60 orig)) = "U60"
+(Kind.Term.show.go (Kind.Term.u60 orig numb)) = (Show.to_string (U60.show numb))
 (Kind.Term.show.go (Kind.Term.op2 orig operator left right)) = (Kind.Printer.text ["(", (Kind.Operator.show operator), " ", (Kind.Term.show left), " ", (Kind.Term.show right), ")"])
 (Show.to_string show) = (show "")
 (Kind.Operator.show (Kind.Operator.add)) = "+"
@@ -153,6 +106,53 @@
 (Kind.Term.show.forall orig name type body) = (U60.if (== name 63) (Kind.Printer.text ["(", (Kind.Term.show type), " -> ", (Kind.Term.show (body (Kind.Term.var orig name 0))), ")"]) (Kind.Printer.text ["((", (Kind.Name.show name), ": ", (Kind.Term.show type), ") -> ", (Kind.Term.show (body (Kind.Term.var orig name 0))), ")"]))
 (U60.show 0) = λstr (String.cons 48 str)
 (U60.show n) = λstr let next = (String.cons (+ 48 (% n 10)) str); let func = (U60.if (< n 10) λh h λh ((U60.show (/ n 10)) h)); (func next)
+(Kind.Term.set_origin new_origin (Kind.Term.typ old_orig)) = (Kind.Term.typ new_origin)
+(Kind.Term.set_origin new_origin (Kind.Term.var old_orig name idx)) = (Kind.Term.var new_origin name idx)
+(Kind.Term.set_origin new_origin (Kind.Term.hol old_orig numb)) = (Kind.Term.hol new_origin numb)
+(Kind.Term.set_origin new_origin (Kind.Term.all old_orig name typ body)) = (Kind.Term.all new_origin name typ body)
+(Kind.Term.set_origin new_origin (Kind.Term.lam old_orig name body)) = (Kind.Term.lam new_origin name body)
+(Kind.Term.set_origin new_origin (Kind.Term.let old_orig name expr body)) = (Kind.Term.let new_origin name expr body)
+(Kind.Term.set_origin new_origin (Kind.Term.ann old_orig expr typ)) = (Kind.Term.ann new_origin expr typ)
+(Kind.Term.set_origin new_origin (Kind.Term.sub old_orig name indx redx expr)) = (Kind.Term.sub new_origin name indx redx expr)
+(Kind.Term.set_origin new_origin (Kind.Term.app old_orig func arg)) = (Kind.Term.app new_origin func arg)
+(Kind.Term.set_origin new_origin (Kind.Term.hlp old_orig)) = (Kind.Term.hlp new_origin)
+(Kind.Term.set_origin new_origin (Kind.Term.U60 old_orig)) = (Kind.Term.U60 new_origin)
+(Kind.Term.set_origin new_origin (Kind.Term.u60 old_orig num)) = (Kind.Term.u60 new_origin num)
+(Kind.Term.set_origin new_origin (Kind.Term.op2 old_orig op left right)) = (Kind.Term.op2 new_origin op left right)
+(Kind.Term.set_origin new_origin (Kind.Term.ct0 ctid old_orig)) = (Kind.Term.ct0 ctid new_origin)
+(Kind.Term.set_origin new_origin (Kind.Term.ct1 ctid old_orig x0)) = (Kind.Term.ct1 ctid new_origin x0)
+(Kind.Term.set_origin new_origin (Kind.Term.ct2 ctid old_orig x0 x1)) = (Kind.Term.ct2 ctid new_origin x0 x1)
+(Kind.Term.set_origin new_origin (Kind.Term.ct3 ctid old_orig x0 x1 x2)) = (Kind.Term.ct3 ctid new_origin x0 x1 x2)
+(Kind.Term.set_origin new_origin (Kind.Term.ct4 ctid old_orig x0 x1 x2 x3)) = (Kind.Term.ct4 ctid new_origin x0 x1 x2 x3)
+(Kind.Term.set_origin new_origin (Kind.Term.ct5 ctid old_orig x0 x1 x2 x3 x4)) = (Kind.Term.ct5 ctid new_origin x0 x1 x2 x3 x4)
+(Kind.Term.set_origin new_origin (Kind.Term.ct6 ctid old_orig x0 x1 x2 x3 x4 x5)) = (Kind.Term.ct6 ctid new_origin x0 x1 x2 x3 x4 x5)
+(Kind.Term.set_origin new_origin (Kind.Term.ct7 ctid old_orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Term.ct7 ctid new_origin x0 x1 x2 x3 x4 x5 x6)
+(Kind.Term.set_origin new_origin (Kind.Term.ct8 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Term.ct8 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7)
+(Kind.Term.set_origin new_origin (Kind.Term.ct9 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Term.ct9 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8)
+(Kind.Term.set_origin new_origin (Kind.Term.ct10 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Term.ct10 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)
+(Kind.Term.set_origin new_origin (Kind.Term.ct11 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Term.ct11 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)
+(Kind.Term.set_origin new_origin (Kind.Term.ct12 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Term.ct12 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)
+(Kind.Term.set_origin new_origin (Kind.Term.ct13 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Term.ct13 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)
+(Kind.Term.set_origin new_origin (Kind.Term.ct14 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Term.ct14 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)
+(Kind.Term.set_origin new_origin (Kind.Term.ct15 ctid old_orig args)) = (Kind.Term.ct15 ctid new_origin args)
+(Kind.Term.set_origin new_origin (Kind.Term.ct16 ctid old_orig args)) = (Kind.Term.ct16 ctid new_origin args)
+(Kind.Term.set_origin new_origin (Kind.Term.fn0 fnid old_orig)) = (Kind.Term.fn0 fnid new_origin)
+(Kind.Term.set_origin new_origin (Kind.Term.fn1 fnid old_orig x0)) = (Kind.Term.fn1 fnid new_origin x0)
+(Kind.Term.set_origin new_origin (Kind.Term.fn2 fnid old_orig x0 x1)) = (Kind.Term.fn2 fnid new_origin x0 x1)
+(Kind.Term.set_origin new_origin (Kind.Term.fn3 fnid old_orig x0 x1 x2)) = (Kind.Term.fn3 fnid new_origin x0 x1 x2)
+(Kind.Term.set_origin new_origin (Kind.Term.fn4 fnid old_orig x0 x1 x2 x3)) = (Kind.Term.fn4 fnid new_origin x0 x1 x2 x3)
+(Kind.Term.set_origin new_origin (Kind.Term.fn5 fnid old_orig x0 x1 x2 x3 x4)) = (Kind.Term.fn5 fnid new_origin x0 x1 x2 x3 x4)
+(Kind.Term.set_origin new_origin (Kind.Term.fn6 fnid old_orig x0 x1 x2 x3 x4 x5)) = (Kind.Term.fn6 fnid new_origin x0 x1 x2 x3 x4 x5)
+(Kind.Term.set_origin new_origin (Kind.Term.fn7 fnid old_orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Term.fn7 fnid new_origin x0 x1 x2 x3 x4 x5 x6)
+(Kind.Term.set_origin new_origin (Kind.Term.fn8 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Term.fn8 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7)
+(Kind.Term.set_origin new_origin (Kind.Term.fn9 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Term.fn9 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8)
+(Kind.Term.set_origin new_origin (Kind.Term.fn10 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Term.fn10 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)
+(Kind.Term.set_origin new_origin (Kind.Term.fn11 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Term.fn11 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)
+(Kind.Term.set_origin new_origin (Kind.Term.fn12 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Term.fn12 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)
+(Kind.Term.set_origin new_origin (Kind.Term.fn13 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Term.fn13 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)
+(Kind.Term.set_origin new_origin (Kind.Term.fn14 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Term.fn14 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)
+(Kind.Term.set_origin new_origin (Kind.Term.fn15 ctid old_orig args)) = (Kind.Term.fn15 ctid new_origin args)
+(Kind.Term.set_origin new_origin (Kind.Term.fn16 ctid old_orig args)) = (Kind.Term.fn16 ctid new_origin args)
 (Kind.API.check_all) = let output = (Kind.API.output (List.reverse (Kind.API.check_functions (Functions)))); output
 (Kind.API.check_functions []) = []
 (Kind.API.check_functions (List.cons f fs)) = let head = (Pair.new f (Kind.API.check_function f)); let tail = (Kind.API.check_functions fs); (List.cons head tail)
@@ -183,8 +183,8 @@
 (Kind.Term.eval (Kind.Term.sub orig name indx redx expr)) = (Kind.Term.eval_sub orig name indx redx (Kind.Term.eval expr))
 (Kind.Term.eval (Kind.Term.app orig expr typ)) = (Kind.Term.eval_app orig (Kind.Term.eval expr) (Kind.Term.eval typ))
 (Kind.Term.eval (Kind.Term.hlp orig)) = (Kind.Term.hlp orig)
-(Kind.Term.eval (Kind.Term.u60 orig)) = (Kind.Term.u60 orig)
-(Kind.Term.eval (Kind.Term.num orig num)) = (Kind.Term.num orig num)
+(Kind.Term.eval (Kind.Term.U60 orig)) = (Kind.Term.U60 orig)
+(Kind.Term.eval (Kind.Term.u60 orig num)) = (Kind.Term.u60 orig num)
 (Kind.Term.eval (Kind.Term.op2 orig op left right)) = (Kind.Term.eval_op orig op (Kind.Term.eval left) (Kind.Term.eval right))
 (Kind.Term.eval (Kind.Term.ct0 ctid orig)) = (Kind.Term.ct0 ctid orig)
 (Kind.Term.eval (Kind.Term.ct1 ctid orig x0)) = (Kind.Term.ct1 ctid orig (Kind.Term.eval x0))
@@ -227,22 +227,22 @@
 (Kind.Term.eval_let orig name expr body) = (body expr)
 (Kind.Term.eval_app orig (Kind.Term.lam orig1 name body) arg) = (body arg)
 (Kind.Term.eval_app orig func arg) = (Kind.Term.app orig func arg)
-(Kind.Term.eval_op orig (Kind.Operator.add) (Kind.Term.num a.orig a.num) (Kind.Term.num b.orig b.num)) = (Kind.Term.num 0 (+ a.num b.num))
-(Kind.Term.eval_op orig (Kind.Operator.sub) (Kind.Term.num a.orig a.num) (Kind.Term.num b.orig b.num)) = (Kind.Term.num 0 (- a.num b.num))
-(Kind.Term.eval_op orig (Kind.Operator.mul) (Kind.Term.num a.orig a.num) (Kind.Term.num b.orig b.num)) = (Kind.Term.num 0 (* a.num b.num))
-(Kind.Term.eval_op orig (Kind.Operator.div) (Kind.Term.num a.orig a.num) (Kind.Term.num b.orig b.num)) = (Kind.Term.num 0 (/ a.num b.num))
-(Kind.Term.eval_op orig (Kind.Operator.mod) (Kind.Term.num a.orig a.num) (Kind.Term.num b.orig b.num)) = (Kind.Term.num 0 (% a.num b.num))
-(Kind.Term.eval_op orig (Kind.Operator.and) (Kind.Term.num a.orig a.num) (Kind.Term.num b.orig b.num)) = (Kind.Term.num 0 (+ a.num b.num))
-(Kind.Term.eval_op orig (Kind.Operator.or) (Kind.Term.num a.orig a.num) (Kind.Term.num b.orig b.num)) = (Kind.Term.num 0 (| a.num b.num))
-(Kind.Term.eval_op orig (Kind.Operator.xor) (Kind.Term.num a.orig a.num) (Kind.Term.num b.orig b.num)) = (Kind.Term.num 0 (^ a.num b.num))
-(Kind.Term.eval_op orig (Kind.Operator.shl) (Kind.Term.num a.orig a.num) (Kind.Term.num b.orig b.num)) = (Kind.Term.num 0 (<< a.num b.num))
-(Kind.Term.eval_op orig (Kind.Operator.shr) (Kind.Term.num a.orig a.num) (Kind.Term.num b.orig b.num)) = (Kind.Term.num 0 (>> a.num b.num))
-(Kind.Term.eval_op orig (Kind.Operator.ltn) (Kind.Term.num a.orig a.num) (Kind.Term.num b.orig b.num)) = (Kind.Term.num 0 (< a.num b.num))
-(Kind.Term.eval_op orig (Kind.Operator.lte) (Kind.Term.num a.orig a.num) (Kind.Term.num b.orig b.num)) = (Kind.Term.num 0 (<= a.num b.num))
-(Kind.Term.eval_op orig (Kind.Operator.eql) (Kind.Term.num a.orig a.num) (Kind.Term.num b.orig b.num)) = (Kind.Term.num 0 (== a.num b.num))
-(Kind.Term.eval_op orig (Kind.Operator.gte) (Kind.Term.num a.orig a.num) (Kind.Term.num b.orig b.num)) = (Kind.Term.num 0 (>= a.num b.num))
-(Kind.Term.eval_op orig (Kind.Operator.gtn) (Kind.Term.num a.orig a.num) (Kind.Term.num b.orig b.num)) = (Kind.Term.num 0 (> a.num b.num))
-(Kind.Term.eval_op orig (Kind.Operator.neq) (Kind.Term.num a.orig a.num) (Kind.Term.num b.orig b.num)) = (Kind.Term.num 0 (!= a.num b.num))
+(Kind.Term.eval_op orig (Kind.Operator.add) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (+ a.num b.num))
+(Kind.Term.eval_op orig (Kind.Operator.sub) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (- a.num b.num))
+(Kind.Term.eval_op orig (Kind.Operator.mul) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (* a.num b.num))
+(Kind.Term.eval_op orig (Kind.Operator.div) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (/ a.num b.num))
+(Kind.Term.eval_op orig (Kind.Operator.mod) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (% a.num b.num))
+(Kind.Term.eval_op orig (Kind.Operator.and) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (+ a.num b.num))
+(Kind.Term.eval_op orig (Kind.Operator.or) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (| a.num b.num))
+(Kind.Term.eval_op orig (Kind.Operator.xor) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (^ a.num b.num))
+(Kind.Term.eval_op orig (Kind.Operator.shl) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (<< a.num b.num))
+(Kind.Term.eval_op orig (Kind.Operator.shr) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (>> a.num b.num))
+(Kind.Term.eval_op orig (Kind.Operator.ltn) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (< a.num b.num))
+(Kind.Term.eval_op orig (Kind.Operator.lte) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (<= a.num b.num))
+(Kind.Term.eval_op orig (Kind.Operator.eql) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (== a.num b.num))
+(Kind.Term.eval_op orig (Kind.Operator.gte) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (>= a.num b.num))
+(Kind.Term.eval_op orig (Kind.Operator.gtn) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (> a.num b.num))
+(Kind.Term.eval_op orig (Kind.Operator.neq) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (!= a.num b.num))
 (Kind.Term.eval_op orig op left right) = (Kind.Term.op2 orig op left right)
 (Kind.Checker.equal (Kind.Term.typ orig) (Kind.Term.typ orig1)) = (Kind.Checker.pure (Bool.true))
 (Kind.Checker.equal (Kind.Term.all a.orig a.name a.type a.body) (Kind.Term.all b.orig b.name b.type b.body)) = (Kind.Checker.bind (Kind.Checker.get_depth) λdep (Kind.Checker.bind (Kind.Checker.equal a.type b.type) λtype (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.equal (a.body (Kind.Term.var a.orig a.name dep)) (b.body (Kind.Term.var b.orig b.name dep))) (Null) (Null) []) λbody (Kind.Checker.pure (Bool.and type body)))))
@@ -251,8 +251,8 @@
 (Kind.Checker.equal (Kind.Term.let a.orig a.name a.expr a.body) (Kind.Term.let b.orig b.name b.expr b.body)) = (Kind.Checker.bind (Kind.Checker.get_depth) λdep (Kind.Checker.bind (Kind.Checker.equal a.expr b.expr) λexpr (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.equal (a.body (Kind.Term.var a.orig a.name dep)) (b.body (Kind.Term.var b.orig b.name dep))) (Null) (Null) []) λbody (Kind.Checker.pure (Bool.and expr body)))))
 (Kind.Checker.equal (Kind.Term.ann a.orig a.expr a.type) (Kind.Term.ann b.orig b.expr b.type)) = (Kind.Checker.bind (Kind.Checker.equal a.expr b.expr) λfunc (Kind.Checker.bind (Kind.Checker.equal a.type b.type) λtype (Kind.Checker.pure (Bool.and func type))))
 (Kind.Checker.equal (Kind.Term.sub a.orig a.name a.indx a.redx a.expr) (Kind.Term.sub b.orig b.name b.indx b.redx b.expr)) = (Kind.Checker.bind (Kind.Checker.equal a.expr b.expr) λfunc (Kind.Checker.pure func))
-(Kind.Checker.equal (Kind.Term.u60 a.orig) (Kind.Term.u60 b.orig)) = (Kind.Checker.pure (Bool.true))
-(Kind.Checker.equal (Kind.Term.num a.orig a.num) (Kind.Term.num b.orig b.num)) = (Kind.Checker.pure (U60.equal a.num b.num))
+(Kind.Checker.equal (Kind.Term.U60 a.orig) (Kind.Term.U60 b.orig)) = (Kind.Checker.pure (Bool.true))
+(Kind.Checker.equal (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Checker.pure (U60.equal a.num b.num))
 (Kind.Checker.equal (Kind.Term.op2 a.orig a.op a.val0 a.val1) (Kind.Term.op2 b.orig b.op b.val0 b.val1)) = let op = (Kind.Operator.equal a.op b.op); (Kind.Checker.bind (Kind.Checker.equal a.val0 b.val0) λval0 (Kind.Checker.bind (Kind.Checker.equal a.val1 b.val1) λval1 (Kind.Checker.pure (Bool.and op (Bool.and val0 val1)))))
 (Kind.Checker.equal (Kind.Term.hol a.orig a.numb) (Kind.Term.hol b.orig b.numb)) = (Bool.if (U60.equal a.numb b.numb) (Kind.Checker.pure (Bool.true)) (Kind.Checker.equal.hol a.orig a.numb (Kind.Term.hol b.orig b.numb)))
 (Kind.Checker.equal (Kind.Term.hol a.orig a.numb) b) = (Kind.Checker.equal.hol a.orig a.numb b)
@@ -314,8 +314,8 @@
 (Kind.Term.fill (Kind.Term.sub orig name indx redx expr) sub) = (Kind.Term.eval_sub orig name indx redx (Kind.Term.fill expr sub))
 (Kind.Term.fill (Kind.Term.app orig expr typ) sub) = (Kind.Term.eval_app orig (Kind.Term.fill expr sub) (Kind.Term.fill typ sub))
 (Kind.Term.fill (Kind.Term.hlp orig) sub) = (Kind.Term.hlp orig)
-(Kind.Term.fill (Kind.Term.u60 orig) sub) = (Kind.Term.u60 orig)
-(Kind.Term.fill (Kind.Term.num orig num) sub) = (Kind.Term.num orig num)
+(Kind.Term.fill (Kind.Term.U60 orig) sub) = (Kind.Term.U60 orig)
+(Kind.Term.fill (Kind.Term.u60 orig num) sub) = (Kind.Term.u60 orig num)
 (Kind.Term.fill (Kind.Term.op2 orig op left right) sub) = (Kind.Term.op2 orig op (Kind.Term.fill left sub) (Kind.Term.fill right sub))
 (Kind.Term.fill (Kind.Term.ct0 ctid orig) sub) = (Kind.Term.ct0 ctid orig)
 (Kind.Term.fill (Kind.Term.ct1 ctid orig x0) sub) = (Kind.Term.ct1 ctid orig (Kind.Term.fill x0 sub))
@@ -379,8 +379,8 @@
 (Kind.Term.fillable (Kind.Term.typ orig) sub) = (Bool.false)
 (Kind.Term.fillable (Kind.Term.var orig name index) sub) = (Bool.false)
 (Kind.Term.fillable (Kind.Term.hlp orig) sub) = (Bool.false)
-(Kind.Term.fillable (Kind.Term.u60 orig) sub) = (Bool.false)
-(Kind.Term.fillable (Kind.Term.num orig num) sub) = (Bool.false)
+(Kind.Term.fillable (Kind.Term.U60 orig) sub) = (Bool.false)
+(Kind.Term.fillable (Kind.Term.u60 orig num) sub) = (Bool.false)
 (Kind.Term.fillable (Kind.Term.all orig name typ body) sub) = (Bool.or (Kind.Term.fillable typ sub) (Kind.Term.fillable (body (Kind.Term.hlp 0)) sub))
 (Kind.Term.fillable (Kind.Term.lam orig name body) sub) = (Kind.Term.fillable (body (Kind.Term.hlp 0)) sub)
 (Kind.Term.fillable (Kind.Term.app orig expr typ) sub) = (Bool.or (Kind.Term.fillable expr sub) (Kind.Term.fillable typ sub))
@@ -470,6 +470,8 @@
 (Kind.Checker.check (Kind.Term.var orig name idx) type) = (Kind.Checker.bind (Kind.Checker.get_right_hand_side) λrhs (Bool.if rhs (Kind.Checker.compare rhs (Kind.Term.var orig name idx) type) (Kind.Checker.extend name type [])))
 (Kind.Checker.check (Kind.Term.hol orig numb) type) = (Kind.Checker.pure (Unit.new))
 (Kind.Checker.check term type) = (Kind.Checker.bind (Kind.Checker.get_right_hand_side) λrhs (Kind.Checker.compare rhs term type))
+(Kind.Checker.compare rhs term type) = (Kind.Term.get_origin term λorig λterm (Kind.Checker.bind (Kind.Checker.infer term) λterm_typ let fun = (Bool.if rhs λterm_typ λtype (Kind.Checker.new_equation orig type term_typ) λterm_typ λtype (Kind.Checker.bind (Kind.Checker.equal (Kind.Term.eval term_typ) (Kind.Term.eval type)) λis_equal (Bool.if is_equal (Kind.Checker.pure (Unit.new)) (Kind.Checker.bind (Kind.Checker.get_context) λctx (Kind.Checker.fail (Kind.Error.impossible_case ctx orig type term_typ)))))); (fun term_typ type)))
+(Kind.Checker.fail err) = λcontext λdepth λrhs λsubst λeqts λerrs (Kind.Result.errored context subst (List.cons err errs))
 (Kind.Checker.infer (Kind.Term.var orig name index)) = (Kind.Checker.bind (Kind.Checker.find index (Maybe.none) λn λt λv (Maybe.some t)) λgot_type (Maybe.match got_type (Kind.Checker.bind (Kind.Checker.get_context) λctx (Kind.Checker.fail (Kind.Error.unbound_variable ctx orig))) λvalue (Kind.Checker.pure value)))
 (Kind.Checker.infer (Kind.Term.hol orig numb)) = (Kind.Checker.bind (Kind.Checker.get_context) λctx (Kind.Checker.fail (Kind.Error.cant_infer_hole ctx orig)))
 (Kind.Checker.infer (Kind.Term.typ orig)) = (Kind.Checker.pure (Kind.Term.typ orig))
@@ -514,9 +516,9 @@
 (Kind.Checker.infer (Kind.Term.fn15 fnid orig x0)) = let expr = (Kind.Checker.infer_args x0); (Kind.Checker.infer (expr (Kind.Term.fn0 fnid orig) orig))
 (Kind.Checker.infer (Kind.Term.fn16 fnid orig x0)) = let expr = (Kind.Checker.infer_args x0); (Kind.Checker.infer (expr (Kind.Term.fn0 fnid orig) orig))
 (Kind.Checker.infer (Kind.Term.hlp orig)) = (Kind.Checker.bind (Kind.Checker.get_context) λctx (Kind.Checker.fail (Kind.Error.inspection ctx orig (Kind.Term.hlp 0))))
-(Kind.Checker.infer (Kind.Term.u60 orig)) = (Kind.Checker.pure (Kind.Term.typ 0))
-(Kind.Checker.infer (Kind.Term.num orig numb)) = (Kind.Checker.pure (Kind.Term.u60 0))
-(Kind.Checker.infer (Kind.Term.op2 orig oper left right)) = (Kind.Checker.bind (Kind.Checker.check left (Kind.Term.u60 0)) λx_7 (Kind.Checker.bind (Kind.Checker.check right (Kind.Term.u60 0)) λx_6 (Kind.Checker.pure (Kind.Term.u60 0))))
+(Kind.Checker.infer (Kind.Term.U60 orig)) = (Kind.Checker.pure (Kind.Term.typ 0))
+(Kind.Checker.infer (Kind.Term.u60 orig numb)) = (Kind.Checker.pure (Kind.Term.U60 0))
+(Kind.Checker.infer (Kind.Term.op2 orig oper left right)) = (Kind.Checker.bind (Kind.Checker.check left (Kind.Term.U60 0)) λx_7 (Kind.Checker.bind (Kind.Checker.check right (Kind.Term.U60 0)) λx_6 (Kind.Checker.pure (Kind.Term.U60 0))))
 (Kind.Checker.infer.forall (Kind.Term.all orig name type body) then_fn else_val) = (then_fn orig name type body)
 (Kind.Checker.infer.forall (Kind.Term.var orig name index) then_fn else_val) = (Kind.Checker.bind (Kind.Checker.find index [] λn λt λv v) λreducs (Kind.Checker.bind (Kind.Checker.infer.forall.try_values reducs then_fn else_val) λresult (Kind.Checker.pure result)))
 (Kind.Checker.infer.forall other then_fn else_val) = else_val
@@ -534,8 +536,8 @@
 (Kind.Term.replace (Kind.Term.sub orig name indx redx expr) idx val) = (Kind.Term.sub orig name indx redx (Kind.Term.replace expr idx val))
 (Kind.Term.replace (Kind.Term.app orig expr typ) idx val) = (Kind.Term.app orig (Kind.Term.replace expr idx val) (Kind.Term.replace typ idx val))
 (Kind.Term.replace (Kind.Term.hlp orig) idx val) = (Kind.Term.hlp orig)
-(Kind.Term.replace (Kind.Term.u60 orig) idx val) = (Kind.Term.u60 orig)
-(Kind.Term.replace (Kind.Term.num orig num) idx val) = (Kind.Term.num orig num)
+(Kind.Term.replace (Kind.Term.U60 orig) idx val) = (Kind.Term.U60 orig)
+(Kind.Term.replace (Kind.Term.u60 orig num) idx val) = (Kind.Term.u60 orig num)
 (Kind.Term.replace (Kind.Term.op2 orig op left right) idx val) = (Kind.Term.op2 orig op (Kind.Term.replace left idx val) (Kind.Term.replace right idx val))
 (Kind.Term.replace (Kind.Term.ct0 ctid orig) idx val) = (Kind.Term.ct0 ctid orig)
 (Kind.Term.replace (Kind.Term.ct1 ctid orig x0) idx val) = (Kind.Term.ct1 ctid orig (Kind.Term.replace x0 idx val))
@@ -570,15 +572,11 @@
 (Kind.Term.replace (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) idx val) = (Kind.Term.args15 (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val) (Kind.Term.replace x10 idx val) (Kind.Term.replace x11 idx val) (Kind.Term.replace x12 idx val) (Kind.Term.replace x13 idx val) (Kind.Term.replace x14 idx val))
 (Kind.Term.replace (Kind.Term.args16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) idx val) = (Kind.Term.args16 (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val) (Kind.Term.replace x10 idx val) (Kind.Term.replace x11 idx val) (Kind.Term.replace x12 idx val) (Kind.Term.replace x13 idx val) (Kind.Term.replace x14 idx val) (Kind.Term.replace x15 idx val))
 (Kind.Term.replace (Kind.Term.hol orig numb) idx val) = (Kind.Term.hol orig numb)
-(Kind.Checker.fail err) = λcontext λdepth λrhs λsubst λeqts λerrs (Kind.Result.errored context subst (List.cons err errs))
 (List.at.u60 [] idx) = (Maybe.none)
 (List.at.u60 (List.cons head tail) 0) = (Maybe.some head)
 (List.at.u60 (List.cons head tail) idx) = (List.at.u60 tail (- idx 1))
 (Kind.Checker.get_context) = λcontext λdepth λrhs λsubst λeqts λerrs (Kind.Result.checked context depth rhs subst eqts errs context)
 (Pair.match (Pair.new fst_ snd_) new) = (new fst_ snd_)
-(Kind.Term.if_all (Kind.Term.all orig name typ body) func_if else) = (func_if orig name typ body)
-(Kind.Term.if_all other func_if else) = else
-(Kind.Checker.compare rhs term type) = (Kind.Term.get_origin term λorig λterm (Kind.Checker.bind (Kind.Checker.infer term) λterm_typ let fun = (Bool.if rhs λterm_typ λtype (Kind.Checker.new_equation orig type term_typ) λterm_typ λtype (Kind.Checker.bind (Kind.Checker.equal (Kind.Term.eval term_typ) (Kind.Term.eval type)) λis_equal (Bool.if is_equal (Kind.Checker.pure (Unit.new)) (Kind.Checker.bind (Kind.Checker.get_context) λctx (Kind.Checker.fail (Kind.Error.impossible_case ctx orig type term_typ)))))); (fun term_typ type)))
 (Kind.Term.get_origin (Kind.Term.typ orig) got) = (got orig (Kind.Term.typ orig))
 (Kind.Term.get_origin (Kind.Term.var orig name index) got) = (got orig (Kind.Term.var orig name index))
 (Kind.Term.get_origin (Kind.Term.hol orig numb) got) = (got orig (Kind.Term.hol orig numb))
@@ -589,8 +587,8 @@
 (Kind.Term.get_origin (Kind.Term.sub orig name indx redx expr) got) = (got orig (Kind.Term.sub orig name indx redx expr))
 (Kind.Term.get_origin (Kind.Term.app orig func arg) got) = (got orig (Kind.Term.app orig func arg))
 (Kind.Term.get_origin (Kind.Term.hlp orig) got) = (got orig (Kind.Term.hlp orig))
-(Kind.Term.get_origin (Kind.Term.u60 orig) got) = (got orig (Kind.Term.u60 orig))
-(Kind.Term.get_origin (Kind.Term.num orig num) got) = (got orig (Kind.Term.num orig num))
+(Kind.Term.get_origin (Kind.Term.U60 orig) got) = (got orig (Kind.Term.U60 orig))
+(Kind.Term.get_origin (Kind.Term.u60 orig num) got) = (got orig (Kind.Term.u60 orig num))
 (Kind.Term.get_origin (Kind.Term.op2 orig op left right) got) = (got orig (Kind.Term.op2 orig op left right))
 (Kind.Term.get_origin (Kind.Term.ct0 ctid orig) got) = (got orig (Kind.Term.ct0 ctid orig))
 (Kind.Term.get_origin (Kind.Term.ct1 ctid orig x0) got) = (got orig (Kind.Term.ct1 ctid orig x0))
@@ -629,6 +627,8 @@
 (Kind.Checker.new_equation orig left right) = λcontext λdepth λrhs λsubst λeqts λerrs (Kind.Result.checked context depth rhs subst (List.append eqts (Kind.Equation.new context orig left right)) errs (Unit.new))
 (List.append [] x) = (List.pure x)
 (List.append (List.cons xs.h xs.t) x) = (List.cons xs.h (List.append xs.t x))
+(Kind.Term.if_all (Kind.Term.all orig name typ body) func_if else) = (func_if orig name typ body)
+(Kind.Term.if_all other func_if else) = else
 (Kind.Checker.run checker rhs) = (checker (Kind.Context.empty) 0 rhs (Kind.Subst.end) [] [])
 (Kind.API.check_function.rules [] type) = []
 (Kind.API.check_function.rules (List.cons rule rules) type) = let head = (Kind.Checker.run (Kind.Checker.unify (Kind.Checker.rule rule type)) (Bool.false)); let tail = (Kind.API.check_function.rules rules type); (List.cons head tail)
@@ -700,8 +700,8 @@
 (Kind.Term.quote.go (Kind.Term.fn15 fnid orig x0)) = (Kind.Term.Quoted.fun fnid orig (Kind.Term.quote.args x0))
 (Kind.Term.quote.go (Kind.Term.fn16 fnid orig x0)) = (Kind.Term.Quoted.fun fnid orig (Kind.Term.quote.args x0))
 (Kind.Term.quote.go (Kind.Term.hlp orig)) = (Kind.Term.Quoted.hlp orig)
-(Kind.Term.quote.go (Kind.Term.u60 orig)) = (Kind.Term.Quoted.u60 orig)
-(Kind.Term.quote.go (Kind.Term.num orig numb)) = (Kind.Term.Quoted.num orig numb)
+(Kind.Term.quote.go (Kind.Term.U60 orig)) = (Kind.Term.Quoted.u60 orig)
+(Kind.Term.quote.go (Kind.Term.u60 orig numb)) = (Kind.Term.Quoted.num orig numb)
 (Kind.Term.quote.go (Kind.Term.op2 orig operator left right)) = (Kind.Term.Quoted.op2 orig operator (Kind.Term.quote.go left) (Kind.Term.quote.go right))
 (Kind.Term.quote.args (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)) = [(Kind.Term.quote.go x0), (Kind.Term.quote.go x1), (Kind.Term.quote.go x2), (Kind.Term.quote.go x3), (Kind.Term.quote.go x4), (Kind.Term.quote.go x5), (Kind.Term.quote.go x6), (Kind.Term.quote.go x7), (Kind.Term.quote.go x8), (Kind.Term.quote.go x9), (Kind.Term.quote.go x10), (Kind.Term.quote.go x11), (Kind.Term.quote.go x12), (Kind.Term.quote.go x13), (Kind.Term.quote.go x14)]
 (Kind.Term.quote.args (Kind.Term.args16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)) = [(Kind.Term.quote.go x0), (Kind.Term.quote.go x1), (Kind.Term.quote.go x2), (Kind.Term.quote.go x3), (Kind.Term.quote.go x4), (Kind.Term.quote.go x5), (Kind.Term.quote.go x6), (Kind.Term.quote.go x7), (Kind.Term.quote.go x8), (Kind.Term.quote.go x9), (Kind.Term.quote.go x10), (Kind.Term.quote.go x11), (Kind.Term.quote.go x12), (Kind.Term.quote.go x13), (Kind.Term.quote.go x14), (Kind.Term.quote.go x15)]

crates/kind-checker/src/compiler/mod.rs

@@ -280,7 +280,7 @@ fn codegen_all_expr(
             ],
         ),
         NumU60 { numb } => mk_lifted_ctr(
-            eval_ctr(quote, TermTag::Num),
+            eval_ctr(quote, TermTag::NUMU60),
             vec![range_to_num(expr.range), mk_u60(*numb)],
         ),
         NumF60 { numb: _ } => todo!(),

crates/kind-checker/src/compiler/tags.rs

@@ -21,7 +21,7 @@ pub enum TermTag {
     Sub,
     Typ,
     U60,
-    Num,
+    NUMU60,
     Binary,
     Hole,
     Hlp,
@@ -55,8 +55,8 @@ impl fmt::Display for TermTag {
             TermTag::Ann => write!(f, "Kind.Term.ann"),
             TermTag::Sub => write!(f, "Kind.Term.sub"),
             TermTag::Typ => write!(f, "Kind.Term.typ"),
-            TermTag::U60 => write!(f, "Kind.Term.u60"),
-            TermTag::Num => write!(f, "Kind.Term.num"),
+            TermTag::U60 => write!(f, "Kind.Term.U60"),
+            TermTag::NUMU60 => write!(f, "Kind.Term.u60"),
             TermTag::Binary => write!(f, "Kind.Term.op2"),
             TermTag::Hole => write!(f, "Kind.Term.hol"),
             TermTag::Hlp => write!(f, "Kind.Term.hlp"),

crates/kind-driver/Cargo.toml

@@ -16,7 +16,7 @@ kind-pass = { path = "../kind-pass" }
 kind-target-hvm = { path = "../kind-target-hvm" }
 kind-target-kdl = { path = "../kind-target-kdl" }
 
-hvm = { git = "https://github.com/Kindelia/HVM.git" }
+hvm = { git = "https://github.com/Kindelia/HVM.git", rev="5599e0c8504bee976b7870b51f0c2d4b57e3bf82" }
 
 anyhow = "1.0.66"
 strsim = "0.10.0"

crates/kind-pass/src/erasure/mod.rs

@@ -308,9 +308,9 @@ impl<'a> ErasureState<'a> {
 
                 // We cannot pattern match on functions in a relevant function.
                 // it would change its behaviour.
-                if relevance == Ambient::Irrelevant {
-                    self.set_relevance(edge, Relevance::Irrelevant, expr.range)
-                }
+                // if relevance == Ambient::Irrelevant {
+                //     self.set_relevance(edge, Relevance::Irrelevant, expr.range)
+                // }
 
                 let params = self.book.entrs.get(name.to_str()).unwrap();
 
@@ -329,9 +329,9 @@ impl<'a> ErasureState<'a> {
 
                 // We cannot pattenr match on functions in a relevant function.
                 // it would change its behaviour.
-                if relevance == Ambient::Irrelevant {
-                    self.set_relevance(edge, Relevance::Irrelevant, expr.range)
-                }
+                // if relevance == Ambient::Irrelevant {
+                //     self.set_relevance(edge, Relevance::Irrelevant, expr.range)
+                // }
 
                 let params = self.book.entrs.get(name.to_str()).unwrap();
 

crates/kind-target-hvm/Cargo.toml

@@ -11,4 +11,4 @@ kind-tree = { path = "../kind-tree" }
 kind-report = { path = "../kind-report" }
 kind-derive = { path = "../kind-derive" }
 
-hvm = { git = "https://github.com/Kindelia/HVM.git" }
+hvm = { git = "https://github.com/Kindelia/HVM.git", rev="5599e0c8504bee976b7870b51f0c2d4b57e3bf82" }

crates/kind-tests/suite/checker/issues/HvmReducesTooMuch.golden

@@ -0,0 +1,15 @@
+   INFO  Inspection.
+
+      * Expected: (Assert (Nat.count_layers n 1)) 
+
+      * Context: 
+      *   n : Nat 
+
+      /--[suite/checker/issues/HvmReducesTooMuch.kind2:13:29]
+      |
+   12 |    Beq_nat_refl (n: Nat) : Assert (Nat.count_layers n 0)
+   13 |    Beq_nat_refl (Nat.succ n) = ?
+      |                                v
+      |                                \Here!
+
+

crates/kind-tests/suite/checker/issues/HvmReducesTooMuch.kind2

@@ -0,0 +1,11 @@
+type Nat {
+    succ (pred: Nat)
+    zero
+}
+
+Nat.count_layers (n: Nat) (m: U60) : U60
+Nat.count_layers (Nat.succ n) m = Nat.count_layers n (+ m 1)
+Nat.count_layers n     m = (+ m 1)
+
+Main : Nat -> U60
+Main = x => Nat.count_layers (Nat.succ x) 0

crates/kind-tree/Cargo.toml

@@ -6,7 +6,7 @@ edition = "2021"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-hvm = { git = "https://github.com/Kindelia/HVM.git" }
+hvm = { git = "https://github.com/Kindelia/HVM.git", rev="5599e0c8504bee976b7870b51f0c2d4b57e3bf82" }
 
 kind-span = {path = "../kind-span"}
 linked-hash-map = "0.5.6"