init

.gitignore

@@ -0,0 +1 @@
+target

Cargo.toml

@@ -0,0 +1,41 @@
+[package]
+name = "bidir"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+anyhow = { version = "1.0.75", features = ["backtrace"] }
+contracts = { version = "0.6.3" }
+dashmap = "5.5.3"
+derivative = "2.2.0"
+env_logger = "0.10.0"
+im = { version = "15.1.0", features = ["proptest", "quickcheck"] }
+lalrpop-util = { version = "0.20.0", features = ["lexer", "regex", "unicode"] }
+lazy_static = "1.4.0"
+leptos_reactive = "0.5.2"
+proptest = "1.4.0"
+proptest-derive = "0.4.0"
+quickcheck = "1.0.3"
+quickcheck_macros = "1.0.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"] }
+
+[features]
+trace_execution = []

build.rs

@@ -0,0 +1,3 @@
+fn main() {
+  lalrpop::process_root().unwrap()
+}

src/abstract_data.rs

@@ -0,0 +1,9 @@
+pub trait Data {
+  /* Required methods                                                      */
+  /*                                                                       */
+
+  /* Provided methods                                                      */
+  /*                                                                       */
+
+  fn synthesize() {}
+}

src/bidir.rs

@@ -0,0 +1,360 @@
+use anyhow::{bail, Result};
+
+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
+
+#[cfg_attr(feature = "trace_execution", trace)]
+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())),
+      None => bail!("existential variable {a} doesn't exist in context"),
+    },
+
+    Type::Polytype(a, t) => {
+      Ok(Type::Polytype(a.clone(), Box::new(app_ctx(ctx, t)?)))
+    }
+
+    Type::Arrow(a, b) => Ok(Type::Arrow(
+      Box::new(app_ctx(ctx, a)?),
+      Box::new(app_ctx(ctx, b)?),
+    )),
+  }
+}
+
+// Figure 9. Algorithmic subtyping
+
+/// Under input context Γ , type A is a subtype of B, with output context ∆
+#[cfg_attr(feature = "trace_execution", trace)]
+pub fn subtype(ctx: &Context, left: &Type, right: &Type) -> Result<Context> {
+  match (left, right) {
+    // <:Unit rule
+    (Type::Unit, Type::Unit) => Ok(ctx.clone()),
+
+    // <:Var rule
+    (Type::Var(x), Type::Var(y)) if x == y && ctx.lookup_type(x).is_some() => Ok(ctx.clone()),
+
+    // <:Exvar rule
+    (Type::Existential(x), Type::Existential(y))
+      if x == y && ctx.lookup_existential(x).is_some() =>
+    {
+      Ok(ctx.clone())
+    }
+
+    // <:InstantiateL
+    (Type::Existential(a), ty_a)
+      if !ty_a
+        .free_vars()
+        .contains(&FreeVar::Existential(a.to_string()))
+        && ctx.lookup_existential(a).is_some() =>
+    {
+      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!(),
+    (Type::Existential(_), Type::Arrow(_, _)) => todo!(),
+    (Type::Polytype(_, _), Type::Unit) => todo!(),
+    (Type::Polytype(_, _), Type::Var(_)) => todo!(),
+    (Type::Polytype(_, _), Type::Existential(_)) => todo!(),
+    (Type::Polytype(_, _), Type::Polytype(_, _)) => todo!(),
+    (Type::Polytype(_, _), Type::Arrow(_, _)) => todo!(),
+    (Type::Arrow(_, _), Type::Unit) => todo!(),
+    (Type::Arrow(_, _), Type::Var(_)) => todo!(),
+    (Type::Arrow(_, _), Type::Existential(_)) => todo!(),
+    (Type::Arrow(_, _), Type::Polytype(_, _)) => todo!(),
+    (Type::Arrow(_, _), Type::Arrow(_, _)) => todo!(),
+
+    _ => bail!("subtyping relation failed between {left:?} and {right:?} (ctx = {ctx:?})"),
+  }
+}
+
+// Figure 10. Instantiation
+
+#[cfg_attr(feature = "trace_execution", trace)]
+pub fn instantiate_left(
+  ctx: &Context,
+  a: &str,
+  ty_a: &Type,
+) -> Result<Context> {
+  match ty_a {
+    // InstLReach rule
+    Type::Existential(b)
+      if ctx.has_existential(a) && ctx.has_existential(b) =>
+    {
+      let mut new_ctx = ctx.clone();
+      {
+        let b_entry = new_ctx
+          .0
+          .iter_mut()
+          .find(
+            |entry| matches!(entry, ContextEntry::ExistentialVar(x) if x == b),
+          )
+          .expect("should exist");
+
+        *b_entry = ContextEntry::ExistentialSolved(
+          b.to_owned(),
+          Monotype::Existential(a.to_owned()),
+        );
+      }
+
+      Ok(new_ctx)
+    }
+
+    Type::Existential(_b) => todo!(),
+
+    Type::Unit => todo!(),
+    Type::Var(_) => todo!(),
+    Type::Polytype(_, _) => todo!(),
+    Type::Arrow(_, _) => todo!(),
+  }
+}
+
+#[cfg_attr(feature = "trace_execution", trace)]
+pub fn instantiate_right(
+  ctx: &Context,
+  ty_a: &Type,
+  a: &str,
+) -> Result<Context> {
+  match ty_a {
+    // InstRArr
+    Type::Arrow(ty_a1, ty_a2) if ctx.has_existential(a) => {
+      // TODO: In case it's already solved?
+      println!("original ctx: {ctx:?}");
+
+      let (ex_a1_s, ex_a2_s, ctx_gamma_aug) =
+        ctx.split_existential_function(a)?;
+
+      let ctx_theta = instantiate_left(&ctx_gamma_aug, &ex_a1_s, &ty_a1)?;
+
+      let ty_a2_aug = app_ctx(&ctx_theta, &ty_a2)?;
+      let ctx_delta = instantiate_right(&ctx_theta, &ty_a2_aug, &ex_a2_s)?;
+
+      Ok(ctx_delta)
+    }
+
+    // InstRAllL
+    Type::Polytype(beta, ty_b) if ctx.has_existential(a) => {
+      let ex_b = gensym_existential();
+      let aug_ctx = ctx.add(vec![
+        ContextEntry::Marker(ex_b.to_owned()),
+        ContextEntry::ExistentialVar(ex_b.to_owned()),
+      ]);
+
+      let aug_b = ty_b.subst(beta, &Type::Existential(ex_b.to_owned()));
+      let out_ctx = instantiate_right(&aug_ctx, &aug_b, a)?;
+
+      let (before, _after) = out_ctx
+        .split_by(
+          |entry| matches!(entry, ContextEntry::Marker(m) if *m == ex_b),
+        )
+        .unwrap();
+
+      Ok(before)
+    }
+
+    // InstRSolve
+    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!(),
+
+    _ => todo!(),
+  }
+}
+
+// Figure 11. Algorithmic typing
+
+#[cfg_attr(feature = "trace_execution", trace)]
+pub fn typecheck(ctx: &Context, term: &Term, ty: &Type) -> Result<Context> {
+  match (term, ty) {
+    // 1I rule
+    (Term::Unit, Type::Unit) => Ok(ctx.clone()),
+
+    // ∀I rule
+    (_e, Type::Polytype(_x, _tyA)) => todo!(),
+
+    // →I rule
+    (Term::Lam(_x, _e), Type::Arrow(_ty_a, _ty_b)) => {
+      let _aug_ctx = ctx.clone();
+      todo!()
+    }
+
+    // Sub rule
+    (term, ty) => {
+      let (ty_a, ctx_theta) = synthesize(ctx, term)?;
+      let a = app_ctx(&ctx_theta, &ty_a)?;
+      let b = app_ctx(&ctx_theta, ty)?;
+      let ctx_delta = subtype(&ctx_theta, &a, &b)?;
+      Ok(ctx_delta)
+    }
+  }
+}
+
+#[cfg_attr(feature = "trace_execution", trace)]
+pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> {
+  match term {
+    // Var rule
+    Term::Var(name) if ctx.has_type(name) => {
+      let (_, ty) = ctx.lookup_type(name).unwrap();
+      Ok((ty, ctx.clone()))
+    }
+    Term::Var(name) => bail!("could not find name {name}"),
+
+    // 1I⇒ rule
+    Term::Unit => Ok((Type::Unit, ctx.clone())),
+
+    // Anno rule
+    Term::Annot(e, ty_a) => {
+      // Make sure the type is well formed
+      // TODO: Have an actual "well-formed" check
+
+      let ctx_delta = typecheck(ctx, &e, ty_a)?;
+      Ok((ty_a.clone(), ctx_delta))
+    }
+
+    // →I⇒' rule
+    Term::Lam(x, e) => {
+      let ex_a_s = gensym_existential();
+      let ex_b_s = gensym_existential();
+
+      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());
+
+      let aug_ctx = ctx.add(vec![
+        ContextEntry::Marker(ex_a_s.clone()),
+        ContextEntry::ExistentialVar(ex_a_s.clone()),
+        ContextEntry::ExistentialVar(ex_b_s.clone()),
+        ContextEntry::TermAnnot(x.clone(), ex_a.clone()),
+      ]);
+
+      let wtf_ctx = typecheck(&aug_ctx, &e, &ex_b)?;
+      info!("WTF CTX {wtf_ctx:?}");
+
+      // Split back out at the marker
+      let (before_marker, after_marker) = wtf_ctx
+        .split_by(|entry| match entry {
+          ContextEntry::Marker(m) if *m == ex_a_s => true,
+          _ => false,
+        })
+        .unwrap();
+      info!("Unsolved: {:?}", after_marker.unsolved_existentials());
+
+      let mut tau =
+        app_ctx(&after_marker, &Type::Arrow(Box::new(ex_a), Box::new(ex_b)))?;
+      for name in after_marker.unsolved_existentials() {
+        warn!("substituting {tau:?} looking for {name}");
+        tau = tau.subst(&name, &Type::Var(ex_gen.clone()));
+      }
+
+      Ok((Type::Polytype(ex_gen, Box::new(tau)), before_marker))
+    }
+
+    // // →I⇒ rule
+    // // > Rule →I⇒ corresponds to Decl→I⇒, one of the guessing rules, so we
+    // // > create new existential variables ^α (for the function domain) and ^β (for
+    // // > the codomain) and check the function body against ^β.  As in ∀App, we do
+    // // > not place a marker before ^α, because ^α and ^β appear in the output type
+    // // > (λx. e ⇒ ^α → ^β).
+    // Term::Lam(x, e) => {
+    //   let ex_a_s = gensym_existential();
+    //   let ex_b_s = gensym_existential();
+    //   let ex_a = Type::Existential(ex_a_s.clone());
+    //   let ex_b = Type::Existential(ex_b_s.clone());
+    //   let aug_ctx = ctx.add(vec![
+    //     ContextEntry::ExistentialVar(ex_a_s.clone()),
+    //     ContextEntry::ExistentialVar(ex_b_s.clone()),
+    //     ContextEntry::TermAnnot(x.clone(), ex_a.clone()),
+    //   ]);
+
+    //   let wtf_ctx = typecheck(&aug_ctx, &e, &ex_b)?;
+    //   Ok((Type::Arrow(Box::new(ex_a), Box::new(ex_b)), ctx.clone()))
+    // }
+
+    // →E rule
+    Term::App(e1, e2) => {
+      let (ty_a, ctx_theta) = synthesize(ctx, e1)?;
+      let app_a = app_ctx(&ctx_theta, &ty_a)?;
+      let (ty_c, ctx_delta) = app_synthesize(&ctx_theta, &app_a, &e2)?;
+      Ok((ty_c, ctx_delta))
+    }
+  }
+}
+
+#[cfg_attr(feature = "trace_execution", trace)]
+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) => {
+      let out_ctx = typecheck(ctx, e, ty_a)?;
+      Ok((*ty_c.clone(), out_ctx))
+    }
+
+    // ∀App rule
+    (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));
+      let (ty, ctx_delta) = app_synthesize(&aug_ctx, &aug_ty, e)?;
+
+      Ok((ty, ctx_delta))
+    }
+
+    // âApp rule
+    (Type::Existential(a), e) if ctx.has_existential(a) => {
+      let (ex_a1_s, ex_a2_s, ctx_gamma_aug) =
+        ctx.split_existential_function(a)?;
+
+      let ex_a1 = Type::Existential(ex_a1_s.clone());
+      let ctx_delta = typecheck(&ctx_gamma_aug, e, &ex_a1)?;
+
+      let ex_a2 = Type::Existential(ex_a2_s.clone());
+      Ok((ex_a2, ctx_delta))
+    }
+
+    _ => bail!("trying to appSynthesize with a non-function type"),
+  }
+}

src/bidir_debruijn.rs

@@ -0,0 +1,365 @@
+use anyhow::{bail, ensure, Result};
+
+use crate::data_debruijn::{
+  Context, ContextEntry, ContextIndex, Monotype, Term, Type, Visitor,
+};
+use crate::gensym::Symbol;
+use crate::DEPTH;
+
+// Figure 8. Applying a context, as a substitution, to a type
+
+#[trace]
+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.get_existential(a) {
+      Some(Some(m)) => Ok(m.into_poly()),
+      Some(None) => Ok(Type::Existential(a.clone())),
+      None => bail!("existential variable {a:?} doesn't exist in context"),
+    },
+
+    // TODO: Is this right?
+    // Type::Polytype(t) => {
+    //   let t = app_ctx(ctx, t)?;
+    //   Ok(Type::Polytype(Box::new(t)))
+    // }
+    Type::Polytype(t) => {
+      // Weaken the context
+      let (aug_ctx, _) =
+        ctx.add(ContextEntry::ExistentialVar(Symbol::default()))?;
+      let t = app_ctx(&aug_ctx, t)?;
+      Ok(Type::Polytype(Box::new(t)))
+    }
+
+    Type::Arrow(a, b) => Ok(Type::Arrow(
+      Box::new(app_ctx(ctx, a)?),
+      Box::new(app_ctx(ctx, b)?),
+    )),
+  }
+}
+
+// Figure 9. Algorithmic subtyping
+
+/// Under input context Γ , type A is a subtype of B, with output context ∆
+pub fn subtype(ctx: &Context, left: &Type, right: &Type) -> Result<Context> {
+  match (left, right) {
+    // <:Unit rule
+    (Type::Unit, Type::Unit) => Ok(ctx.clone()),
+
+    // <:Var rule
+    (Type::Var(x), Type::Var(y)) if x == y && ctx.get_type(x).is_some() => {
+      Ok(ctx.clone())
+    }
+
+    // <:Exvar rule
+    (Type::Existential(x), Type::Existential(y))
+      if x == y && ctx.get_existential(x).is_some() =>
+    {
+      Ok(ctx.clone())
+    }
+
+    // <:InstantiateL
+    (Type::Existential(a) , ty_a) if ctx.get_existential(a).is_some() => {
+      instantiate_left(ctx, a, ty_a)
+    }
+
+    // <:InstantiateR
+    (ty_a, Type::Existential(a)) if ctx.get_existential(a).is_some() => {
+      instantiate_right (ctx, ty_a, a)
+    }
+
+    (Type::Unit, Type::Var(_)) => todo!("wtf? {left:?} {right:?}"),
+    (Type::Unit, Type::Polytype(_)) => todo!(),
+    (Type::Unit, Type::Arrow(_, _)) => todo!(),
+    (Type::Var(_), Type::Unit) => todo!(),
+    (Type::Var(_), Type::Var(_)) => todo!(),
+    (Type::Var(_), Type::Existential(_)) => todo!(),
+    (Type::Var(_), Type::Polytype(_)) => todo!(),
+    (Type::Var(_), Type::Arrow(_, _)) => todo!(),
+    (Type::Existential(_), Type::Unit) => todo!(),
+    (Type::Existential(_), Type::Var(_)) => todo!(),
+    (Type::Existential(_), Type::Existential(_)) => todo!(),
+    (Type::Existential(_), Type::Polytype(_)) => todo!(),
+    (Type::Existential(_), Type::Arrow(_, _)) => todo!(),
+    (Type::Polytype(_), Type::Unit) => todo!(),
+    (Type::Polytype(_), Type::Var(_)) => todo!(),
+    (Type::Polytype(_), Type::Existential(_)) => todo!(),
+    (Type::Polytype(_), Type::Polytype(_)) => todo!(),
+    (Type::Polytype(_), Type::Arrow(_, _)) => todo!(),
+    (Type::Arrow(_, _), Type::Unit) => todo!(),
+    (Type::Arrow(_, _), Type::Var(_)) => todo!(),
+    (Type::Arrow(_, _), Type::Existential(_)) => todo!(),
+    (Type::Arrow(_, _), Type::Polytype(_)) => todo!(),
+    (Type::Arrow(_, _), Type::Arrow(_, _)) => todo!(),
+
+    _ => bail!("subtyping relation failed between {left:?} and {right:?} (ctx = {ctx:?})"),
+  }
+}
+
+// Figure 10. Instantiation
+
+#[trace]
+pub fn instantiate_left(
+  ctx: &Context,
+  a: &ContextIndex,
+  ty_a: &Type,
+) -> Result<Context> {
+  match ty_a {
+    // InstLReach rule
+    Type::Existential(b)
+      if ctx.get_existential(a).is_some()
+        && ctx.get_existential(b).is_some() =>
+    {
+      let mut new_ctx = ctx.clone();
+      {
+        let b_entry = new_ctx
+          .vector
+          .get_mut(b.debruijn_level)
+          .expect("should exist");
+
+        ensure!(
+          matches!(b_entry, ContextEntry::ExistentialVar(_)),
+          "not an existential variable"
+        );
+
+        *b_entry =
+          ContextEntry::ExistentialSolved(Monotype::Existential(a.to_owned()));
+      }
+
+      Ok(new_ctx)
+    }
+
+    Type::Existential(_b) => todo!(),
+    Type::Unit => todo!(),
+    Type::Var(_) => todo!(),
+    Type::Polytype(_) => todo!(),
+
+    // InstLArr rule
+    Type::Arrow(ty_a1, ty_a2) => {
+      let (aug_ctx_a2, a2_idx) =
+        ctx.add(ContextEntry::ExistentialVar(Symbol::default()))?;
+      let (aug_ctx_a1, a1_idx) =
+        ctx.add(ContextEntry::ExistentialVar(Symbol::default()))?;
+      let (aug_ctx, a_idx) =
+        ctx.add(ContextEntry::ExistentialSolved(Monotype::Arrow(
+          Box::new(Monotype::Existential(a1_idx.clone())),
+          Box::new(Monotype::Existential(a2_idx.clone())),
+        )))?;
+
+      let a1 = Type::Existential(a1_idx.clone());
+      let a2 = Type::Existential(a2_idx.clone());
+
+      let ctx_theta = instantiate_right(&aug_ctx, &ty_a1, &a1_idx)?;
+
+      let replaced_a2 = app_ctx(&ctx_theta, &ty_a2)?;
+      let ctx_delta = instantiate_left(&ctx_theta, &a2_idx, &replaced_a2)?;
+
+      Ok(ctx_delta)
+    }
+  }
+}
+
+#[trace]
+pub fn instantiate_right(
+  ctx: &Context,
+  ty_a: &Type,
+  a: &ContextIndex,
+) -> Result<Context> {
+  match ty_a {
+    // InstRSolve rule
+    ty if ty.is_mono() => {
+      let mut new_ctx = ctx.clone();
+      {
+        let a_entry = new_ctx
+          .vector
+          .get_mut(a.debruijn_level)
+          .expect("should exist");
+
+        println!("ty: {ty:?}, a_entry: {a_entry:?}");
+        ensure!(
+          matches!(a_entry, ContextEntry::ExistentialVar(_)),
+          "{a_entry:?} (@ {a:?}) is not an existential variable",
+        );
+
+        *a_entry = ContextEntry::ExistentialSolved(ty.try_into_mono().unwrap());
+      }
+      Ok(new_ctx)
+    }
+
+    Type::Unit => todo!("a={a:?}, ty_a={ty_a:?}, ctx={ctx:?}"),
+    Type::Var(_) => todo!(),
+    Type::Existential(_) => todo!(),
+    Type::Polytype(_) => todo!(),
+    Type::Arrow(_, _) => todo!(),
+  }
+}
+
+// Figure 11. Algorithmic typing
+
+#[trace]
+pub fn typecheck(ctx: &Context, term: &Term, ty: &Type) -> Result<Context> {
+  match (term, ty) {
+    // 1I rule
+    (Term::Unit, Type::Unit) => Ok(ctx.clone()),
+
+    // ∀I rule
+    (_e, Type::Polytype(_t)) => todo!(),
+
+    // →I rule
+    (Term::Lam(_e), Type::Arrow(_ty_a, _ty_b)) => {
+      todo!()
+    }
+
+    // Sub rule
+    (term, ty) => {
+      let (ty_a, ctx_theta) = synthesize(ctx, term)?;
+      let a = app_ctx(&ctx_theta, &ty_a)?;
+      let b = app_ctx(&ctx_theta, ty)?;
+      let ctx_delta = subtype(&ctx_theta, &a, &b)?;
+      Ok(ctx_delta)
+    }
+  }
+}
+
+#[trace]
+pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> {
+  match term {
+    // 1I⇒ rule
+    Term::Unit => Ok((Type::Unit, ctx.clone())),
+
+    // Var rule
+    Term::Var(index) => {
+      let ty = match ctx.get_type(index) {
+        Some(v) => v,
+        None => bail!("no TermAnnot at index {index:?} of context: {ctx:?}"),
+      };
+      Ok((ty, ctx.clone()))
+    }
+
+    // →E rule
+    Term::App(e1, e2) => {
+      let (ty_a, ctx_theta) = synthesize(ctx, e1)?;
+      let app_a = app_ctx(&ctx_theta, &ty_a)?;
+      let (ty_c, ctx_delta) = app_synthesize(&ctx_theta, &app_a, &e2)?;
+      Ok((ty_c, ctx_delta))
+    }
+
+    // →I⇒' rule
+    Term::Lam(e) => {
+      let (aug_ctx, marker_idx) = ctx.add(ContextEntry::Marker)?;
+      let (aug_ctx_at_a, ex_a_idx) =
+        aug_ctx.add(ContextEntry::ExistentialVar(Symbol::default()))?;
+      let (aug_ctx_at_b, ex_b_idx) =
+        aug_ctx_at_a.add(ContextEntry::ExistentialVar(Symbol::default()))?;
+
+      let ex_a = Type::Existential(ex_a_idx.clone());
+      let ex_b = Type::Existential(ex_b_idx.clone());
+
+      let (aug_ctx, _annot_idx) =
+        aug_ctx_at_b.add(ContextEntry::TermAnnot(ex_a.clone()))?;
+
+      struct V(usize, usize);
+      impl Visitor for V {
+        fn visit_index(&self, index: &mut ContextIndex) -> Result<()> {
+          index.debruijn_index += self.0;
+          index.debruijn_level = self.1 - 1 - index.debruijn_index;
+          Ok(())
+        }
+      }
+
+      let ex_a_2 = ex_b.transform_with_visitor(&V(2, aug_ctx.size()))?;
+      let ex_b_2 = ex_b.transform_with_visitor(&V(1, aug_ctx.size()))?;
+      let e_2 = e.transform_with_visitor(&V(0, aug_ctx.size()))?;
+
+      let wtf_ctx = typecheck(&aug_ctx, &e_2, &ex_b_2)?;
+
+      let (before_marker, after_marker) = wtf_ctx.split_at(&marker_idx);
+
+      // Bump the levels down since we're splitting teh array
+      struct V2(usize, usize);
+      impl Visitor for V2 {
+        fn visit_index(&self, index: &mut ContextIndex) -> Result<()> {
+          index.debruijn_level -= self.0;
+          index.debruijn_index = self.1 - 1 - index.debruijn_level;
+
+          Ok(())
+        }
+      }
+      let after_marker =
+        after_marker.transform_with_visitor(&V2(1, after_marker.size()))?;
+
+      // τ=[∆'](â→β)
+      let tau = Type::Arrow(Box::new(ex_a_2), Box::new(ex_b_2));
+      let tau = tau.transform_with_visitor(&V2(1, after_marker.size()))?;
+      let tau = app_ctx(&after_marker, &tau)?;
+
+      // let mut before_marker = before_marker;
+      // before_marker.vector.push_back(ContextEntry::ExistentialVar);
+
+      Ok((Type::Polytype(Box::new(tau)), before_marker))
+    }
+
+    Term::Annot(_, _) => todo!(),
+  }
+}
+
+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) => {
+      let out_ctx = typecheck(ctx, e, ty_a)?;
+      Ok((*ty_c.clone(), out_ctx))
+    }
+
+    // ∀App rule
+    (Type::Polytype(ty_a), e) => {
+      let (aug_ctx, a_idx) =
+        ctx.add(ContextEntry::ExistentialVar(Symbol::default()))?;
+      let aug_ty = ty_a.subst(&a_idx, Type::Existential(a_idx.clone()));
+      let (ty, ctx_delta) = app_synthesize(&aug_ctx, &aug_ty, e)?;
+
+      Ok((ty, ctx_delta))
+    }
+
+    // âApp rule
+    (Type::Existential(a), e) if ctx.get_existential(a).is_some() => {
+      let (aug_ctx_a2, a2_idx) =
+        ctx.add(ContextEntry::ExistentialVar(Symbol::default()))?;
+      let (aug_ctx_a1, a1_idx) =
+        ctx.add(ContextEntry::ExistentialVar(Symbol::default()))?;
+      let (aug_ctx, a_idx) =
+        ctx.add(ContextEntry::ExistentialSolved(Monotype::Arrow(
+          Box::new(Monotype::Existential(a1_idx.clone())),
+          Box::new(Monotype::Existential(a2_idx.clone())),
+        )))?;
+      // let (ex_a1_s, ex_a2_s, ctx_gamma_aug) =
+      //   ctx.split_existential_function(a)?;
+      // let ex_a1 = Type::Existential(ex_a1_s.clone());
+
+      let a1 = Type::Existential(a1_idx);
+      let a2 = Type::Existential(a2_idx);
+      let ctx_delta = typecheck(&aug_ctx, e, &a1)?;
+
+      Ok((a2, ctx_delta))
+    }
+
+    (Type::Unit, Term::Unit) => todo!(),
+    (Type::Unit, Term::Var(_)) => todo!(),
+    (Type::Unit, Term::Lam(_)) => todo!(),
+    (Type::Unit, Term::App(_, _)) => todo!(),
+    (Type::Unit, Term::Annot(_, _)) => todo!(),
+    (Type::Var(_), Term::Unit) => todo!(),
+    (Type::Var(_), Term::Var(_)) => todo!(),
+    (Type::Var(_), Term::Lam(_)) => todo!(),
+    (Type::Var(_), Term::App(_, _)) => todo!(),
+    (Type::Var(_), Term::Annot(_, _)) => todo!(),
+
+    _ => bail!("trying to appSynthesize with a non-function type"),
+  }
+}

src/data.rs

@@ -0,0 +1,322 @@
+use std::{fmt, hash::Hash};
+
+use anyhow::{bail, Result};
+use im::{HashSet, Vector};
+
+use crate::gensym::gensym_existential;
+
+#[derive(Clone)]
+pub enum Term {
+  Unit,
+  Var(String),
+  Lam(String, Box<Term>),
+  App(Box<Term>, Box<Term>),
+  Annot(Box<Term>, Type),
+}
+
+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::Lam(arg0, arg1) => write!(f, "(λ{}.{:?})", arg0, arg1),
+      Self::App(arg0, arg1) => write!(f, "({:?} · {:?})", arg0, arg1),
+      Self::Annot(arg0, arg1) => write!(f, "({:?} : {:?})", arg0, arg1),
+    }
+  }
+}
+
+#[derive(Clone)]
+pub enum Type {
+  Unit,
+  Var(String),
+  Existential(String),
+  Polytype(String, Box<Type>),
+  Arrow(Box<Type>, Box<Type>),
+}
+
+impl fmt::Debug for Type {
+  fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+    match self {
+      Self::Unit => write!(f, "𝟙"),
+      Self::Var(arg0) => write!(f, "{}", arg0),
+      Self::Existential(arg0) => write!(f, "{}", arg0),
+      Self::Polytype(arg0, arg1) => write!(f, "(∀ {} . {:?})", arg0, arg1),
+      Self::Arrow(arg0, arg1) => write!(f, "({:?} -> {:?})", arg0, arg1),
+    }
+  }
+}
+
+impl Type {
+  pub fn into_mono(&self) -> Option<Monotype> {
+    match self {
+      Type::Unit => Some(Monotype::Unit),
+      Type::Var(x) => Some(Monotype::Var(x.clone())),
+      Type::Existential(x) => Some(Monotype::Existential(x.clone())),
+      Type::Polytype(_, _) => None,
+      Type::Arrow(a, b) => Some(Monotype::Arrow(
+        Box::new(a.into_mono()?),
+        Box::new(b.into_mono()?),
+      )),
+    }
+  }
+
+  #[inline]
+  pub fn is_mono(&self) -> bool {
+    self.into_mono().is_some()
+  }
+}
+
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+pub enum FreeVar {
+  Var(String),
+  Existential(String),
+}
+
+impl Type {
+  pub fn free_vars(&self) -> HashSet<FreeVar> {
+    fn free_vars_with_context(ctx: &Context, ty: &Type) -> HashSet<FreeVar> {
+      match ty {
+        Type::Unit => HashSet::default(),
+        Type::Var(x) if ctx.lookup_type(x).is_some() => HashSet::default(),
+        Type::Var(x) => [FreeVar::Var(x.to_owned())].into_iter().collect(),
+        Type::Existential(x) if ctx.lookup_existential(x).is_some() => {
+          HashSet::default()
+        }
+        Type::Existential(x) => {
+          [FreeVar::Existential(x.to_owned())].into_iter().collect()
+        }
+        Type::Polytype(x, ty_a) => {
+          let new_ctx =
+            ctx.add(vec![ContextEntry::ExistentialVar(x.to_owned())]);
+          free_vars_with_context(&new_ctx, &ty_a)
+        }
+        Type::Arrow(ty_a, ty_b) => {
+          let a_vars = free_vars_with_context(&ctx, &ty_a);
+          let b_vars = free_vars_with_context(&ctx, &ty_b);
+          a_vars.union(b_vars)
+        }
+      }
+    }
+
+    free_vars_with_context(&Context::default(), self)
+  }
+
+  pub fn subst(&self, var: &str, replacement: &Type) -> Type {
+    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(
+        Box::new(a.subst(var, replacement)),
+        Box::new(b.subst(var, replacement)),
+      ),
+    }
+  }
+}
+
+#[derive(Clone)]
+pub enum Monotype {
+  Unit,
+  Var(String),
+  Existential(String),
+  Arrow(Box<Monotype>, Box<Monotype>),
+}
+
+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::Existential(arg0) => write!(f, "{}", arg0),
+      Self::Arrow(arg0, arg1) => write!(f, "({arg0:?} -> {arg1:?})"),
+    }
+  }
+}
+
+impl Monotype {
+  pub fn into_poly(&self) -> Type {
+    match self {
+      Monotype::Unit => Type::Unit,
+      Monotype::Var(x) => Type::Var(x.clone()),
+      Monotype::Existential(x) => Type::Existential(x.clone()),
+      Monotype::Arrow(a, b) => {
+        Type::Arrow(Box::new(a.into_poly()), Box::new(b.into_poly()))
+      }
+    }
+  }
+}
+
+#[derive(Clone)]
+pub enum ContextEntry {
+  TypeVar(String),
+  TermAnnot(String, Type),
+  ExistentialVar(String),
+  ExistentialSolved(String, Monotype),
+  Marker(String),
+}
+
+impl fmt::Debug for ContextEntry {
+  fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+    match self {
+      Self::TypeVar(arg0) => write!(f, "{}", arg0),
+      Self::TermAnnot(arg0, arg1) => write!(f, "{} : {:?}", arg0, arg1),
+      Self::ExistentialVar(arg0) => write!(f, "{}", arg0),
+      Self::ExistentialSolved(arg0, arg1) => write!(f, "{} ≔ {:?}", arg0, arg1),
+      Self::Marker(arg0) => write!(f, "▶{}", arg0),
+    }
+  }
+}
+
+#[derive(Debug, Clone)]
+pub enum CompleteContextEntry {
+  TypeVar(String),
+  TermAnnot(String, Type),
+  ExistentialSolved(String, Monotype),
+  Marker(String),
+}
+
+#[derive(Clone, Default)]
+pub struct Context(pub(crate) Vector<ContextEntry>);
+
+impl fmt::Debug for Context {
+  fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+    f.write_str("Γ")?;
+    for rule in self.0.iter() {
+      f.write_str(", ")?;
+      rule.fmt(f)?;
+    }
+    Ok(())
+  }
+}
+
+impl Context {
+  pub fn add(&self, entries: Vec<ContextEntry>) -> Context {
+    let mut new_ctx = self.clone();
+    for entry in entries {
+      new_ctx.0.push_back(entry);
+    }
+    new_ctx
+  }
+
+  /// Looks up a polytype by name, also returning an index
+  pub fn lookup_type(&self, name: impl AsRef<str>) -> Option<(usize, Type)> {
+    self
+      .0
+      .iter()
+      .enumerate()
+      .find_map(|(i, entry)| match entry {
+        ContextEntry::TermAnnot(n, t) if n == name.as_ref() => {
+          Some((i, t.clone()))
+        }
+        _ => None,
+      })
+  }
+
+  #[inline]
+  pub fn has_type(&self, name: impl AsRef<str>) -> bool {
+    self.lookup_type(name).is_some()
+  }
+
+  /// Looks up an existential variable by name
+  /// - Returns Some(Some(t)) if solved
+  /// - Returns Some(None) if exists but unsolved
+  /// - Returns None if not found
+  pub fn lookup_existential(
+    &self,
+    name: impl AsRef<str>,
+  ) -> Option<(usize, Option<Monotype>)> {
+    self
+      .0
+      .iter()
+      .enumerate()
+      .find_map(|(i, entry)| match entry {
+        ContextEntry::ExistentialVar(n) if n == name.as_ref() => {
+          Some((i, None))
+        }
+        ContextEntry::ExistentialSolved(n, t) if n == name.as_ref() => {
+          Some((i, Some(t.clone())))
+        }
+        _ => None,
+      })
+  }
+
+  #[inline]
+  pub fn has_existential(&self, name: impl AsRef<str>) -> bool {
+    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();
+
+    for entry in self.0.iter() {
+      match entry {
+        ContextEntry::ExistentialVar(n) => {
+          unsolved.insert(n.clone());
+        }
+        _ => {}
+      }
+    }
+
+    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
+  }
+
+  pub fn split_existential_function(
+    &self,
+    var: &str,
+  ) -> Result<(String, String, Context)> {
+    let mut ctx = self.clone();
+    let idx = match ctx.lookup_existential(var) {
+      Some((idx, _)) => idx,
+      None => bail!("wtf?"),
+    };
+
+    let ex_a1_s = gensym_existential();
+    let ex_a2_s = gensym_existential();
+    ctx.0[idx] = ContextEntry::ExistentialSolved(
+      var.to_owned(),
+      Monotype::Arrow(
+        Box::new(Monotype::Existential(ex_a1_s.to_owned())),
+        Box::new(Monotype::Existential(ex_a2_s.to_owned())),
+      ),
+    );
+    ctx
+      .0
+      .insert(idx, ContextEntry::ExistentialVar(ex_a1_s.to_owned()));
+    ctx
+      .0
+      .insert(idx, ContextEntry::ExistentialVar(ex_a2_s.to_owned()));
+
+    Ok((ex_a1_s, ex_a2_s, ctx))
+  }
+}

src/data_debruijn.rs

@@ -0,0 +1,591 @@
+use std::fmt::{self};
+
+use anyhow::Result;
+use im::Vector;
+
+use crate::{
+  data,
+  gensym::{gensym_type, Symbol},
+};
+
+/// A lambda calculus term.
+#[derive(Clone)]
+pub enum Term {
+  /// Unit type
+  Unit,
+
+  /// Variable, with a reference into the context.
+  /// The entry pointed to by this index MUST be a TypeVar.
+  Var(ContextIndex),
+
+  /// Lambda abstraction.
+  Lam(Box<Term>),
+
+  /// Lambda application.
+  App(Box<Term>, Box<Term>),
+
+  /// Type annotation
+  Annot(Box<Term>, Type),
+}
+
+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::Lam(arg1) => write!(f, "(λ.{:?})", arg1),
+      Self::App(arg0, arg1) => write!(f, "({:?} · {:?})", arg0, arg1),
+      Self::Annot(arg0, arg1) => write!(f, "({:?} : {:?})", arg0, arg1),
+    }
+  }
+}
+
+// impl Arbitrary for Term {
+//   fn arbitrary(g: &mut Gen) -> Self {
+//     // let var = Term::Var(ContextIndex::arbitrary(g));
+//     match g.choose(&[0, 1, 2, 3, 4]).unwrap() {
+//       0 => Term::Unit,
+//       1 => Term::Var(ContextIndex::arbitrary(g)),
+//       2 => Term::Lam(Box::new(Term::arbitrary(g))),
+//       3 => {
+//         Term::App(Box::new(Term::arbitrary(g)), Box::new(Term::arbitrary(g)))
+//       }
+//       4 => Term::Annot(Box::new(Term::arbitrary(g)), Type::Unit),
+//       _ => unreachable!(),
+//     }
+//   }
+// }
+
+impl Term {
+  pub fn transform_with_visitor<V: Visitor>(
+    &self,
+    visitor: &V,
+  ) -> Result<Term> {
+    let mut expr = self.clone();
+    visitor.visit_term_before(&mut expr)?;
+    let mut expr = match expr {
+      Term::Var(index) => {
+        let mut index = index.clone();
+        visitor.visit_index(&mut index)?;
+        Term::Var(index)
+      }
+      Term::Lam(body) => {
+        // TODO:
+        body.transform_with_visitor(visitor)?
+      }
+      Term::App(a, b) => {
+        let a = a.transform_with_visitor(visitor)?;
+        let b = b.transform_with_visitor(visitor)?;
+        Term::App(Box::new(a), Box::new(b))
+      }
+      Term::Annot(_, _) => todo!(),
+      _ => expr,
+    };
+    visitor.visit_term_after(&mut expr)?;
+    Ok(expr)
+  }
+}
+
+#[derive(Clone)]
+pub enum Type {
+  Unit,
+  Var(ContextIndex),
+  Existential(ContextIndex),
+  Polytype(Box<Type>),
+  Arrow(Box<Type>, Box<Type>),
+}
+
+impl fmt::Debug for Type {
+  fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+    match self {
+      Self::Unit => write!(f, "𝟙"),
+      Self::Var(arg0) => write!(f, "{:?}", arg0),
+      Self::Existential(arg0) => write!(f, "ex{:?}", arg0),
+      Self::Polytype(arg1) => write!(f, "(∀.{:?})", arg1),
+      Self::Arrow(arg0, arg1) => write!(f, "({:?} -> {:?})", arg0, arg1),
+    }
+  }
+}
+
+impl Type {
+  /// Attempt to turn this polytype into a monotype.
+  ///
+  /// This fails if any sub-expression of this type contains a polytype expression.
+  pub fn try_into_mono(&self) -> Option<Monotype> {
+    match self {
+      Type::Unit => Some(Monotype::Unit),
+      Type::Var(x) => Some(Monotype::Var(x.clone())),
+      Type::Existential(x) => Some(Monotype::Existential(x.clone())),
+
+      // Polytypes cannot be converted to monotypes
+      Type::Polytype(_) => None,
+
+      Type::Arrow(a, b) => Some(Monotype::Arrow(
+        Box::new(a.try_into_mono()?),
+        Box::new(b.try_into_mono()?),
+      )),
+    }
+  }
+
+  #[inline]
+  pub fn is_mono(&self) -> bool {
+    self.try_into_mono().is_some()
+  }
+
+  pub fn subst(&self, before: &ContextIndex, after: Type) -> Type {
+    match self {
+      Type::Unit => Type::Unit,
+      Type::Var(index) if index.debruijn_level == before.debruijn_level => {
+        after
+      }
+      Type::Var(index) => Type::Var(index.clone()),
+      Type::Existential(index)
+        if index.debruijn_level == before.debruijn_level =>
+      {
+        after
+      }
+      Type::Existential(index) => Type::Existential(index.clone()),
+      Type::Polytype(_) => todo!(),
+      Type::Arrow(a, b) => Type::Arrow(
+        Box::new(a.subst(before, after.clone())),
+        Box::new(b.subst(before, after.clone())),
+      ),
+    }
+  }
+
+  pub fn transform_with_visitor<V: Visitor>(
+    &self,
+    visitor: &V,
+  ) -> Result<Type> {
+    let mut ty = self.clone();
+    visitor.visit_type_before(&mut ty)?;
+    let mut ty = match ty {
+      Type::Var(_) => todo!(),
+      Type::Existential(index) => {
+        let mut index = index.clone();
+        visitor.visit_index(&mut index)?;
+        Type::Existential(index)
+      }
+      Type::Polytype(_) => todo!(),
+      Type::Arrow(a, b) => {
+        let a = a.transform_with_visitor(visitor)?;
+        let b = b.transform_with_visitor(visitor)?;
+        Type::Arrow(Box::new(a), Box::new(b))
+      }
+      _ => ty,
+    };
+    visitor.visit_type_after(&mut ty)?;
+    Ok(ty)
+  }
+}
+
+#[derive(Clone)]
+pub enum Monotype {
+  Unit,
+  Var(ContextIndex),
+  Existential(ContextIndex),
+  Arrow(Box<Monotype>, Box<Monotype>),
+}
+
+impl fmt::Debug for Monotype {
+  fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+    match self {
+      Self::Unit => write!(f, "m𝟙"),
+      Self::Var(arg0) => write!(f, "m{:?}", arg0),
+      Self::Existential(arg0) => write!(f, "m'ex{:?}", arg0),
+      Self::Arrow(arg0, arg1) => write!(f, "m({:?} -> {:?})", arg0, arg1),
+    }
+  }
+}
+
+impl Monotype {
+  pub fn into_poly(&self) -> Type {
+    match self {
+      Monotype::Unit => Type::Unit,
+      Monotype::Var(x) => Type::Var(x.clone()),
+      Monotype::Existential(x) => Type::Existential(x.clone()),
+      Monotype::Arrow(a, b) => {
+        Type::Arrow(Box::new(a.into_poly()), Box::new(b.into_poly()))
+      }
+    }
+  }
+
+  pub fn transform_with_visitor<V: Visitor>(
+    &self,
+    visitor: &V,
+  ) -> Result<Monotype> {
+    let mut ty = self.clone();
+    visitor.visit_monotype_before(&mut ty)?;
+    let mut ty = match ty {
+      Monotype::Var(_) => todo!(),
+      Monotype::Existential(index) => {
+        let mut index = index.clone();
+        visitor.visit_index(&mut index)?;
+        Monotype::Existential(index)
+      }
+      Monotype::Arrow(a, b) => {
+        let a = a.transform_with_visitor(visitor)?;
+        let b = b.transform_with_visitor(visitor)?;
+        Monotype::Arrow(Box::new(a), Box::new(b))
+      }
+      _ => ty,
+    };
+    visitor.visit_monotype_after(&mut ty)?;
+    Ok(ty)
+  }
+}
+
+#[derive(Clone)]
+pub enum ContextEntry {
+  TypeVar(Symbol),
+  TermAnnot(Type),
+  ExistentialVar(Symbol),
+  ExistentialSolved(Monotype),
+  Marker,
+}
+
+impl ContextEntry {
+  pub fn name(&self) -> String {
+    match self {
+      ContextEntry::TypeVar(name) | ContextEntry::ExistentialVar(name) => {
+        name.0.to_owned()
+      }
+      _ => String::new(),
+    }
+  }
+}
+
+impl fmt::Debug for ContextEntry {
+  fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+    match self {
+      Self::TypeVar(name) => write!(f, "Ty({name})"),
+      Self::TermAnnot(arg0) => f.debug_tuple("Annot").field(arg0).finish(),
+      Self::ExistentialVar(name) => write!(f, "ExVar({name})"),
+      Self::ExistentialSolved(arg0) => {
+        f.debug_tuple("ExSolv").field(arg0).finish()
+      }
+      Self::Marker => write!(f, "▶"),
+    }
+  }
+}
+
+#[derive(Debug, Clone)]
+pub enum CompleteContextEntry {
+  TypeVar(String),
+  TermAnnot(String, Type),
+  ExistentialSolved(String, Monotype),
+  Marker(String),
+}
+
+#[derive(Clone)]
+pub struct Context {
+  // TODO: Make this not pub(crate)
+  pub(crate) vector: Vector<ContextEntry>,
+}
+
+impl fmt::Debug for Context {
+  fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+    write!(f, "Γ{:?}", self.vector)
+  }
+}
+
+impl Default for Context {
+  fn default() -> Self {
+    let vector = Vector::default();
+
+    Context { vector }
+  }
+}
+
+impl Context {
+  #[inline]
+  pub fn size(&self) -> usize {
+    self.vector.len()
+  }
+
+  pub fn add(&self, item: ContextEntry) -> Result<(Context, ContextIndex)> {
+    let idx = self.vector.len();
+    struct V;
+    impl Visitor for V {
+      fn visit_index(&self, index: &mut ContextIndex) -> Result<()> {
+        index.debruijn_index += 1;
+        Ok(())
+      }
+    }
+    let mut new_ctx = self.transform_with_visitor(&V)?;
+    let name = item.name();
+    new_ctx.vector.push_back(item);
+
+    let idx = ContextIndex {
+      debruijn_index: 0,
+      debruijn_level: idx,
+      label: name,
+    };
+    Ok((new_ctx, idx))
+  }
+
+  pub fn get<'a>(&'a self, index: &ContextIndex) -> Option<&ContextEntry> {
+    let item = self.vector.get(index.debruijn_level)?;
+    Some(item)
+  }
+
+  pub fn get_existential(
+    &self,
+    index: &ContextIndex,
+  ) -> Option<Option<Monotype>> {
+    let item = self.get(index)?;
+
+    match item {
+      ContextEntry::ExistentialSolved(t) => Some(Some(t.clone())),
+      ContextEntry::ExistentialVar(_) => Some(None),
+      _ => None,
+    }
+  }
+
+  pub fn get_type(&self, index: &ContextIndex) -> Option<Type> {
+    let item = self.get(index)?;
+
+    match item {
+      ContextEntry::TermAnnot(t) => Some(t.clone()),
+      _ => None,
+    }
+  }
+
+  pub fn unsolved_existentials(&self) -> Vec<ContextIndex> {
+    let mut unsolved = Vec::new();
+    for (idx, item) in self.vector.iter().enumerate() {
+      match item {
+        ContextEntry::ExistentialVar(_) => {
+          let index = ContextIndex {
+            debruijn_level: idx,
+            debruijn_index: self.vector.len() - idx,
+            label: item.name(),
+          };
+          unsolved.push(index)
+        }
+        _ => {}
+      }
+    }
+    unsolved
+  }
+
+  /// Splits the context
+  pub fn split_at(&self, index: &ContextIndex) -> (Context, Context) {
+    let (before, mut after) =
+      self.vector.clone().split_at(index.debruijn_level);
+    after.pop_front();
+
+    (Context { vector: before }, Context { vector: after })
+  }
+
+  pub fn is_valid(&self) -> bool {
+    for item in self.vector.iter() {
+      match item {
+        ContextEntry::TermAnnot(_) => todo!(),
+        ContextEntry::ExistentialSolved(_) => todo!(),
+        _ => {}
+      }
+    }
+    true
+  }
+
+  pub fn ensure_validity(&self) -> bool {
+    fn ensure_item_validity(ctx: &Context, item: &ContextEntry) -> bool {
+      match item {
+        ContextEntry::TermAnnot(ty) => ensure_type_validity(ctx, ty),
+        ContextEntry::ExistentialSolved(ty) => {
+          ensure_monotype_validity(ctx, ty)
+        }
+        _ => true,
+      }
+    }
+
+    fn ensure_type_validity(ctx: &Context, ty: &Type) -> bool {
+      match ty {
+        Type::Var(idx) => ensure_index_validity(ctx, idx),
+        Type::Existential(idx) => ensure_index_validity(ctx, idx),
+        Type::Polytype(ty) => ensure_type_validity(ctx, ty),
+        Type::Arrow(ty1, ty2) => {
+          ensure_type_validity(ctx, ty1) && ensure_type_validity(ctx, ty2)
+        }
+        _ => true,
+      }
+    }
+
+    fn ensure_monotype_validity(ctx: &Context, ty: &Monotype) -> bool {
+      match ty {
+        Monotype::Var(idx) => ensure_index_validity(ctx, idx),
+        Monotype::Existential(idx) => ensure_index_validity(ctx, idx),
+        Monotype::Arrow(ty1, ty2) => {
+          ensure_monotype_validity(ctx, ty1)
+            && ensure_monotype_validity(ctx, ty2)
+        }
+        _ => true,
+      }
+    }
+
+    fn ensure_index_validity(ctx: &Context, idx: &ContextIndex) -> bool {
+      idx.debruijn_index + idx.debruijn_level == ctx.vector.len()
+    }
+
+    self
+      .vector
+      .iter()
+      .all(|item| ensure_item_validity(self, item))
+  }
+
+  pub fn transform_with_visitor<V: Visitor>(
+    &self,
+    visitor: &V,
+  ) -> Result<Context> {
+    Ok(Context {
+      vector: self
+        .vector
+        .iter()
+        .map(|entry| {
+          let mut entry = entry.clone();
+          visitor.visit_context_entry_before(&mut entry)?;
+          let mut entry = match entry {
+            ContextEntry::TermAnnot(ty) => {
+              ContextEntry::TermAnnot(ty.transform_with_visitor(visitor)?)
+            }
+            ContextEntry::ExistentialSolved(ty) => {
+              ContextEntry::ExistentialSolved(
+                ty.transform_with_visitor(visitor)?,
+              )
+            }
+            _ => entry,
+          };
+          visitor.visit_context_entry_after(&mut entry)?;
+          Ok(entry)
+        })
+        .collect::<Result<_>>()?,
+    })
+  }
+}
+
+/// An index into the context.
+#[derive(Clone, PartialEq, Eq)]
+pub struct ContextIndex {
+  pub(crate) debruijn_index: usize,
+  pub(crate) debruijn_level: usize,
+  pub(crate) label: String,
+}
+
+impl fmt::Debug for ContextIndex {
+  fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+    write!(
+      f,
+      "{}#{}/{}",
+      self.label, self.debruijn_level, self.debruijn_index
+    )
+  }
+}
+
+// impl Arbitrary for ContextIndex {
+//   fn arbitrary(g: &mut Gen) -> Self {
+//     ContextIndex {
+//       debruijn_index: usize::arbitrary(g),
+//       debruijn_level: usize::arbitrary(g),
+//     }
+//   }
+// }
+
+/* Convert                                                                    */
+
+pub fn convert_term(term: &data::Term) -> Term {
+  fn convert_term_with_context(
+    ctx: &data::Context,
+    ctx2: &Context,
+    term: &data::Term,
+  ) -> Term {
+    match term {
+      data::Term::Unit => Term::Unit,
+
+      data::Term::Var(name) => {
+        println!("Looking up name {name}");
+        let (idx, _) = ctx.lookup_type(name).unwrap();
+
+        let index = ContextIndex {
+          debruijn_index: 0,
+          debruijn_level: idx,
+          label: name.to_owned(),
+        };
+        Term::Var(index)
+      }
+
+      data::Term::Lam(arg, body) => {
+        let ty = gensym_type();
+        let aug_ctx = ctx.add(vec![data::ContextEntry::TermAnnot(
+          arg.to_owned(),
+          data::Type::Var(ty.clone()),
+        )]);
+        let body = convert_term_with_context(&aug_ctx, ctx2, body);
+        Term::Lam(Box::new(body))
+      }
+
+      data::Term::App(func, arg) => {
+        let func = convert_term_with_context(ctx, ctx2, &func);
+        let arg = convert_term_with_context(ctx, ctx2, &arg);
+        Term::App(Box::new(func), Box::new(arg))
+      }
+
+      data::Term::Annot(term, ty) => {
+        let term = convert_term_with_context(ctx, ctx2, &term);
+        let ty = convert_ty_with_context(ctx, ctx2, &ty);
+        Term::Annot(Box::new(term), ty)
+      }
+    }
+  }
+
+  fn convert_ty_with_context(
+    _ctx: &data::Context,
+    _ctx2: &Context,
+    ty: &data::Type,
+  ) -> Type {
+    match ty {
+      data::Type::Unit => Type::Unit,
+
+      data::Type::Var(_) => todo!(),
+      data::Type::Existential(_) => todo!(),
+      data::Type::Polytype(_, _) => todo!(),
+      data::Type::Arrow(_, _) => todo!(),
+    }
+  }
+
+  convert_term_with_context(
+    &data::Context::default(),
+    &Context::default(),
+    term,
+  )
+}
+
+pub trait Visitor {
+  fn visit_context_entry_before(&self, expr: &mut ContextEntry) -> Result<()> {
+    Ok(())
+  }
+  fn visit_context_entry_after(&self, expr: &mut ContextEntry) -> Result<()> {
+    Ok(())
+  }
+  fn visit_type_before(&self, expr: &mut Type) -> Result<()> {
+    Ok(())
+  }
+  fn visit_type_after(&self, expr: &mut Type) -> Result<()> {
+    Ok(())
+  }
+  fn visit_monotype_before(&self, expr: &mut Monotype) -> Result<()> {
+    Ok(())
+  }
+  fn visit_monotype_after(&self, expr: &mut Monotype) -> Result<()> {
+    Ok(())
+  }
+  fn visit_term_before(&self, expr: &mut Term) -> Result<()> {
+    Ok(())
+  }
+  fn visit_term_after(&self, expr: &mut Term) -> Result<()> {
+    Ok(())
+  }
+  fn visit_index(&self, index: &mut ContextIndex) -> Result<()> {
+    Ok(())
+  }
+}

src/gensym.rs

@@ -0,0 +1,58 @@
+use core::fmt;
+use std::fmt::Formatter;
+
+use dashmap::DashMap;
+
+thread_local! {
+  static CTRMAP: DashMap<&'static str, usize> = DashMap::new();
+}
+
+const EXISTENTIALS: [&'static str; 24] = [
+  "α", "β", "γ", "δ", "ε", "ζ", "η", "θ", "ι", "κ", "λ", "μ", "ν", "ξ", "ο",
+  "π", "ρ", "σ", "τ", "υ", "φ", "χ", "ψ", "ω",
+];
+
+const TYPEVARS: [&'static str; 26] = [
+  "A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M", "N", "O",
+  "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z",
+];
+
+#[derive(Debug, Clone)]
+pub struct Symbol(pub(crate) String);
+
+impl Default for Symbol {
+  fn default() -> Self {
+    let i = idx("wtf");
+    Self(format!("var{}", i))
+  }
+}
+
+impl fmt::Display for Symbol {
+  fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
+    self.0.fmt(f)
+  }
+}
+
+pub fn gensym() -> String {
+  let i = idx("wtf");
+  format!("var{}", i)
+}
+
+pub fn gensym_existential() -> String {
+  let result = idx("existential");
+  format!("{}\u{0302}", EXISTENTIALS[result])
+}
+
+pub fn gensym_type() -> String {
+  let result = idx("existential");
+  format!("{}\u{0302}", TYPEVARS[result])
+}
+
+fn idx(ty: &'static str) -> usize {
+  CTRMAP.with(|ctrmap| {
+    let mut g = ctrmap.entry(ty).or_insert(0);
+    let ctr = *g;
+    *g += 1;
+    ctr
+  })
+}

src/lib.rs

@@ -0,0 +1,32 @@
+#[macro_use]
+extern crate quickcheck;
+#[macro_use]
+extern crate quickcheck_macros;
+#[macro_use]
+extern crate contracts;
+#[macro_use]
+extern crate derivative;
+#[macro_use]
+extern crate tracing;
+#[macro_use]
+extern crate trace;
+
+use lalrpop_util::lalrpop_mod;
+
+// #[macro_export]
+// pub mod fmt;
+
+pub mod abstract_data;
+pub mod bidir;
+pub mod data;
+
+pub mod bidir_debruijn;
+pub mod data_debruijn;
+
+mod gensym;
+#[cfg(test)]
+mod tests;
+
+lalrpop_mod!(pub parser);
+
+trace::init_depth_var!();

src/main.rs

@@ -0,0 +1,60 @@
+use anyhow::Result;
+use bidir::{
+  bidir_debruijn::{app_ctx, synthesize},
+  data_debruijn::convert_term,
+  data_debruijn::Context,
+  parser::TermParser,
+};
+use rustyline::{Config, DefaultEditor};
+
+fn main() -> Result<()> {
+  let term_parser = TermParser::new();
+
+  let rl_config = Config::builder().auto_add_history(true).build();
+  let mut rl = DefaultEditor::with_config(rl_config)?;
+
+  loop {
+    let line = match rl.readline(">> ") {
+      Ok(line) => line,
+      Err(_) => break,
+    };
+
+    // let line = r"\x.\y.x";
+
+    let parsed_term = match term_parser.parse(&line) {
+      Ok(term) => term,
+      Err(err) => {
+        eprintln!("parser error: {err}");
+        continue;
+      }
+    };
+    println!("parsed: {:?}", parsed_term);
+
+    let converted_term = convert_term(&parsed_term);
+    println!("converted: {converted_term:?}");
+
+    let ctx = Context::default();
+    let (ty, out_ctx) = match synthesize(&ctx, &converted_term) {
+      Ok(v) => v,
+      Err(err) => {
+        eprintln!("typecheck error: {err}");
+        eprintln!("{}", err.backtrace());
+        continue;
+      }
+    };
+
+    let ty = match app_ctx(&out_ctx, &ty) {
+      Ok(v) => v,
+      Err(err) => {
+        eprintln!("substitution error: {err}");
+        eprintln!("{}", err.backtrace());
+        continue;
+      }
+    };
+
+    println!("synthesized: {:?}", ty);
+    // break;
+  }
+
+  Ok(())
+}

src/parser.lalrpop

@@ -0,0 +1,49 @@
+grammar;
+
+use crate::data::*;
+
+pub Term: Term = {
+  #[precedence(level = "1")]
+  "()" => Term::Unit,
+  "(" <term:TermReset> ")" => term,
+  Ident => Term::Var(<>),
+
+  #[precedence(level = "2")]
+  "λ" <name:Ident> "." <term:Term> => Term::Lam(name, Box::new(term)),
+  "\\" <name:Ident> "." <term:Term> => Term::Lam(name, Box::new(term)),
+
+  #[precedence(level = "4")]
+  <term:Term> ":" <ty:Type> => Term::Annot(Box::new(term), ty),
+
+  #[precedence(level = "5")]
+  #[assoc(side = "left")]
+  <func:Term> <arg:Term> => Term::App(Box::new(func), Box::new(arg)),
+}
+
+// https://github.com/lalrpop/lalrpop/issues/596
+TermReset: Term = <Term>;
+
+pub Type: Type = {
+  #[precedence(level = "0")]
+  "()" => Type::Unit,
+  "(" <ty:TypeReset> ")" => ty,
+
+  Ident => Type::Var(<>),
+  ExistIdent => Type::Existential(<>),
+  "forall" <name:Ident> "." <ty:Type> => Type::Polytype(name, Box::new(ty)),
+
+  #[precedence(level = "5")]
+  #[assoc(side = "right")]
+  <a:Type> "->" <b:Type> => Type::Arrow(Box::new(a), Box::new(b)),
+};
+
+// https://github.com/lalrpop/lalrpop/issues/596
+TypeReset: Type = <Type>;
+
+ExistIdent: String = {
+  r"\^[A-Za-z_]+" => <>.to_string(),
+}
+
+pub Ident: String = {
+  r"[A-Za-z_]+" => <>.to_string(),
+}

src/tests.rs

@@ -0,0 +1,60 @@
+use anyhow::{bail, Result};
+
+use crate::{
+  bidir_debruijn::{app_ctx, synthesize},
+  data_debruijn::Context,
+  data_debruijn::{convert_term, Term},
+  parser::TermParser,
+};
+
+fn term_of(str: &'static str) -> Result<Term> {
+  let term_parser = TermParser::new();
+  let term = term_parser.parse(str)?;
+  let converted = convert_term(&term);
+  Ok(converted)
+}
+
+#[test]
+fn test_id_only() -> Result<()> {
+  let id = term_of(r"\x.x")?;
+  let ctx = Context::default();
+  let (ty, out_ctx) = synthesize(&ctx, &id)?;
+  bail!("[test] Synthesized: {:?} (context = {:?})", ty, out_ctx);
+  Ok(())
+}
+
+#[test]
+fn test_id_of_unit() -> Result<()> {
+  let id_of_unit = term_of(r"(\x.x) ()")?;
+  let ctx = Context::default();
+
+  let (ty, out_ctx) = synthesize(&ctx, &id_of_unit)?;
+  // let wtf = app_ctx(&out_ctx, &ty);
+  // println!("WTF: {wtf:?}");
+  bail!("[test] Synthesized: {:?} (context = {:?})", ty, out_ctx);
+  Ok(())
+}
+
+#[test]
+fn test_add() -> Result<()> {
+  let add = term_of(r"\m.\n.\f.\x. (m f (n f x))")?;
+  let ctx = Context::default();
+
+  let (ty, out_ctx) = match synthesize(&ctx, &add) {
+    Ok(v) => v,
+    Err(err) => {
+      error!("WTF? {err}");
+      error!("{}", err.backtrace());
+      return Err(err);
+    }
+  };
+  bail!("[test] Synthesized: {:?} (context = {:?})", ty, out_ctx);
+  Ok(())
+}
+
+// #[quickcheck]
+// fn quickly_check(term: Term) -> Result<()> {
+//   let ctx = Context::default();
+//   synthesize(&ctx, &term)?;
+//   Ok(())
+// }