diff --git a/.gitignore b/.gitignore
index ec464113b6..87b0876181 100644
--- a/.gitignore
+++ b/.gitignore
@@ -56,3 +56,6 @@ setup.log
 
 # Backup of opam lock file
 hazel.opam.locked.old
+
+# Code coverage
+_coverage/
diff --git a/Makefile b/Makefile
index c1f5943d07..5eef59a1d4 100644
--- a/Makefile
+++ b/Makefile
@@ -25,7 +25,7 @@ setup-student:
 
 dev-helper:
 	dune fmt --auto-promote || true
-	dune build @src/fmt --auto-promote src --profile dev
+	dune build @ocaml-index @src/fmt --auto-promote src --profile dev
 
 dev: setup-instructor dev-helper
 
@@ -35,7 +35,7 @@ fmt:
 	dune fmt --auto-promote
 
 watch: setup-instructor
-	dune build @src/fmt --auto-promote src --profile dev --watch
+	dune build @ocaml-index @src/fmt --auto-promote src --profile dev --watch
 
 watch-release: setup-instructor
 	dune build @src/fmt --auto-promote src --profile release --watch
@@ -60,11 +60,19 @@ repl:
 
 test:
 	dune fmt --auto-promote || true
-	dune build @src/fmt @test/fmt --auto-promote src test --profile dev
+	dune build @ocaml-index @src/fmt @test/fmt --auto-promote src test --profile dev
 	node $(TEST_DIR)/haz3ltest.bc.js
 
 watch-test:
-	dune build @fmt @runtest --auto-promote --watch
+	dune build @ocaml-index @fmt @runtest --auto-promote --watch
+
+coverage:
+	dune build @src/fmt @test/fmt --auto-promote src test --profile dev
+	dune runtest --instrument-with bisect_ppx --force
+	bisect-ppx-report summary
+
+generate-coverage-html:
+	bisect-ppx-report html
 
 clean:
 	dune clean
diff --git a/README.md b/README.md
index a15bdd424e..15caf27308 100644
--- a/README.md
+++ b/README.md
@@ -197,6 +197,9 @@ You can run all of the unit tests located in `test` by running `make test`.
 
 Unit tests are written using the [Alcotest framework](https://github.com/mirage/alcotest).
 
+#### Coverage
+Code coverage is provided by [bisect_ppx](https://github.com/aantron/bisect_ppx). To collect coverage statistics from tests run `make coverage`. After coverage statistics are generated, running `make generate-coverage-html` will generate a local webpage at `_coverage/index.html` that can be viewed to see line coverage per module.
+
 ### Continuous Integration
 
 When you push your branch to the main `hazelgrove/hazel` repository, we 
diff --git a/dune-project b/dune-project
index 1194593485..4dd3442bc4 100644
--- a/dune-project
+++ b/dune-project
@@ -26,9 +26,11 @@
   (menhir
    (>= 2.0))
   yojson
-  reason
+  (reason (>= 3.12.0))
   ppx_yojson_conv_lib
   ppx_yojson_conv
+  incr_dom
+  bisect_ppx
   (omd (>= 2.0.0~alpha4))
   ezjs_idb
   bonsai
diff --git a/hazel.opam b/hazel.opam
index e78b188325..09ee887ab3 100644
--- a/hazel.opam
+++ b/hazel.opam
@@ -11,9 +11,10 @@ depends: [
   "ocaml" {>= "5.2.0"}
   "menhir" {>= "2.0"}
   "yojson"
-  "reason"
+  "reason" {>= "3.12.0"}
   "ppx_yojson_conv_lib"
   "ppx_yojson_conv"
+  "bisect_ppx"
   "omd" {>= "2.0.0~alpha4"}
   "ezjs_idb"
   "bonsai"
diff --git a/hazel.opam.locked b/hazel.opam.locked
index b2cfce2cea..856b83ad33 100644
--- a/hazel.opam.locked
+++ b/hazel.opam.locked
@@ -39,6 +39,7 @@ depends: [
   "bigstringaf" {= "0.10.0"}
   "bin_prot" {= "v0.16.0"}
   "bonsai" {= "v0.16.0"}
+  "bisect_ppx" {= "2.8.3"}
   "camlp-streams" {= "5.0.1"}
   "chrome-trace" {= "3.16.0"}
   "cmdliner" {= "1.3.0"}
diff --git a/src/haz3lcore/dune b/src/haz3lcore/dune
index 77e2ca3fe1..a0d9770816 100644
--- a/src/haz3lcore/dune
+++ b/src/haz3lcore/dune
@@ -4,6 +4,8 @@
  (name haz3lcore)
  (libraries util sexplib unionFind uuidm virtual_dom yojson core)
  (js_of_ocaml)
+ (instrumentation
+  (backend bisect_ppx))
  (preprocess
   (pps
    ppx_yojson_conv
diff --git a/src/haz3lcore/dynamics/Builtins.re b/src/haz3lcore/dynamics/Builtins.re
index 4479989fd5..c47617edc6 100644
--- a/src/haz3lcore/dynamics/Builtins.re
+++ b/src/haz3lcore/dynamics/Builtins.re
@@ -41,13 +41,13 @@ let fn =
 module Pervasives = {
   module Impls = {
     /* constants */
-    let infinity = DHExp.Float(Float.infinity) |> fresh;
-    let neg_infinity = DHExp.Float(Float.neg_infinity) |> fresh;
-    let nan = DHExp.Float(Float.nan) |> fresh;
-    let epsilon_float = DHExp.Float(epsilon_float) |> fresh;
-    let pi = DHExp.Float(Float.pi) |> fresh;
-    let max_int = DHExp.Int(Int.max_int) |> fresh;
-    let min_int = DHExp.Int(Int.min_int) |> fresh;
+    let infinity = Float(Float.infinity) |> fresh;
+    let neg_infinity = Float(Float.neg_infinity) |> fresh;
+    let nan = Float(Float.nan) |> fresh;
+    let epsilon_float = Float(epsilon_float) |> fresh;
+    let pi = Float(Float.pi) |> fresh;
+    let max_int = Int(Int.max_int) |> fresh;
+    let min_int = Int(Int.min_int) |> fresh;
 
     let unary = (f: DHExp.t => result, d: DHExp.t) => {
       switch (f(d)) {
@@ -180,8 +180,8 @@ module Pervasives = {
           switch (convert(s)) {
           | Some(n) => Ok(wrap(n))
           | None =>
-            let d' = DHExp.BuiltinFun(name) |> DHExp.fresh;
-            let d' = DHExp.Ap(Forward, d', d) |> DHExp.fresh;
+            let d' = BuiltinFun(name) |> DHExp.fresh;
+            let d' = Ap(Forward, d', d) |> DHExp.fresh;
             let d' = DynamicErrorHole(d', InvalidOfString) |> DHExp.fresh;
             Ok(d');
           }
@@ -204,8 +204,7 @@ module Pervasives = {
             Ok(
               fresh(
                 DynamicErrorHole(
-                  DHExp.Ap(Forward, DHExp.BuiltinFun(name) |> fresh, d1)
-                  |> fresh,
+                  Ap(Forward, BuiltinFun(name) |> fresh, d1) |> fresh,
                   DivideByZero,
                 ),
               ),
diff --git a/src/haz3lcore/dynamics/Casts.re b/src/haz3lcore/dynamics/Casts.re
index 170d057e76..a69f560dd5 100644
--- a/src/haz3lcore/dynamics/Casts.re
+++ b/src/haz3lcore/dynamics/Casts.re
@@ -39,7 +39,7 @@ let grounded_Forall =
   );
 let grounded_Prod = length =>
   NotGroundOrHole(
-    Prod(ListUtil.replicate(length, Typ.Unknown(Internal) |> Typ.temp))
+    Prod(ListUtil.replicate(length, Unknown(Internal) |> Typ.temp))
     |> Typ.temp,
   );
 let grounded_Sum: unit => Typ.sum_map =
@@ -50,7 +50,7 @@ let grounded_List =
 let rec ground_cases_of = (ty: Typ.t): ground_cases => {
   let is_hole: Typ.t => bool =
     fun
-    | {term: Typ.Unknown(_), _} => true
+    | {term: Unknown(_), _} => true
     | _ => false;
   switch (Typ.term_of(ty)) {
   | Unknown(_) => Hole
@@ -67,7 +67,7 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => {
   | Prod(tys) =>
     if (List.for_all(
           fun
-          | ({term: Typ.Unknown(_), _}: Typ.t) => true
+          | ({term: Unknown(_), _}: Typ.t) => true
           | _ => false,
           tys,
         )) {
@@ -132,12 +132,12 @@ let rec transition = (~recursive=false, d: DHExp.t): option(DHExp.t) => {
         | Some(d1) => d1
         | None => inner_cast
         };
-      Some(DHExp.Cast(inner_cast, t2_grounded, t2) |> DHExp.fresh);
+      Some(Cast(inner_cast, t2_grounded, t2) |> DHExp.fresh);
 
     | (NotGroundOrHole(t1_grounded), Hole) =>
       /* ITGround rule */
       Some(
-        DHExp.Cast(Cast(d1, t1, t1_grounded) |> DHExp.fresh, t1_grounded, t2)
+        Cast(Cast(d1, t1, t1_grounded) |> DHExp.fresh, t1_grounded, t2)
         |> DHExp.fresh,
       )
 
@@ -187,7 +187,7 @@ let pattern_fixup = (p: DHPat.t): DHPat.t => {
       let (p1, d1) = unwrap_casts(p1);
       (
         p1,
-        {term: DHExp.Cast(d1, t1, t2), copied: p.copied, ids: p.ids}
+        {term: Cast(d1, t1, t2), copied: p.copied, ids: p.ids}
         |> transition_multiple,
       );
     | _ => (p, hole)
@@ -198,13 +198,13 @@ let pattern_fixup = (p: DHPat.t): DHPat.t => {
     | EmptyHole => p
     | Cast(d1, t1, t2) =>
       let p1 = rewrap_casts((p, d1));
-      {term: DHPat.Cast(p1, t1, t2), copied: d.copied, ids: d.ids};
+      {term: Cast(p1, t1, t2), copied: d.copied, ids: d.ids};
     | FailedCast(d1, t1, t2) =>
       let p1 = rewrap_casts((p, d1));
       {
         term:
-          DHPat.Cast(
-            DHPat.Cast(p1, t1, Typ.fresh(Unknown(Internal))) |> DHPat.fresh,
+          Cast(
+            Cast(p1, t1, Typ.fresh(Unknown(Internal))) |> DHPat.fresh,
             Typ.fresh(Unknown(Internal)),
             t2,
           ),
diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
index c1f3aa12d7..27ec1ef5b3 100644
--- a/src/haz3lcore/dynamics/Elaborator.re
+++ b/src/haz3lcore/dynamics/Elaborator.re
@@ -23,10 +23,10 @@ let fresh_cast = (d: DHExp.t, t1: Typ.t, t2: Typ.t): DHExp.t => {
     ? d
     : {
       let d' =
-        DHExp.Cast(d, t1, Typ.temp(Unknown(Internal)))
+        Cast(d, t1, Typ.temp(Unknown(Internal)))
         |> DHExp.fresh
         |> Casts.transition_multiple;
-      DHExp.Cast(d', Typ.temp(Unknown(Internal)), t2)
+      Cast(d', Typ.temp(Unknown(Internal)), t2)
       |> DHExp.fresh
       |> Casts.transition_multiple;
     };
@@ -63,11 +63,11 @@ let elaborated_type = (m: Statics.Map.t, uexp: UExp.t): (Typ.t, Ctx.t, 'a) => {
     | Syn => self_ty
     | SynFun =>
       let (ty1, ty2) = Typ.matched_arrow(ctx, self_ty);
-      Typ.Arrow(ty1, ty2) |> Typ.temp;
+      Arrow(ty1, ty2) |> Typ.temp;
     | SynTypFun =>
       let (tpat, ty) = Typ.matched_forall(ctx, self_ty);
       let tpat = Option.value(tpat, ~default=TPat.fresh(EmptyHole));
-      Typ.Forall(tpat, ty) |> Typ.temp;
+      Forall(tpat, ty) |> Typ.temp;
     // We need to remove the synswitches from this type.
     | Ana(ana_ty) => Typ.match_synswitch(ana_ty, self_ty)
     };
@@ -90,11 +90,11 @@ let elaborated_pat_type = (m: Statics.Map.t, upat: UPat.t): (Typ.t, Ctx.t) => {
     | Syn => self_ty
     | SynFun =>
       let (ty1, ty2) = Typ.matched_arrow(ctx, self_ty);
-      Typ.Arrow(ty1, ty2) |> Typ.temp;
+      Arrow(ty1, ty2) |> Typ.temp;
     | SynTypFun =>
       let (tpat, ty) = Typ.matched_forall(ctx, self_ty);
       let tpat = Option.value(tpat, ~default=TPat.fresh(EmptyHole));
-      Typ.Forall(tpat, ty) |> Typ.temp;
+      Forall(tpat, ty) |> Typ.temp;
     | Ana(ana_ty) =>
       switch (prev_synswitch) {
       | None => ana_ty
@@ -125,9 +125,7 @@ let rec elaborate_pattern =
       |> List.map2((p, t) => fresh_pat_cast(p, t, inner_type), _, tys)
       |> (
         ps' =>
-          DHPat.ListLit(ps')
-          |> rewrap
-          |> cast_from(List(inner_type) |> Typ.temp)
+          ListLit(ps') |> rewrap |> cast_from(List(inner_type) |> Typ.temp)
       );
     | Cons(p1, p2) =>
       let (p1', ty1) = elaborate_pattern(m, p1);
@@ -138,19 +136,17 @@ let rec elaborate_pattern =
         |> Option.value(~default=Typ.temp(Unknown(Internal)));
       let p1'' = fresh_pat_cast(p1', ty1, ty_inner);
       let p2'' = fresh_pat_cast(p2', ty2, List(ty_inner) |> Typ.temp);
-      DHPat.Cons(p1'', p2'')
-      |> rewrap
-      |> cast_from(List(ty_inner) |> Typ.temp);
+      Cons(p1'', p2'') |> rewrap |> cast_from(List(ty_inner) |> Typ.temp);
     | Tuple(ps) =>
       let (ps', tys) = List.map(elaborate_pattern(m), ps) |> ListUtil.unzip;
-      DHPat.Tuple(ps') |> rewrap |> cast_from(Typ.Prod(tys) |> Typ.temp);
+      Tuple(ps') |> rewrap |> cast_from(Prod(tys) |> Typ.temp);
     | Ap(p1, p2) =>
       let (p1', ty1) = elaborate_pattern(m, p1);
       let (p2', ty2) = elaborate_pattern(m, p2);
       let (ty1l, ty1r) = Typ.matched_arrow(ctx, ty1);
       let p1'' = fresh_pat_cast(p1', ty1, Arrow(ty1l, ty1r) |> Typ.temp);
       let p2'' = fresh_pat_cast(p2', ty2, ty1l);
-      DHPat.Ap(p1'', p2'') |> rewrap |> cast_from(ty1r);
+      Ap(p1'', p2'') |> rewrap |> cast_from(ty1r);
     | Invalid(_)
     | EmptyHole
     | MultiHole(_)
@@ -213,7 +209,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
     switch (term) {
     | Invalid(_)
     | Undefined
-    | EmptyHole => uexp |> cast_from(Typ.temp(Typ.Unknown(Internal)))
+    | EmptyHole => uexp |> cast_from(Typ.temp(Unknown(Internal)))
     | MultiHole(stuff) =>
       Any.map_term(
         ~f_exp=(_, exp) => {elaborate(m, exp) |> fst},
@@ -223,9 +219,9 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
       |> List.map(_, stuff)
       |> (
         stuff =>
-          DHExp.MultiHole(stuff)
+          MultiHole(stuff)
           |> rewrap
-          |> cast_from(Typ.temp(Typ.Unknown(Internal)))
+          |> cast_from(Typ.temp(Unknown(Internal)))
       )
     | DynamicErrorHole(e, err) =>
       let (e', _) = elaborate(m, e);
@@ -245,10 +241,10 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
     | ListLit(es) =>
       let (ds, tys) = List.map(elaborate(m), es) |> ListUtil.unzip;
       let inner_type =
-        Typ.join_all(~empty=Typ.Unknown(Internal) |> Typ.temp, ctx, tys)
-        |> Option.value(~default=Typ.temp(Typ.Unknown(Internal)));
+        Typ.join_all(~empty=Unknown(Internal) |> Typ.temp, ctx, tys)
+        |> Option.value(~default=Typ.temp(Unknown(Internal)));
       let ds' = List.map2((d, t) => fresh_cast(d, t, inner_type), ds, tys);
-      Exp.ListLit(ds') |> rewrap |> cast_from(List(inner_type) |> Typ.temp);
+      ListLit(ds') |> rewrap |> cast_from(List(inner_type) |> Typ.temp);
     | Constructor(c, _) =>
       let mode =
         switch (Id.Map.find_opt(Exp.rep_id(uexp), m)) {
@@ -266,23 +262,23 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
     | Fun(p, e, env, n) =>
       let (p', typ) = elaborate_pattern(m, p);
       let (e', tye) = elaborate(m, e);
-      Exp.Fun(p', e', env, n)
+      Fun(p', e', env, n)
       |> rewrap
       |> cast_from(Arrow(typ, tye) |> Typ.temp);
     | TypFun(tpat, e, name) =>
       let (e', tye) = elaborate(m, e);
-      Exp.TypFun(tpat, e', name)
+      TypFun(tpat, e', name)
       |> rewrap
-      |> cast_from(Typ.Forall(tpat, tye) |> Typ.temp);
+      |> cast_from(Forall(tpat, tye) |> Typ.temp);
     | Tuple(es) =>
       let (ds, tys) = List.map(elaborate(m), es) |> ListUtil.unzip;
-      Exp.Tuple(ds) |> rewrap |> cast_from(Prod(tys) |> Typ.temp);
+      Tuple(ds) |> rewrap |> cast_from(Prod(tys) |> Typ.temp);
     | Var(v) =>
       uexp
       |> cast_from(
            Ctx.lookup_var(ctx, v)
            |> Option.map((x: Ctx.var_entry) => x.typ |> Typ.normalize(ctx))
-           |> Option.value(~default=Typ.temp(Typ.Unknown(Internal))),
+           |> Option.value(~default=Typ.temp(Unknown(Internal))),
          )
     | Let(p, def, body) =>
       let add_name: (option(string), DHExp.t) => DHExp.t = (
@@ -305,9 +301,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
         let def = add_name(Pat.get_var(p), def);
         let (def, ty2) = elaborate(m, def);
         let (body, ty) = elaborate(m, body);
-        Exp.Let(p, fresh_cast(def, ty2, ty1), body)
-        |> rewrap
-        |> cast_from(ty);
+        Let(p, fresh_cast(def, ty2, ty1), body) |> rewrap |> cast_from(ty);
       } else {
         // TODO: Add names to mutually recursive functions
         // TODO: Don't add fixpoint if there already is one
@@ -315,14 +309,12 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
         let (def, ty2) = elaborate(m, def);
         let (body, ty) = elaborate(m, body);
         let fixf = FixF(p, fresh_cast(def, ty2, ty1), None) |> DHExp.fresh;
-        Exp.Let(p, fixf, body) |> rewrap |> cast_from(ty);
+        Let(p, fixf, body) |> rewrap |> cast_from(ty);
       };
     | FixF(p, e, env) =>
       let (p', typ) = elaborate_pattern(m, p);
       let (e', tye) = elaborate(m, e);
-      Exp.FixF(p', fresh_cast(e', tye, typ), env)
-      |> rewrap
-      |> cast_from(typ);
+      FixF(p', fresh_cast(e', tye, typ), env) |> rewrap |> cast_from(typ);
     | TyAlias(_, _, e) =>
       let (e', tye) = elaborate(m, e);
       e' |> cast_from(tye);
@@ -332,7 +324,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
       let (tyf1, tyf2) = Typ.matched_arrow(ctx, tyf);
       let f'' = fresh_cast(f', tyf, Arrow(tyf1, tyf2) |> Typ.temp);
       let a'' = fresh_cast(a', tya, tyf1);
-      Exp.Ap(dir, f'', a'') |> rewrap |> cast_from(tyf2);
+      Ap(dir, f'', a'') |> rewrap |> cast_from(tyf2);
     | DeferredAp(f, args) =>
       let (f', tyf) = elaborate(m, f);
       let (args', tys) = List.map(elaborate(m), args) |> ListUtil.unzip;
@@ -350,7 +342,10 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
           ((arg, _)) => Exp.is_deferral(arg),
           List.combine(args, ty_fargs),
         );
-      let remaining_arg_ty = Prod(List.map(snd, remaining_args)) |> Typ.temp;
+      let remaining_arg_ty =
+        List.length(remaining_args) == 1
+          ? snd(List.hd(remaining_args))
+          : Prod(List.map(snd, remaining_args)) |> Typ.temp;
       DeferredAp(f'', args'')
       |> rewrap
       |> cast_from(Arrow(remaining_arg_ty, tyf2) |> Typ.temp);
@@ -371,11 +366,11 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
       let (f', tyf) = elaborate(m, f);
       let ty =
         Typ.join(~fix=false, ctx, tyt, tyf)
-        |> Option.value(~default=Typ.temp(Typ.Unknown(Internal)));
+        |> Option.value(~default=Typ.temp(Unknown(Internal)));
       let c'' = fresh_cast(c', tyc, Bool |> Typ.temp);
       let t'' = fresh_cast(t', tyt, ty);
       let f'' = fresh_cast(f', tyf, ty);
-      Exp.If(c'', t'', f'') |> rewrap |> cast_from(ty);
+      If(c'', t'', f'') |> rewrap |> cast_from(ty);
     | Seq(e1, e2) =>
       let (e1', _) = elaborate(m, e1);
       let (e2', ty2) = elaborate(m, e2);
@@ -427,10 +422,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
         Constructor("$e", Unknown(Internal) |> Typ.temp) |> rewrap
       | Var("v") =>
         Constructor("$v", Unknown(Internal) |> Typ.temp) |> rewrap
-      | _ =>
-        DHExp.EmptyHole
-        |> rewrap
-        |> cast_from(Typ.temp(Typ.Unknown(Internal)))
+      | _ => EmptyHole |> rewrap |> cast_from(Typ.temp(Unknown(Internal)))
       }
     | UnOp(Int(Minus), e) =>
       let (e', t) = elaborate(m, e);
@@ -533,7 +525,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
       |> cast_from(
            Ctx.lookup_var(Builtins.ctx_init, fn)
            |> Option.map((x: Ctx.var_entry) => x.typ)
-           |> Option.value(~default=Typ.temp(Typ.Unknown(Internal))),
+           |> Option.value(~default=Typ.temp(Unknown(Internal))),
          )
     | Match(e, cases) =>
       let (e', t) = elaborate(m, e);
@@ -541,15 +533,15 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
       let (ps', ptys) =
         List.map(elaborate_pattern(m), ps) |> ListUtil.unzip;
       let joined_pty =
-        Typ.join_all(~empty=Typ.Unknown(Internal) |> Typ.temp, ctx, ptys)
-        |> Option.value(~default=Typ.temp(Typ.Unknown(Internal)));
+        Typ.join_all(~empty=Unknown(Internal) |> Typ.temp, ctx, ptys)
+        |> Option.value(~default=Typ.temp(Unknown(Internal)));
       let ps'' =
         List.map2((p, t) => fresh_pat_cast(p, t, joined_pty), ps', ptys);
       let e'' = fresh_cast(e', t, joined_pty);
       let (es', etys) = List.map(elaborate(m), es) |> ListUtil.unzip;
       let joined_ety =
-        Typ.join_all(~empty=Typ.Unknown(Internal) |> Typ.temp, ctx, etys)
-        |> Option.value(~default=Typ.temp(Typ.Unknown(Internal)));
+        Typ.join_all(~empty=Unknown(Internal) |> Typ.temp, ctx, etys)
+        |> Option.value(~default=Typ.temp(Unknown(Internal)));
       let es'' =
         List.map2((e, t) => fresh_cast(e, t, joined_ety), es', etys);
       Match(e'', List.combine(ps'', es''))
diff --git a/src/haz3lcore/dynamics/EvalCtx.re b/src/haz3lcore/dynamics/EvalCtx.re
index bed931c8d3..1f60bfa70a 100644
--- a/src/haz3lcore/dynamics/EvalCtx.re
+++ b/src/haz3lcore/dynamics/EvalCtx.re
@@ -51,106 +51,103 @@ let rec compose = (ctx: t, d: DHExp.t): DHExp.t => {
   | Mark => d
   | Term({term, ids}) =>
     let wrap = DHExp.mk(ids);
-    DHExp.(
-      switch (term) {
-      | Closure(env, ctx) =>
-        let d = compose(ctx, d);
-        Closure(env, d) |> wrap;
-      | Filter(flt, ctx) =>
-        let d = compose(ctx, d);
-        Filter(flt, d) |> wrap;
-      | Seq1(ctx, d2) =>
-        let d1 = compose(ctx, d);
-        Seq(d1, d2) |> wrap;
-      | Seq2(d1, ctx) =>
-        let d2 = compose(ctx, d);
-        Seq(d1, d2) |> wrap;
-      | Ap1(dir, ctx, d2) =>
-        let d1 = compose(ctx, d);
-        Ap(dir, d1, d2) |> wrap;
-      | Ap2(dir, d1, ctx) =>
-        let d2 = compose(ctx, d);
-        Ap(dir, d1, d2) |> wrap;
-      | DeferredAp1(ctx, d2s) =>
-        let d1 = compose(ctx, d);
-        DeferredAp(d1, d2s) |> wrap;
-      | DeferredAp2(d1, ctx, (ld, rd)) =>
-        let d2 = compose(ctx, d);
-        DeferredAp(d1, ListUtil.rev_concat(ld, [d2, ...rd])) |> wrap;
-      | If1(ctx, d2, d3) =>
-        let d' = compose(ctx, d);
-        If(d', d2, d3) |> wrap;
-      | If2(d1, ctx, d3) =>
-        let d' = compose(ctx, d);
-        If(d1, d', d3) |> wrap;
-      | If3(d1, d2, ctx) =>
-        let d' = compose(ctx, d);
-        If(d1, d2, d') |> wrap;
-      | Test(ctx) =>
-        let d1 = compose(ctx, d);
-        Test(d1) |> wrap;
-      | UnOp(op, ctx) =>
-        let d1 = compose(ctx, d);
-        UnOp(op, d1) |> wrap;
-      | BinOp1(op, ctx, d2) =>
-        let d1 = compose(ctx, d);
-        BinOp(op, d1, d2) |> wrap;
-      | BinOp2(op, d1, ctx) =>
-        let d2 = compose(ctx, d);
-        BinOp(op, d1, d2) |> wrap;
-      | Cons1(ctx, d2) =>
-        let d1 = compose(ctx, d);
-        Cons(d1, d2) |> wrap;
-      | Cons2(d1, ctx) =>
-        let d2 = compose(ctx, d);
-        Cons(d1, d2) |> wrap;
-      | ListConcat1(ctx, d2) =>
-        let d1 = compose(ctx, d);
-        ListConcat(d1, d2) |> wrap;
-      | ListConcat2(d1, ctx) =>
-        let d2 = compose(ctx, d);
-        ListConcat(d1, d2) |> wrap;
-      | Tuple(ctx, (ld, rd)) =>
-        let d = compose(ctx, d);
-        Tuple(ListUtil.rev_concat(ld, [d, ...rd])) |> wrap;
-      | ListLit(ctx, (ld, rd)) =>
-        let d = compose(ctx, d);
-        ListLit(ListUtil.rev_concat(ld, [d, ...rd])) |> wrap;
-      | MultiHole(ctx, (ld, rd)) =>
-        let d = compose(ctx, d);
-        MultiHole(ListUtil.rev_concat(ld, [TermBase.Any.Exp(d), ...rd]))
-        |> wrap;
-      | Let1(dp, ctx, d2) =>
-        let d = compose(ctx, d);
-        Let(dp, d, d2) |> wrap;
-      | Let2(dp, d1, ctx) =>
-        let d = compose(ctx, d);
-        Let(dp, d1, d) |> wrap;
-      | Fun(dp, ctx, env, v) =>
-        let d = compose(ctx, d);
-        Fun(dp, d, env, v) |> wrap;
-      | FixF(v, ctx, env) =>
-        let d = compose(ctx, d);
-        FixF(v, d, env) |> wrap;
-      | Cast(ctx, ty1, ty2) =>
-        let d = compose(ctx, d);
-        Cast(d, ty1, ty2) |> wrap;
-      | FailedCast(ctx, ty1, ty2) =>
-        let d = compose(ctx, d);
-        FailedCast(d, ty1, ty2) |> wrap;
-      | DynamicErrorHole(ctx, err) =>
-        let d = compose(ctx, d);
-        DynamicErrorHole(d, err) |> wrap;
-      | MatchScrut(ctx, rules) =>
-        let d = compose(ctx, d);
-        Match(d, rules) |> wrap;
-      | MatchRule(scr, p, ctx, (lr, rr)) =>
-        let d = compose(ctx, d);
-        Match(scr, ListUtil.rev_concat(lr, [(p, d), ...rr])) |> wrap;
-      | TypAp(ctx, ty) =>
-        let d = compose(ctx, d);
-        TypAp(d, ty) |> wrap;
-      }
-    );
+    switch (term) {
+    | Closure(env, ctx) =>
+      let d = compose(ctx, d);
+      Closure(env, d) |> wrap;
+    | Filter(flt, ctx) =>
+      let d = compose(ctx, d);
+      Filter(flt, d) |> wrap;
+    | Seq1(ctx, d2) =>
+      let d1 = compose(ctx, d);
+      Seq(d1, d2) |> wrap;
+    | Seq2(d1, ctx) =>
+      let d2 = compose(ctx, d);
+      Seq(d1, d2) |> wrap;
+    | Ap1(dir, ctx, d2) =>
+      let d1 = compose(ctx, d);
+      Ap(dir, d1, d2) |> wrap;
+    | Ap2(dir, d1, ctx) =>
+      let d2 = compose(ctx, d);
+      Ap(dir, d1, d2) |> wrap;
+    | DeferredAp1(ctx, d2s) =>
+      let d1 = compose(ctx, d);
+      DeferredAp(d1, d2s) |> wrap;
+    | DeferredAp2(d1, ctx, (ld, rd)) =>
+      let d2 = compose(ctx, d);
+      DeferredAp(d1, ListUtil.rev_concat(ld, [d2, ...rd])) |> wrap;
+    | If1(ctx, d2, d3) =>
+      let d' = compose(ctx, d);
+      If(d', d2, d3) |> wrap;
+    | If2(d1, ctx, d3) =>
+      let d' = compose(ctx, d);
+      If(d1, d', d3) |> wrap;
+    | If3(d1, d2, ctx) =>
+      let d' = compose(ctx, d);
+      If(d1, d2, d') |> wrap;
+    | Test(ctx) =>
+      let d1 = compose(ctx, d);
+      Test(d1) |> wrap;
+    | UnOp(op, ctx) =>
+      let d1 = compose(ctx, d);
+      UnOp(op, d1) |> wrap;
+    | BinOp1(op, ctx, d2) =>
+      let d1 = compose(ctx, d);
+      BinOp(op, d1, d2) |> wrap;
+    | BinOp2(op, d1, ctx) =>
+      let d2 = compose(ctx, d);
+      BinOp(op, d1, d2) |> wrap;
+    | Cons1(ctx, d2) =>
+      let d1 = compose(ctx, d);
+      Cons(d1, d2) |> wrap;
+    | Cons2(d1, ctx) =>
+      let d2 = compose(ctx, d);
+      Cons(d1, d2) |> wrap;
+    | ListConcat1(ctx, d2) =>
+      let d1 = compose(ctx, d);
+      ListConcat(d1, d2) |> wrap;
+    | ListConcat2(d1, ctx) =>
+      let d2 = compose(ctx, d);
+      ListConcat(d1, d2) |> wrap;
+    | Tuple(ctx, (ld, rd)) =>
+      let d = compose(ctx, d);
+      Tuple(ListUtil.rev_concat(ld, [d, ...rd])) |> wrap;
+    | ListLit(ctx, (ld, rd)) =>
+      let d = compose(ctx, d);
+      ListLit(ListUtil.rev_concat(ld, [d, ...rd])) |> wrap;
+    | MultiHole(ctx, (ld, rd)) =>
+      let d = compose(ctx, d);
+      MultiHole(ListUtil.rev_concat(ld, [Exp(d), ...rd])) |> wrap;
+    | Let1(dp, ctx, d2) =>
+      let d = compose(ctx, d);
+      Let(dp, d, d2) |> wrap;
+    | Let2(dp, d1, ctx) =>
+      let d = compose(ctx, d);
+      Let(dp, d1, d) |> wrap;
+    | Fun(dp, ctx, env, v) =>
+      let d = compose(ctx, d);
+      Fun(dp, d, env, v) |> wrap;
+    | FixF(v, ctx, env) =>
+      let d = compose(ctx, d);
+      FixF(v, d, env) |> wrap;
+    | Cast(ctx, ty1, ty2) =>
+      let d = compose(ctx, d);
+      Cast(d, ty1, ty2) |> wrap;
+    | FailedCast(ctx, ty1, ty2) =>
+      let d = compose(ctx, d);
+      FailedCast(d, ty1, ty2) |> wrap;
+    | DynamicErrorHole(ctx, err) =>
+      let d = compose(ctx, d);
+      DynamicErrorHole(d, err) |> wrap;
+    | MatchScrut(ctx, rules) =>
+      let d = compose(ctx, d);
+      Match(d, rules) |> wrap;
+    | MatchRule(scr, p, ctx, (lr, rr)) =>
+      let d = compose(ctx, d);
+      Match(scr, ListUtil.rev_concat(lr, [(p, d), ...rr])) |> wrap;
+    | TypAp(ctx, ty) =>
+      let d = compose(ctx, d);
+      TypAp(d, ty) |> wrap;
+    };
   };
 };
diff --git a/src/haz3lcore/dynamics/Evaluator.re b/src/haz3lcore/dynamics/Evaluator.re
index fb877accd7..628b493e1d 100644
--- a/src/haz3lcore/dynamics/Evaluator.re
+++ b/src/haz3lcore/dynamics/Evaluator.re
@@ -118,6 +118,7 @@ module EvaluatorEVMode: {
     | (BoxedReady, Constructor) => (BoxedValue, c)
     | (IndetReady, Constructor) => (Indet, c)
     | (IndetBlocked, _) => (Indet, c)
+    | (_, Value) => (BoxedValue, c)
     | (_, Indet) => (Indet, c)
     };
 };
diff --git a/src/haz3lcore/dynamics/EvaluatorStep.re b/src/haz3lcore/dynamics/EvaluatorStep.re
index f25f25603f..0882fa223f 100644
--- a/src/haz3lcore/dynamics/EvaluatorStep.re
+++ b/src/haz3lcore/dynamics/EvaluatorStep.re
@@ -136,6 +136,7 @@ module Decompose = {
         | (undo, Result.BoxedValue, env, v) =>
           switch (rl(v)) {
           | Constructor => Result.BoxedValue
+          | Value => Result.BoxedValue
           | Indet => Result.Indet
           | Step(s) => Result.Step([EvalObj.mk(Mark, env, undo, s.kind)])
           // TODO: Actually show these exceptions to the user!
@@ -187,6 +188,7 @@ module TakeStep = {
         state_update();
         Some(expr);
       | Constructor
+      | Value
       | Indet => None
       };
 
diff --git a/src/haz3lcore/dynamics/FilterEnvironment.re b/src/haz3lcore/dynamics/FilterEnvironment.re
index 284e7353d3..ac59a874bc 100644
--- a/src/haz3lcore/dynamics/FilterEnvironment.re
+++ b/src/haz3lcore/dynamics/FilterEnvironment.re
@@ -1,2 +1,2 @@
-type t = list(TermBase.StepperFilterKind.filter);
+type t = list(TermBase.filter);
 let extends = (flt, env) => [flt, ...env];
diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re
index d6d0bcc543..61fd72f1bd 100644
--- a/src/haz3lcore/dynamics/FilterMatcher.re
+++ b/src/haz3lcore/dynamics/FilterMatcher.re
@@ -24,7 +24,9 @@ let evaluate_extend_env_with_pat =
         {
           ids,
           copied,
-          IdTagged.term: TermBase.Exp.FixF(pat, exp, Some(to_extend)),
+          IdTagged.term: (
+            FixF(pat, exp, Some(to_extend)): TermBase.exp_term
+          ),
         },
       )),
       to_extend,
@@ -36,14 +38,12 @@ let evaluate_extend_env_with_pat =
         binding =>
           (
             binding,
-            TermBase.Exp.Let(
-              pat,
-              {
-                ids,
-                copied,
-                term: TermBase.Exp.FixF(pat, exp, Some(to_extend)),
-              },
-              TermBase.Exp.Var(binding) |> IdTagged.fresh,
+            (
+              Let(
+                pat,
+                {ids, copied, term: FixF(pat, exp, Some(to_extend))},
+                (Var(binding): TermBase.exp_term) |> IdTagged.fresh,
+              ): TermBase.exp_term
             )
             |> IdTagged.fresh,
           ),
@@ -75,13 +75,13 @@ let tangle =
     let denv_subst: list((string, 'a)) =
       List.mapi(
         (i, binding) =>
-          (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh),
+          (binding, (Var(ids[i]): TermBase.exp_term) |> IdTagged.fresh),
         dvars,
       );
     let fenv_subst: list((string, 'a)) =
       List.mapi(
         (i, binding) =>
-          (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh),
+          (binding, (Var(ids[i]): TermBase.exp_term) |> IdTagged.fresh),
         fvars,
       );
     let denv = evaluate_extend_env(Environment.of_list(denv_subst), denv);
@@ -356,13 +356,13 @@ and matches_fun =
     let denv_subst: list((string, 'a)) =
       List.mapi(
         (i, binding) =>
-          (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh),
+          (binding, (Var(ids[i]): TermBase.exp_term) |> IdTagged.fresh),
         dvars,
       );
     let fenv_subst: list((string, 'a)) =
       List.mapi(
         (i, binding) =>
-          (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh),
+          (binding, (Var(ids[i]): TermBase.exp_term) |> IdTagged.fresh),
         fvars,
       );
     let denv = evaluate_extend_env(Environment.of_list(denv_subst), denv);
@@ -387,11 +387,7 @@ and matches_utpat = (d: TPat.t, f: TPat.t): bool => {
 };
 
 let matches =
-    (
-      ~env: ClosureEnvironment.t,
-      ~exp: DHExp.t,
-      ~flt: TermBase.StepperFilterKind.filter,
-    )
+    (~env: ClosureEnvironment.t, ~exp: DHExp.t, ~flt: TermBase.filter)
     : option(FilterAction.t) =>
   if (matches_exp(~denv=env, exp, ~fenv=env, flt.pat)) {
     Some(flt.act);
diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re
index a54c9d18d8..5c936426b9 100644
--- a/src/haz3lcore/dynamics/Transition.re
+++ b/src/haz3lcore/dynamics/Transition.re
@@ -91,7 +91,8 @@ type rule =
       is_value: bool,
     })
   | Constructor
-  | Indet;
+  | Indet
+  | Value;
 
 let (let-unbox) = ((request, v), f) =>
   switch (Unboxing.unbox(request, v)) {
@@ -331,7 +332,7 @@ module Transition = (EV: EV_MODE) => {
           (d2, ds) => DeferredAp2(d1, d2, ds) |> wrap_ctx,
           ds,
         );
-      Constructor;
+      Value;
     | Ap(dir, d1, d2) =>
       let. _ = otherwise(env, (d1, (d2, _)) => Ap(dir, d1, d2) |> rewrap)
       and. d1' =
@@ -392,18 +393,25 @@ module Transition = (EV: EV_MODE) => {
         } else {
           Indet;
         }
-      /* This case isn't currently used because deferrals are elaborated away */
       | DeferredAp(d3, d4s) =>
         let n_args =
           List.length(
-            List.map(
+            List.filter(
               fun
               | {term: Deferral(_), _} => true
               | _ => false: Exp.t => bool,
               d4s,
             ),
           );
-        let-unbox args = (Tuple(n_args), d2);
+        let-unbox args =
+          if (n_args == 1) {
+            (
+              Tuple(n_args),
+              Tuple([d2]) |> fresh // TODO Should we not be going to a tuple?
+            );
+          } else {
+            (Tuple(n_args), d2);
+          };
         let new_args = {
           let rec go = (deferred, args) =>
             switch ((deferred: list(Exp.t))) {
diff --git a/src/haz3lcore/dynamics/TypeAssignment.re b/src/haz3lcore/dynamics/TypeAssignment.re
index f4979d94bf..59b58aa56f 100644
--- a/src/haz3lcore/dynamics/TypeAssignment.re
+++ b/src/haz3lcore/dynamics/TypeAssignment.re
@@ -161,16 +161,16 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) =>
       };
     let* ctx = dhpat_extend_ctx(dhp, ty_p, ctx);
     let* ty2 = typ_of_dhexp(ctx, m, d);
-    Some(Typ.Arrow(ty_p, ty2) |> Typ.temp);
+    Some(Arrow(ty_p, ty2) |> Typ.temp);
   | TypFun({term: Var(name), _} as utpat, d, _)
       when !Ctx.shadows_typ(ctx, name) =>
     let ctx =
       Ctx.extend_tvar(ctx, {name, id: TPat.rep_id(utpat), kind: Abstract});
     let* ty = typ_of_dhexp(ctx, m, d);
-    Some(Typ.Forall(utpat, ty) |> Typ.temp);
+    Some(Forall(utpat, ty) |> Typ.temp);
   | TypFun(_, d, _) =>
     let* ty = typ_of_dhexp(ctx, m, d);
-    Some(Typ.Forall(Var("?") |> TPat.fresh, ty) |> Typ.temp);
+    Some(Forall(Var("?") |> TPat.fresh, ty) |> Typ.temp);
   | TypAp(d, ty1) =>
     let* ty = typ_of_dhexp(ctx, m, d);
     let* (name, ty2) = Typ.matched_forall_strict(ctx, ty);
@@ -209,8 +209,8 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) =>
         |> OptUtil.sequence;
       switch (tys) {
       | [] => Some(tyr)
-      | [ty] => Some(Typ.Arrow(ty, tyr) |> Typ.temp)
-      | tys => Some(Typ.Arrow(Prod(tys) |> Typ.temp, tyr) |> Typ.temp)
+      | [ty] => Some(Arrow(ty, tyr) |> Typ.temp)
+      | tys => Some(Arrow(Prod(tys) |> Typ.temp, tyr) |> Typ.temp)
       };
     } else {
       None;
@@ -221,7 +221,7 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) =>
     Some(var.typ);
   | Test(dtest) =>
     let* ty = typ_of_dhexp(ctx, m, dtest);
-    Typ.eq(ty, Bool |> Typ.temp) ? Some(Typ.Prod([]) |> Typ.temp) : None;
+    Typ.eq(ty, Bool |> Typ.temp) ? Some(Prod([]) |> Typ.temp) : None;
   | Bool(_) => Some(Bool |> Typ.temp)
   | Int(_) => Some(Int |> Typ.temp)
   | Float(_) => Some(Float |> Typ.temp)
diff --git a/src/haz3lcore/dynamics/ValueChecker.re b/src/haz3lcore/dynamics/ValueChecker.re
index 39f43daeed..a6e5ab30f0 100644
--- a/src/haz3lcore/dynamics/ValueChecker.re
+++ b/src/haz3lcore/dynamics/ValueChecker.re
@@ -1,4 +1,3 @@
-open DHExp;
 open Transition;
 
 type t =
@@ -69,6 +68,7 @@ module ValueCheckerEVMode: {
     | (_, _, Constructor) => r
     | (_, Expr, Indet) => Expr
     | (_, _, Indet) => Indet
+    | (_, _, Value) => Value
     | (true, _, Step(_)) => Expr
     | (false, _, Step(_)) => r
     };
diff --git a/src/haz3lcore/lang/term/TPat.re b/src/haz3lcore/lang/term/TPat.re
index 3dade36b54..583f805851 100644
--- a/src/haz3lcore/lang/term/TPat.re
+++ b/src/haz3lcore/lang/term/TPat.re
@@ -10,7 +10,7 @@ include TermBase.TPat;
 let rep_id: t => Id.t = IdTagged.rep_id;
 let fresh: term => t = IdTagged.fresh;
 
-let hole = (tms: list(TermBase.Any.t)) =>
+let hole = (tms: list(TermBase.Any.t)): TermBase.TPat.term =>
   switch (tms) {
   | [] => EmptyHole
   | [_, ..._] => MultiHole(tms)
diff --git a/src/haz3lcore/lang/term/Typ.re b/src/haz3lcore/lang/term/Typ.re
index 5dc0b73aaa..c9a6f0c204 100644
--- a/src/haz3lcore/lang/term/Typ.re
+++ b/src/haz3lcore/lang/term/Typ.re
@@ -34,7 +34,7 @@ let fresh: term => t = IdTagged.fresh;
 let temp: term => t = term => {term, ids: [Id.invalid], copied: false};
 let rep_id: t => Id.t = IdTagged.rep_id;
 
-let hole = (tms: list(TermBase.Any.t)) =>
+let hole = (tms: list(TermBase.Any.t)): TermBase.Typ.term =>
   switch (tms) {
   | [] => Unknown(Hole(EmptyHole))
   | [_, ..._] => Unknown(Hole(MultiHole(tms)))
@@ -137,7 +137,8 @@ let of_source = List.map((source: source) => source.ty);
    but right now TypeHole strictly predominates over Internal
    which strictly predominates over SynSwitch. */
 let join_type_provenance =
-    (p1: type_provenance, p2: type_provenance): type_provenance =>
+    (p1: TermBase.type_provenance, p2: TermBase.type_provenance)
+    : TermBase.type_provenance =>
   switch (p1, p2) {
   | (Hole(h1), Hole(h2)) when h1 == h2 => Hole(h1)
   | (Hole(EmptyHole), Hole(EmptyHole) | SynSwitch)
diff --git a/src/haz3lcore/prog/CachedStatics.re b/src/haz3lcore/prog/CachedStatics.re
index f2bc13d113..3df0669dc3 100644
--- a/src/haz3lcore/prog/CachedStatics.re
+++ b/src/haz3lcore/prog/CachedStatics.re
@@ -8,7 +8,11 @@ type statics = {
 };
 
 let empty_statics: statics = {
-  term: UExp.{ids: [Id.invalid], copied: false, term: Tuple([])},
+  term: {
+    ids: [Id.invalid],
+    copied: false,
+    term: Tuple([]),
+  },
   info_map: Id.Map.empty,
   error_ids: [],
 };
diff --git a/src/haz3lcore/statics/Ctx.re b/src/haz3lcore/statics/Ctx.re
index 9791b6cd0f..f213a18cb7 100644
--- a/src/haz3lcore/statics/Ctx.re
+++ b/src/haz3lcore/statics/Ctx.re
@@ -2,14 +2,14 @@ open Util;
 
 [@deriving (show({with_path: false}), sexp, yojson)]
 type kind =
-  | Singleton(TermBase.Typ.t)
+  | Singleton(TermBase.typ_t)
   | Abstract;
 
 [@deriving (show({with_path: false}), sexp, yojson)]
 type var_entry = {
   name: Var.t,
   id: Id.t,
-  typ: TermBase.Typ.t,
+  typ: TermBase.typ_t,
 };
 
 [@deriving (show({with_path: false}), sexp, yojson)]
@@ -99,7 +99,9 @@ let lookup_alias = (ctx: t, name: string): option(TermBase.Typ.t) =>
   | Some(Singleton(ty)) => Some(ty)
   | Some(Abstract) => None
   | None =>
-    Some(TermBase.Typ.Unknown(Hole(Invalid(name))) |> IdTagged.fresh)
+    Some(
+      (Unknown(Hole(Invalid(name))): TermBase.Typ.term) |> IdTagged.fresh,
+    )
   };
 
 let add_ctrs = (ctx: t, name: string, id: Id.t, ctrs: TermBase.Typ.sum_map): t =>
@@ -112,11 +114,10 @@ let add_ctrs = (ctx: t, name: string, id: Id.t, ctrs: TermBase.Typ.sum_map): t =
           id,
           typ:
             switch (typ) {
-            | None => TermBase.Typ.Var(name) |> IdTagged.fresh
+            | None => (Var(name): TermBase.typ_term) |> IdTagged.fresh
             | Some(typ) =>
-              TermBase.Typ.Arrow(
-                typ,
-                TermBase.Typ.Var(name) |> IdTagged.fresh,
+              (
+                Arrow(typ, (Var(name): TermBase.typ_term) |> IdTagged.fresh): TermBase.typ_term
               )
               |> IdTagged.fresh
             },
diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re
index 673af0bb89..d1edb9d16a 100644
--- a/src/haz3lcore/statics/MakeTerm.re
+++ b/src/haz3lcore/statics/MakeTerm.re
@@ -61,11 +61,11 @@ let is_grout = tiles =>
 let is_rules = ((ts, kids): tiles): option(Aba.t(UPat.t, UExp.t)) => {
   open OptUtil.Syntax;
   let+ ps =
-    ts
+    (ts: list(tile))
     |> List.map(
          fun
-         | (_, (["|", "=>"], [Any.Pat(p)])) => Some(p)
-         | _ => None,
+         | (_, (["|", "=>"], [Pat(p)])) => Some(p)
+         | _ => None: tile => option(TermBase.pat_t),
        )
     |> OptUtil.sequence
   and+ clauses =
@@ -73,7 +73,7 @@ let is_rules = ((ts, kids): tiles): option(Aba.t(UPat.t, UExp.t)) => {
     |> List.map(
          fun
          | Exp(clause) => Some(clause)
-         | _ => None,
+         | _ => None: TermBase.any_t => option(TermBase.exp_t),
        )
     |> OptUtil.sequence;
   Aba.mk(ps, clauses);
@@ -494,7 +494,7 @@ and tpat_term: unsorted => TPat.term = {
 //   return(r => Rul(r), ids, {ids, term});
 // }
 and rul = (unsorted: unsorted): Rul.t => {
-  let hole = Rul.Hole(kids_of_unsorted(unsorted));
+  let hole: Rul.term = Hole(kids_of_unsorted(unsorted));
   switch (exp(unsorted)) {
   | {term: MultiHole(_), _} =>
     switch (unsorted) {
diff --git a/src/haz3lcore/statics/Mode.re b/src/haz3lcore/statics/Mode.re
index 5a85dbecd9..2415399627 100644
--- a/src/haz3lcore/statics/Mode.re
+++ b/src/haz3lcore/statics/Mode.re
@@ -152,6 +152,7 @@ let typap_mode: t = SynTypFun;
 let of_deferred_ap_args = (length: int, ty_ins: list(Typ.t)): list(t) =>
   (
     List.length(ty_ins) == length
-      ? ty_ins : List.init(length, _ => Typ.Unknown(Internal) |> Typ.temp)
+      ? ty_ins
+      : List.init(length, _ => (Unknown(Internal): Typ.term) |> Typ.temp)
   )
   |> List.map(ty => Ana(ty));
diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
index aca1ce0389..443c94155b 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -276,13 +276,13 @@ and uexp_to_info_map =
       copied: false,
       term:
         switch (e.term) {
-        | Var("e") => UExp.Constructor("$e", Unknown(Internal) |> Typ.temp)
-        | Var("v") => UExp.Constructor("$v", Unknown(Internal) |> Typ.temp)
+        | Var("e") => Constructor("$e", Unknown(Internal) |> Typ.temp)
+        | Var("v") => Constructor("$v", Unknown(Internal) |> Typ.temp)
         | _ => e.term
         },
     };
-    let ty_in = Typ.Var("$Meta") |> Typ.temp;
-    let ty_out = Typ.Unknown(Internal) |> Typ.temp;
+    let ty_in = Var("$Meta") |> Typ.temp;
+    let ty_out = Unknown(Internal) |> Typ.temp;
     let (e, m) = go(~mode=Ana(ty_in), e, m);
     add(~self=Just(ty_out), ~co_ctx=e.co_ctx, m);
   | UnOp(op, e) =>
@@ -426,8 +426,7 @@ and uexp_to_info_map =
         let def_ctx = p_ana'.ctx;
         let (def_base2, _) = go'(~ctx=def_ctx, ~mode=Ana(p_syn.ty), def, m);
         let ana_ty_fn = ((ty_fn1, ty_fn2), ty_p) => {
-          Typ.term_of(ty_p) == Typ.Unknown(SynSwitch)
-          && !Typ.eq(ty_fn1, ty_fn2)
+          Typ.term_of(ty_p) == Unknown(SynSwitch) && !Typ.eq(ty_fn1, ty_fn2)
             ? ty_fn1 : ty_p;
         };
         let ana =
@@ -438,7 +437,7 @@ and uexp_to_info_map =
           | ((Prod(ty_fns1), Prod(ty_fns2)), Prod(ty_ps)) =>
             let tys =
               List.map2(ana_ty_fn, List.combine(ty_fns1, ty_fns2), ty_ps);
-            Typ.Prod(tys) |> Typ.temp;
+            Prod(tys) |> Typ.temp;
           | ((_, _), _) => ana_ty_fn((def_base.ty, def_base2.ty), p_syn.ty)
           };
         let (def, m) = go'(~ctx=def_ctx, ~mode=Ana(ana), def, m);
@@ -616,7 +615,7 @@ and uexp_to_info_map =
              use a different name than the alias for the recursive parameter */
           //let ty_rec = Typ.Rec("α", Typ.subst(Var("α"), name, ty_pre));
           let ty_rec =
-            Typ.Rec(TPat.Var(name) |> IdTagged.fresh, utyp) |> Typ.temp;
+            Rec((Var(name): TPat.term) |> IdTagged.fresh, utyp) |> Typ.temp;
           let ctx_def =
             Ctx.extend_alias(ctx, name, TPat.rep_id(typat), ty_rec);
           (ty_rec, ctx_def, ctx_def);
@@ -697,7 +696,7 @@ and upat_to_info_map =
   let atomic = (self, constraint_) => add(~self, ~ctx, ~constraint_, m);
   let ancestors = [UPat.rep_id(upat)] @ ancestors;
   let go = upat_to_info_map(~is_synswitch, ~ancestors, ~co_ctx);
-  let unknown = Typ.Unknown(is_synswitch ? SynSwitch : Internal) |> Typ.temp;
+  let unknown = Unknown(is_synswitch ? SynSwitch : Internal) |> Typ.temp;
   let ctx_fold = (ctx: Ctx.t, m) =>
     List.fold_left2(
       ((ctx, tys, cons, m), e, mode) =>
diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re
index 0493150865..92eef8161e 100644
--- a/src/haz3lcore/statics/Term.re
+++ b/src/haz3lcore/statics/Term.re
@@ -31,7 +31,7 @@ module Pat = {
 
   let fresh: term => t = IdTagged.fresh;
 
-  let hole = (tms: list(TermBase.Any.t)) =>
+  let hole = (tms: list(TermBase.Any.t)): TermBase.Pat.term =>
     switch (tms) {
     | [] => EmptyHole
     | [_, ..._] => MultiHole(tms)
@@ -597,7 +597,7 @@ module Any = {
     | Typ(t) => Some(t)
     | _ => None;
 
-  let rec ids =
+  let rec ids: TermBase.any_t => list(Id.t) =
     fun
     | Exp(tm) => tm.ids
     | Pat(tm) => tm.ids
@@ -620,7 +620,7 @@ module Any = {
   // (This would change for n-tuples if we decided parentheses are necessary.)
   let rep_id =
     fun
-    | Exp(tm) => Exp.rep_id(tm)
+    | (Exp(tm): TermBase.any_t) => Exp.rep_id(tm)
     | Pat(tm) => Pat.rep_id(tm)
     | Typ(tm) => Typ.rep_id(tm)
     | TPat(tm) => TPat.rep_id(tm)
diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re
index f0585955c6..02bd8400d4 100644
--- a/src/haz3lcore/statics/TermBase.re
+++ b/src/haz3lcore/statics/TermBase.re
@@ -2,6 +2,10 @@ open Util;
 
 let continue = x => x;
 let stop = (_, x) => x;
+[@deriving (show({with_path: false}), sexp, yojson)]
+type deferral_position_t =
+  | InAp
+  | OutsideAp;
 
 /*
    This megafile contains the definitions of the expression data types in
@@ -42,16 +46,127 @@ let stop = (_, x) => x;
      the id of the closure.
  */
 
+[@deriving (show({with_path: false}), sexp, yojson)]
+type any_t =
+  | Exp(exp_t)
+  | Pat(pat_t)
+  | Typ(typ_t)
+  | TPat(tpat_t)
+  | Rul(rul_t)
+  | Nul(unit)
+  | Any(unit)
+and exp_term =
+  | Invalid(string)
+  | EmptyHole
+  | MultiHole(list(any_t))
+  | DynamicErrorHole(exp_t, InvalidOperationError.t)
+  | FailedCast(exp_t, typ_t, typ_t)
+  | Deferral(deferral_position_t)
+  | Undefined
+  | Bool(bool)
+  | Int(int)
+  | Float(float)
+  | String(string)
+  | ListLit(list(exp_t))
+  | Constructor(string, typ_t) // Typ.t field is only meaningful in dynamic expressions
+  | Fun(
+      pat_t,
+      exp_t,
+      [@show.opaque] option(closure_environment_t),
+      option(Var.t),
+    )
+  | TypFun(tpat_t, exp_t, option(Var.t))
+  | Tuple(list(exp_t))
+  | Var(Var.t)
+  | Let(pat_t, exp_t, exp_t)
+  | FixF(pat_t, exp_t, option(closure_environment_t))
+  | TyAlias(tpat_t, typ_t, exp_t)
+  | Ap(Operators.ap_direction, exp_t, exp_t)
+  | TypAp(exp_t, typ_t)
+  | DeferredAp(exp_t, list(exp_t))
+  | If(exp_t, exp_t, exp_t)
+  | Seq(exp_t, exp_t)
+  | Test(exp_t)
+  | Filter(stepper_filter_kind_t, exp_t)
+  | Closure([@show.opaque] closure_environment_t, exp_t)
+  | Parens(exp_t) // (
+  | Cons(exp_t, exp_t)
+  | ListConcat(exp_t, exp_t)
+  | UnOp(Operators.op_un, exp_t)
+  | BinOp(Operators.op_bin, exp_t, exp_t)
+  | BuiltinFun(string)
+  | Match(exp_t, list((pat_t, exp_t)))
+  /* INVARIANT: in dynamic expressions, casts must be between
+     two consistent types. Both types should be normalized in
+     dynamics for the cast calculus to work right. */
+  | Cast(exp_t, typ_t, typ_t)
+and exp_t = IdTagged.t(exp_term)
+and pat_term =
+  | Invalid(string)
+  | EmptyHole
+  | MultiHole(list(any_t))
+  | Wild
+  | Int(int)
+  | Float(float)
+  | Bool(bool)
+  | String(string)
+  | ListLit(list(pat_t))
+  | Constructor(string, typ_t) // Typ.t field is only meaningful in dynamic patterns
+  | Cons(pat_t, pat_t)
+  | Var(Var.t)
+  | Tuple(list(pat_t))
+  | Parens(pat_t)
+  | Ap(pat_t, pat_t)
+  | Cast(pat_t, typ_t, typ_t)
+and pat_t = IdTagged.t(pat_term)
+and typ_term =
+  | Unknown(type_provenance)
+  | Int
+  | Float
+  | Bool
+  | String
+  | Var(string)
+  | List(typ_t)
+  | Arrow(typ_t, typ_t)
+  | Sum(ConstructorMap.t(typ_t))
+  | Prod(list(typ_t))
+  | Parens(typ_t)
+  | Ap(typ_t, typ_t)
+  | Rec(tpat_t, typ_t)
+  | Forall(tpat_t, typ_t)
+and typ_t = IdTagged.t(typ_term)
+and tpat_term =
+  | Invalid(string)
+  | EmptyHole
+  | MultiHole(list(any_t))
+  | Var(string)
+and tpat_t = IdTagged.t(tpat_term)
+and rul_term =
+  | Invalid(string)
+  | Hole(list(any_t))
+  | Rules(exp_t, list((pat_t, exp_t)))
+and rul_t = IdTagged.t(rul_term)
+and environment_t = VarBstMap.Ordered.t_(exp_t)
+and closure_environment_t = (Id.t, environment_t)
+and stepper_filter_kind_t =
+  | Filter(filter)
+  | Residue(int, FilterAction.t)
+and type_hole =
+  | Invalid(string)
+  | EmptyHole
+  | MultiHole(list(any_t))
+and type_provenance =
+  | SynSwitch
+  | Hole(type_hole)
+  | Internal
+and filter = {
+  pat: exp_t,
+  act: FilterAction.t,
+};
+
 module rec Any: {
   [@deriving (show({with_path: false}), sexp, yojson)]
-  type t =
-    | Exp(Exp.t)
-    | Pat(Pat.t)
-    | Typ(Typ.t)
-    | TPat(TPat.t)
-    | Rul(Rul.t)
-    | Nul(unit)
-    | Any(unit);
+  type t = any_t;
 
   let map_term:
     (
@@ -68,14 +183,7 @@ module rec Any: {
   let fast_equal: (t, t) => bool;
 } = {
   [@deriving (show({with_path: false}), sexp, yojson)]
-  type t =
-    | Exp(Exp.t)
-    | Pat(Pat.t)
-    | Typ(Typ.t)
-    | TPat(TPat.t)
-    | Rul(Rul.t)
-    | Nul(unit)
-    | Any(unit);
+  type t = any_t;
 
   let map_term =
       (
@@ -127,58 +235,11 @@ module rec Any: {
 }
 and Exp: {
   [@deriving (show({with_path: false}), sexp, yojson)]
-  type deferral_position =
-    | InAp
-    | OutsideAp;
-
+  type term = exp_term;
   [@deriving (show({with_path: false}), sexp, yojson)]
-  type term =
-    | Invalid(string)
-    | EmptyHole
-    | MultiHole(list(Any.t))
-    | DynamicErrorHole(t, InvalidOperationError.t)
-    | FailedCast(t, Typ.t, Typ.t)
-    | Deferral(deferral_position)
-    | Undefined
-    | Bool(bool)
-    | Int(int)
-    | Float(float)
-    | String(string)
-    | ListLit(list(t))
-    | Constructor(string, Typ.t) // Typ.t field is only meaningful in dynamic expressions
-    | Fun(
-        Pat.t,
-        t,
-        [@show.opaque] option(ClosureEnvironment.t),
-        option(Var.t),
-      )
-    | TypFun(TPat.t, t, option(Var.t))
-    | Tuple(list(t))
-    | Var(Var.t)
-    | Let(Pat.t, t, t)
-    | FixF(Pat.t, t, option(ClosureEnvironment.t))
-    | TyAlias(TPat.t, Typ.t, t)
-    | Ap(Operators.ap_direction, t, t)
-    | TypAp(t, Typ.t)
-    | DeferredAp(t, list(t))
-    | If(t, t, t)
-    | Seq(t, t)
-    | Test(t)
-    | Filter(StepperFilterKind.t, t)
-    | Closure([@show.opaque] ClosureEnvironment.t, t)
-    | Parens(t) // (
-    | Cons(t, t)
-    | ListConcat(t, t)
-    | UnOp(Operators.op_un, t)
-    | BinOp(Operators.op_bin, t, t)
-    | BuiltinFun(string)
-    | Match(t, list((Pat.t, t)))
-    /* INVARIANT: in dynamic expressions, casts must be between
-       two consistent types. Both types should be normalized in
-       dynamics for the cast calculus to work right. */
-    | Cast(t, Typ.t, Typ.t) // first Typ.t field is only meaningful in dynamic expressions
-  and t = IdTagged.t(term);
-
+  type t = exp_t;
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type deferral_position = deferral_position_t;
   let map_term:
     (
       ~f_exp: (Exp.t => Exp.t, Exp.t) => Exp.t=?,
@@ -194,54 +255,11 @@ and Exp: {
   let fast_equal: (t, t) => bool;
 } = {
   [@deriving (show({with_path: false}), sexp, yojson)]
-  type deferral_position =
-    | InAp
-    | OutsideAp;
-
+  type term = exp_term;
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type t = exp_t;
   [@deriving (show({with_path: false}), sexp, yojson)]
-  type term =
-    | Invalid(string)
-    | EmptyHole
-    | MultiHole(list(Any.t))
-    | DynamicErrorHole(t, InvalidOperationError.t)
-    | FailedCast(t, Typ.t, Typ.t)
-    | Deferral(deferral_position)
-    | Undefined
-    | Bool(bool)
-    | Int(int)
-    | Float(float)
-    | String(string)
-    | ListLit(list(t))
-    | Constructor(string, Typ.t)
-    | Fun(
-        Pat.t,
-        t,
-        [@show.opaque] option(ClosureEnvironment.t),
-        option(Var.t),
-      )
-    | TypFun(TPat.t, t, option(string))
-    | Tuple(list(t))
-    | Var(Var.t)
-    | Let(Pat.t, t, t)
-    | FixF(Pat.t, t, [@show.opaque] option(ClosureEnvironment.t))
-    | TyAlias(TPat.t, Typ.t, t)
-    | Ap(Operators.ap_direction, t, t) // note: function is always first then argument; even in pipe mode
-    | TypAp(t, Typ.t)
-    | DeferredAp(t, list(t))
-    | If(t, t, t)
-    | Seq(t, t)
-    | Test(t)
-    | Filter(StepperFilterKind.t, t)
-    | Closure([@show.opaque] ClosureEnvironment.t, t)
-    | Parens(t)
-    | Cons(t, t)
-    | ListConcat(t, t)
-    | UnOp(Operators.op_un, t)
-    | BinOp(Operators.op_bin, t, t)
-    | BuiltinFun(string) /// Doesn't currently have a distinguishable syntax
-    | Match(t, list((Pat.t, t)))
-    | Cast(t, Typ.t, Typ.t)
-  and t = IdTagged.t(term);
+  type deferral_position = deferral_position_t;
 
   let map_term =
       (
@@ -448,24 +466,9 @@ and Exp: {
 }
 and Pat: {
   [@deriving (show({with_path: false}), sexp, yojson)]
-  type term =
-    | Invalid(string)
-    | EmptyHole
-    | MultiHole(list(Any.t))
-    | Wild
-    | Int(int)
-    | Float(float)
-    | Bool(bool)
-    | String(string)
-    | ListLit(list(t))
-    | Constructor(string, Typ.t) // Typ.t field is only meaningful in dynamic patterns
-    | Cons(t, t)
-    | Var(Var.t)
-    | Tuple(list(t))
-    | Parens(t)
-    | Ap(t, t)
-    | Cast(t, Typ.t, Typ.t) // The second Typ.t field is only meaningful in dynamic patterns
-  and t = IdTagged.t(term);
+  type term = pat_term; // The second Typ.t field is only meaningful in dynamic patterns
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type t = pat_t;
 
   let map_term:
     (
@@ -482,24 +485,9 @@ and Pat: {
   let fast_equal: (t, t) => bool;
 } = {
   [@deriving (show({with_path: false}), sexp, yojson)]
-  type term =
-    | Invalid(string)
-    | EmptyHole
-    | MultiHole(list(Any.t))
-    | Wild
-    | Int(int)
-    | Float(float)
-    | Bool(bool)
-    | String(string)
-    | ListLit(list(t))
-    | Constructor(string, Typ.t)
-    | Cons(t, t)
-    | Var(Var.t)
-    | Tuple(list(t))
-    | Parens(t)
-    | Ap(t, t)
-    | Cast(t, Typ.t, Typ.t) // The second one is hidden from the user
-  and t = IdTagged.t(term);
+  type term = pat_term;
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type t = pat_t;
 
   let map_term =
       (
@@ -543,7 +531,7 @@ and Pat: {
     x |> f_pat(rec_call);
   };
 
-  let rec fast_equal = (p1, p2) =>
+  let rec fast_equal = (p1: t, p2: t) =>
     switch (p1 |> IdTagged.term_of, p2 |> IdTagged.term_of) {
     | (Parens(x), _) => fast_equal(x, p2)
     | (_, Parens(x)) => fast_equal(p1, x)
@@ -588,38 +576,9 @@ and Pat: {
 }
 and Typ: {
   [@deriving (show({with_path: false}), sexp, yojson)]
-  type type_hole =
-    | Invalid(string)
-    | EmptyHole
-    | MultiHole(list(Any.t));
-
-  /* TYPE_PROVENANCE: From whence does an unknown type originate?
-     Is it generated from an unannotated pattern variable (SynSwitch),
-     a pattern variable annotated with a type hole (TypeHole), or
-     generated by an internal judgement (Internal)? */
-  [@deriving (show({with_path: false}), sexp, yojson)]
-  type type_provenance =
-    | SynSwitch
-    | Hole(type_hole)
-    | Internal;
-
+  type term = typ_term;
   [@deriving (show({with_path: false}), sexp, yojson)]
-  type term =
-    | Unknown(Typ.type_provenance)
-    | Int
-    | Float
-    | Bool
-    | String
-    | Var(string)
-    | List(t)
-    | Arrow(t, t)
-    | Sum(ConstructorMap.t(t))
-    | Prod(list(t))
-    | Parens(t)
-    | Ap(t, t)
-    | Rec(TPat.t, t)
-    | Forall(TPat.t, t)
-  and t = IdTagged.t(term);
+  type t = typ_t;
 
   type sum_map = ConstructorMap.t(t);
 
@@ -640,38 +599,9 @@ and Typ: {
   let fast_equal: (t, t) => bool;
 } = {
   [@deriving (show({with_path: false}), sexp, yojson)]
-  type type_hole =
-    | Invalid(string)
-    | EmptyHole
-    | MultiHole(list(Any.t));
-
-  /* TYPE_PROVENANCE: From whence does an unknown type originate?
-     Is it generated from an unannotated pattern variable (SynSwitch),
-     a pattern variable annotated with a type hole (TypeHole), or
-     generated by an internal judgement (Internal)? */
-  [@deriving (show({with_path: false}), sexp, yojson)]
-  type type_provenance =
-    | SynSwitch
-    | Hole(type_hole)
-    | Internal;
-
+  type term = typ_term;
   [@deriving (show({with_path: false}), sexp, yojson)]
-  type term =
-    | Unknown(Typ.type_provenance)
-    | Int
-    | Float
-    | Bool
-    | String
-    | Var(string)
-    | List(t)
-    | Arrow(t, t)
-    | Sum(ConstructorMap.t(t))
-    | Prod(list(t))
-    | Parens(t)
-    | Ap(t, t)
-    | Rec(TPat.t, t)
-    | Forall(TPat.t, t)
-  and t = IdTagged.t(term);
+  type t = typ_t;
 
   type sum_map = ConstructorMap.t(t);
 
@@ -729,12 +659,12 @@ and Typ: {
     x |> f_typ(rec_call);
   };
 
-  let rec subst = (s: t, x: TPat.t, ty: t) => {
+  let rec subst = (s: t, x: TPat.t, ty: t): typ_t => {
     switch (TPat.tyvar_of_utpat(x)) {
     | Some(str) =>
       let (term, rewrap) = IdTagged.unwrap(ty);
       switch (term) {
-      | Int => Int |> rewrap
+      | Int => (Int: typ_term) |> rewrap
       | Float => Float |> rewrap
       | Bool => Bool |> rewrap
       | String => String |> rewrap
@@ -811,12 +741,9 @@ and Typ: {
 }
 and TPat: {
   [@deriving (show({with_path: false}), sexp, yojson)]
-  type term =
-    | Invalid(string)
-    | EmptyHole
-    | MultiHole(list(Any.t))
-    | Var(string)
-  and t = IdTagged.t(term);
+  type term = tpat_term;
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type t = tpat_t;
 
   let map_term:
     (
@@ -835,12 +762,9 @@ and TPat: {
   let fast_equal: (t, t) => bool;
 } = {
   [@deriving (show({with_path: false}), sexp, yojson)]
-  type term =
-    | Invalid(string)
-    | EmptyHole
-    | MultiHole(list(Any.t))
-    | Var(string)
-  and t = IdTagged.t(term);
+  type term = tpat_term;
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type t = tpat_t;
 
   let map_term =
       (
@@ -889,11 +813,9 @@ and TPat: {
 }
 and Rul: {
   [@deriving (show({with_path: false}), sexp, yojson)]
-  type term =
-    | Invalid(string)
-    | Hole(list(Any.t))
-    | Rules(Exp.t, list((Pat.t, Exp.t)))
-  and t = IdTagged.t(term);
+  type term = rul_term;
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type t = rul_t;
 
   let map_term:
     (
@@ -910,11 +832,9 @@ and Rul: {
   let fast_equal: (t, t) => bool;
 } = {
   [@deriving (show({with_path: false}), sexp, yojson)]
-  type term =
-    | Invalid(string)
-    | Hole(list(Any.t))
-    | Rules(Exp.t, list((Pat.t, Exp.t)))
-  and t = IdTagged.t(term);
+  type term = rul_term;
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type t = rul_t;
 
   let map_term =
       (
@@ -977,18 +897,16 @@ and Environment: {
      (module type of VarBstMap.Ordered) with
       type t_('a) = VarBstMap.Ordered.t_('a);
 
-  [@deriving (show({with_path: false}), sexp, yojson)]
-  type t = t_(Exp.t);
+  type t = environment_t;
 } = {
   include VarBstMap.Ordered;
 
-  [@deriving (show({with_path: false}), sexp, yojson)]
-  type t = t_(Exp.t);
+  type t = environment_t;
 }
 
 and ClosureEnvironment: {
   [@deriving (show({with_path: false}), sexp, yojson)]
-  type t;
+  type t = closure_environment_t;
 
   let wrap: (Id.t, Environment.t) => t;
 
@@ -999,7 +917,7 @@ and ClosureEnvironment: {
 
   let of_environment: Environment.t => t;
 
-  let id_equal: (t, t) => bool;
+  let id_equal: (closure_environment_t, closure_environment_t) => bool;
 
   let empty: t;
   let is_empty: t => bool;
@@ -1025,7 +943,7 @@ and ClosureEnvironment: {
 } = {
   module Inner: {
     [@deriving (show({with_path: false}), sexp, yojson)]
-    type t;
+    type t = closure_environment_t;
 
     let wrap: (Id.t, Environment.t) => t;
 
@@ -1033,7 +951,7 @@ and ClosureEnvironment: {
     let map_of: t => Environment.t;
   } = {
     [@deriving (show({with_path: false}), sexp, yojson)]
-    type t = (Id.t, Environment.t);
+    type t = closure_environment_t;
 
     let wrap = (ei, map): t => (ei, map);
 
@@ -1100,15 +1018,7 @@ and ClosureEnvironment: {
 }
 and StepperFilterKind: {
   [@deriving (show({with_path: false}), sexp, yojson)]
-  type filter = {
-    pat: Exp.t,
-    act: FilterAction.t,
-  };
-
-  [@deriving (show({with_path: false}), sexp, yojson)]
-  type t =
-    | Filter(filter)
-    | Residue(int, FilterAction.t);
+  type t = stepper_filter_kind_t;
 
   let map_term:
     (
@@ -1127,17 +1037,9 @@ and StepperFilterKind: {
   let fast_equal: (t, t) => bool;
 } = {
   [@deriving (show({with_path: false}), sexp, yojson)]
-  type filter = {
-    pat: Exp.t,
-    act: FilterAction.t,
-  };
-
-  [@deriving (show({with_path: false}), sexp, yojson)]
-  type t =
-    | Filter(filter)
-    | Residue(int, FilterAction.t);
+  type t = stepper_filter_kind_t;
 
-  let map = (mapper, filter) => {
+  let map = (mapper, filter: t): t => {
     switch (filter) {
     | Filter({act, pat}) => Filter({act, pat: mapper(pat)})
     | Residue(idx, act) => Residue(idx, act)
@@ -1155,12 +1057,15 @@ and StepperFilterKind: {
       ) => {
     let exp_map_term =
       Exp.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any);
-    fun
-    | Filter({pat: e, act}) => Filter({pat: exp_map_term(e), act})
-    | Residue(i, a) => Residue(i, a);
+    (
+      fun
+      | Filter({pat: e, act}) => Filter({pat: exp_map_term(e), act})
+      | Residue(i, a) => Residue(i, a):
+        t => t
+    );
   };
 
-  let fast_equal = (f1, f2) =>
+  let fast_equal = (f1: t, f2: t) =>
     switch (f1, f2) {
     | (Filter({pat: e1, act: a1}), Filter({pat: e2, act: a2})) =>
       Exp.fast_equal(e1, e2) && a1 == a2
diff --git a/src/haz3lcore/zipper/Editor.re b/src/haz3lcore/zipper/Editor.re
index cd05476fd9..bdb3e014cc 100644
--- a/src/haz3lcore/zipper/Editor.re
+++ b/src/haz3lcore/zipper/Editor.re
@@ -8,7 +8,11 @@ module CachedStatics = {
   };
 
   let empty: t = {
-    term: UExp.{ids: [Id.invalid], copied: false, term: Tuple([])},
+    term: {
+      ids: [Id.invalid],
+      copied: false,
+      term: Tuple([]),
+    },
     info_map: Id.Map.empty,
     error_ids: [],
   };
diff --git a/src/haz3lcore/zipper/EditorUtil.re b/src/haz3lcore/zipper/EditorUtil.re
index ff59e48f55..23265f8a2a 100644
--- a/src/haz3lcore/zipper/EditorUtil.re
+++ b/src/haz3lcore/zipper/EditorUtil.re
@@ -1,50 +1,48 @@
 let rec append_exp = (e1: Exp.t, e2: Exp.t): Exp.t => {
-  Exp.(
-    switch (e1.term) {
-    | EmptyHole
-    | Invalid(_)
-    | MultiHole(_)
-    | DynamicErrorHole(_)
-    | FailedCast(_)
-    | Undefined
-    | Deferral(_)
-    | Bool(_)
-    | Int(_)
-    | Float(_)
-    | String(_)
-    | ListLit(_)
-    | Constructor(_)
-    | Closure(_)
-    | Fun(_)
-    | TypFun(_)
-    | FixF(_)
-    | Tuple(_)
-    | Var(_)
-    | Ap(_)
-    | TypAp(_)
-    | DeferredAp(_)
-    | If(_)
-    | Test(_)
-    | Parens(_)
-    | Cons(_)
-    | ListConcat(_)
-    | UnOp(_)
-    | BinOp(_)
-    | BuiltinFun(_)
-    | Cast(_)
-    | Match(_) => Exp.{ids: [Id.mk()], copied: false, term: Seq(e1, e2)}
-    | Seq(e11, e12) =>
-      let e12' = append_exp(e12, e2);
-      {ids: e1.ids, copied: false, term: Seq(e11, e12')};
-    | Filter(kind, ebody) =>
-      let ebody' = append_exp(ebody, e2);
-      {ids: e1.ids, copied: false, term: Filter(kind, ebody')};
-    | Let(p, edef, ebody) =>
-      let ebody' = append_exp(ebody, e2);
-      {ids: e1.ids, copied: false, term: Let(p, edef, ebody')};
-    | TyAlias(tp, tdef, ebody) =>
-      let ebody' = append_exp(ebody, e2);
-      {ids: e1.ids, copied: false, term: TyAlias(tp, tdef, ebody')};
-    }
-  );
+  switch (e1.term) {
+  | EmptyHole
+  | Invalid(_)
+  | MultiHole(_)
+  | DynamicErrorHole(_)
+  | FailedCast(_)
+  | Undefined
+  | Deferral(_)
+  | Bool(_)
+  | Int(_)
+  | Float(_)
+  | String(_)
+  | ListLit(_)
+  | Constructor(_)
+  | Closure(_)
+  | Fun(_)
+  | TypFun(_)
+  | FixF(_)
+  | Tuple(_)
+  | Var(_)
+  | Ap(_)
+  | TypAp(_)
+  | DeferredAp(_)
+  | If(_)
+  | Test(_)
+  | Parens(_)
+  | Cons(_)
+  | ListConcat(_)
+  | UnOp(_)
+  | BinOp(_)
+  | BuiltinFun(_)
+  | Cast(_)
+  | Match(_) => {ids: [Id.mk()], copied: false, term: Seq(e1, e2)}
+  | Seq(e11, e12) =>
+    let e12' = append_exp(e12, e2);
+    {ids: e1.ids, copied: false, term: Seq(e11, e12')};
+  | Filter(kind, ebody) =>
+    let ebody' = append_exp(ebody, e2);
+    {ids: e1.ids, copied: false, term: Filter(kind, ebody')};
+  | Let(p, edef, ebody) =>
+    let ebody' = append_exp(ebody, e2);
+    {ids: e1.ids, copied: false, term: Let(p, edef, ebody')};
+  | TyAlias(tp, tdef, ebody) =>
+    let ebody' = append_exp(ebody, e2);
+    {ids: e1.ids, copied: false, term: TyAlias(tp, tdef, ebody')};
+  };
 };
diff --git a/src/haz3lschool/Exercise.re b/src/haz3lschool/Exercise.re
index 2b3414e494..eda13f1942 100644
--- a/src/haz3lschool/Exercise.re
+++ b/src/haz3lschool/Exercise.re
@@ -908,23 +908,22 @@ module F = (ExerciseEnv: ExerciseEnv) => {
     hidden_tests: 'a,
   };
 
-  let wrap_filter = (act: FilterAction.action, term: UExp.t): UExp.t =>
-    Exp.{
-      term:
-        Exp.Filter(
-          Filter({
-            act: FilterAction.(act, One),
-            pat: {
-              term: Constructor("$e", Unknown(Internal) |> Typ.temp),
-              copied: false,
-              ids: [Id.mk()],
-            },
-          }),
-          term,
-        ),
-      copied: false,
-      ids: [Id.mk()],
-    };
+  let wrap_filter = (act: FilterAction.action, term: UExp.t): UExp.t => {
+    term:
+      Filter(
+        Filter({
+          act: FilterAction.(act, One),
+          pat: {
+            term: Constructor("$e", Unknown(Internal) |> Typ.temp),
+            copied: false,
+            ids: [Id.mk()],
+          },
+        }),
+        term,
+      ),
+    copied: false,
+    ids: [Id.mk()],
+  };
 
   let term_of = (editor: Editor.t): UExp.t =>
     MakeTerm.from_zip_for_sem(editor.state.zipper).term;
diff --git a/src/haz3lweb/Main.re b/src/haz3lweb/Main.re
index e0a77ae29b..d6c92d0927 100644
--- a/src/haz3lweb/Main.re
+++ b/src/haz3lweb/Main.re
@@ -4,8 +4,6 @@ open Haz3lweb;
 open Bonsai.Let_syntax;
 
 let scroll_to_caret = ref(true);
-let edit_action_applied = ref(true);
-let last_edit_action = ref(JsUtil.timestamp());
 
 let restart_caret_animation = () =>
   // necessary to trigger reflow
@@ -19,7 +17,7 @@ let restart_caret_animation = () =>
   | _ => ()
   };
 
-let apply = (model, action, ~schedule_action): Model.t => {
+let apply = (model, action, ~schedule_action, ~schedule_autosave): Model.t => {
   restart_caret_animation();
 
   let get_settings = (model: Model.t): Settings.t => model.settings;
@@ -85,16 +83,6 @@ let apply = (model, action, ~schedule_action): Model.t => {
   };
 };
 
-let app =
-  Bonsai.state_machine0(
-    (module Model),
-    (module Update),
-    ~apply_action=
-      (~inject, ~schedule_event) =>
-        apply(~schedule_action=x => schedule_event(inject(x))),
-    ~default_model=Model.load(Model.blank),
-  );
-
 /* This subcomponent is used to run an effect once when the app starts up,
    After the first draw */
 let on_startup = effect => {
@@ -112,31 +100,44 @@ let on_startup = effect => {
 };
 
 let view = {
-  let%sub app = app;
+  let%sub save_scheduler = BonsaiUtil.Alarm.alarm;
+  let%sub app =
+    Bonsai.state_machine1(
+      (module Model),
+      (module Update),
+      ~apply_action=
+        (~inject, ~schedule_event, input) => {
+          let schedule_action = x => schedule_event(inject(x));
+          let schedule_autosave = action =>
+            switch (input) {
+            | Active((_, alarm_inject)) =>
+              schedule_event(alarm_inject(action))
+            | Inactive => ()
+            };
+          apply(~schedule_action, ~schedule_autosave);
+        },
+      ~default_model=Model.load(Model.blank),
+      save_scheduler,
+    );
   let%sub () = {
     on_startup(
       Bonsai.Value.map(~f=((_model, inject)) => inject(Startup), app),
     );
   };
-  let%sub after_display = {
-    let%arr (_model, inject) = app;
-    if (scroll_to_caret.contents) {
-      scroll_to_caret := false;
-      JsUtil.scroll_cursor_into_view_if_needed();
-    };
-    if (edit_action_applied^
-        && JsUtil.timestamp()
-        -. last_edit_action^ > 1000.0) {
-      /* If an edit action has been applied, but no other edit action
-         has been applied for 1 second, save the model. */
-      edit_action_applied := false;
-      print_endline("Saving...");
-      inject(Update.Save);
-    } else {
-      Ui_effect.Ignore;
-    };
+  let after_display = {
+    Bonsai.Effect.of_sync_fun(
+      () =>
+        if (scroll_to_caret.contents) {
+          scroll_to_caret := false;
+          JsUtil.scroll_cursor_into_view_if_needed();
+        },
+      (),
+    );
   };
-  let%sub () = Bonsai.Edge.after_display(after_display);
+  let save_effect = Bonsai.Value.map(~f=((_, g)) => g(Update.Save), app);
+  let%sub () = BonsaiUtil.Alarm.listen(save_scheduler, ~event=save_effect);
+  let%sub () =
+    Bonsai.Edge.after_display(after_display |> Bonsai.Value.return);
   let%arr (model, inject) = app;
   Haz3lweb.Page.view(~inject, model);
 };
diff --git a/src/haz3lweb/Update.re b/src/haz3lweb/Update.re
index ddf2853646..b5e9b99580 100644
--- a/src/haz3lweb/Update.re
+++ b/src/haz3lweb/Update.re
@@ -518,7 +518,9 @@ let apply = (model: Model.t, update: t, ~schedule_action): Result.t(Model.t) =>
     | DebugConsole(key) =>
       DebugConsole.print(model, key);
       Ok(model);
-    | Save => Model.save_and_return(model)
+    | Save =>
+      print_endline("Saving...");
+      Model.save_and_return(model);
     | InitImportAll(file) =>
       JsUtil.read_file(file, data => schedule_action(FinishImportAll(data)));
       Ok(model);
diff --git a/src/haz3lweb/dune b/src/haz3lweb/dune
index d3e42ec636..e2792b76b8 100644
--- a/src/haz3lweb/dune
+++ b/src/haz3lweb/dune
@@ -8,6 +8,8 @@
 (library
  (name workerServer)
  (modules WorkerServer)
+ (instrumentation
+  (backend bisect_ppx))
  (libraries
   bonsai
   bonsai.web
@@ -29,6 +31,8 @@
 
 (library
  (name haz3lweb)
+ (instrumentation
+  (backend bisect_ppx))
  (modules
   (:standard \ Main)
   \
@@ -55,7 +59,8 @@
    ppx_let
    ppx_sexp_conv
    ppx_deriving.show
-   ppx_yojson_conv)))
+   ppx_yojson_conv
+   bonsai.ppx_bonsai)))
 
 (executable
  (name main)
diff --git a/src/haz3lweb/view/Cell.re b/src/haz3lweb/view/Cell.re
index 166e8bd200..ffec6fe5b8 100644
--- a/src/haz3lweb/view/Cell.re
+++ b/src/haz3lweb/view/Cell.re
@@ -435,7 +435,7 @@ let locked =
           statics.info_map,
           statics.term,
         )
-      : DHExp.Bool(true) |> DHExp.fresh;
+      : Bool(true) |> DHExp.fresh;
   let elab: Elaborator.Elaboration.t = {d: elab};
   let result: ModelResult.t =
     settings.core.dynamics
diff --git a/src/haz3lweb/view/ExplainThis.re b/src/haz3lweb/view/ExplainThis.re
index 5dad22abb5..3ab1065785 100644
--- a/src/haz3lweb/view/ExplainThis.re
+++ b/src/haz3lweb/view/ExplainThis.re
@@ -534,7 +534,7 @@ let get_doc =
             (term)
             : (list(Node.t), (list(Node.t), ColorSteps.t), list(Node.t)) =>
       switch ((term: Exp.term)) {
-      | Exp.Invalid(_) => simple("Not a valid expression")
+      | Invalid(_) => simple("Not a valid expression")
       | DynamicErrorHole(_)
       | FailedCast(_)
       | Closure(_)
@@ -1981,7 +1981,7 @@ let get_doc =
           doc,
         );
       switch (tl.term) {
-      | Pat.Cons(hd2, tl2) =>
+      | Cons(hd2, tl2) =>
         if (ListPat.cons2_pat.id == get_specificity_level(ListPat.cons2)) {
           let hd2_id = List.nth(hd2.ids, 0);
           let tl2_id = List.nth(tl2.ids, 0);
@@ -2202,7 +2202,7 @@ let get_doc =
           doc,
         );
       switch (result.term) {
-      | Typ.Arrow(arg2, result2) =>
+      | Arrow(arg2, result2) =>
         if (ArrowTyp.arrow3_typ.id == get_specificity_level(ArrowTyp.arrow3)) {
           let arg2_id = List.nth(arg2.ids, 0);
           let result2_id = List.nth(result2.ids, 0);
diff --git a/src/haz3lweb/view/Type.re b/src/haz3lweb/view/Type.re
index 622dcf766e..82dfd0a9e3 100644
--- a/src/haz3lweb/view/Type.re
+++ b/src/haz3lweb/view/Type.re
@@ -21,7 +21,7 @@ let rec view_ty = (~strip_outer_parens=false, ty: Haz3lcore.Typ.t): Node.t =>
     div(
       ~attrs=[
         clss(["typ-view", "atom", "unknown"]),
-        Attr.title(Typ.show_type_provenance(prov)),
+        Attr.title(TermBase.show_type_provenance(prov)),
       ],
       [text("?") /*, prov_view(prov)*/],
     )
@@ -98,7 +98,7 @@ let rec view_ty = (~strip_outer_parens=false, ty: Haz3lcore.Typ.t): Node.t =>
     div(
       ~attrs=[
         clss(["typ-view", "atom", "unknown"]),
-        Attr.title(Typ.show_type_provenance(Internal)),
+        Attr.title(TermBase.show_type_provenance(Internal)),
       ],
       [text("?") /*, prov_view(prov)*/],
     )
diff --git a/src/pretty/dune b/src/pretty/dune
index 868d03defc..c131965aff 100644
--- a/src/pretty/dune
+++ b/src/pretty/dune
@@ -3,6 +3,8 @@
 (library
  (name pretty)
  (libraries util sexplib)
+ (instrumentation
+  (backend bisect_ppx))
  (preprocess
   (pps ppx_let ppx_sexp_conv)))
 
diff --git a/src/util/BonsaiUtil.re b/src/util/BonsaiUtil.re
new file mode 100644
index 0000000000..127172ce21
--- /dev/null
+++ b/src/util/BonsaiUtil.re
@@ -0,0 +1,42 @@
+open Core;
+open Bonsai;
+open Bonsai.Let_syntax;
+
+module Alarm = {
+  module Action = {
+    [@deriving sexp]
+    type t =
+      | SetAlarm(Time_ns.Alternate_sexp.t)
+      | SnoozeAlarm(Time_ns.Alternate_sexp.t)
+      | UnsetAlarm;
+  };
+
+  let alarm =
+    state_machine0(
+      (module Time_ns.Alternate_sexp),
+      (module Action),
+      ~default_model=Time_ns.max_value_representable,
+      ~apply_action=(~inject as _, ~schedule_event as _, model, action) => {
+      switch (action) {
+      | SetAlarm(time) => time
+      | SnoozeAlarm(time) => Time_ns.max(time, model)
+      | UnsetAlarm => Time_ns.max_value_representable
+      }
+    });
+
+  let listen = (alarm, ~event) => {
+    let%sub before_or_after = Clock.at(alarm |> Value.map(~f=fst));
+    Edge.on_change(
+      (module Clock.Before_or_after),
+      before_or_after,
+      ~callback={
+        open Clock.Before_or_after;
+        let%map (_, inject) = alarm
+        and event = event;
+        fun
+        | After => Effect.Many([inject(Action.UnsetAlarm), event])
+        | Before => Effect.Ignore;
+      },
+    );
+  };
+};
diff --git a/src/util/ListUtil.re b/src/util/ListUtil.re
index 9c6bed90b0..8481df4f0a 100644
--- a/src/util/ListUtil.re
+++ b/src/util/ListUtil.re
@@ -1,12 +1,5 @@
 let rev_if = (b: bool) => b ? List.rev : Fun.id;
 
-let dedup = xs =>
-  List.fold_right(
-    (x, deduped) => List.mem(x, deduped) ? deduped : [x, ...deduped],
-    xs,
-    [],
-  );
-
 let dedup_f = (f, xs) =>
   List.fold_right(
     (x, deduped) => List.exists(f(x), deduped) ? deduped : [x, ...deduped],
@@ -14,9 +7,22 @@ let dedup_f = (f, xs) =>
     [],
   );
 
-let are_duplicates = xs =>
-  List.length(List.sort_uniq(compare, xs)) == List.length(xs);
+let dedup = xs => dedup_f((==), xs);
 
+/**
+  Groups elements of a list by a specified key.
+
+ {b Note: The groups are not guaranteed to preserve the order of elements from the original list. }
+
+  @param key
+  The key function used to determine the grouping key.
+
+  @param xs
+  The list of elements to be grouped.
+
+  @return
+  A list of tuples where each tuple contains the grouping key and a list of elements that belong to that group.
+*/
 let group_by = (key: 'x => 'k, xs: list('x)): list(('k, list('x))) =>
   List.fold_left(
     (grouped, x) => {
@@ -32,7 +38,7 @@ let group_by = (key: 'x => 'k, xs: list('x)): list(('k, list('x))) =>
     xs,
   );
 
-let rec range = (~lo=0, hi) =>
+let rec range = (~lo: int=0, hi: int) =>
   if (lo > hi) {
     raise(Invalid_argument("ListUtil.range"));
   } else if (lo == hi) {
@@ -171,7 +177,15 @@ let split_sublist_opt =
 let split_sublist =
     (i: int, j: int, xs: list('x)): (list('x), list('x), list('x)) =>
   switch (split_sublist_opt(i, j, xs)) {
-  | None => raise(Invalid_argument("ListUtil.split_sublist"))
+  | None =>
+    raise(
+      Invalid_argument(
+        "ListUtil.split_sublist: "
+        ++ string_of_int(i)
+        ++ ", "
+        ++ string_of_int(j),
+      ),
+    )
   | Some(r) => r
   };
 let sublist = ((i, j), xs: list('x)): list('x) => {
diff --git a/src/util/Util.re b/src/util/Util.re
index c901907b60..2c7f084100 100644
--- a/src/util/Util.re
+++ b/src/util/Util.re
@@ -1,4 +1,5 @@
 module Aba = Aba;
+module BonsaiUtil = BonsaiUtil;
 module Direction = Direction;
 module Either = Either;
 module IntMap = IntMap;
diff --git a/src/util/dune b/src/util/dune
index a3494db579..f50e6ac0f7 100644
--- a/src/util/dune
+++ b/src/util/dune
@@ -2,13 +2,16 @@
  (name util)
  (libraries re base ptmap bonsai bonsai.web virtual_dom yojson)
  (js_of_ocaml)
+ (instrumentation
+  (backend bisect_ppx))
  (preprocess
   (pps
    ppx_yojson_conv
    js_of_ocaml-ppx
    ppx_let
    ppx_sexp_conv
-   ppx_deriving.show)))
+   ppx_deriving.show
+   bonsai.ppx_bonsai)))
 
 (env
  (dev
diff --git a/test/Test_Elaboration.re b/test/Test_Elaboration.re
index 2516f25227..c515487535 100644
--- a/test/Test_Elaboration.re
+++ b/test/Test_Elaboration.re
@@ -180,6 +180,15 @@ let let_fun = () =>
 let deferral = () =>
   alco_check(
     "string_sub(\"hello\", 1, _)",
+    DeferredAp(
+      Var("string_sub") |> Exp.fresh,
+      [
+        String("hello") |> Exp.fresh,
+        Int(1) |> Exp.fresh,
+        Deferral(InAp) |> Exp.fresh,
+      ],
+    )
+    |> Exp.fresh,
     dhexp_of_uexp(
       DeferredAp(
         Var("string_sub") |> Exp.fresh,
@@ -191,7 +200,13 @@ let deferral = () =>
       )
       |> Exp.fresh,
     ),
-    dhexp_of_uexp(
+  );
+
+let ap_deferral_single_argument = () =>
+  alco_check(
+    "string_sub(\"hello\", 1, _)(2)",
+    Ap(
+      Forward,
       DeferredAp(
         Var("string_sub") |> Exp.fresh,
         [
@@ -201,6 +216,106 @@ let deferral = () =>
         ],
       )
       |> Exp.fresh,
+      Int(2) |> Exp.fresh,
+    )
+    |> Exp.fresh,
+    dhexp_of_uexp(
+      Ap(
+        Forward,
+        DeferredAp(
+          Var("string_sub") |> Exp.fresh,
+          [
+            String("hello") |> Exp.fresh,
+            Int(1) |> Exp.fresh,
+            Deferral(InAp) |> Exp.fresh,
+          ],
+        )
+        |> Exp.fresh,
+        Int(2) |> Exp.fresh,
+      )
+      |> Exp.fresh,
+    ),
+  );
+
+let ap_of_deferral_of_hole = () =>
+  alco_check(
+    "?(_, _, 3)(1., true)",
+    Ap(
+      Forward,
+      DeferredAp(
+        Cast(
+          Cast(
+            EmptyHole |> Exp.fresh,
+            Unknown(Internal) |> Typ.fresh,
+            Arrow(
+              Unknown(Internal) |> Typ.fresh,
+              Unknown(Internal) |> Typ.fresh,
+            )
+            |> Typ.fresh,
+          )
+          |> Exp.fresh,
+          Arrow(
+            Unknown(Internal) |> Typ.fresh,
+            Unknown(Internal) |> Typ.fresh,
+          )
+          |> Typ.fresh,
+          Arrow(
+            Prod([
+              Unknown(Internal) |> Typ.fresh,
+              Unknown(Internal) |> Typ.fresh,
+              Unknown(Internal) |> Typ.fresh,
+            ])
+            |> Typ.fresh,
+            Unknown(Internal) |> Typ.fresh,
+          )
+          |> Typ.fresh,
+        )
+        |> Exp.fresh,
+        [
+          Deferral(InAp) |> Exp.fresh,
+          Deferral(InAp) |> Exp.fresh,
+          Cast(
+            Int(3) |> Exp.fresh,
+            Int |> Typ.fresh,
+            Unknown(Internal) |> Typ.fresh,
+          )
+          |> Exp.fresh,
+        ],
+      )
+      |> Exp.fresh,
+      Tuple([
+        Cast(
+          Float(1.) |> Exp.fresh,
+          Float |> Typ.fresh,
+          Unknown(Internal) |> Typ.fresh,
+        )
+        |> Exp.fresh,
+        Cast(
+          Bool(true) |> Exp.fresh,
+          Bool |> Typ.fresh,
+          Unknown(Internal) |> Typ.fresh,
+        )
+        |> Exp.fresh,
+      ])
+      |> Exp.fresh,
+    )
+    |> Exp.fresh,
+    dhexp_of_uexp(
+      Ap(
+        Forward,
+        DeferredAp(
+          EmptyHole |> Exp.fresh,
+          [
+            Deferral(InAp) |> Exp.fresh,
+            Deferral(InAp) |> Exp.fresh,
+            Int(3) |> Exp.fresh,
+          ],
+        )
+        |> Exp.fresh,
+        Tuple([Float(1.) |> Exp.fresh, Bool(true) |> Exp.fresh])
+        |> Exp.fresh,
+      )
+      |> Exp.fresh,
     ),
   );
 
@@ -220,4 +335,14 @@ let elaboration_tests = [
     `Quick,
     deferral,
   ),
+  test_case(
+    "Function application with a single remaining argument after deferral",
+    `Quick,
+    ap_deferral_single_argument,
+  ),
+  test_case(
+    "Function application with a deferral of a hole",
+    `Quick,
+    ap_of_deferral_of_hole,
+  ),
 ];
diff --git a/test/Test_Evaluator.re b/test/Test_Evaluator.re
index fc159425b2..37fcaba764 100644
--- a/test/Test_Evaluator.re
+++ b/test/Test_Evaluator.re
@@ -2,22 +2,6 @@ open Alcotest;
 open Haz3lcore;
 let dhexp_typ = testable(Fmt.using(Exp.show, Fmt.string), DHExp.fast_equal);
 
-let ids = List.init(12, _ => Id.mk());
-let id_at = x => x |> List.nth(ids);
-let statics = Statics.mk(CoreSettings.on, Builtins.ctx_init);
-
-// Get the type from the statics
-let type_of = f => {
-  let s = statics(f);
-  switch (Id.Map.find(IdTagged.rep_id(f), s)) {
-  | InfoExp({ty, _}) => Some(ty)
-  | _ => None
-  };
-};
-
-let int_evaluation =
-  Evaluator.evaluate(Builtins.env_init, {d: Exp.Int(8) |> Exp.fresh});
-
 let evaluation_test = (msg, expected, unevaluated) =>
   check(
     dhexp_typ,
@@ -38,7 +22,156 @@ let test_sum = () =>
     BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh) |> Exp.fresh,
   );
 
+let test_function_application = () =>
+  evaluation_test(
+    "float_of_int(1)",
+    Float(1.0) |> Exp.fresh,
+    Ap(Forward, Var("float_of_int") |> Exp.fresh, Int(1) |> Exp.fresh)
+    |> Exp.fresh,
+  );
+
+let test_function_deferral = () =>
+  evaluation_test(
+    "string_sub(\"hello\", 1, _)(2)",
+    String("el") |> Exp.fresh,
+    Ap(
+      Forward,
+      DeferredAp(
+        Var("string_sub") |> Exp.fresh,
+        [
+          String("hello") |> Exp.fresh,
+          Int(1) |> Exp.fresh,
+          Deferral(InAp) |> Exp.fresh,
+        ],
+      )
+      |> Exp.fresh,
+      Int(2) |> Exp.fresh,
+    )
+    |> Exp.fresh,
+  );
+
+let tet_ap_of_hole_deferral = () =>
+  evaluation_test(
+    "?(_, _, 3)(1., true)",
+    Ap(
+      Forward,
+      Cast(
+        Cast(
+          EmptyHole |> Exp.fresh,
+          Unknown(Internal) |> Typ.fresh,
+          Arrow(
+            Unknown(Internal) |> Typ.fresh,
+            Unknown(Internal) |> Typ.fresh,
+          )
+          |> Typ.fresh,
+        )
+        |> Exp.fresh,
+        Arrow(
+          Unknown(Internal) |> Typ.fresh,
+          Unknown(Internal) |> Typ.fresh,
+        )
+        |> Typ.fresh,
+        Arrow(
+          Prod([
+            Unknown(Internal) |> Typ.fresh,
+            Unknown(Internal) |> Typ.fresh,
+            Unknown(Internal) |> Typ.fresh,
+          ])
+          |> Typ.fresh,
+          Unknown(Internal) |> Typ.fresh,
+        )
+        |> Typ.fresh,
+      )
+      |> Exp.fresh,
+      Tuple([
+        Cast(
+          Float(1.) |> Exp.fresh,
+          Float |> Typ.fresh,
+          Unknown(Internal) |> Typ.fresh,
+        )
+        |> Exp.fresh,
+        Cast(
+          Bool(true) |> Exp.fresh,
+          Bool |> Typ.fresh,
+          Unknown(Internal) |> Typ.fresh,
+        )
+        |> Exp.fresh,
+        Cast(
+          Int(3) |> Exp.fresh,
+          Int |> Typ.fresh,
+          Unknown(Internal) |> Typ.fresh,
+        )
+        |> Exp.fresh,
+      ])
+      |> Exp.fresh,
+    )
+    |> Exp.fresh,
+    Ap(
+      Forward,
+      DeferredAp(
+        Cast(
+          Cast(
+            EmptyHole |> Exp.fresh,
+            Unknown(Internal) |> Typ.fresh,
+            Arrow(
+              Unknown(Internal) |> Typ.fresh,
+              Unknown(Internal) |> Typ.fresh,
+            )
+            |> Typ.fresh,
+          )
+          |> Exp.fresh,
+          Arrow(
+            Unknown(Internal) |> Typ.fresh,
+            Unknown(Internal) |> Typ.fresh,
+          )
+          |> Typ.fresh,
+          Arrow(
+            Prod([
+              Unknown(Internal) |> Typ.fresh,
+              Unknown(Internal) |> Typ.fresh,
+              Unknown(Internal) |> Typ.fresh,
+            ])
+            |> Typ.fresh,
+            Unknown(Internal) |> Typ.fresh,
+          )
+          |> Typ.fresh,
+        )
+        |> Exp.fresh,
+        [
+          Deferral(InAp) |> Exp.fresh,
+          Deferral(InAp) |> Exp.fresh,
+          Cast(
+            Int(3) |> Exp.fresh,
+            Int |> Typ.fresh,
+            Unknown(Internal) |> Typ.fresh,
+          )
+          |> Exp.fresh,
+        ],
+      )
+      |> Exp.fresh,
+      Tuple([
+        Cast(
+          Float(1.) |> Exp.fresh,
+          Float |> Typ.fresh,
+          Unknown(Internal) |> Typ.fresh,
+        )
+        |> Exp.fresh,
+        Cast(
+          Bool(true) |> Exp.fresh,
+          Bool |> Typ.fresh,
+          Unknown(Internal) |> Typ.fresh,
+        )
+        |> Exp.fresh,
+      ])
+      |> Exp.fresh,
+    )
+    |> Exp.fresh,
+  );
+
 let tests = [
   test_case("Integer literal", `Quick, test_int),
   test_case("Integer sum", `Quick, test_sum),
+  test_case("Function application", `Quick, test_function_application),
+  test_case("Function deferral", `Quick, test_function_deferral),
+  test_case("Deferral applied to hole", `Quick, tet_ap_of_hole_deferral),
 ];
diff --git a/test/Test_ListUtil.re b/test/Test_ListUtil.re
new file mode 100644
index 0000000000..9abfca4f07
--- /dev/null
+++ b/test/Test_ListUtil.re
@@ -0,0 +1,610 @@
+open Alcotest;
+open Util;
+
+let tests = (
+  "ListUtil",
+  [
+    test_case(
+      "rev_if with false",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3];
+        check(list(int), "Same list", xs, ListUtil.rev_if(false, xs));
+      },
+    ),
+    test_case(
+      "rev_if with true",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3];
+        check(
+          list(int),
+          "Reversed list",
+          [3, 2, 1],
+          ListUtil.rev_if(true, xs),
+        );
+      },
+    ),
+    test_case(
+      "dedup",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 2];
+        check(list(int), "Unique list", [1, 3, 2], ListUtil.dedup(xs)); // TODO: Interesting the order here is messed up because of fold_right
+      },
+    ),
+    test_case(
+      "dedup_f",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 2];
+        check(
+          list(int),
+          "Unique list",
+          [1, 3, 2],
+          ListUtil.dedup_f((==), xs),
+        ); // TODO: Interesting the order here is messed up because of fold_right
+      },
+    ),
+    test_case(
+      "group_by with constant function preserves list",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 4, 5];
+        check(
+          list(pair(unit, list(int))),
+          "singleton group",
+          [((), List.rev(xs))],
+          ListUtil.group_by(__ => (), xs),
+        );
+      },
+    ),
+    test_case(
+      "group_by groups into evens/odds",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 4, 5];
+        check(
+          list(pair(int, list(int))),
+          "odds and evens",
+          [(1, [5, 3, 1]), (0, [4, 2])],
+          ListUtil.group_by(x => x mod 2, xs),
+        );
+      },
+    ),
+    test_case("range generates sequential integers [1,6)", `Quick, () => {
+      check(list(int), "1-5", [1, 2, 3, 4, 5], ListUtil.range(~lo=1, 6))
+    }),
+    test_case("range defaults lower bound to 0", `Quick, () => {
+      check(list(int), "0-5", [0, 1, 2, 3, 4, 5], ListUtil.range(6))
+    }),
+    test_case("range lo = hi is empty", `Quick, () => {
+      check(list(int), "empty list", [], ListUtil.range(~lo=1, 1))
+    }),
+    test_case("Invalid range raises error", `Quick, () => {
+      check_raises(
+        "Invalid range",
+        Invalid_argument("ListUtil.range"),
+        () => {
+          let _ = ListUtil.range(~lo=2, 1);
+          ();
+        },
+      )
+    }),
+    test_case(
+      "mk_frame creates a frame from the beginning",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 4, 5];
+        check(
+          pair(list(int), list(int)),
+          "frame",
+          ([], xs),
+          ListUtil.mk_frame(0, xs),
+        );
+      },
+    ),
+    test_case(
+      "mk_frame creates a frame from the end",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 4, 5];
+        check(
+          pair(list(int), list(int)),
+          "frame",
+          (List.rev(xs), []),
+          ListUtil.mk_frame(5, xs),
+        );
+      },
+    ),
+    test_case(
+      "mk_frame raises when making a frame past the end",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 4, 5];
+        check_raises(
+          "raises invalid argument",
+          Invalid_argument("ListUtil.mk_frame"),
+          () => {
+            let _ = ListUtil.mk_frame(6, xs);
+            ();
+          },
+        );
+      },
+    ),
+    test_case(
+      "mk_frame raises when making a frame before the beginning",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 4, 5];
+        check_raises(
+          "raises invalid argument",
+          Invalid_argument("ListUtil.mk_frame"),
+          () => {
+            let _ = ListUtil.mk_frame(-1, xs);
+            ();
+          },
+        );
+      },
+    ),
+    test_case(
+      "mk_frame makes a frame splitting the list",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 4, 5];
+        check(
+          pair(list(int), list(int)),
+          "frame",
+          (List.rev([1, 2, 3]), [4, 5]),
+          ListUtil.mk_frame(3, xs),
+        );
+      },
+    ),
+    test_case(
+      "mk_frame makes a frame splitting the list",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 4, 5];
+        check(
+          pair(list(int), list(int)),
+          "frame",
+          (List.rev([1, 2, 3]), [4, 5]),
+          ListUtil.mk_frame(3, xs),
+        );
+      },
+    ),
+    test_case(
+      "split with no found element returns the original list",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 4, 5];
+        check(
+          triple(list(int), option(int), list(int)),
+          "split",
+          (xs, None, []),
+          ListUtil.split(xs, __ => false),
+        );
+      },
+    ),
+    test_case(
+      "split with first found returns the head and tail",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 4, 5];
+        check(
+          triple(list(int), option(int), list(int)),
+          "split",
+          ([], Some(1), [2, 3, 4, 5]),
+          ListUtil.split(xs, __ => true),
+        );
+      },
+    ),
+    test_case(
+      "splits on the middle element",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 4, 5];
+        check(
+          triple(list(int), option(int), list(int)),
+          "split",
+          ([1, 2], Some(3), [4, 5]),
+          ListUtil.split(xs, (==)(3)),
+        );
+      },
+    ),
+    test_case(
+      "combine_opt",
+      `Quick,
+      () => {
+        check(
+          option(list(pair(string, int))),
+          "Same size lists",
+          Some([("a", 1), ("b", 2), ("c", 3)]),
+          ListUtil.combine_opt(["a", "b", "c"], [1, 2, 3]),
+        );
+        check(
+          option(list(pair(string, int))),
+          "Empty Lists",
+          Some([]),
+          ListUtil.combine_opt([], []),
+        );
+        check(
+          option(list(pair(string, int))),
+          "Inconsistent size lists",
+          None,
+          ListUtil.combine_opt(["a"], [1, 2]),
+        );
+      },
+    ),
+    test_case(
+      "is_empty with empty list",
+      `Quick,
+      () => {
+        let xs = [];
+        check(bool, "Returns true", true, ListUtil.is_empty(xs));
+      },
+    ),
+    test_case(
+      "is_empty with non-empty list",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3];
+        check(bool, "Returns false", false, ListUtil.is_empty(xs));
+      },
+    ),
+    test_case(
+      "flat_map with empty list",
+      `Quick,
+      () => {
+        let xs = [];
+        let f = x => [x, x];
+        check(list(int), "Empty list", [], ListUtil.flat_map(f, xs));
+      },
+    ),
+    test_case(
+      "flat_map with non-empty list",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3];
+        let f = x => [x, x];
+        check(
+          list(int),
+          "Doubled list",
+          [1, 1, 2, 2, 3, 3],
+          ListUtil.flat_map(f, xs),
+        );
+      },
+    ),
+    test_case(
+      "flat_map with non-empty list and empty result",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3];
+        let f = _ => [];
+        check(list(int), "Empty list", [], ListUtil.flat_map(f, xs));
+      },
+    ),
+    test_case(
+      "join with empty list",
+      `Quick,
+      () => {
+        let xs = [];
+        check(list(string), "Empty list", ListUtil.join(",", xs), []);
+      },
+    ),
+    test_case(
+      "join with single element list",
+      `Quick,
+      () => {
+        let xs = ["a"];
+        check(
+          list(string),
+          "Single element list",
+          ListUtil.join(",", xs),
+          ["a"],
+        );
+      },
+    ),
+    test_case(
+      "join with multiple element list",
+      `Quick,
+      () => {
+        let xs = ["a", "b", "c"];
+        check(
+          list(string),
+          "Multiple element list",
+          ListUtil.join(",", xs),
+          ["a", ",", "b", ",", "c"],
+        );
+      },
+    ),
+    test_case(
+      "hd_opt with empty list",
+      `Quick,
+      () => {
+        let xs = [];
+        check(option(int), "None", None, ListUtil.hd_opt(xs));
+      },
+    ),
+    test_case(
+      "hd_opt with non-empty list",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3];
+        check(option(int), "Some", Some(1), ListUtil.hd_opt(xs));
+      },
+    ),
+    test_case(
+      "nth_opt with empty list",
+      `Quick,
+      () => {
+        let xs = [];
+        check(option(int), "None", None, ListUtil.nth_opt(0, xs));
+      },
+    ),
+    test_case(
+      "nth_opt with non-empty list",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3];
+        check(option(int), "Some", Some(2), ListUtil.nth_opt(1, xs));
+      },
+    ),
+    test_case(
+      "nth_opt with out of bounds index",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3];
+        check(option(int), "None", None, ListUtil.nth_opt(3, xs));
+      },
+    ),
+    test_case(
+      "split_n_opt with empty list",
+      `Quick,
+      () => {
+        let xs = [];
+        check(
+          option(pair(list(int), list(int))),
+          "Empty list",
+          Some(([], [])),
+          ListUtil.split_n_opt(0, xs),
+        );
+      },
+    ),
+    test_case(
+      "split_n_opt with non-empty list",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 4, 5];
+        check(
+          option(pair(list(int), list(int))),
+          "Split list",
+          Some(([1, 2, 3], [4, 5])),
+          ListUtil.split_n_opt(3, xs),
+        );
+      },
+    ),
+    test_case(
+      "split_n_opt with out of bounds index",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 4, 5];
+        check(
+          option(pair(list(int), list(int))),
+          "None",
+          None,
+          ListUtil.split_n_opt(6, xs),
+        );
+      },
+    ),
+    test_case(
+      "split_n_opt with zero index",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 4, 5];
+        check(
+          option(pair(list(int), list(int))),
+          "Empty first part",
+          Some(([], xs)),
+          ListUtil.split_n_opt(0, xs),
+        );
+      },
+    ),
+    test_case(
+      "split_n with empty list",
+      `Quick,
+      () => {
+        let xs = [];
+        check(
+          pair(list(int), list(int)),
+          "Empty list",
+          ([], []),
+          ListUtil.split_n(0, xs),
+        );
+      },
+    ),
+    test_case(
+      "split_n with non-empty list",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 4, 5];
+        check(
+          pair(list(int), list(int)),
+          "Split list",
+          ([1, 2, 3], [4, 5]),
+          ListUtil.split_n(3, xs),
+        );
+      },
+    ),
+    test_case(
+      "split_n with out of bounds index",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 4, 5];
+        check_raises(
+          "raises invalid argument",
+          Invalid_argument("ListUtil.split_n: 6"),
+          () => {
+            let _ = ListUtil.split_n(6, xs);
+            ();
+          },
+        );
+      },
+    ),
+    test_case(
+      "split_n with zero index",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 4, 5];
+        check(
+          pair(list(int), list(int)),
+          "Empty first part",
+          ([], xs),
+          ListUtil.split_n(0, xs),
+        );
+      },
+    ),
+    test_case(
+      "split_sublist_opt with empty list",
+      `Quick,
+      () => {
+        let xs = [];
+        check(
+          option(triple(list(int), list(int), list(int))),
+          "Empty list",
+          Some(([], [], [])),
+          ListUtil.split_sublist_opt(0, 0, xs),
+        );
+      },
+    ),
+    test_case(
+      "split_sublist_opt with non-empty list",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 4, 5];
+        check(
+          option(triple(list(int), list(int), list(int))),
+          "Split list",
+          Some(([1, 2], [3, 4], [5])),
+          ListUtil.split_sublist_opt(2, 4, xs),
+        );
+      },
+    ),
+    test_case(
+      "split_sublist_opt with out of bounds index",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 4, 5];
+        check(
+          option(triple(list(int), list(int), list(int))),
+          "None",
+          None,
+          ListUtil.split_sublist_opt(6, 7, xs),
+        );
+      },
+    ),
+    test_case(
+      "split_sublist_opt with zero index",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 4, 5];
+        check(
+          option(triple(list(int), list(int), list(int))),
+          "Empty first part",
+          Some(([], [], xs)),
+          ListUtil.split_sublist_opt(0, 0, xs),
+        );
+      },
+    ),
+    test_case(
+      "split_sublist with empty list",
+      `Quick,
+      () => {
+        let xs = [];
+        check(
+          triple(list(int), list(int), list(int)),
+          "Empty list",
+          ([], [], []),
+          ListUtil.split_sublist(0, 0, xs),
+        );
+      },
+    ),
+    test_case(
+      "split_sublist with non-empty list",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 4, 5];
+        check(
+          triple(list(int), list(int), list(int)),
+          "Split list",
+          ([1, 2], [3, 4], [5]),
+          ListUtil.split_sublist(2, 4, xs),
+        );
+      },
+    ),
+    test_case(
+      "split_sublist with out of bounds index",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 4, 5];
+        check_raises(
+          "raises invalid argument",
+          Invalid_argument("ListUtil.split_sublist: 6, 7"),
+          () => {
+            let _ = ListUtil.split_sublist(6, 7, xs);
+            ();
+          },
+        );
+      },
+    ),
+    test_case(
+      "split_sublist with zero index",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 4, 5];
+        check(
+          triple(list(int), list(int), list(int)),
+          "Empty first part",
+          ([], [], xs),
+          ListUtil.split_sublist(0, 0, xs),
+        );
+      },
+    ),
+    test_case(
+      "sublist with empty list",
+      `Quick,
+      () => {
+        let xs = [];
+        check(list(int), "Empty list", [], ListUtil.sublist((0, 0), xs));
+      },
+    ),
+    test_case(
+      "sublist with non-empty list",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 4, 5];
+        check(
+          list(int),
+          "Sublist",
+          [2, 3, 4],
+          ListUtil.sublist((1, 4), xs),
+        );
+      },
+    ),
+    test_case(
+      "sublist with out of bounds index",
+      `Quick,
+      () => {
+        let xs = [1, 2, 3, 4, 5];
+        check_raises(
+          "raises invalid argument",
+          Invalid_argument("ListUtil.split_sublist: 6, 7"),
+          () => {
+            let _ = ListUtil.sublist((6, 7), xs);
+            ();
+          },
+        );
+      },
+    ),
+  ],
+);
diff --git a/test/Test_MakeTerm.re b/test/Test_MakeTerm.re
new file mode 100644
index 0000000000..46818664a9
--- /dev/null
+++ b/test/Test_MakeTerm.re
@@ -0,0 +1,82 @@
+/**
+ * This file contains tests to validate the `MakeTerm` module's ability to convert
+ * zippers into expressions.
+ */
+open Alcotest;
+open Haz3lcore;
+
+let exp_typ = testable(Fmt.using(Exp.show, Fmt.string), Exp.fast_equal);
+
+let parse_exp = (s: string) =>
+  MakeTerm.from_zip_for_sem(Option.get(Printer.zipper_of_string(s))).term;
+let exp_check = (expected, actual) =>
+  check(exp_typ, actual, expected, parse_exp(actual));
+
+let tests = [
+  test_case("Integer Literal", `Quick, () => {
+    exp_check(Int(0) |> Exp.fresh, "0")
+  }),
+  test_case("Empty Hole", `Quick, () => {
+    exp_check(EmptyHole |> Exp.fresh, "?")
+  }),
+  test_case("Free Variable", `Quick, () => {
+    exp_check(Var("x") |> Exp.fresh, "x")
+  }),
+  test_case("Parenthesized Expression", `Quick, () => {
+    exp_check(Parens(Int(0) |> Exp.fresh) |> Exp.fresh, "(0)")
+  }),
+  test_case("Let Expression", `Quick, () => {
+    exp_check(
+      Let(
+        Var("x") |> Pat.fresh,
+        Int(1) |> Exp.fresh,
+        Var("x") |> Exp.fresh,
+      )
+      |> Exp.fresh,
+      "let x = 1 in x",
+    )
+  }),
+  test_case("Function Application", `Quick, () => {
+    exp_check(
+      Ap(Forward, Var("f") |> Exp.fresh, Var("x") |> Exp.fresh) |> Exp.fresh,
+      "f(x)",
+    )
+  }),
+  test_case("Named Function Definition", `Quick, () => {
+    exp_check(
+      Let(
+        Var("f") |> Pat.fresh,
+        Fun(Var("x") |> Pat.fresh, Var("x") |> Exp.fresh, None, None)  // It seems as though the function naming happens during elaboration and not during parsing
+        |> Exp.fresh,
+        Int(1) |> Exp.fresh,
+      )
+      |> Exp.fresh,
+      "let f = fun x -> x in 1",
+    )
+  }),
+  test_case("Incomplete Function Definition", `Quick, () => {
+    exp_check(
+      Let(
+        EmptyHole |> Pat.fresh,
+        Fun(Var("x") |> Pat.fresh, EmptyHole |> Exp.fresh, None, None)
+        |> Exp.fresh,
+        EmptyHole |> Exp.fresh,
+      )
+      |> Exp.fresh,
+      "let    = fun x ->   in  ",
+    )
+  }),
+  test_case("Constructor", `Quick, () => {
+    exp_check(
+      Constructor("A", Unknown(Internal) |> Typ.fresh) |> Exp.fresh,
+      "A",
+    )
+  }),
+  test_case("Type Alias", `Quick, () => {
+    exp_check(
+      TyAlias(Var("x") |> TPat.fresh, Int |> Typ.fresh, Int(1) |> Exp.fresh)
+      |> Exp.fresh,
+      "type x = Int in 1",
+    )
+  }),
+];
diff --git a/test/dune b/test/dune
index 832c9689f2..3b9dc8bb2e 100644
--- a/test/dune
+++ b/test/dune
@@ -2,7 +2,7 @@
 
 (test
  (name haz3ltest)
- (libraries haz3lcore alcotest junit junit_alcotest)
+ (libraries haz3lcore alcotest junit junit_alcotest bisect_ppx.runtime)
  (modes js)
  (preprocess
-  (pps js_of_ocaml-ppx)))
+  (pps js_of_ocaml-ppx ppx_deriving.show)))
diff --git a/test/haz3ltest.re b/test/haz3ltest.re
index 3e13ae44b7..8e4a838b0a 100644
--- a/test/haz3ltest.re
+++ b/test/haz3ltest.re
@@ -3,11 +3,14 @@ open Junit_alcotest;
 let (suite, _) =
   run_and_report(
     ~and_exit=false,
-    "Dynamics",
+    "HazelTests",
     [
       ("Elaboration", Test_Elaboration.elaboration_tests),
       ("Statics", Test_Statics.tests),
       ("Evaluator", Test_Evaluator.tests),
+      Test_ListUtil.tests,
+      ("MakeTerm", Test_MakeTerm.tests),
     ],
   );
 Junit.to_file(Junit.make([suite]), "junit_tests.xml");
+Bisect.Runtime.write_coverage_data();