id of unit

Cargo.lock

@@ -38,12 +38,16 @@ version = "0.1.0"
 dependencies = [
  "anyhow",
  "dashmap",
+ "env_logger",
  "im",
  "lalrpop",
  "lalrpop-util",
  "lazy_static",
  "rustyline",
+ "test-log",
  "trace",
+ "tracing",
+ "tracing-subscriber",
 ]
 
 [[package]]
@@ -118,6 +122,15 @@ dependencies = [
  "parking_lot_core",
 ]
 
+[[package]]
+name = "deranged"
+version = "0.3.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0f32d04922c60427da6f9fef14d042d9edddef64cb9d4ce0d64d0685fbeb1fd3"
+dependencies = [
+ "powerfmt",
+]
+
 [[package]]
 name = "diff"
 version = "0.1.13"
@@ -166,6 +179,19 @@ version = "0.1.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "c34f04666d835ff5d62e058c3995147c06f42fe86ff053337632bca83e42702d"
 
+[[package]]
+name = "env_logger"
+version = "0.10.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "85cdab6a89accf66733ad5a1693a4dcced6aeff64602b634530dd73c1f3ee9f0"
+dependencies = [
+ "humantime",
+ "is-terminal",
+ "log",
+ "regex",
+ "termcolor",
+]
+
 [[package]]
 name = "equivalent"
 version = "1.0.1"
@@ -241,6 +267,12 @@ dependencies = [
  "windows-sys",
 ]
 
+[[package]]
+name = "humantime"
+version = "2.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4"
+
 [[package]]
 name = "im"
 version = "15.1.0"
@@ -285,6 +317,12 @@ dependencies = [
  "either",
 ]
 
+[[package]]
+name = "itoa"
+version = "1.0.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "af150ab688ff2122fcef229be89cb50dd66af9e01a4ff320cc137eecc9bacc38"
+
 [[package]]
 name = "lalrpop"
 version = "0.20.0"
@@ -362,6 +400,15 @@ version = "0.4.20"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "b5e6163cb8c49088c2c36f57875e58ccd8c87c7427f7fbd50ea6710b2f3f2e8f"
 
+[[package]]
+name = "matchers"
+version = "0.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8263075bb86c5a1b1427b5ae862e8889656f126e9f77c484496e8b47cf5c5558"
+dependencies = [
+ "regex-automata 0.1.10",
+]
+
 [[package]]
 name = "memchr"
 version = "2.6.4"
@@ -394,12 +441,28 @@ dependencies = [
  "libc",
 ]
 
+[[package]]
+name = "nu-ansi-term"
+version = "0.46.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "77a8165726e8236064dbb45459242600304b42a5ea24ee2948e18e023bf7ba84"
+dependencies = [
+ "overload",
+ "winapi",
+]
+
 [[package]]
 name = "once_cell"
 version = "1.18.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "dd8b5dd2ae5ed71462c540258bedcb51965123ad7e7ccf4b9a8cafaa4a63576d"
 
+[[package]]
+name = "overload"
+version = "0.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b15813163c1d831bf4a13c3610c05c0d03b39feb07f7e09fa234dac9b15aaf39"
+
 [[package]]
 name = "parking_lot"
 version = "0.12.1"
@@ -448,6 +511,18 @@ version = "0.5.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "5be167a7af36ee22fe3115051bc51f6e6c7054c9348e28deb4f49bd6f705a315"
 
+[[package]]
+name = "pin-project-lite"
+version = "0.2.13"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8afb450f006bf6385ca15ef45d71d2288452bc3683ce2e2cacc0d18e4be60b58"
+
+[[package]]
+name = "powerfmt"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "439ee305def115ba05938db6eb1644ff94165c5ab5e9420d1c1bcedbba909391"
+
 [[package]]
 name = "precomputed-hash"
 version = "0.1.1"
@@ -525,10 +600,19 @@ checksum = "380b951a9c5e80ddfd6136919eef32310721aa4aacd4889a8d39124b026ab343"
 dependencies = [
  "aho-corasick",
  "memchr",
- "regex-automata",
+ "regex-automata 0.4.3",
  "regex-syntax 0.8.2",
 ]
 
+[[package]]
+name = "regex-automata"
+version = "0.1.10"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6c230d73fb8d8c1b9c0b3135c5142a8acee3a0558fb8db5cf1cb65f8d7862132"
+dependencies = [
+ "regex-syntax 0.6.29",
+]
+
 [[package]]
 name = "regex-automata"
 version = "0.4.3"
@@ -540,6 +624,12 @@ dependencies = [
  "regex-syntax 0.8.2",
 ]
 
+[[package]]
+name = "regex-syntax"
+version = "0.6.29"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f162c6dd7b008981e4d40210aca20b4bd0f9b60ca9271061b07f78537722f2e1"
+
 [[package]]
 name = "regex-syntax"
 version = "0.7.5"
@@ -594,12 +684,58 @@ dependencies = [
  "winapi",
 ]
 
+[[package]]
+name = "ryu"
+version = "1.0.15"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1ad4cc8da4ef723ed60bced201181d83791ad433213d8c24efffda1eec85d741"
+
 [[package]]
 name = "scopeguard"
 version = "1.2.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49"
 
+[[package]]
+name = "serde"
+version = "1.0.192"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bca2a08484b285dcb282d0f67b26cadc0df8b19f8c12502c13d966bf9482f001"
+dependencies = [
+ "serde_derive",
+]
+
+[[package]]
+name = "serde_derive"
+version = "1.0.192"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d6c7207fbec9faa48073f3e3074cbe553af6ea512d7c21ba46e434e70ea9fbc1"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn 2.0.38",
+]
+
+[[package]]
+name = "serde_json"
+version = "1.0.108"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3d1c7e3eac408d115102c4c24ad393e0821bb3a5df4d506a80f85f7a742a526b"
+dependencies = [
+ "itoa",
+ "ryu",
+ "serde",
+]
+
+[[package]]
+name = "sharded-slab"
+version = "0.1.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f40ca3c46823713e0d4209592e8d6e826aa57e928f09752619fc696c499637f6"
+dependencies = [
+ "lazy_static",
+]
+
 [[package]]
 name = "siphasher"
 version = "0.3.11"
@@ -674,6 +810,26 @@ dependencies = [
  "winapi",
 ]
 
+[[package]]
+name = "termcolor"
+version = "1.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6093bad37da69aab9d123a8091e4be0aa4a03e4d601ec641c327398315f62b64"
+dependencies = [
+ "winapi-util",
+]
+
+[[package]]
+name = "test-log"
+version = "0.2.13"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f66edd6b6cd810743c0c71e1d085e92b01ce6a72782032e3f794c8284fe4bcdd"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn 2.0.38",
+]
+
 [[package]]
 name = "thiserror"
 version = "1.0.50"
@@ -694,6 +850,45 @@ dependencies = [
  "syn 2.0.38",
 ]
 
+[[package]]
+name = "thread_local"
+version = "1.1.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3fdd6f064ccff2d6567adcb3873ca630700f00b5ad3f060c25b5dcfd9a4ce152"
+dependencies = [
+ "cfg-if",
+ "once_cell",
+]
+
+[[package]]
+name = "time"
+version = "0.3.30"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c4a34ab300f2dee6e562c10a046fc05e358b29f9bf92277f30c3c8d82275f6f5"
+dependencies = [
+ "deranged",
+ "itoa",
+ "powerfmt",
+ "serde",
+ "time-core",
+ "time-macros",
+]
+
+[[package]]
+name = "time-core"
+version = "0.1.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ef927ca75afb808a4d64dd374f00a2adf8d0fcff8e7b184af886c3c87ec4a3f3"
+
+[[package]]
+name = "time-macros"
+version = "0.2.15"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4ad70d68dba9e1f8aceda7aa6711965dfec1cac869f311a51bd08b3a2ccbce20"
+dependencies = [
+ "time-core",
+]
+
 [[package]]
 name = "tiny-keccak"
 version = "2.0.2"
@@ -714,6 +909,81 @@ dependencies = [
  "syn 1.0.109",
 ]
 
+[[package]]
+name = "tracing"
+version = "0.1.40"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c3523ab5a71916ccf420eebdf5521fcef02141234bbc0b8a49f2fdc4544364ef"
+dependencies = [
+ "pin-project-lite",
+ "tracing-attributes",
+ "tracing-core",
+]
+
+[[package]]
+name = "tracing-attributes"
+version = "0.1.27"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn 2.0.38",
+]
+
+[[package]]
+name = "tracing-core"
+version = "0.1.32"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c06d3da6113f116aaee68e4d601191614c9053067f9ab7f6edbcb161237daa54"
+dependencies = [
+ "once_cell",
+ "valuable",
+]
+
+[[package]]
+name = "tracing-log"
+version = "0.1.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f751112709b4e791d8ce53e32c4ed2d353565a795ce84da2285393f41557bdf2"
+dependencies = [
+ "log",
+ "once_cell",
+ "tracing-core",
+]
+
+[[package]]
+name = "tracing-serde"
+version = "0.1.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bc6b213177105856957181934e4920de57730fc69bf42c37ee5bb664d406d9e1"
+dependencies = [
+ "serde",
+ "tracing-core",
+]
+
+[[package]]
+name = "tracing-subscriber"
+version = "0.3.17"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "30a651bc37f915e81f087d86e62a18eec5f79550c7faff886f7090b4ea757c77"
+dependencies = [
+ "matchers",
+ "nu-ansi-term",
+ "once_cell",
+ "regex",
+ "serde",
+ "serde_json",
+ "sharded-slab",
+ "smallvec",
+ "thread_local",
+ "time",
+ "tracing",
+ "tracing-core",
+ "tracing-log",
+ "tracing-serde",
+]
+
 [[package]]
 name = "typenum"
 version = "1.17.0"
@@ -750,6 +1020,12 @@ version = "0.2.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "711b9620af191e0cdc7468a8d14e709c3dcdb115b36f838e601583af800a370a"
 
+[[package]]
+name = "valuable"
+version = "0.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "830b7e5d4d90034032940e4ace0d9a9a057e7a45cd94e6c007832e39edb82f6d"
+
 [[package]]
 name = "version_check"
 version = "0.9.4"
@@ -778,6 +1054,15 @@ version = "0.4.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6"
 
+[[package]]
+name = "winapi-util"
+version = "0.1.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f29e6f9198ba0d26b4c9f07dbe6f9ed633e1f3d5b8b414090084349e46a52596"
+dependencies = [
+ "winapi",
+]
+
 [[package]]
 name = "winapi-x86_64-pc-windows-gnu"
 version = "0.4.0"

bidir/Cargo.toml

@@ -8,11 +8,17 @@ edition = "2021"
 [dependencies]
 anyhow = "1.0.75"
 dashmap = "5.5.3"
+env_logger = "0.10.0"
 im = "15.1.0"
 lalrpop-util = { version = "0.20.0", features = ["lexer", "regex", "unicode"] }
 lazy_static = "1.4.0"
 rustyline = "12.0.0"
 trace = "0.1.7"
+tracing = "0.1.40"
+tracing-subscriber = { version = "0.3.17", features = ["env-filter", "json", "regex", "serde", "time", "tracing"] }
 
 [build-dependencies]
 lalrpop = "0.20.0"
+
+[dev-dependencies]
+test-log = { version = "0.2.13", features = ["trace"] }

bidir/src/bidir.rs

@@ -1,14 +1,16 @@
 use anyhow::{bail, Result};
 
-use crate::DEPTH;
-
 use crate::data::{Context, ContextEntry, FreeVar, Monotype, Term, Type};
 use crate::gensym::gensym_existential;
 
 // Figure 8. Applying a context, as a substitution, to a type
 
+#[instrument]
 pub fn app_ctx(ctx: &Context, ty: &Type) -> Result<Type> {
   match ty {
+    Type::Unit => Ok(Type::Unit),
+    Type::Var(s) => Ok(Type::Var(s.clone())),
+
     Type::Existential(a) => match ctx.lookup_existential(a) {
       Some((_, Some(m))) => Ok(m.into_poly()),
       Some((_, None)) => Ok(Type::Existential(a.clone())),
@@ -21,14 +23,13 @@ pub fn app_ctx(ctx: &Context, ty: &Type) -> Result<Type> {
       Box::new(app_ctx(ctx, a)?),
       Box::new(app_ctx(ctx, b)?),
     )),
-    _ => todo!("shiiet ctx = {ctx:?}, ty = {ty:?}"),
   }
 }
 
 // Figure 9. Algorithmic subtyping
 
 /// Under input context Γ , type A is a subtype of B, with output context ∆
-#[trace]
+#[instrument]
 pub fn subtype(ctx: &Context, left: &Type, right: &Type) -> Result<Context> {
   match (left, right) {
     // <:Unit rule
@@ -44,8 +45,9 @@ pub fn subtype(ctx: &Context, left: &Type, right: &Type) -> Result<Context> {
       Ok(ctx.clone())
     }
 
+    // <:InstantiateL
     (Type::Existential(a), ty_a)
-      if !right
+      if !ty_a
         .free_vars()
         .contains(&FreeVar::Existential(a.to_string()))
         && ctx.lookup_existential(a).is_some() =>
@@ -53,6 +55,18 @@ pub fn subtype(ctx: &Context, left: &Type, right: &Type) -> Result<Context> {
       let ctx_delta = instantiate_left(ctx, a, ty_a)?;
       Ok(ctx_delta)
     }
+
+    // <:InstantiateR
+    (ty_a, Type::Existential(a))
+      if !ty_a
+        .free_vars()
+        .contains(&FreeVar::Existential(a.to_string()))
+        && ctx.lookup_existential(a).is_some() =>
+    {
+      let ctx_delta = instantiate_right(ctx, ty_a, a)?;
+      Ok(ctx_delta)
+    }
+
     (Type::Existential(_), Type::Unit) => todo!(),
     (Type::Existential(_), Type::Var(_)) => todo!(),
     (Type::Existential(_), Type::Polytype(_, _)) => todo!(),
@@ -74,7 +88,6 @@ pub fn subtype(ctx: &Context, left: &Type, right: &Type) -> Result<Context> {
 
 // Figure 10. Instantiation
 
-#[trace]
 pub fn instantiate_left(ctx: &Context, a: &str, ty_a: &Type) -> Result<Context> {
   match ty_a {
     // InstLReach rule
@@ -103,9 +116,36 @@ pub fn instantiate_left(ctx: &Context, a: &str, ty_a: &Type) -> Result<Context>
   }
 }
 
+pub fn instantiate_right(ctx: &Context, ty_a: &Type, a: &str) -> Result<Context> {
+  match ty_a {
+    ty_a if ty_a.is_mono() && ctx.has_existential(a) => {
+      let (before, after) = ctx
+        .split_by(|entry| match entry {
+          ContextEntry::ExistentialVar(n) if n == a => true,
+          _ => false,
+        })
+        .unwrap();
+
+      let ty_a_mono = ty_a.into_mono().unwrap();
+
+      Ok(Context::unsplit(
+        &before,
+        ContextEntry::ExistentialSolved(a.to_owned(), ty_a_mono),
+        &after,
+      ))
+    }
+
+    Type::Unit => todo!(),
+    Type::Var(_) => todo!(),
+    Type::Existential(_) => todo!(),
+    Type::Polytype(_, _) => todo!(),
+    Type::Arrow(_, _) => todo!(),
+  }
+}
+
 // Figure 11. Algorithmic typing
 
-#[trace]
+#[instrument]
 pub fn typecheck(ctx: &Context, term: &Term, ty: &Type) -> Result<Context> {
   match (term, ty) {
     // 1I rule
@@ -131,7 +171,7 @@ pub fn typecheck(ctx: &Context, term: &Term, ty: &Type) -> Result<Context> {
   }
 }
 
-#[trace]
+#[instrument]
 pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> {
   match term {
     // Var rule
@@ -158,7 +198,7 @@ pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> {
       let ex_a_s = gensym_existential();
       let ex_b_s = gensym_existential();
 
-      let ex_gen = format!("{}->", ex_a_s);
+      let ex_gen = format!("{}→", ex_a_s);
 
       let ex_a = Type::Existential(ex_a_s.clone());
       let ex_b = Type::Existential(ex_b_s.clone());
@@ -171,29 +211,23 @@ pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> {
       ]);
 
       let wtf_ctx = typecheck(&aug_ctx, &e, &ex_b)?;
-      println!("WTF CTX {wtf_ctx:?}");
+      info!("WTF CTX {wtf_ctx:?}");
 
       // Split back out at the marker
-      let (before_marker, after_marker) = {
+      let (before_marker, after_marker) = wtf_ctx
-        let marker_idx = wtf_ctx
+        .split_by(|entry| match entry {
-          .0
+          ContextEntry::Marker(m) if *m == ex_a_s => true,
-          .iter()
+          _ => false,
-          .position(|entry| match entry {
+        })
-            ContextEntry::Marker(m) if *m == ex_a_s => true,
+        .unwrap();
-            _ => false,
+      info!("Unsolved: {:?}", after_marker.unsolved_existentials());
-          })
-          .unwrap();
-
-        // println!("Marker index: {marker_idx}");
-        wtf_ctx.0.clone().split_at(marker_idx)
-      };
-      let before_marker = Context(before_marker);
-      let after_marker = Context(after_marker);
 
       let mut tau = app_ctx(&after_marker, &Type::Arrow(Box::new(ex_a), Box::new(ex_b)))?;
       for name in after_marker.unsolved_existentials() {
-        tau = tau.subst(name, &Type::Var(ex_gen.clone()));
+        warn!("substituting {tau:?} looking for {name}");
+        tau = tau.subst(&name, &Type::Var(ex_gen.clone()));
       }
+      info!("ex_gen = {ex_gen}, tau = {tau:?}");
 
       Ok((Type::Polytype(ex_gen, Box::new(tau)), before_marker))
     }
@@ -230,17 +264,25 @@ pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> {
   }
 }
 
-#[trace]
+#[instrument]
 pub fn app_synthesize(ctx: &Context, fun_ty: &Type, term: &Term) -> Result<(Type, Context)> {
   match (fun_ty, term) {
     // →App rule
     (Type::Arrow(ty_a, ty_c), e) => {
+      info!("→App rule");
       typecheck(ctx, e, ty_a)?;
       Ok((*ty_c.clone(), ctx.clone()))
     }
 
     // ∀App rule
-    (Type::Polytype(_, _), _) => todo!(),
+    (Type::Polytype(a, ty_a), e) => {
+      let ex_s = gensym_existential();
+      let ex = ContextEntry::ExistentialVar(ex_s.clone());
+      let aug_ctx = ctx.add(vec![ex.clone()]);
+
+      let aug_ty = ty_a.subst(&a, &Type::Existential(ex_s));
+      app_synthesize(&aug_ctx, &aug_ty, e)
+    }
 
     // âApp rule
     (Type::Existential(_), _) => todo!(),

bidir/src/data.rs

@@ -15,7 +15,7 @@ impl fmt::Debug for Term {
   fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
     match self {
       Self::Unit => write!(f, "unit"),
-      Self::Var(arg0) => write!(f, "`{}", arg0),
+      Self::Var(arg0) => write!(f, "{}", arg0),
       Self::Lam(arg0, arg1) => write!(f, "(λ{}.{:?})", arg0, arg1),
       Self::App(arg0, arg1) => write!(f, "({:?} · {:?})", arg0, arg1),
       Self::Annot(arg0, arg1) => write!(f, "({:?} : {:?})", arg0, arg1),
@@ -94,12 +94,12 @@ impl Type {
     free_vars_with_context(&Context::default(), self)
   }
 
-  pub fn subst(&self, var: impl AsRef<str>, replacement: &Type) -> Type {
+  pub fn subst(&self, var: &str, replacement: &Type) -> Type {
-    let var = var.as_ref();
     match self {
       Type::Unit => Type::Unit,
       Type::Var(n) if n == var => replacement.clone(),
       Type::Var(n) => Type::Var(n.clone()),
+      Type::Existential(s) if s == var => replacement.clone(),
       Type::Existential(s) => Type::Existential(s.clone()),
       Type::Polytype(a, t) => Type::Polytype(a.clone(), Box::new(t.subst(var, replacement))),
       Type::Arrow(a, b) => Type::Arrow(
@@ -122,7 +122,7 @@ impl fmt::Debug for Monotype {
   fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
     match self {
       Self::Unit => write!(f, "𝟙"),
-      Self::Var(arg0) => write!(f, "`{}", arg0),
+      Self::Var(arg0) => write!(f, "{}", arg0),
       Self::Existential(arg0) => write!(f, "{}", arg0),
       Self::Arrow(arg0, arg1) => write!(f, "({arg0:?} -> {arg1:?})"),
     }
@@ -152,9 +152,9 @@ pub enum ContextEntry {
 impl fmt::Debug for ContextEntry {
   fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
     match self {
-      Self::TypeVar(arg0) => write!(f, "`{}", arg0),
+      Self::TypeVar(arg0) => write!(f, "{}", arg0),
       Self::TermAnnot(arg0, arg1) => write!(f, "{} : {:?}", arg0, arg1),
-      Self::ExistentialVar(arg0) => write!(f, "`{}", arg0),
+      Self::ExistentialVar(arg0) => write!(f, "{}", arg0),
       Self::ExistentialSolved(arg0, arg1) => write!(f, "{} = {:?}", arg0, arg1),
       Self::Marker(arg0) => write!(f, "▶{}", arg0),
     }
@@ -230,6 +230,7 @@ impl Context {
     self.lookup_existential(name).is_some()
   }
 
+  /// Returns a list of names of unsolved existentials
   pub fn unsolved_existentials(&self) -> HashSet<String> {
     let mut unsolved = HashSet::new();
 
@@ -244,4 +245,24 @@ impl Context {
 
     unsolved
   }
+
+  /// Returns (before, after)
+  pub fn split_by<P>(&self, p: P) -> Option<(Context, Context)>
+  where
+    P: Fn(&ContextEntry) -> bool,
+  {
+    let (before, after) = {
+      let idx = self.0.iter().position(p)?;
+      self.0.clone().split_at(idx)
+    };
+
+    Some((Context(before), Context(after)))
+  }
+
+  pub fn unsplit(left: &Context, center: ContextEntry, right: &Context) -> Context {
+    let mut res = left.clone();
+    res.0.push_back(center);
+    res.0.extend(right.0.clone().into_iter());
+    res
+  }
 }

bidir/src/lib.rs

@@ -1,5 +1,7 @@
 #[macro_use]
 extern crate trace;
+#[macro_use]
+extern crate tracing;
 
 use lalrpop_util::lalrpop_mod;
 

bidir/src/tests.rs

@@ -16,7 +16,7 @@ fn test_id() -> Result<()> {
   let id = id_term!();
   let ctx = Context::default();
   let (ty, out_ctx) = synthesize(&ctx, &id)?;
-  println!("Synthesis result: {ty:?} | {out_ctx:?}");
+  bail!("Synthesized: {:?} (context = {:?})", ty, out_ctx);
 
   Ok(())
 }
@@ -27,6 +27,7 @@ fn test_id_of_unit() -> Result<()> {
   let id_of_unit = Term::App(Box::new(id), Box::new(Term::Unit));
   let ctx = Context::default();
 
-  bail!("Result: {:?}", synthesize(&ctx, &id_of_unit));
+  let (ty, out_ctx) = synthesize(&ctx, &id_of_unit)?;
+  bail!("Synthesized: {:?} (context = {:?})", ty, out_ctx);
   Ok(())
 }