diff --git a/src/haz3lcore/dynamics/Builtins.re b/src/haz3lcore/dynamics/Builtins.re
index 9acd003c3b..3563c735d7 100644
--- a/src/haz3lcore/dynamics/Builtins.re
+++ b/src/haz3lcore/dynamics/Builtins.re
@@ -1,6 +1,5 @@
 open Util;
 open OptUtil.Syntax;
-open DHExp;
 
 /*
    Built-in functions for Hazel.
@@ -10,6 +9,7 @@ open DHExp;
 
    See the existing ones for reference.
  */
+module Fresh = IdTagged.FreshGrammar;
 
 [@deriving (show({with_path: false}), sexp)]
 type builtin =
@@ -47,14 +47,15 @@ let (let-unbox) = ((request, v), f) =>
 
 module Pervasives = {
   module Impls = {
+    open Fresh.Exp;
     /* constants */
-    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 infinity = float(Float.infinity);
+    let neg_infinity = float(Float.neg_infinity);
+    let nan = float(Float.nan);
+    let epsilon_float = float(epsilon_float);
+    let pi = float(Float.pi);
+    let max_int = int(Int.max_int);
+    let min_int = int(Int.min_int);
 
     [@warning "-8"]
     // let-unbox guarantees that the tuple will have length 2
@@ -73,52 +74,52 @@ module Pervasives = {
 
     let is_finite = d => {
       let-unbox f = (Float, d);
-      Some(fresh(Bool(Float.is_finite(f))));
+      Some(bool(Float.is_finite(f)));
     };
 
     let is_infinite = d => {
       let-unbox f = (Float, d);
-      Some(fresh(Bool(Float.is_infinite(f))));
+      Some(bool(Float.is_infinite(f)));
     };
 
     let is_nan = d => {
       let-unbox f = (Float, d);
-      Some(fresh(Bool(Float.is_nan(f))));
+      Some(bool(Float.is_nan(f)));
     };
 
     let string_of_int = d => {
       let-unbox n = (Int, d);
-      Some(fresh(String(string_of_int(n))));
+      Some(string(string_of_int(n)));
     };
 
     let string_of_float = d => {
       let-unbox f = (Float, d);
-      Some(fresh(String(string_of_float(f))));
+      Some(string(string_of_float(f)));
     };
 
     let string_of_bool = d => {
       let-unbox b = (Bool, d);
-      Some(fresh(String(string_of_bool(b))));
+      Some(string(string_of_bool(b)));
     };
 
     let int_of_float = d => {
       let-unbox f = (Float, d);
-      Some(fresh(Int(int_of_float(f))));
+      Some(int(int_of_float(f)));
     };
 
     let float_of_int = d => {
       let-unbox n = (Int, d);
-      Some(fresh(Float(float_of_int(n))));
+      Some(float(float_of_int(n)));
     };
 
     let abs = d => {
       let-unbox n = (Int, d);
-      Some(fresh(Int(abs(n))));
+      Some(int(abs(n)));
     };
 
     let float_op = (fn, d) => {
       let-unbox f = (Float, d);
-      Some(fresh(Float(fn(f))));
+      Some(float(fn(f)));
     };
 
     let abs_float = float_op(abs_float);
@@ -146,19 +147,16 @@ module Pervasives = {
       switch (convert(s)) {
       | Some(n) => Some(wrap(n))
       | None =>
-        let d' = BuiltinFun(name) |> DHExp.fresh;
-        let d' = Ap(Forward, d', d) |> DHExp.fresh;
-        let d' = DynamicErrorHole(d', InvalidOfString) |> DHExp.fresh;
+        let d' = builtin_fun(name);
+        let d' = ap(Forward, d', d);
+        let d' = dynamic_error_hole(d', InvalidOfString);
         Some(d');
       };
     };
 
-    let int_of_string =
-      of_string(int_of_string_opt, n => Int(n) |> DHExp.fresh);
-    let float_of_string =
-      of_string(float_of_string_opt, f => Float(f) |> DHExp.fresh);
-    let bool_of_string =
-      of_string(bool_of_string_opt, b => Bool(b) |> DHExp.fresh);
+    let int_of_string = of_string(int_of_string_opt, n => int(n));
+    let float_of_string = of_string(float_of_string_opt, f => float(f));
+    let bool_of_string = of_string(bool_of_string_opt, b => bool(b));
 
     let int_mod = name =>
       binary((d1, d2) => {
@@ -166,33 +164,31 @@ module Pervasives = {
         let-unbox n = (Int, d2);
         if (n == 0) {
           Some(
-            fresh(
-              DynamicErrorHole(
-                Ap(Forward, BuiltinFun(name) |> fresh, d1) |> fresh,
-                DivideByZero,
-              ),
+            dynamic_error_hole(
+              ap(Forward, builtin_fun(name), d1),
+              DivideByZero,
             ),
           );
         } else {
-          Some(fresh(Int(m mod n)));
+          Some(int(m mod n));
         };
       });
 
     let string_length = d => {
       let-unbox s = (String, d);
-      Some(fresh(Int(String.length(s))));
+      Some(int(String.length(s)));
     };
 
     let string_compare =
       binary((d1, d2) => {
         let-unbox s1 = (String, d1);
         let-unbox s2 = (String, d2);
-        Some(fresh(Int(String.compare(s1, s2))));
+        Some(int(String.compare(s1, s2)));
       });
 
     let string_trim = d => {
       let-unbox s = (String, d);
-      Some(fresh(String(String.trim(s))));
+      Some(string(String.trim(s)));
     };
 
     let string_of: DHExp.t => option(string) =
@@ -206,7 +202,7 @@ module Pervasives = {
         let-unbox s1 = (String, d1);
         let-unbox xs = (List, d2);
         let* xs' = List.map(string_of, xs) |> Util.OptUtil.sequence;
-        Some(fresh(String(String.concat(s1, xs'))));
+        Some(string(String.concat(s1, xs')));
       });
 
     let string_sub = name =>
@@ -214,7 +210,7 @@ module Pervasives = {
         let-unbox s = (String, d1);
         let-unbox idx = (Int, d2);
         let-unbox len = (Int, d3);
-        try(Some(fresh(String(String.sub(s, idx, len))))) {
+        try(Some(string(String.sub(s, idx, len)))) {
         | _ =>
           let d' = BuiltinFun(name) |> DHExp.fresh;
           let d' = Ap(Forward, d', d1) |> DHExp.fresh;
@@ -228,8 +224,8 @@ module Pervasives = {
         let-unbox s = (String, d1);
         let-unbox sep = (String, d2);
         let split_str = Util.StringUtil.plain_split(sep, s);
-        let split_str' = List.map(s => String(s) |> DHExp.fresh, split_str);
-        Some(fresh(ListLit(split_str')));
+        let split_str' = List.map(s => string(s), split_str);
+        Some(list_lit(split_str'));
       });
   };
 
@@ -237,76 +233,78 @@ module Pervasives = {
 
   // Update src/haz3lmenhir/Lexer.mll when any new builtin is added
   let builtins =
-    VarMap.empty
-    |> const("infinity", Float, infinity)
-    |> const("neg_infinity", Float, neg_infinity)
-    |> const("nan", Float, nan)
-    |> const("epsilon_float", Float, epsilon_float)
-    |> const("pi", Float, pi)
-    |> const("max_int", Int, max_int)
-    |> const("min_int", Int, min_int)
-    |> fn("is_finite", Float, Bool, is_finite)
-    |> fn("is_infinite", Float, Bool, is_infinite)
-    |> fn("is_nan", Float, Bool, is_nan)
-    |> fn("int_of_float", Float, Int, int_of_float)
-    |> fn("float_of_int", Int, Float, float_of_int)
-    |> fn("string_of_int", Int, String, string_of_int)
-    |> fn("string_of_float", Float, String, string_of_float)
-    |> fn("string_of_bool", Bool, String, string_of_bool)
-    |> fn("int_of_string", String, Int, int_of_string("int_of_string"))
-    |> fn(
-         "float_of_string",
-         String,
-         Float,
-         float_of_string("float_of_string"),
-       )
-    |> fn("bool_of_string", String, Bool, bool_of_string("bool_of_string"))
-    |> fn("abs", Int, Int, abs)
-    |> fn("abs_float", Float, Float, abs_float)
-    |> fn("ceil", Float, Float, ceil)
-    |> fn("floor", Float, Float, floor)
-    |> fn("exp", Float, Float, exp)
-    |> fn("log", Float, Float, log)
-    |> fn("log10", Float, Float, log10)
-    |> fn("sqrt", Float, Float, sqrt)
-    |> fn("sin", Float, Float, sin)
-    |> fn("cos", Float, Float, cos)
-    |> fn("tan", Float, Float, tan)
-    |> fn("asin", Float, Float, asin)
-    |> fn("acos", Float, Float, acos)
-    |> fn("atan", Float, Float, atan)
-    |> fn(
-         "mod",
-         Prod([Int |> Typ.fresh, Int |> Typ.fresh]),
-         Int,
-         int_mod("mod"),
-       )
-    |> fn("string_length", String, Int, string_length)
-    |> fn(
-         "string_compare",
-         Prod([String |> Typ.fresh, String |> Typ.fresh]),
-         Int,
-         string_compare,
-       )
-    |> fn("string_trim", String, String, string_trim)
-    |> fn(
-         "string_concat",
-         Prod([String |> Typ.fresh, List(String |> Typ.fresh) |> Typ.fresh]),
-         String,
-         string_concat,
-       )
-    |> fn(
-         "string_sub",
-         Prod([String |> Typ.fresh, Int |> Typ.fresh, Int |> Typ.fresh]),
-         String,
-         string_sub("string_sub"),
-       )
-    |> fn(
-         "string_split",
-         Prod([String |> Typ.fresh, String |> Typ.fresh]),
-         List(String |> Typ.fresh),
-         string_split("string_split"),
-       );
+    Fresh.Typ.(
+      VarMap.empty
+      |> const("infinity", Float, infinity)
+      |> const("neg_infinity", Float, neg_infinity)
+      |> const("nan", Float, nan)
+      |> const("epsilon_float", Float, epsilon_float)
+      |> const("pi", Float, pi)
+      |> const("max_int", Int, max_int)
+      |> const("min_int", Int, min_int)
+      |> fn("is_finite", Float, Bool, is_finite)
+      |> fn("is_infinite", Float, Bool, is_infinite)
+      |> fn("is_nan", Float, Bool, is_nan)
+      |> fn("int_of_float", Float, Int, int_of_float)
+      |> fn("float_of_int", Int, Float, float_of_int)
+      |> fn("string_of_int", Int, String, string_of_int)
+      |> fn("string_of_float", Float, String, string_of_float)
+      |> fn("string_of_bool", Bool, String, string_of_bool)
+      |> fn("int_of_string", String, Int, int_of_string("int_of_string"))
+      |> fn(
+           "float_of_string",
+           String,
+           Float,
+           float_of_string("float_of_string"),
+         )
+      |> fn(
+           "bool_of_string",
+           String,
+           Bool,
+           bool_of_string("bool_of_string"),
+         )
+      |> fn("abs", Int, Int, abs)
+      |> fn("abs_float", Float, Float, abs_float)
+      |> fn("ceil", Float, Float, ceil)
+      |> fn("floor", Float, Float, floor)
+      |> fn("exp", Float, Float, exp)
+      |> fn("log", Float, Float, log)
+      |> fn("log10", Float, Float, log10)
+      |> fn("sqrt", Float, Float, sqrt)
+      |> fn("sin", Float, Float, sin)
+      |> fn("cos", Float, Float, cos)
+      |> fn("tan", Float, Float, tan)
+      |> fn("asin", Float, Float, asin)
+      |> fn("acos", Float, Float, acos)
+      |> fn("atan", Float, Float, atan)
+      |> fn("mod", Prod([int(), int()]), Int, int_mod("mod"))
+      |> fn("string_length", String, Int, string_length)
+      |> fn(
+           "string_compare",
+           Prod([string(), string()]),
+           Int,
+           string_compare,
+         )
+      |> fn("string_trim", String, String, string_trim)
+      |> fn(
+           "string_concat",
+           Prod([string(), list(string())]),
+           String,
+           string_concat,
+         )
+      |> fn(
+           "string_sub",
+           Prod([string(), int(), int()]),
+           String,
+           string_sub("string_sub"),
+         )
+      |> fn(
+           "string_split",
+           Prod([string(), string()]),
+           List(string()),
+           string_split("string_split"),
+         )
+    );
 };
 
 let ctx_init: Ctx.t = {
@@ -318,13 +316,13 @@ let ctx_init: Ctx.t = {
     Ctx.TVarEntry({
       name: "$Meta",
       id: Id.invalid,
-      kind: Ctx.Singleton(Sum(meta_cons_map) |> Typ.fresh),
+      kind: Ctx.Singleton(Fresh.Typ.sum(meta_cons_map)),
     });
   List.map(
     fun
     | (name, Const(typ, _)) => Ctx.VarEntry({name, typ, id: Id.invalid})
     | (name, Fn(t1, t2, _)) =>
-      Ctx.VarEntry({name, typ: Arrow(t1, t2) |> Typ.fresh, id: Id.invalid}),
+      Ctx.VarEntry({name, typ: Fresh.Typ.arrow(t1, t2), id: Id.invalid}),
     Pervasives.builtins,
   )
   |> Ctx.extend(_, meta)
@@ -345,7 +343,7 @@ let env_init: Environment.t =
       fun
       | (name, Const(_, d)) => Environment.extend(env, (name, d))
       | (name, Fn(_)) =>
-        Environment.extend(env, (name, BuiltinFun(name) |> fresh)),
+        Environment.extend(env, (name, Fresh.Exp.builtin_fun(name))),
     Environment.empty,
     Pervasives.builtins,
   );
diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re
index 4331b7d493..5bb58c2c98 100644
--- a/src/haz3lcore/dynamics/Transition.re
+++ b/src/haz3lcore/dynamics/Transition.re
@@ -134,6 +134,7 @@ module type EV_MODE = {
 module Transition = (EV: EV_MODE) => {
   open EV;
   open DHExp;
+  open IdTagged.FreshGrammar.Exp;
 
   // Default state update
   let state_update = () => ();
@@ -152,7 +153,7 @@ module Transition = (EV: EV_MODE) => {
     | (_, Step(_)) => r
     | (None, Constructor | Indet | Value) =>
       Step({
-        expr: Closure(env, expr) |> fresh,
+        expr: closure(env, expr),
         state_update,
         kind: WrapClosure,
         is_value: false,
@@ -224,7 +225,7 @@ module Transition = (EV: EV_MODE) => {
       let.wrap_closure _ = env;
       let.match env' = (env, matches(dp, d1'));
       Step({
-        expr: Closure(env', d2) |> fresh,
+        expr: closure(env', d2),
         state_update,
         kind: LetBind,
         is_value: false,
@@ -253,7 +254,7 @@ module Transition = (EV: EV_MODE) => {
             env,
           );
         Step({
-          expr: Closure(env'', d1) |> fresh,
+          expr: closure(env'', d1),
           state_update,
           kind: FixUnwrap,
           is_value: false,
@@ -267,19 +268,14 @@ module Transition = (EV: EV_MODE) => {
             binding =>
               (
                 binding,
-                Let(
-                  dp,
-                  FixF(dp, d1, Some(env)) |> rewrap,
-                  Var(binding) |> fresh,
-                )
-                |> fresh,
+                let_(dp, FixF(dp, d1, Some(env)) |> rewrap, var(binding)),
               ),
             bindings,
           );
         let env'' =
           evaluate_extend_env(Environment.of_list(substitutions), env);
         Step({
-          expr: Closure(env'', d1) |> fresh,
+          expr: closure(env'', d1),
           state_update,
           kind: FixUnwrap,
           is_value: false,
@@ -295,7 +291,7 @@ module Transition = (EV: EV_MODE) => {
         | Matches(b) => b ? Pass : Fail
         };
       Step({
-        expr: Tuple([]) |> fresh,
+        expr: tuple([]),
         state_update: () =>
           update_test(state, DHExp.rep_id(d), (d', result)),
         kind: UpdateTest,
@@ -327,12 +323,11 @@ module Transition = (EV: EV_MODE) => {
         /* Rule ITTApCast */
         Step({
           expr:
-            Cast(
-              TypAp(d'', tau) |> Exp.fresh,
+            cast(
+              typ_ap(d'', tau),
               Typ.subst(tau, tp1, t1),
               Typ.subst(tau, tp2, t2),
-            )
-            |> Exp.fresh,
+            ),
           state_update,
           kind: CastTypAp,
           is_value: false,
@@ -365,20 +360,15 @@ module Transition = (EV: EV_MODE) => {
       | FunEnv(dp, d3, env') =>
         let.match env'' = (env', matches(dp, d2'));
         Step({
-          expr: Closure(env'', d3) |> fresh,
+          expr: closure(env'', d3),
           state_update,
           kind: FunAp,
           is_value: false,
         });
       | FunCast(d3', ty1, ty2, ty1', ty2') =>
         Step({
-          expr:
-            Cast(
-              Ap(dir, d3', Cast(d2', ty1', ty1) |> fresh) |> fresh,
-              ty2,
-              ty2',
-            )
-            |> fresh,
+          expr: cast(ap(dir, d3', cast(d2', ty1', ty1)), ty2, ty2'),
+
           state_update,
           kind: CastAp,
           is_value: false,
@@ -413,7 +403,7 @@ module Transition = (EV: EV_MODE) => {
           if (n_args == 1) {
             (
               Tuple(n_args),
-              Tuple([d2]) |> fresh // TODO Should we not be going to a tuple?
+              tuple([d2]) // TODO Should we not be going to a tuple?
             );
           } else {
             (Tuple(n_args), d2);
@@ -431,7 +421,7 @@ module Transition = (EV: EV_MODE) => {
           go(d4s, args);
         };
         Step({
-          expr: Ap(Forward, d3, Tuple(new_args) |> fresh) |> fresh,
+          expr: ap(Forward, d3, tuple(new_args)),
           state_update,
           kind: DeferredAp,
           is_value: false,
@@ -477,7 +467,7 @@ module Transition = (EV: EV_MODE) => {
         );
       let-unbox n = (Int, d1');
       Step({
-        expr: Int(- n) |> fresh,
+        expr: int(- n),
         state_update,
         kind: UnOp(Int(Minus)),
         is_value: true,
@@ -492,7 +482,7 @@ module Transition = (EV: EV_MODE) => {
         );
       let-unbox b = (Bool, d1');
       Step({
-        expr: Bool(!b) |> fresh,
+        expr: bool(!b),
         state_update,
         kind: UnOp(Bool(Not)),
         is_value: true,
@@ -508,7 +498,7 @@ module Transition = (EV: EV_MODE) => {
       let.wrap_closure _ = env;
       let-unbox b1 = (Bool, d1');
       Step({
-        expr: b1 ? d2 : Bool(false) |> fresh,
+        expr: b1 ? d2 : bool(false),
         state_update,
         kind: BinBoolOp(And),
         is_value: false,
@@ -524,7 +514,7 @@ module Transition = (EV: EV_MODE) => {
       let.wrap_closure _ = env;
       let-unbox b1 = (Bool, d1');
       Step({
-        expr: b1 ? Bool(true) |> fresh : d2,
+        expr: b1 ? bool(true) : d2,
         state_update,
         kind: BinBoolOp(Or),
         is_value: false,
@@ -547,32 +537,30 @@ module Transition = (EV: EV_MODE) => {
       let-unbox n2 = (Int, d2');
       Step({
         expr:
-          (
-            switch (op) {
-            | Plus => Int(n1 + n2)
-            | Minus => Int(n1 - n2)
-            | Power when n2 < 0 =>
-              DynamicErrorHole(
-                BinOp(Int(op), d1', d2') |> rewrap,
-                NegativeExponent,
-              )
-            | Power => Int(IntUtil.ipow(n1, n2))
-            | Times => Int(n1 * n2)
-            | Divide when n2 == 0 =>
-              DynamicErrorHole(
-                BinOp(Int(op), d1', d2') |> rewrap,
-                DivideByZero,
-              )
-            | Divide => Int(n1 / n2)
-            | LessThan => Bool(n1 < n2)
-            | LessThanOrEqual => Bool(n1 <= n2)
-            | GreaterThan => Bool(n1 > n2)
-            | GreaterThanOrEqual => Bool(n1 >= n2)
-            | Equals => Bool(n1 == n2)
-            | NotEquals => Bool(n1 != n2)
-            }
-          )
-          |> fresh,
+          switch (op) {
+          | Plus => int(n1 + n2)
+          | Minus => int(n1 - n2)
+          | Power when n2 < 0 =>
+            dynamic_error_hole(
+              BinOp(Int(op), d1', d2') |> rewrap,
+              NegativeExponent,
+            )
+          | Power => int(IntUtil.ipow(n1, n2))
+          | Times => int(n1 * n2)
+          | Divide when n2 == 0 =>
+            dynamic_error_hole(
+              BinOp(Int(op), d1', d2') |> rewrap,
+              DivideByZero,
+            )
+          | Divide => int(n1 / n2)
+          | LessThan => bool(n1 < n2)
+          | LessThanOrEqual => bool(n1 <= n2)
+          | GreaterThan => bool(n1 > n2)
+          | GreaterThanOrEqual => bool(n1 >= n2)
+          | Equals => bool(n1 == n2)
+          | NotEquals => bool(n1 != n2)
+          },
+
         state_update,
         kind: BinIntOp(op),
         // False so that InvalidOperations are caught and made indet by the next step
@@ -597,22 +585,20 @@ module Transition = (EV: EV_MODE) => {
       let-unbox n2 = (Float, d2');
       Step({
         expr:
-          (
-            switch (op) {
-            | Plus => Float(n1 +. n2)
-            | Minus => Float(n1 -. n2)
-            | Power => Float(n1 ** n2)
-            | Times => Float(n1 *. n2)
-            | Divide => Float(n1 /. n2)
-            | LessThan => Bool(n1 < n2)
-            | LessThanOrEqual => Bool(n1 <= n2)
-            | GreaterThan => Bool(n1 > n2)
-            | GreaterThanOrEqual => Bool(n1 >= n2)
-            | Equals => Bool(n1 == n2)
-            | NotEquals => Bool(n1 != n2)
-            }
-          )
-          |> fresh,
+          switch (op) {
+          | Plus => float(n1 +. n2)
+          | Minus => float(n1 -. n2)
+          | Power => float(n1 ** n2)
+          | Times => float(n1 *. n2)
+          | Divide => float(n1 /. n2)
+          | LessThan => bool(n1 < n2)
+          | LessThanOrEqual => bool(n1 <= n2)
+          | GreaterThan => bool(n1 > n2)
+          | GreaterThanOrEqual => bool(n1 >= n2)
+          | Equals => bool(n1 == n2)
+          | NotEquals => bool(n1 != n2)
+          },
+
         state_update,
         kind: BinFloatOp(op),
         is_value: true,
@@ -637,8 +623,8 @@ module Transition = (EV: EV_MODE) => {
       Step({
         expr:
           switch (op) {
-          | Concat => String(s1 ++ s2) |> fresh
-          | Equals => Bool(s1 == s2) |> fresh
+          | Concat => string(s1 ++ s2)
+          | Equals => bool(s1 == s2)
           },
         state_update,
         kind: BinStringOp(op),
@@ -691,7 +677,7 @@ module Transition = (EV: EV_MODE) => {
         req_final(req(state, env), d2 => Cons2(d1, d2) |> wrap_ctx, d2);
       let-unbox ds = (List, d2');
       Step({
-        expr: ListLit([d1', ...ds]) |> fresh,
+        expr: list_lit([d1', ...ds]),
         state_update,
         kind: ListCons,
         is_value: true,
@@ -713,7 +699,7 @@ module Transition = (EV: EV_MODE) => {
       let-unbox ds1 = (List, d1');
       let-unbox ds2 = (List, d2');
       Step({
-        expr: ListLit(ds1 @ ds2) |> fresh,
+        expr: list_lit(ds1 @ ds2),
         state_update,
         kind: ListConcat,
         is_value: true,
@@ -748,7 +734,7 @@ module Transition = (EV: EV_MODE) => {
       switch (next_rule(rules)) {
       | Some((env', d2)) =>
         Step({
-          expr: Closure(evaluate_extend_env(env', env), d2) |> fresh,
+          expr: closure(evaluate_extend_env(env', env), d2),
           state_update,
           kind: CaseApply,
           is_value: false,
diff --git a/src/haz3lcore/lang/Operators.re b/src/haz3lcore/lang/Operators.re
index a7df230b5a..bf732a114d 100644
--- a/src/haz3lcore/lang/Operators.re
+++ b/src/haz3lcore/lang/Operators.re
@@ -1,21 +1,21 @@
-[@deriving (show({with_path: false}), sexp, yojson, eq)]
+[@deriving (show({with_path: false}), sexp, yojson, eq, enumerate)]
 type op_un_bool =
   | Not;
 
-[@deriving (show({with_path: false}), sexp, yojson, eq)]
+[@deriving (show({with_path: false}), sexp, yojson, eq, enumerate)]
 type op_un_meta =
   | Unquote;
 
-[@deriving (show({with_path: false}), sexp, yojson, eq)]
+[@deriving (show({with_path: false}), sexp, yojson, eq, enumerate)]
 type op_un_int =
   | Minus;
 
-[@deriving (show({with_path: false}), sexp, yojson, eq)]
+[@deriving (show({with_path: false}), sexp, yojson, eq, enumerate)]
 type op_bin_bool =
   | And
   | Or;
 
-[@deriving (show({with_path: false}), sexp, yojson, eq)]
+[@deriving (show({with_path: false}), sexp, yojson, eq, enumerate)]
 type op_bin_int =
   | Plus
   | Minus
@@ -29,7 +29,7 @@ type op_bin_int =
   | Equals
   | NotEquals;
 
-[@deriving (show({with_path: false}), sexp, yojson, eq)]
+[@deriving (show({with_path: false}), sexp, yojson, eq, enumerate)]
 type op_bin_float =
   | Plus
   | Minus
@@ -43,25 +43,25 @@ type op_bin_float =
   | Equals
   | NotEquals;
 
-[@deriving (show({with_path: false}), sexp, yojson, eq)]
+[@deriving (show({with_path: false}), sexp, yojson, eq, enumerate)]
 type op_bin_string =
   | Concat
   | Equals;
 
-[@deriving (show({with_path: false}), sexp, yojson, eq)]
+[@deriving (show({with_path: false}), sexp, yojson, eq, enumerate)]
 type op_un =
   | Meta(op_un_meta)
   | Int(op_un_int)
   | Bool(op_un_bool);
 
-[@deriving (show({with_path: false}), sexp, yojson, eq)]
+[@deriving (show({with_path: false}), sexp, yojson, eq, enumerate)]
 type op_bin =
   | Int(op_bin_int)
   | Float(op_bin_float)
   | Bool(op_bin_bool)
   | String(op_bin_string);
 
-[@deriving (show({with_path: false}), sexp, yojson, eq)]
+[@deriving (show({with_path: false}), sexp, yojson, eq, enumerate)]
 type ap_direction =
   | Forward
   | Reverse;
diff --git a/src/haz3lcore/lang/term/Cls.re b/src/haz3lcore/lang/term/Cls.re
index e1acb702c8..a874488a24 100644
--- a/src/haz3lcore/lang/term/Cls.re
+++ b/src/haz3lcore/lang/term/Cls.re
@@ -1,4 +1,4 @@
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, enumerate)]
 type t =
   | Exp(Exp.cls)
   | Pat(Pat.cls)
diff --git a/src/haz3lcore/lang/term/Grammar.re b/src/haz3lcore/lang/term/Grammar.re
index 982ba74bad..b8a555df8d 100644
--- a/src/haz3lcore/lang/term/Grammar.re
+++ b/src/haz3lcore/lang/term/Grammar.re
@@ -417,3 +417,400 @@ and map_type_hole_annotation:
     | MultiHole(l) => MultiHole(List.map(x => map_any_annotation(f, x), l))
     };
   };
+
+module type DefaultAnnotation = {
+  type t;
+  let default_value: unit => t;
+};
+
+module Factory = (DefaultAnnotation: DefaultAnnotation) => {
+  type exp = exp_t(DefaultAnnotation.t);
+  type pat = pat_t(DefaultAnnotation.t);
+  type typ = typ_t(DefaultAnnotation.t);
+  type tpat = tpat_t(DefaultAnnotation.t);
+  type typ_provenance = type_provenance(DefaultAnnotation.t);
+
+  let default_annotation = ann =>
+    Option.value(~default=DefaultAnnotation.default_value(), ann);
+  module Exp = {
+    let invalid = (~ann=?, s): exp_t(DefaultAnnotation.t) => {
+      term: Invalid(s),
+      annotation: default_annotation(ann),
+    };
+    let empty_hole = (~ann=?, ()): exp_t(DefaultAnnotation.t) => {
+      term: EmptyHole,
+      annotation: default_annotation(ann),
+    };
+    let multi_hole = (~ann=?, l): exp_t(DefaultAnnotation.t) => {
+      term: MultiHole(l),
+      annotation: default_annotation(ann),
+    };
+    let dynamic_error_hole = (~ann=?, e, err): exp_t(DefaultAnnotation.t) => {
+      term: DynamicErrorHole(e, err),
+      annotation: default_annotation(ann),
+    };
+    let failed_cast = (~ann=?, e, t1, t2): exp_t(DefaultAnnotation.t) => {
+      term: FailedCast(e, t1, t2),
+      annotation: default_annotation(ann),
+    };
+    let deferral = (~ann=?, pos): exp_t(DefaultAnnotation.t) => {
+      term: Deferral(pos),
+      annotation: default_annotation(ann),
+    };
+    let undefined = (~ann=?, ()): exp_t(DefaultAnnotation.t) => {
+      term: Undefined,
+      annotation: default_annotation(ann),
+    };
+    let bool = (~ann=?, b): exp_t(DefaultAnnotation.t) => {
+      term: Bool(b),
+      annotation: default_annotation(ann),
+    };
+    let int = (~ann=?, i): exp_t(DefaultAnnotation.t) => {
+      term: Int(i),
+      annotation: default_annotation(ann),
+    };
+    let float = (~ann=?, f): exp_t(DefaultAnnotation.t) => {
+      term: Float(f),
+      annotation: default_annotation(ann),
+    };
+    let string = (~ann=?, s): exp_t(DefaultAnnotation.t) => {
+      term: String(s),
+      annotation: default_annotation(ann),
+    };
+    let list_lit = (~ann=?, l): exp_t(DefaultAnnotation.t) => {
+      term: ListLit(l),
+      annotation: default_annotation(ann),
+    };
+    let constructor = (~ann=?, s, t): exp_t(DefaultAnnotation.t) => {
+      term: Constructor(s, t),
+      annotation: default_annotation(ann),
+    };
+    let fn = (~ann=?, p, e, t, v): exp_t(DefaultAnnotation.t) => {
+      term: Fun(p, e, t, v),
+      annotation: default_annotation(ann),
+    };
+    let typ_fun = (~ann=?, p, e, v): exp_t(DefaultAnnotation.t) => {
+      term: TypFun(p, e, v),
+      annotation: default_annotation(ann),
+    };
+    let tuple = (~ann=?, l): exp_t(DefaultAnnotation.t) => {
+      term: Tuple(l),
+      annotation: default_annotation(ann),
+    };
+    let label = (~ann=?, l): exp_t(DefaultAnnotation.t) => {
+      term: Label(l),
+      annotation: default_annotation(ann),
+    };
+    let tup_label = (~ann=?, l, e): exp_t(DefaultAnnotation.t) => {
+      term: TupLabel(l, e),
+      annotation: default_annotation(ann),
+    };
+    let dot = (~ann=?, e1, e2): exp_t(DefaultAnnotation.t) => {
+      term: Dot(e1, e2),
+      annotation: default_annotation(ann),
+    };
+    let var = (~ann=?, v): exp_t(DefaultAnnotation.t) => {
+      term: Var(v),
+      annotation: default_annotation(ann),
+    };
+    let let_ = (~ann=?, p, e1, e2): exp_t(DefaultAnnotation.t) => {
+      term: Let(p, e1, e2),
+      annotation: default_annotation(ann),
+    };
+    let fix_f = (~ann=?, p, e, env): exp_t(DefaultAnnotation.t) => {
+      term: FixF(p, e, env),
+      annotation: default_annotation(ann),
+    };
+    let ty_alias = (~ann=?, p, t, e): exp_t(DefaultAnnotation.t) => {
+      term: TyAlias(p, t, e),
+      annotation: default_annotation(ann),
+    };
+    let ap = (~ann=?, d, e1, e2): exp_t(DefaultAnnotation.t) => {
+      term: Ap(d, e1, e2),
+      annotation: default_annotation(ann),
+    };
+    let typ_ap = (~ann=?, e, t): exp_t(DefaultAnnotation.t) => {
+      term: TypAp(e, t),
+      annotation: default_annotation(ann),
+    };
+    let deferred_ap = (~ann=?, e, l): exp_t(DefaultAnnotation.t) => {
+      term: DeferredAp(e, l),
+      annotation: default_annotation(ann),
+    };
+    let if_ = (~ann=?, e1, e2, e3): exp_t(DefaultAnnotation.t) => {
+      term: If(e1, e2, e3),
+      annotation: default_annotation(ann),
+    };
+    let seq = (~ann=?, e1, e2): exp_t(DefaultAnnotation.t) => {
+      term: Seq(e1, e2),
+      annotation: default_annotation(ann),
+    };
+    let test = (~ann=?, e): exp_t(DefaultAnnotation.t) => {
+      term: Test(e),
+      annotation: default_annotation(ann),
+    };
+    let filter = (~ann=?, k, e): exp_t(DefaultAnnotation.t) => {
+      term: Filter(k, e),
+      annotation: default_annotation(ann),
+    };
+    let closure = (~ann=?, env, e): exp_t(DefaultAnnotation.t) => {
+      term: Closure(env, e),
+      annotation: default_annotation(ann),
+    };
+    let parens = (~ann=?, e): exp_t(DefaultAnnotation.t) => {
+      term: Parens(e),
+      annotation: default_annotation(ann),
+    };
+    let cons = (~ann=?, e1, e2): exp_t(DefaultAnnotation.t) => {
+      term: Cons(e1, e2),
+      annotation: default_annotation(ann),
+    };
+    let list_concat = (~ann=?, e1, e2): exp_t(DefaultAnnotation.t) => {
+      term: ListConcat(e1, e2),
+      annotation: default_annotation(ann),
+    };
+    let un_op = (~ann=?, op, e): exp_t(DefaultAnnotation.t) => {
+      term: UnOp(op, e),
+      annotation: default_annotation(ann),
+    };
+    let bin_op = (~ann=?, op, e1, e2): exp_t(DefaultAnnotation.t) => {
+      term: BinOp(op, e1, e2),
+      annotation: default_annotation(ann),
+    };
+    let builtin_fun = (~ann=?, s): exp_t(DefaultAnnotation.t) => {
+      term: BuiltinFun(s),
+      annotation: default_annotation(ann),
+    };
+    let match = (~ann=?, e, l): exp_t(DefaultAnnotation.t) => {
+      term: Match(e, l),
+      annotation: default_annotation(ann),
+    };
+    let cast = (~ann=?, e, t1, t2): exp_t(DefaultAnnotation.t) => {
+      term: Cast(e, t1, t2),
+      annotation: default_annotation(ann),
+    };
+  };
+  module Pat = {
+    let invalid = (~ann=?, s): pat_t(DefaultAnnotation.t) => {
+      term: Invalid(s),
+      annotation: default_annotation(ann),
+    };
+    let empty_hole = (~ann=?, ()): pat_t(DefaultAnnotation.t) => {
+      term: EmptyHole,
+      annotation: default_annotation(ann),
+    };
+    let multi_hole = (~ann=?, l): pat_t(DefaultAnnotation.t) => {
+      term: MultiHole(l),
+      annotation: default_annotation(ann),
+    };
+    let wild = (~ann=?, ()): pat_t(DefaultAnnotation.t) => {
+      term: Wild,
+      annotation: default_annotation(ann),
+    };
+    let int = (~ann=?, i): pat_t(DefaultAnnotation.t) => {
+      term: Int(i),
+      annotation: default_annotation(ann),
+    };
+    let float = (~ann=?, f): pat_t(DefaultAnnotation.t) => {
+      term: Float(f),
+      annotation: default_annotation(ann),
+    };
+    let bool = (~ann=?, b): pat_t(DefaultAnnotation.t) => {
+      term: Bool(b),
+      annotation: default_annotation(ann),
+    };
+    let string = (~ann=?, s): pat_t(DefaultAnnotation.t) => {
+      term: String(s),
+      annotation: default_annotation(ann),
+    };
+    let list_lit = (~ann=?, l): pat_t(DefaultAnnotation.t) => {
+      term: ListLit(l),
+      annotation: default_annotation(ann),
+    };
+    let constructor = (~ann=?, s, t): pat_t(DefaultAnnotation.t) => {
+      term: Constructor(s, t),
+      annotation: default_annotation(ann),
+    };
+    let cons = (~ann=?, p1, p2): pat_t(DefaultAnnotation.t) => {
+      term: Cons(p1, p2),
+      annotation: default_annotation(ann),
+    };
+    let var = (~ann=?, v): pat_t(DefaultAnnotation.t) => {
+      term: Var(v),
+      annotation: default_annotation(ann),
+    };
+    let tuple = (~ann=?, l): pat_t(DefaultAnnotation.t) => {
+      term: Tuple(l),
+      annotation: default_annotation(ann),
+    };
+    let label = (~ann=?, l): pat_t(DefaultAnnotation.t) => {
+      term: Label(l),
+      annotation: default_annotation(ann),
+    };
+    let tup_label = (~ann=?, p1, p2): pat_t(DefaultAnnotation.t) => {
+      term: TupLabel(p1, p2),
+      annotation: default_annotation(ann),
+    };
+    let parens = (~ann=?, p): pat_t(DefaultAnnotation.t) => {
+      term: Parens(p),
+      annotation: default_annotation(ann),
+    };
+    let ap = (~ann=?, p1, p2): pat_t(DefaultAnnotation.t) => {
+      term: Ap(p1, p2),
+      annotation: default_annotation(ann),
+    };
+    let cast = (~ann=?, p, t1, t2): pat_t(DefaultAnnotation.t) => {
+      term: Cast(p, t1, t2),
+      annotation: default_annotation(ann),
+    };
+  };
+
+  module Typ = {
+    let unknown = (~ann=?, p): typ_t(DefaultAnnotation.t) => {
+      term: Unknown(p),
+      annotation: default_annotation(ann),
+    };
+    let int = (~ann=?, ()): typ_t(DefaultAnnotation.t) => {
+      term: Int,
+      annotation: default_annotation(ann),
+    };
+    let float = (~ann=?, ()): typ_t(DefaultAnnotation.t) => {
+      term: Float,
+      annotation: default_annotation(ann),
+    };
+    let bool = (~ann=?, ()): typ_t(DefaultAnnotation.t) => {
+      term: Bool,
+      annotation: default_annotation(ann),
+    };
+    let string = (~ann=?, ()): typ_t(DefaultAnnotation.t) => {
+      term: String,
+      annotation: default_annotation(ann),
+    };
+    let var = (~ann=?, s): typ_t(DefaultAnnotation.t) => {
+      term: Var(s),
+      annotation: default_annotation(ann),
+    };
+    let list = (~ann=?, t): typ_t(DefaultAnnotation.t) => {
+      term: List(t),
+      annotation: default_annotation(ann),
+    };
+    let arrow = (~ann=?, t1, t2): typ_t(DefaultAnnotation.t) => {
+      term: Arrow(t1, t2),
+      annotation: default_annotation(ann),
+    };
+    let sum = (~ann=?, m): typ_t(DefaultAnnotation.t) => {
+      term: Sum(m),
+      annotation: default_annotation(ann),
+    };
+    let prod = (~ann=?, l): typ_t(DefaultAnnotation.t) => {
+      term: Prod(l),
+      annotation: default_annotation(ann),
+    };
+    let label = (~ann=?, l): typ_t(DefaultAnnotation.t) => {
+      term: Label(l),
+      annotation: default_annotation(ann),
+    };
+    let tup_label = (~ann=?, t1, t2): typ_t(DefaultAnnotation.t) => {
+      term: TupLabel(t1, t2),
+      annotation: default_annotation(ann),
+    };
+    let parens = (~ann=?, t): typ_t(DefaultAnnotation.t) => {
+      term: Parens(t),
+      annotation: default_annotation(ann),
+    };
+    let ap = (~ann=?, t1, t2): typ_t(DefaultAnnotation.t) => {
+      term: Ap(t1, t2),
+      annotation: default_annotation(ann),
+    };
+    let rec_ = (~ann=?, tp, t): typ_t(DefaultAnnotation.t) => {
+      term: Rec(tp, t),
+      annotation: default_annotation(ann),
+    };
+    let forall = (~ann=?, tp, t): typ_t(DefaultAnnotation.t) => {
+      term: Forall(tp, t),
+      annotation: default_annotation(ann),
+    };
+  };
+
+  module TPat = {
+    let invalid = (~ann=?, s): tpat_t(DefaultAnnotation.t) => {
+      term: Invalid(s),
+      annotation: default_annotation(ann),
+    };
+    let empty_hole = (~ann=?, ()): tpat_t(DefaultAnnotation.t) => {
+      term: EmptyHole,
+      annotation: default_annotation(ann),
+    };
+    let multi_hole = (~ann=?, l): tpat_t(DefaultAnnotation.t) => {
+      term: MultiHole(l),
+      annotation: default_annotation(ann),
+    };
+    let var = (~ann=?, s): tpat_t(DefaultAnnotation.t) => {
+      term: Var(s),
+      annotation: default_annotation(ann),
+    };
+  };
+
+  module Rul = {
+    let rul_invalid = (~ann=?, s): rul_t(DefaultAnnotation.t) => {
+      term: Invalid(s),
+      annotation: default_annotation(ann),
+    };
+    let rul_hole = (~ann=?, l): rul_t(DefaultAnnotation.t) => {
+      term: Hole(l),
+      annotation: default_annotation(ann),
+    };
+    let rul_rules = (~ann=?, e, l): rul_t(DefaultAnnotation.t) => {
+      term: Rules(e, l),
+      annotation: default_annotation(ann),
+    };
+  };
+
+  let environment = (env): environment_t(DefaultAnnotation.t) => {
+    VarBstMap.Ordered.mapo(((_, y)) => map_exp_annotation(x => x, y), env);
+  };
+
+  let closure_environment =
+      (id, env): closure_environment_t(DefaultAnnotation.t) => {
+    (id, environment(env));
+  };
+
+  module StepperFilter = {
+    let filter = (f): stepper_filter_kind_t(DefaultAnnotation.t) => {
+      Filter({pat: map_exp_annotation(x => x, f.pat), act: f.act});
+    };
+    let residue = (i, act): stepper_filter_kind_t(DefaultAnnotation.t) => {
+      Residue(i, act);
+    };
+  };
+
+  module TypeHole = {
+    let invalid = (s): type_hole(DefaultAnnotation.t) => {
+      Invalid(s);
+    };
+    let empty_hole = (): type_hole(DefaultAnnotation.t) => {
+      EmptyHole;
+    };
+    let multi_hole = (l): type_hole(DefaultAnnotation.t) => {
+      MultiHole(l);
+    };
+  };
+
+  module TypeProvenance = {
+    let syn_switch = (): type_provenance(DefaultAnnotation.t) => {
+      SynSwitch;
+    };
+    let hole = (h): type_provenance(DefaultAnnotation.t) => {
+      Hole(h);
+    };
+    let internal = (): type_provenance(DefaultAnnotation.t) => {
+      Internal;
+    };
+  };
+};
+
+module UnitGrammar =
+  Factory({
+    type t = unit;
+    let default_value = () => ();
+  });
diff --git a/src/haz3lcore/lang/term/IdTagged.re b/src/haz3lcore/lang/term/IdTagged.re
index 47f4a259a0..647ccfcf19 100644
--- a/src/haz3lcore/lang/term/IdTagged.re
+++ b/src/haz3lcore/lang/term/IdTagged.re
@@ -13,6 +13,8 @@ module IdTag = {
        at the end of evaluation to keep them unique.*/
     copied: bool,
   };
+
+  let fresh = (): t => {ids: [Id.mk()], copied: false};
 };
 
 [@deriving (show({with_path: false}), sexp, yojson)]
@@ -24,13 +26,7 @@ type t('a) = Grammar.Annotated.t('a, IdTag.t);
 //     fmt_a(formatter, ta.term);
 //   };
 let fresh = (term: 'a): Grammar.Annotated.t('a, IdTag.t) => {
-  {
-    term,
-    annotation: {
-      ids: [Id.mk()],
-      copied: false,
-    },
-  };
+  {term, annotation: IdTag.fresh()};
 };
 let fresh_deterministic = (prev_id, term): t('a) => {
   {
@@ -72,3 +68,9 @@ let replace_temp = ({term, annotation: {ids, copied}}: t('a)): t('a) => {
     copied,
   },
 };
+
+module FreshGrammar =
+  Grammar.Factory({
+    type t = IdTag.t;
+    let default_value = (): IdTag.t => IdTag.fresh();
+  });
diff --git a/src/haz3lcore/lang/term/TPat.re b/src/haz3lcore/lang/term/TPat.re
index b36b2e1cb8..f66f6bdfc8 100644
--- a/src/haz3lcore/lang/term/TPat.re
+++ b/src/haz3lcore/lang/term/TPat.re
@@ -1,4 +1,4 @@
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, enumerate, eq)]
 type cls =
   | Invalid
   | EmptyHole
@@ -17,7 +17,7 @@ let hole = (tms: list(TermBase.Any.t)): TermBase.TPat.term =>
   | [_, ..._] => MultiHole(tms)
   };
 
-let cls_of_term: term => cls =
+let cls_of_term: Grammar.tpat_term('a) => cls =
   fun
   | Invalid(_) => Invalid
   | EmptyHole => EmptyHole
diff --git a/src/haz3lcore/lang/term/Term.re b/src/haz3lcore/lang/term/Term.re
index 09f542300d..f99f407292 100644
--- a/src/haz3lcore/lang/term/Term.re
+++ b/src/haz3lcore/lang/term/Term.re
@@ -1,5 +1,5 @@
 module Pat = {
-  [@deriving (show({with_path: false}), sexp, yojson)]
+  [@deriving (show({with_path: false}), sexp, yojson, enumerate, eq)]
   type cls =
     | Invalid
     | EmptyHole
@@ -39,7 +39,7 @@ module Pat = {
     | [_, ..._] => MultiHole(tms)
     };
 
-  let cls_of_term: term => cls =
+  let cls_of_term: Grammar.pat_term('a) => cls =
     fun
     | Invalid(_) => Invalid
     | EmptyHole => EmptyHole
@@ -333,12 +333,11 @@ module Pat = {
 };
 
 module Exp = {
-  [@deriving (show({with_path: false}), sexp, yojson)]
+  [@deriving (show({with_path: false}), sexp, yojson, enumerate, eq)]
   type cls =
     | Invalid
     | EmptyHole
     | MultiHole
-    | StaticErrorHole
     | DynamicErrorHole
     | FailedCast
     | Deferral
@@ -356,14 +355,12 @@ module Exp = {
     | Tuple
     | Dot
     | Var
-    | MetaVar
     | Let
     | FixF
     | TyAlias
     | Ap
     | TypAp
     | DeferredAp
-    | Pipeline
     | If
     | Seq
     | Test
@@ -400,7 +397,7 @@ module Exp = {
   let term_of: t => term = IdTagged.term_of;
   let unwrap: t => (term, term => t) = IdTagged.unwrap;
 
-  let cls_of_term: term => cls =
+  let cls_of_term: Grammar.exp_term('a) => cls =
     fun
     | Invalid(_) => Invalid
     | EmptyHole => EmptyHole
@@ -447,7 +444,6 @@ module Exp = {
     | Invalid => "Invalid expression"
     | MultiHole => "Broken expression"
     | EmptyHole => "Empty expression hole"
-    | StaticErrorHole => "Static error hole"
     | DynamicErrorHole => "Dynamic error hole"
     | FailedCast => "Failed cast"
     | Deferral => "Deferral"
@@ -465,14 +461,12 @@ module Exp = {
     | TupLabel => "Labeled Tuple Item"
     | Dot => "Dot operator"
     | Var => "Variable reference"
-    | MetaVar => "Meta variable reference"
     | Let => "Let expression"
     | FixF => "Fixpoint operator"
     | TyAlias => "Type Alias definition"
     | Ap => "Application"
     | TypAp => "Type application"
     | DeferredAp => "Partial Application"
-    | Pipeline => "Pipeline expression"
     | If => "If expression"
     | Seq => "Sequence expression"
     | Test => "Test"
@@ -882,7 +876,7 @@ module Exp = {
 module Rul = {
   include TermBase.Rul;
 
-  [@deriving (show({with_path: false}), sexp, yojson)]
+  [@deriving (show({with_path: false}), sexp, yojson, enumerate)]
   type cls =
     | Rule;
 
diff --git a/src/haz3lcore/lang/term/Typ.re b/src/haz3lcore/lang/term/Typ.re
index 255f4b12c2..d6f2dd508a 100644
--- a/src/haz3lcore/lang/term/Typ.re
+++ b/src/haz3lcore/lang/term/Typ.re
@@ -1,7 +1,7 @@
 open Util;
 open OptUtil.Syntax;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, enumerate, eq)]
 type cls =
   | Invalid
   | EmptyHole
@@ -19,7 +19,7 @@ type cls =
   | Sum
   | List
   | Var
-  | Constructor
+  | Constructor // Constructor does not exist on Typ.term it's being used here as a hack for the cursors inspector
   | Parens
   | Ap
   | Rec
@@ -29,7 +29,6 @@ include TermBase.Typ;
 
 let term_of: t => term = IdTagged.term_of;
 let unwrap: t => (term, term => t) = IdTagged.unwrap;
-let rep_id: t => Id.t = IdTagged.rep_id;
 
 let fresh: term => t = IdTagged.fresh;
 /* fresh assigns a random id, whereas temp assigns Id.invalid, which
@@ -80,7 +79,7 @@ let hole = (tms: list(TermBase.Any.t)): TermBase.Typ.term =>
   | [_, ..._] => Unknown(Hole(MultiHole(tms)))
   };
 
-let cls_of_term: term => cls =
+let cls_of_term: Grammar.typ_term('a) => cls =
   fun
   | Unknown(Hole(Invalid(_))) => Invalid
   | Unknown(Hole(EmptyHole)) => EmptyHole
diff --git a/src/haz3lcore/tiles/Secondary.re b/src/haz3lcore/tiles/Secondary.re
index 7db7861256..b0173b3e1e 100644
--- a/src/haz3lcore/tiles/Secondary.re
+++ b/src/haz3lcore/tiles/Secondary.re
@@ -1,6 +1,6 @@
 open Util;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, enumerate)]
 type cls =
   | Whitespace
   | Comment;
diff --git a/src/haz3lmenhir/Conversion.re b/src/haz3lmenhir/Conversion.re
index 32da68b30a..93abe491f4 100644
--- a/src/haz3lmenhir/Conversion.re
+++ b/src/haz3lmenhir/Conversion.re
@@ -1,8 +1,10 @@
 include Sexplib.Std;
 
-// mutable array to gather indicated IDs when generating expressions
-let indicated_ids = Dynarray.create();
-
+module IndicatedG =
+  Haz3lcore.Grammar.Factory({
+    type t = bool;
+    let default_value = () => false;
+  });
 module FilterAction = {
   open Haz3lcore.FilterAction;
   let of_menhir_ast = (a: AST.filter_action): t => {
@@ -189,154 +191,119 @@ module Operators = {
 };
 
 module rec Exp: {
-  let term_of_menhir_ast: AST.exp => Haz3lcore.Exp.term;
-  let of_menhir_ast': AST.exp => Haz3lcore.Exp.t;
-  let of_menhir_ast: AST.exp => (Haz3lcore.Exp.t, list(Haz3lcore.Id.t));
-  let of_core: Haz3lcore.Exp.t => AST.exp;
+  let of_menhir_ast: AST.exp => IndicatedG.exp;
+  let of_core: IndicatedG.exp => AST.exp;
+  let get_indicated_ids:
+    IndicatedG.exp => (Haz3lcore.Exp.t, list(Haz3lcore.Id.t));
 } = {
-  let rec term_of_menhir_ast = (exp: AST.exp): Haz3lcore.Exp.term => {
+  open IndicatedG.Exp;
+  let rec of_menhir_ast = (exp: AST.exp): IndicatedG.exp => {
     switch (exp) {
-    | InvalidExp(s) => Invalid(s)
-    | Int(i) => Int(i)
-    | Float(f) => Float(f)
-    | String(s) => String(s)
-    | Bool(b) => Bool(b)
-    | Var(x) => Var(x)
+    | InvalidExp(s) => invalid(s)
+    | Int(i) => int(i)
+    | Float(f) => float(f)
+    | String(s) => string(s)
+    | Bool(b) => bool(b)
+    | Var(x) => var(x)
     | Constructor(x, ty) =>
-      Constructor(x, Option.map(Typ.of_menhir_ast', ty))
-    | Deferral => Deferral(InAp)
-    // switch (pos) {
-    // | InAp => Deferral(InAp)
-    // | OutsideAp => Deferral(OutsideAp)
-    // }
-    | ListExp(l) => ListLit(List.map(of_menhir_ast', l))
-    | TupleExp([TupLabel(_) as tl]) =>
-      Parens(Tuple([of_menhir_ast'(tl)]) |> Haz3lcore.Exp.fresh)
-    | TupleExp([e]) => Parens(of_menhir_ast'(e))
-    | TupleExp(e) =>
-      Parens(Tuple(List.map(of_menhir_ast', e)) |> Haz3lcore.Exp.fresh)
-    | Label(s) => Label(s)
-    | TupLabel(e1, e2) => TupLabel(of_menhir_ast'(e1), of_menhir_ast'(e2))
-    | Dot(e1, e2) => Dot(of_menhir_ast'(e1), of_menhir_ast'(e2))
+      constructor(x, Option.map(Typ.of_menhir_ast, ty))
+    | Deferral => deferral(InAp)
+    | ListExp(l) => list_lit(List.map(of_menhir_ast, l))
+    | TupleExp([TupLabel(_) as tl]) => parens(tuple([of_menhir_ast(tl)]))
+    | TupleExp([e]) => parens(of_menhir_ast(e))
+    | TupleExp(e) => parens(tuple(List.map(of_menhir_ast, e)))
+    | Label(s) => label(s)
+    | TupLabel(e1, e2) => tup_label(of_menhir_ast(e1), of_menhir_ast(e2))
+    | Dot(e1, e2) => dot(of_menhir_ast(e1), of_menhir_ast(e2))
     | Let(p, e1, e2) =>
-      Let(Pat.of_menhir_ast'(p), of_menhir_ast'(e1), of_menhir_ast'(e2))
-    | FixF(p, e) => FixF(Pat.of_menhir_ast'(p), of_menhir_ast'(e), None)
+      let_(Pat.of_menhir_ast(p), of_menhir_ast(e1), of_menhir_ast(e2))
+    | FixF(p, e) => fix_f(Pat.of_menhir_ast(p), of_menhir_ast(e), None)
     | TypFun(t, e) =>
-      TypFun(TPat.of_menhir_ast(t), of_menhir_ast'(e), None)
-    | Undefined => Undefined
+      typ_fun(TPat.of_menhir_ast(t), of_menhir_ast(e), None)
+    | Undefined => undefined()
     | TyAlias(tp, ty, e) =>
-      let ty = Typ.of_menhir_ast'(ty);
+      let ty = Typ.of_menhir_ast(ty);
       let ty =
         switch (ty) {
         | {term: Parens(ty), _} => ty
         | _ => ty
         };
-      TyAlias(TPat.of_menhir_ast(tp), ty, of_menhir_ast'(e));
-    | BuiltinFun(s) => BuiltinFun(s)
+      ty_alias(TPat.of_menhir_ast(tp), ty, of_menhir_ast(e));
+    | BuiltinFun(s) => builtin_fun(s)
     | Fun(p, e, name_opt) =>
       switch (name_opt) {
       | Some(name_str) =>
-        Fun(Pat.of_menhir_ast'(p), of_menhir_ast'(e), None, Some(name_str))
-      | None => Fun(Pat.of_menhir_ast'(p), of_menhir_ast'(e), None, None)
+        fn(Pat.of_menhir_ast(p), of_menhir_ast(e), None, Some(name_str))
+      | None => fn(Pat.of_menhir_ast(p), of_menhir_ast(e), None, None)
       }
     | ApExp(e1, args) =>
       switch (args) {
       | TupleExp(l) =>
         List.mem(AST.Deferral, l)
-          ? DeferredAp(of_menhir_ast'(e1), List.map(of_menhir_ast', l))
-          : Ap(
+          ? deferred_ap(of_menhir_ast(e1), List.map(of_menhir_ast, l))
+          : ap(
               Haz3lcore.Operators.Forward,
-              of_menhir_ast'(e1),
-              of_menhir_ast'(args),
+              of_menhir_ast(e1),
+              of_menhir_ast(args),
             )
-      | Deferral => DeferredAp(of_menhir_ast'(e1), [args |> of_menhir_ast'])
+      | Deferral => deferred_ap(of_menhir_ast(e1), [args |> of_menhir_ast])
 
       | _ =>
-        Ap(
+        ap(
           Haz3lcore.Operators.Forward,
-          of_menhir_ast'(e1),
-          of_menhir_ast'(args),
+          of_menhir_ast(e1),
+          of_menhir_ast(args),
         )
       }
     | BinExp(e1, op, e2) =>
-      BinOp(
+      bin_op(
         Operators.of_menhir_ast(op),
-        of_menhir_ast'(e1),
-        of_menhir_ast'(e2),
+        of_menhir_ast(e1),
+        of_menhir_ast(e2),
       )
 
     | If(e1, e2, e3) =>
-      If(of_menhir_ast'(e1), of_menhir_ast'(e2), of_menhir_ast'(e3))
+      if_(of_menhir_ast(e1), of_menhir_ast(e2), of_menhir_ast(e3))
     | CaseExp(e, l) =>
-      let d_scrut = of_menhir_ast'(e);
+      let d_scrut = of_menhir_ast(e);
       let d_rules =
         List.map(
-          ((pat, exp)) => (Pat.of_menhir_ast'(pat), of_menhir_ast'(exp)),
+          ((pat, exp)) => (Pat.of_menhir_ast(pat), of_menhir_ast(exp)),
           l,
         );
-      Match(d_scrut, d_rules);
+      match(d_scrut, d_rules);
     | Cast(e, t1, t2) =>
-      Cast(
-        of_menhir_ast'(e),
-        Typ.of_menhir_ast'(t1),
-        Typ.of_menhir_ast'(t2),
-      )
+      cast(of_menhir_ast(e), Typ.of_menhir_ast(t1), Typ.of_menhir_ast(t2))
     | FailedCast(e, t1, t2) =>
-      FailedCast(
-        of_menhir_ast'(e),
-        Typ.of_menhir_ast'(t1),
-        Typ.of_menhir_ast'(t2),
+      failed_cast(
+        of_menhir_ast(e),
+        Typ.of_menhir_ast(t1),
+        Typ.of_menhir_ast(t2),
       )
-    | EmptyHole => EmptyHole
-    | Seq(e1, e2) => Seq(of_menhir_ast'(e1), of_menhir_ast'(e2))
-    | Test(e) => Test(of_menhir_ast'(e))
-    | Cons(e1, e2) => Cons(of_menhir_ast'(e1), of_menhir_ast'(e2))
+    | EmptyHole => empty_hole()
+    | Seq(e1, e2) => seq(of_menhir_ast(e1), of_menhir_ast(e2))
+    | Test(e) => test(of_menhir_ast(e))
+    | Cons(e1, e2) => cons(of_menhir_ast(e1), of_menhir_ast(e2))
     | ListConcat(e1, e2) =>
-      ListConcat(of_menhir_ast'(e1), of_menhir_ast'(e2))
+      list_concat(of_menhir_ast(e1), of_menhir_ast(e2))
     | Filter(a, cond, body) =>
-      let dcond = of_menhir_ast'(cond);
-      let dbody = of_menhir_ast'(body);
+      let dcond = of_menhir_ast(cond);
+      let dbody = of_menhir_ast(body);
       let act = FilterAction.of_menhir_ast(a);
-      Filter(Filter({pat: dcond, act}), dbody);
-    | TypAp(e, ty) => TypAp(of_menhir_ast'(e), Typ.of_menhir_ast'(ty))
+      filter(Filter({pat: dcond, act}), dbody);
+    | TypAp(e, ty) => typ_ap(of_menhir_ast(e), Typ.of_menhir_ast(ty))
     | UnOp(op, e) =>
-      UnOp(Operators.op_un_of_menhir_ast(op), of_menhir_ast'(e))
+      un_op(Operators.op_un_of_menhir_ast(op), of_menhir_ast(e))
     | DynamicErrorHole(e, s) =>
-      DynamicErrorHole(
-        of_menhir_ast'(e),
+      dynamic_error_hole(
+        of_menhir_ast(e),
         Haz3lcore.InvalidOperationError.t_of_sexp(sexp_of_string(s)),
       )
-    | IndicationExp(_) =>
-      failwith(
-        "IndicationExp should not appear as argument to term_of_menhir_ast.",
-      )
-    };
-  }
-  and of_menhir_ast' = (exp: AST.exp): Haz3lcore.Exp.t => {
-    switch (exp) {
-    | IndicationExp(e) =>
-      let id = Haz3lcore.Id.mk();
-      Dynarray.add_last(indicated_ids, id);
-      {
-        term: term_of_menhir_ast(e),
-        annotation: {
-          ids: [id],
-          copied: false,
-        },
-      };
-    | _ => Haz3lcore.IdTagged.fresh(term_of_menhir_ast(exp))
+    | IndicationExp(e) => {annotation: true, term: of_menhir_ast(e).term}
     };
   };
 
-  let of_menhir_ast =
-      (exp: AST.exp): (Haz3lcore.Exp.t, list(Haz3lcore.Id.t)) => {
-    Dynarray.clear(indicated_ids);
-    let e = of_menhir_ast'(exp);
-    let ids = Dynarray.to_list(indicated_ids);
-    (e, ids);
-  };
-
-  let rec of_core = (exp: Haz3lcore.Exp.t): AST.exp => {
+  let rec of_core = (exp: IndicatedG.exp): AST.exp => {
     switch (exp.term) {
     | Invalid(_) => InvalidExp("Invalid")
     | Int(i) => Int(i)
@@ -396,89 +363,83 @@ module rec Exp: {
     | Ap(Reverse, _, _) => raise(Failure("Reverse not supported"))
     };
   };
+
+  let get_indicated_ids =
+      (indicated_exp: IndicatedG.exp)
+      : (Haz3lcore.Exp.t, list(Haz3lcore.Id.t)) => {
+    open Haz3lcore;
+    // mutable array to gather indicated IDs when generating expressions
+    let indicated_ids = Dynarray.create();
+    let e =
+      Grammar.map_exp_annotation(
+        (indicated): IdTagged.IdTag.t => {
+          let id = Id.mk();
+          if (indicated) {
+            Dynarray.add_last(indicated_ids, id);
+          };
+          {ids: [id], copied: false};
+        },
+        indicated_exp,
+      );
+    let ids = Dynarray.to_list(indicated_ids);
+    (e, ids);
+  };
 }
 and Typ: {
-  let of_menhir_ast': AST.typ => Haz3lcore.Typ.t;
-
-  let of_core: Haz3lcore.Typ.t => AST.typ;
+  let of_menhir_ast: AST.typ => IndicatedG.typ;
+  let of_core: IndicatedG.typ => AST.typ;
 } = {
-  let rec of_menhir_ast' = (typ: AST.typ): Haz3lcore.Typ.t => {
+  open IndicatedG.Typ;
+  let rec of_menhir_ast = (typ: AST.typ): IndicatedG.typ => {
     switch (typ) {
-    | IndicationTyp(t) =>
-      let id = Haz3lcore.Id.mk();
-      Dynarray.add_last(indicated_ids, id);
-      {
-        term: term_of_menhir_ast(t),
-        annotation: {
-          ids: [id],
-          copied: false,
-        },
-      };
-    | _ => Haz3lcore.IdTagged.fresh(term_of_menhir_ast(typ))
-    };
-  }
-  and term_of_menhir_ast = (typ: AST.typ): Haz3lcore.Typ.term => {
-    switch (typ) {
-    | InvalidTyp(s) => Unknown(Hole(Invalid(s)))
-    | IntType => Int
-    | FloatType => Float
-    | BoolType => Bool
-    | StringType => String
+    | InvalidTyp(s) => unknown(Hole(Invalid(s)))
+    | IntType => int()
+    | FloatType => float()
+    | BoolType => bool()
+    | StringType => string()
     | UnknownType(p) =>
       switch (p) {
-      | Internal => Unknown(Internal)
-      | EmptyHole => Unknown(Hole(EmptyHole))
+      | Internal => unknown(Internal)
+      | EmptyHole => unknown(Hole(EmptyHole))
       }
-    | TypVar(s) => Var(s)
-    | TupleType([t]) => Parens(of_menhir_ast'(t))
-    | TupleType(ts) =>
-      Parens(Prod(List.map(of_menhir_ast', ts)) |> Haz3lcore.Typ.fresh)
-    | LabelType(s) => Label(s)
+    | TypVar(s) => var(s)
+    | TupleType([t]) => parens(of_menhir_ast(t))
+    | TupleType(ts) => parens(prod(List.map(of_menhir_ast, ts)))
+    | LabelType(s) => label(s)
     | TupLabelType(t1, t2) =>
-      TupLabel(of_menhir_ast'(t1), of_menhir_ast'(t2))
-    | ArrayType(t) => List(of_menhir_ast'(t))
-    | ArrowType(t1, t2) => Arrow(of_menhir_ast'(t1), of_menhir_ast'(t2))
+      tup_label(of_menhir_ast(t1), of_menhir_ast(t2))
+    | ArrayType(t) => list(of_menhir_ast(t))
+    | ArrowType(t1, t2) => arrow(of_menhir_ast(t1), of_menhir_ast(t2))
     | SumTyp(sumterms) =>
       open Haz3lcore;
-      let converted_terms: list(ConstructorMap.variant(TermBase.typ_t)) =
+      let converted_terms: list(ConstructorMap.variant(IndicatedG.typ)) =
         List.map(
-          (sumterm: AST.sumterm): ConstructorMap.variant(TermBase.typ_t) =>
+          (sumterm: AST.sumterm): ConstructorMap.variant(IndicatedG.typ) =>
             switch (sumterm) {
             | Variant(name, typ) =>
-              Variant(name, [Id.mk()], Option.map(of_menhir_ast', typ))
-            | BadEntry(typ) => BadEntry(of_menhir_ast'(typ))
+              Variant(name, [Id.mk()], Option.map(of_menhir_ast, typ))
+            | BadEntry(typ) => BadEntry(of_menhir_ast(typ))
             },
           sumterms,
         );
-      Parens(Sum(converted_terms) |> Typ.fresh); // Adds parens due to MakeTerm
+      parens(sum(converted_terms));
     | ForallType(tp, t) =>
-      Parens(
-        Forall(TPat.of_menhir_ast(tp), of_menhir_ast'(t))
-        |> Haz3lcore.Typ.fresh,
-      )
+      parens(forall(TPat.of_menhir_ast(tp), of_menhir_ast(t)))
     | RecType(tp, t) =>
-      Parens(
-        Rec(TPat.of_menhir_ast(tp), of_menhir_ast'(t))
-        |> Haz3lcore.Typ.fresh,
-      ) // Parens because of (rec ? -> Bool, ())
-    | IndicationTyp(_) =>
-      raise(
-        Failure(
-          "IndicationExp should not appear as argument to term_of_menhir_ast.",
-        ),
-      )
+      parens(rec_(TPat.of_menhir_ast(tp), of_menhir_ast(t)))
+    | IndicationTyp(t) => {annotation: true, term: of_menhir_ast(t).term}
     };
   };
 
   let of_core_type_provenance =
-      (p: Haz3lcore.TermBase.type_provenance): AST.typ_provenance => {
+      (p: IndicatedG.typ_provenance): AST.typ_provenance => {
     switch (p) {
     | Internal => Internal
     | Hole(EmptyHole) => EmptyHole
     | _ => raise(Failure("Unknown type_provenance"))
     };
   };
-  let rec of_core = (typ: Haz3lcore.Typ.t): AST.typ => {
+  let rec of_core = (typ: IndicatedG.typ): AST.typ => {
     switch (typ.term) {
     | Int => IntType
     | Float => FloatType
@@ -498,7 +459,7 @@ and Typ: {
     | Sum(constructors) =>
       let sumterms =
         List.map(
-          (variant: Haz3lcore.ConstructorMap.variant(Haz3lcore.Typ.t)): AST.sumterm => {
+          (variant: Haz3lcore.ConstructorMap.variant(IndicatedG.typ)): AST.sumterm => {
             switch (variant) {
             | Variant(name, _, None) => Variant(name, None)
             | Variant(name, _, Some(t)) => Variant(name, Some(of_core(t)))
@@ -512,22 +473,19 @@ and Typ: {
   };
 }
 and TPat: {
-  let of_menhir_ast: AST.tpat => Haz3lcore.TPat.t;
-  let term_of_menhir_ast: AST.tpat => Haz3lcore.TPat.term;
-  let of_core: Haz3lcore.TPat.t => AST.tpat;
+  let of_menhir_ast: AST.tpat => IndicatedG.tpat;
+  let of_core: IndicatedG.tpat => AST.tpat;
 } = {
-  let rec term_of_menhir_ast = (tpat: AST.tpat): Haz3lcore.TPat.term => {
+  open IndicatedG.TPat;
+  let of_menhir_ast = (tpat: AST.tpat): IndicatedG.tpat => {
     switch (tpat) {
-    | InvalidTPat(s) => Invalid(s)
-    | EmptyHoleTPat => EmptyHole
-    | VarTPat(s) => Var(s)
+    | InvalidTPat(s) => invalid(s)
+    | EmptyHoleTPat => empty_hole()
+    | VarTPat(s) => var(s)
     };
-  }
-  and of_menhir_ast = (tpat: AST.tpat) => {
-    Haz3lcore.IdTagged.fresh(term_of_menhir_ast(tpat));
   };
 
-  let of_core = (tpat: Haz3lcore.TPat.t): AST.tpat => {
+  let of_core = (tpat: IndicatedG.tpat): AST.tpat => {
     switch (tpat.term) {
     | EmptyHole => EmptyHoleTPat
     | Var(x) => VarTPat(x)
@@ -537,66 +495,42 @@ and TPat: {
   };
 }
 and Pat: {
-  let term_of_menhir_ast: AST.pat => Haz3lcore.Pat.term;
-  let of_menhir_ast': AST.pat => Haz3lcore.Pat.t;
-  let of_core: Haz3lcore.Pat.t => AST.pat;
+  let of_menhir_ast: AST.pat => IndicatedG.pat;
+  let of_core: IndicatedG.pat => AST.pat;
 } = {
-  let rec term_of_menhir_ast = (pat: AST.pat): Haz3lcore.Pat.term => {
+  open IndicatedG.Pat;
+  let rec of_menhir_ast = (pat: AST.pat): IndicatedG.pat => {
     switch (pat) {
-    | InvalidPat(s) => Invalid(s)
-    | IntPat(i) => Int(i)
-    | FloatPat(f) => Float(f)
+    | InvalidPat(s) => invalid(s)
+    | IntPat(i) => int(i)
+    | FloatPat(f) => float(f)
     | CastPat(p, t1, t2) =>
-      Parens(
-        Cast(
-          of_menhir_ast'(p),
-          Typ.of_menhir_ast'(t1),
-          Typ.of_menhir_ast'(t2),
-        )
-        |> Haz3lcore.Pat.fresh,
+      parens(
+        cast(
+          of_menhir_ast(p),
+          Typ.of_menhir_ast(t1),
+          Typ.of_menhir_ast(t2),
+        ),
       )
-    | VarPat(x) => Var(x)
+    | VarPat(x) => var(x)
     | ConstructorPat(x, ty) =>
-      Constructor(x, Option.map(Typ.of_menhir_ast', ty))
-    | StringPat(s) => String(s)
-    | TuplePat(pats) =>
-      Parens(Tuple(List.map(of_menhir_ast', pats)) |> Haz3lcore.Pat.fresh)
-    | ApPat(pat1, pat2) => Ap(of_menhir_ast'(pat1), of_menhir_ast'(pat2))
+      constructor(x, Option.map(Typ.of_menhir_ast, ty))
+    | StringPat(s) => string(s)
+    | TuplePat(pats) => parens(tuple(List.map(of_menhir_ast, pats)))
+    | ApPat(pat1, pat2) => ap(of_menhir_ast(pat1), of_menhir_ast(pat2))
     | ConsPat(p1, p2) =>
-      Parens(
-        Cons(of_menhir_ast'(p1), of_menhir_ast'(p2)) |> Haz3lcore.Pat.fresh,
-      )
-    | BoolPat(b) => Bool(b)
-    | EmptyHolePat => EmptyHole
-    | WildPat => Wild
-    | LabelPat(s) => Label(s)
+      parens(cons(of_menhir_ast(p1), of_menhir_ast(p2)))
+    | BoolPat(b) => bool(b)
+    | EmptyHolePat => empty_hole()
+    | WildPat => wild()
+    | LabelPat(s) => label(s)
     | TupLabelPat(p1, p2) =>
-      TupLabel(of_menhir_ast'(p1), of_menhir_ast'(p2))
-    | ListPat(l) => ListLit(List.map(of_menhir_ast', l))
-    | IndicationPat(_) =>
-      raise(
-        Failure(
-          "IndicationPat should not appear as argument to term_of_menhir_ast.",
-        ),
-      )
-    };
-  }
-  and of_menhir_ast' = (pat: AST.pat): Haz3lcore.Pat.t => {
-    switch (pat) {
-    | IndicationPat(p) =>
-      let id = Haz3lcore.Id.mk();
-      Dynarray.add_last(indicated_ids, id);
-      {
-        term: term_of_menhir_ast(p),
-        annotation: {
-          ids: [id],
-          copied: false,
-        },
-      };
-    | _ => Haz3lcore.IdTagged.fresh(term_of_menhir_ast(pat))
+      tup_label(of_menhir_ast(p1), of_menhir_ast(p2))
+    | ListPat(l) => list_lit(List.map(of_menhir_ast, l))
+    | IndicationPat(p) => {annotation: true, term: of_menhir_ast(p).term}
     };
   };
-  let rec of_core = (pat: Haz3lcore.Pat.t): AST.pat => {
+  let rec of_core = (pat: IndicatedG.pat): AST.pat => {
     switch (pat.term) {
     | Invalid(_) => InvalidPat("Invalid")
     | Int(i) => IntPat(i)
diff --git a/test/Test_Coverage.re b/test/Test_Coverage.re
index e4a7bea4b2..9904cba0ab 100644
--- a/test/Test_Coverage.re
+++ b/test/Test_Coverage.re
@@ -20,7 +20,10 @@ let has_errors = (name: string, exp: string, errors: list(Info.error)) => {
     name,
     `Quick,
     () => {
-      let (e, ids) = parse_menhir(exp);
+      let indicated_exp: Grammar.exp_t(bool) = parse_menhir(exp);
+      let (e, ids) =
+        Haz3lmenhir.Conversion.Exp.get_indicated_ids(indicated_exp);
+
       let s = statics(e);
       let actual_errors = Statics.collect_errors(s);
       let expected_errors = Id.Map.of_list(List.combine(ids, errors));
diff --git a/test/Test_Elaboration.re b/test/Test_Elaboration.re
index 69ad35d5d7..072fbe7978 100644
--- a/test/Test_Elaboration.re
+++ b/test/Test_Elaboration.re
@@ -879,13 +879,17 @@ in 1|},
 module MenhirElaborationTests = {
   //dhexp = expected
   //uexp = tested
-  let alco_check_menhir = (name: string, dhexp: string, uexp: Term.Exp.t) => {
-    let (e, _) =
-      Haz3lmenhir.Conversion.Exp.of_menhir_ast(
-        Haz3lmenhir.Interface.parse_program(dhexp),
-      );
-    alco_check(name, e, dhexp_of_uexp(uexp));
-  };
+  let alco_check_menhir = (name: string, dhexp: string, uexp: Term.Exp.t) =>
+    alco_check(
+      name,
+      Grammar.map_exp_annotation(
+        _ => IdTagged.IdTag.fresh(),
+        Haz3lmenhir.Conversion.Exp.of_menhir_ast(
+          Haz3lmenhir.Interface.parse_program(dhexp),
+        ),
+      ),
+      dhexp_of_uexp(uexp),
+    );
 
   //Test for an empty hole
   let empty_hole_str = "?";
diff --git a/test/Test_Grammar.re b/test/Test_Grammar.re
index 11e7565e8e..d899ab9c05 100644
--- a/test/Test_Grammar.re
+++ b/test/Test_Grammar.re
@@ -1,5 +1,5 @@
 open Haz3lcore;
-
+open Alcotest;
 let qcheck_map_annotation_test =
   QCheck.Test.make(
     ~name="Map annotation to something and back",
@@ -9,7 +9,12 @@ let qcheck_map_annotation_test =
       Haz3lmenhir.AST.gen_exp_sized(7),
     ),
     exp => {
-      let (core_exp, _) = Haz3lmenhir.Conversion.Exp.of_menhir_ast(exp);
+      let indicated_exp = Haz3lmenhir.Conversion.Exp.of_menhir_ast(exp);
+      let core_exp =
+        Grammar.map_exp_annotation(
+          _ => IdTagged.IdTag.fresh(),
+          indicated_exp,
+        );
       let _ = [%derive.show: Exp.t](core_exp); // Gets coverage for show
       Grammar.equal_exp_t(
         (==),
@@ -18,7 +23,227 @@ let qcheck_map_annotation_test =
       );
     },
   );
+
+/*
+ * Constructs a sample expression from a given class expression.
+ * This is used to make sure we have a factory function for every expression
+ * and to make sure that we can actually construct one for every class.
+ * The correspondence is tested below.
+ */
+let sample_expression = (cls_exp: Exp.cls): Grammar.UnitGrammar.exp => {
+  Grammar.UnitGrammar.(
+    Exp.(
+      switch (cls_exp) {
+      | Invalid => invalid("invalid")
+      | EmptyHole => empty_hole()
+      | MultiHole => multi_hole([Exp(empty_hole()), Exp(empty_hole())])
+      | DynamicErrorHole => dynamic_error_hole(empty_hole(), DivideByZero)
+      | FailedCast => failed_cast(empty_hole(), Typ.int(), Typ.string())
+      | Deferral => deferral(InAp)
+      | Undefined => undefined()
+      | Bool => bool(true)
+      | Int => int(1)
+      | Float => float(2.)
+      | String => string("hello")
+      | ListLit => list_lit([])
+      | Constructor => constructor("A", None)
+      | Fun => fn(Pat.var("x"), var("x"), None, None)
+      | TypFun => typ_fun(TPat.var("x"), empty_hole(), None)
+      | Label => label("label")
+      | TupLabel => tup_label(label("label"), empty_hole())
+      | Tuple => tuple([])
+      | Dot => dot(empty_hole(), empty_hole())
+      | Var => var("x")
+      | Let => let_(Pat.empty_hole(), empty_hole(), empty_hole())
+      | FixF => fix_f(Pat.empty_hole(), empty_hole(), None)
+      | TyAlias =>
+        ty_alias(
+          TPat.empty_hole(),
+          Typ.unknown(Hole(EmptyHole)),
+          empty_hole(),
+        )
+      | Ap => ap(Forward, empty_hole(), empty_hole())
+      | TypAp => typ_ap(empty_hole(), Typ.unknown(Hole(EmptyHole)))
+      | DeferredAp => deferred_ap(empty_hole(), [empty_hole()])
+      | If => if_(empty_hole(), empty_hole(), empty_hole())
+      | Seq => seq(empty_hole(), empty_hole())
+      | Test => test(empty_hole())
+      | Filter =>
+        filter(StepperFilter.residue(0, (Step, One)), empty_hole())
+      | Closure =>
+        module M = {
+          include VarBstMap.Ordered;
+        };
+
+        closure(closure_environment(Id.mk(), M.empty), empty_hole());
+      | Parens => parens(empty_hole())
+      | Cons => cons(empty_hole(), empty_hole())
+      | UnOp(op) => un_op(op, empty_hole())
+      | BinOp(op) => bin_op(op, empty_hole(), empty_hole())
+      | BuiltinFun => builtin_fun("string_compare")
+      | Match => match(empty_hole(), [])
+      | Cast => cast(empty_hole(), Typ.int(), Typ.string())
+      | ListConcat => list_concat(empty_hole(), empty_hole())
+      }
+    )
+  );
+};
+
+let sample_pattern = (cls_pat: Pat.cls): Grammar.UnitGrammar.pat => {
+  Grammar.UnitGrammar.(
+    Pat.(
+      switch (cls_pat) {
+      | Invalid => invalid("invalid")
+      | EmptyHole => empty_hole()
+      | MultiHole => multi_hole([Pat(empty_hole()), Pat(empty_hole())])
+      | Bool => bool(true)
+      | Int => int(1)
+      | Float => float(2.)
+      | String => string("hello")
+      | ListLit => list_lit([])
+      | Constructor => constructor("A", None)
+      | Var => var("x")
+      | Tuple => tuple([])
+      | Cons => cons(empty_hole(), empty_hole())
+      | Label => label("label")
+      | TupLabel => tup_label(label("label"), empty_hole())
+      | Parens => parens(empty_hole())
+      | Ap => ap(empty_hole(), empty_hole())
+      | Cast => cast(empty_hole(), Typ.int(), Typ.string())
+      | Wild => wild()
+      }
+    )
+  );
+};
+
+let sample_type = (cls_typ: Typ.cls): Grammar.UnitGrammar.typ => {
+  Grammar.UnitGrammar.(
+    Typ.(
+      switch (cls_typ) {
+      | Invalid => unknown(Hole(Invalid("invalid")))
+      | Int => int()
+      | Float => float()
+      | String => string()
+      | Bool => bool()
+      | List => list(unknown(Hole(EmptyHole)))
+      | Arrow => arrow(unknown(Hole(EmptyHole)), unknown(Hole(EmptyHole)))
+      | Var => var("x")
+      | Prod => prod([])
+      | TupLabel =>
+        tup_label(unknown(Hole(EmptyHole)), unknown(Hole(EmptyHole)))
+      | Parens => parens(unknown(Hole(EmptyHole)))
+      | Ap => ap(unknown(Hole(EmptyHole)), unknown(Hole(EmptyHole)))
+      | Rec => rec_(TPat.var("x"), unknown(Hole(EmptyHole)))
+      | Forall => forall(TPat.var("x"), unknown(Hole(EmptyHole)))
+      | EmptyHole => unknown(Hole(EmptyHole))
+      | SynSwitch => unknown(SynSwitch)
+      | Internal => unknown(Internal)
+      | Label => label("label")
+      | MultiHole => unknown(Hole(MultiHole([])))
+      | Sum => sum([])
+      | Constructor => assert(false) // Excluded because there is no Typ constructor
+      }
+    )
+  );
+};
+
+let sample_tpat = (cls_tpat: TPat.cls): Grammar.UnitGrammar.tpat => {
+  Grammar.UnitGrammar.(
+    TPat.(
+      switch (cls_tpat) {
+      | Invalid => invalid("invalid")
+      | EmptyHole => empty_hole()
+      | Var => var("x")
+      | MultiHole => multi_hole([TPat(empty_hole()), TPat(empty_hole())])
+      }
+    )
+  );
+};
+
 let tests = (
   "Grammar",
-  [QCheck_alcotest.to_alcotest(qcheck_map_annotation_test)],
+  [
+    test_case(
+      "Expression classes are correct",
+      `Quick,
+      () => {
+        let exp_classes = Exp.all_of_cls;
+        let cls_testable =
+          testable(Fmt.using(Exp.show_cls, Fmt.string), Exp.equal_cls);
+        List.iter(
+          cls =>
+            check(
+              cls_testable,
+              Exp.show_cls(cls) ++ " Equivalency",
+              cls,
+              Exp.cls_of_term(sample_expression(cls).term),
+            ),
+          exp_classes,
+        );
+      },
+    ),
+    test_case(
+      "Pattern classes are correct",
+      `Quick,
+      () => {
+        let pat_classes = Pat.all_of_cls;
+        let cls_testable =
+          testable(Fmt.using(Pat.show_cls, Fmt.string), Pat.equal_cls);
+        List.iter(
+          cls =>
+            check(
+              cls_testable,
+              Pat.show_cls(cls) ++ " Equivalency",
+              cls,
+              Pat.cls_of_term(sample_pattern(cls).term),
+            ),
+          pat_classes,
+        );
+      },
+    ),
+    test_case(
+      "Type classes are correct",
+      `Quick,
+      () => {
+        let typ_classes = Typ.all_of_cls;
+        let cls_testable =
+          testable(Fmt.using(Typ.show_cls, Fmt.string), Typ.equal_cls);
+        List.iter(
+          (cls: Typ.cls) => {
+            switch (cls) {
+            | Constructor => ()
+            | _ =>
+              check(
+                cls_testable,
+                Typ.show_cls(cls) ++ " Equivalency",
+                cls,
+                Typ.cls_of_term(sample_type(cls).term),
+              )
+            }
+          },
+          typ_classes,
+        );
+      },
+    ),
+    test_case(
+      "Type pattern classes are correct",
+      `Quick,
+      () => {
+        let tpat_classes = TPat.all_of_cls;
+        let cls_testable =
+          testable(Fmt.using(TPat.show_cls, Fmt.string), TPat.equal_cls);
+        List.iter(
+          cls =>
+            check(
+              cls_testable,
+              TPat.show_cls(cls) ++ " Equivalency",
+              cls,
+              TPat.cls_of_term(sample_tpat(cls).term),
+            ),
+          tpat_classes,
+        );
+      },
+    ),
+    QCheck_alcotest.to_alcotest(qcheck_map_annotation_test),
+  ],
 );
diff --git a/test/Test_MakeTerm.re b/test/Test_MakeTerm.re
index c3c98fb6db..4f747c10f4 100644
--- a/test/Test_MakeTerm.re
+++ b/test/Test_MakeTerm.re
@@ -4,7 +4,7 @@
  */
 open Alcotest;
 open Haz3lcore;
-
+module Fresh = IdTagged.FreshGrammar;
 let exp_typ = testable(Fmt.using(Exp.show, Fmt.string), Exp.fast_equal);
 
 let parse_exp = (s: string) => {
@@ -16,217 +16,139 @@ let parse_exp = (s: string) => {
 let exp_check = (expected, actual) =>
   check(exp_typ, actual, expected, parse_exp(actual));
 
-let tests = (
-  "MakeTerm",
-  [
-    test_case("Integer Literal", `Quick, () => {
-      exp_check(Int(0) |> Exp.fresh, "0")
-    }),
-    test_case("Float literal", `Quick, () => {
-      exp_check(Float(2.000000) |> Exp.fresh, "2.000000")
-    }),
-    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("Floating operation", `Quick, () => {
-      exp_check(
-        BinOp(
-          Float(Plus),
-          Float(1.0) |> Exp.fresh,
-          Float(2.0) |> Exp.fresh,
+let tests =
+  Fresh.(
+    "MakeTerm",
+    Exp.[
+      test_case("Integer Literal", `Quick, () => exp_check(int(0), "0")),
+      test_case("Float literal", `Quick, () =>
+        exp_check(float(2.000000), "2.000000")
+      ),
+      test_case("Empty Hole", `Quick, () => exp_check(empty_hole(), "?")),
+      test_case("Free Variable", `Quick, () => exp_check(var("x"), "x")),
+      test_case("Parenthesized Expression", `Quick, () =>
+        exp_check(parens(int(0)), "(0)")
+      ),
+      test_case("Floating operation", `Quick, () =>
+        exp_check(bin_op(Float(Plus), float(1.0), float(2.0)), "1. +. 2.")
+      ),
+      test_case("Let Expression", `Quick, () =>
+        exp_check(let_(Pat.var("x"), int(1), var("x")), "let x = 1 in x")
+      ),
+      test_case("Function Application", `Quick, () =>
+        exp_check(ap(Forward, var("f"), var("x")), "f(x)")
+      ),
+      test_case("Named Function Definition", `Quick, () =>
+        exp_check(
+          let_(
+            Pat.var("f"),
+            fn(Pat.var("x"), var("x"), None, None), // It seems as though the function naming happens during elaboration and not during parsing
+            int(1),
+          ),
+          "let f = fun x -> x in 1",
         )
-        |> Exp.fresh,
-        "1. +. 2.",
-      )
-    }),
-    test_case("Let Expression", `Quick, () => {
-      exp_check(
-        Let(
-          Var("x") |> Pat.fresh,
-          Int(1) |> Exp.fresh,
-          Var("x") |> Exp.fresh,
+      ),
+      test_case("Incomplete Function Definition", `Quick, () =>
+        exp_check(
+          let_(
+            Pat.empty_hole(),
+            fn(Pat.var("x"), empty_hole(), None, None),
+            empty_hole(),
+          ),
+          "let    = fun x ->   in  ",
         )
-        |> 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,
+      ),
+      test_case("Constructor", `Quick, () =>
+        exp_check(constructor("A", None), "A")
+      ),
+      test_case("Type Alias", `Quick, () =>
+        exp_check(
+          ty_alias(TPat.var("x"), Typ.int(), int(1)),
+          "type x = Int in 1",
         )
-        |> 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,
+      ),
+      test_case("Singleton Labled Tuple ascription in let", `Quick, () =>
+        exp_check(
+          let_(
+            Pat.cast(
+              Pat.var("x"),
+              Typ.(parens(prod([tup_label(label("l"), string())]))),
+              Typ.unknown(Internal),
+            ),
+            parens(string("a")),
+            var("x"),
+          ),
+          "let x : (l=String) = (\"a\") in x",
         )
-        |> Exp.fresh,
-        "let    = fun x ->   in  ",
-      )
-    }),
-    test_case("Constructor", `Quick, () => {
-      exp_check(Constructor("A", None) |> Exp.fresh, "A")
-    }),
-    test_case("Type Alias", `Quick, () => {
-      exp_check(
-        TyAlias(
-          Var("x") |> TPat.fresh,
-          Int |> Typ.fresh,
-          Int(1) |> Exp.fresh,
+      ),
+      test_case("Assigning labeled tuple to variable", `Quick, () =>
+        exp_check(
+          let_(
+            Pat.var("x"),
+            parens(tuple([tup_label(label("l"), int(32))])),
+            let_(
+              Pat.(
+                cast(
+                  var("y"),
+                  Typ.(parens(prod([tup_label(label("l"), int())]))),
+                  Typ.unknown(Internal),
+                )
+              ),
+              var("x"),
+              var("y"),
+            ),
+          ),
+          "let x = (l=32) in
+             let y : (l=Int) = x in y",
         )
-        |> Exp.fresh,
-        "type x = Int in 1",
-      )
-    }),
-    test_case("Singleton Labled Tuple ascription in let", `Quick, () => {
-      exp_check(
-        Let(
-          Cast(
-            Var("x") |> Pat.fresh,
-            Parens(
-              Prod([
-                TupLabel(Label("l") |> Typ.fresh, String |> Typ.fresh)
-                |> Typ.fresh,
-              ])
-              |> Typ.fresh,
-            )
-            |> Typ.fresh,
-            Unknown(Internal) |> Typ.fresh,
-          )
-          |> Pat.fresh,
-          Parens(String("a") |> Exp.fresh) |> Exp.fresh,
-          Var("x") |> Exp.fresh,
+      ),
+      test_case("Multiple labels tuple", `Quick, () =>
+        exp_check(
+          parens(
+            tuple([
+              tup_label(label("l"), int(32)),
+              tup_label(label("l2"), string("")),
+            ]),
+          ),
+          {|(l=32, l2="")|},
         )
-        |> Exp.fresh,
-        "let x : (l=String) = (\"a\") in x",
-      )
-    }),
-    test_case("Assigning labeled tuple to variable", `Quick, () => {
-      exp_check(
-        Let(
-          Var("x") |> Pat.fresh,
-          Parens(
-            Tuple([
-              TupLabel(Label("l") |> Exp.fresh, Int(32) |> Exp.fresh)
-              |> Exp.fresh,
-            ])
-            |> Exp.fresh,
-          )
-          |> Exp.fresh,
-          Let(
-            Cast(
-              Var("y") |> Pat.fresh,
-              Parens(
-                Prod([
-                  TupLabel(Label("l") |> Typ.fresh, Int |> Typ.fresh)
-                  |> Typ.fresh,
-                ])
-                |> Typ.fresh,
+      ),
+      test_case("Multiple labels in let tuple", `Quick, () =>
+        exp_check(
+          let_(
+            Pat.(
+              cast(
+                var("x"),
+                Typ.(
+                  parens(
+                    prod([
+                      tup_label(label("l"), int()),
+                      tup_label(label("l2"), string()),
+                    ]),
+                  )
+                ),
+                Typ.unknown(Internal),
               )
-              |> Typ.fresh,
-              Unknown(Internal) |> Typ.fresh,
-            )
-            |> Pat.fresh,
-            Var("x") |> Exp.fresh,
-            Var("y") |> Exp.fresh,
-          )
-          |> Exp.fresh,
-        )
-        |> Exp.fresh,
-        "let x = (l=32) in
-       let y : (l=Int) = x in y",
-      )
-    }),
-    test_case("Multiple labels tuple", `Quick, () =>
-      exp_check(
-        Parens(
-          Tuple([
-            TupLabel(Label("l") |> Exp.fresh, Int(32) |> Exp.fresh)
-            |> Exp.fresh,
-            TupLabel(Label("l2") |> Exp.fresh, String("") |> Exp.fresh)
-            |> Exp.fresh,
-          ])
-          |> Exp.fresh,
-        )
-        |> Exp.fresh,
-        {|(l=32, l2="")|},
-      )
-    ),
-    test_case("Multiple labels in let tuple", `Quick, () =>
-      exp_check(
-        Let(
-          Cast(
-            Var("x") |> Pat.fresh,
-            Parens(
-              Prod([
-                TupLabel(Label("l") |> Typ.fresh, Int |> Typ.fresh)
-                |> Typ.fresh,
-                TupLabel(Label("l2") |> Typ.fresh, String |> Typ.fresh)
-                |> Typ.fresh,
-              ])
-              |> Typ.fresh,
-            )
-            |> Typ.fresh,
-            Unknown(Internal) |> Typ.fresh,
-          )
-          |> Pat.fresh,
-          Parens(
-            Tuple([
-              TupLabel(Label("l") |> Exp.fresh, Int(32) |> Exp.fresh)
-              |> Exp.fresh,
-              TupLabel(Label("l2") |> Exp.fresh, String("") |> Exp.fresh)
-              |> Exp.fresh,
-            ])
-            |> Exp.fresh,
-          )
-          |> Exp.fresh,
-          Var("x") |> Exp.fresh,
+            ),
+            parens(
+              tuple([
+                tup_label(label("l"), int(32)),
+                tup_label(label("l2"), string("")),
+              ]),
+            ),
+            var("x"),
+          ),
+          {|let x : (l=Int, l2=String) = (l=32, l2="") in x|},
         )
-        |> Exp.fresh,
-        {|let x : (l=Int, l2=String) = (l=32, l2="") in x|},
-      )
-    ),
-    test_case("Malformed label in singleton tuple", `Quick, () =>
-      exp_check(
-        Parens(
-          Tuple([
-            TupLabel(
-              MultiHole([Exp(Int(1) |> Exp.fresh)]) |> Exp.fresh,
-              Int(3) |> Exp.fresh,
-            )
-            |> Exp.fresh,
-          ])
-          |> Exp.fresh,
+      ),
+      test_case("Malformed label in singleton tuple", `Quick, () =>
+        exp_check(
+          parens(tuple([tup_label(multi_hole([Exp(int(1))]), int(3))])),
+          "(1=3)",
         )
-        |> Exp.fresh,
-        "(1=3)",
-      )
-    ),
-    test_case("Scientific notation floating point", `Quick, () => {
-      exp_check(Float(1.2e30) |> Exp.fresh, "1.2e30")
-    }),
-  ],
-);
+      ),
+      test_case("Scientific notation floating point", `Quick, () =>
+        exp_check(float(1.2e30), "1.2e30")
+      ),
+    ],
+  );
diff --git a/test/Test_Menhir.re b/test/Test_Menhir.re
index 95d16379bf..823cc93479 100644
--- a/test/Test_Menhir.re
+++ b/test/Test_Menhir.re
@@ -1,7 +1,7 @@
 open Haz3lmenhir;
 open Alcotest;
 open Haz3lcore;
-
+module Fresh = IdTagged.FreshGrammar;
 let alco_check =
   testable(
     Fmt.using(Haz3lcore.Exp.show, Fmt.string),
@@ -20,7 +20,7 @@ let strip_parens_and_add_builtins =
             VarMap.lookup(Haz3lcore.Builtins.Pervasives.builtins, x);
           cont(
             switch (builtin) {
-            | Some(Fn(_, _, _)) => cont(BuiltinFun(x) |> Exp.fresh)
+            | Some(Fn(_, _, _)) => cont(Fresh.Exp.builtin_fun(x))
             | Some(Const(_, _))
             | None => cont(e)
             },
@@ -48,17 +48,17 @@ let make_term_parse = (s: string) =>
     MakeTerm.from_zip_for_sem(Option.get(Printer.zipper_of_string(s))).term,
   );
 
-let menhir_parse = (s: string) => {
-  let (e, _) =
-    Haz3lmenhir.Conversion.Exp.of_menhir_ast(
-      Haz3lmenhir.Interface.parse_program(s),
-    );
-  e;
-};
-
-let menhir_matches = (exp: Term.Exp.t, actual: string) => {
-  alco_check("menhir matches expected parse", exp, menhir_parse(actual));
-};
+let menhir_matches = (exp: Term.Exp.t, actual: string) =>
+  alco_check(
+    "menhir matches expected parse",
+    exp,
+    Grammar.map_exp_annotation(
+      _: IdTagged.IdTag.t => {ids: [Id.invalid], copied: false},
+      Haz3lmenhir.Conversion.Exp.of_menhir_ast(
+        Haz3lmenhir.Interface.parse_program(actual),
+      ),
+    ),
+  );
 
 let menhir_only_test = (name: string, exp: Term.Exp.t, actual: string) =>
   test_case(name, `Quick, () => {menhir_matches(exp, actual)});
@@ -87,7 +87,12 @@ let menhir_maketerm_equivalent_test =
     alco_check(
       "Menhir parse matches MakeTerm parse",
       make_term_parse(actual),
-      menhir_parse(actual),
+      Grammar.map_exp_annotation(
+        _: IdTagged.IdTag.t => {ids: [Id.invalid], copied: false},
+        Haz3lmenhir.Conversion.Exp.of_menhir_ast(
+          Haz3lmenhir.Interface.parse_program(actual),
+        ),
+      ),
     )
   });
 
@@ -102,10 +107,9 @@ let qcheck_menhir_maketerm_equivalent_test =
     ~count=100,
     QCheck.make(~print=AST.show_exp, AST.gen_exp_sized(7)),
     exp => {
-      let core_exp = {
-        let (e, _) = Conversion.Exp.of_menhir_ast(exp);
-        e;
-      };
+      let unit_exp = Conversion.Exp.of_menhir_ast(exp);
+      let core_exp =
+        Grammar.map_exp_annotation(_ => IdTagged.IdTag.fresh(), unit_exp);
 
       let segment =
         ExpToSegment.exp_to_segment(
@@ -117,13 +121,17 @@ let qcheck_menhir_maketerm_equivalent_test =
       let serialized = Printer.of_segment(~holes=Some("?"), segment);
       let make_term_parsed = make_term_parse(serialized);
       let menhir_parsed = Haz3lmenhir.Interface.parse_program(serialized);
-      let menhir_parsed_converted = {
-        let (e, _) = Haz3lmenhir.Conversion.Exp.of_menhir_ast(menhir_parsed);
-        e;
-      };
+      let menhir_parsed_converted =
+        Haz3lmenhir.Conversion.Exp.of_menhir_ast(menhir_parsed);
 
       switch (
-        Haz3lcore.DHExp.fast_equal(make_term_parsed, menhir_parsed_converted)
+        Haz3lcore.DHExp.fast_equal(
+          make_term_parsed,
+          Grammar.map_exp_annotation(
+            _ => IdTagged.IdTag.fresh(),
+            menhir_parsed_converted,
+          ),
+        )
       ) {
       | true => true
       | false => false
@@ -153,11 +161,9 @@ let qcheck_menhir_serialized_equivalent_test =
     ~count=1000,
     QCheck.make(~print=AST.show_exp, AST.gen_exp_sized(7)),
     exp => {
-      let core_exp = {
-        let (e, _) = Conversion.Exp.of_menhir_ast(exp);
-        e;
-      };
-
+      let unit_exp = Conversion.Exp.of_menhir_ast(exp);
+      let core_exp =
+        Grammar.map_exp_annotation(_ => IdTagged.IdTag.fresh(), unit_exp);
       let segment =
         ExpToSegment.exp_to_segment(
           ~settings={
@@ -176,367 +182,258 @@ let qcheck_menhir_serialized_equivalent_test =
     },
   );
 
-let tests = (
-  "MenhirParser",
-  [
-    full_parser_test("Integer Literal", Int(8) |> Exp.fresh, "8"),
-    full_parser_test(
-      "Fun",
-      Fun(Var("x") |> Pat.fresh, Var("x") |> Exp.fresh, None, None)
-      |> Exp.fresh,
-      "fun x -> x",
-    ),
-    full_parser_test(
-      "String Literal",
-      String("Hello World") |> Exp.fresh,
-      {|"Hello World"|},
-    ),
-    full_parser_test("Bool Literal", Bool(true) |> Exp.fresh, "true"),
-    full_parser_test("Empty Hole", EmptyHole |> Exp.fresh, "?"),
-    full_parser_test("Var", Var("x") |> Exp.fresh, "x"),
-    full_parser_test(
-      "Parens",
-      Parens(Var("y") |> Exp.fresh) |> Exp.fresh,
-      "(y)",
-    ),
-    full_parser_test(
-      "BinOp",
-      BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh)
-      |> Exp.fresh,
-      "4 + 5",
-    ),
-    full_parser_test(
-      "Let",
-      Let(
-        Var("x") |> Pat.fresh,
-        Int(5) |> Exp.fresh,
-        Var("x") |> Exp.fresh,
-      )
-      |> Exp.fresh,
-      "let x = 5 in x",
-    ),
-    full_parser_test(
-      "Tuple",
-      Tuple([Int(4) |> Exp.fresh, Int(5) |> Exp.fresh]) |> Exp.fresh,
-      "(4, 5)",
-    ),
-    full_parser_test(
-      "Match",
-      Match(
-        Int(4) |> Exp.fresh,
-        [
-          (Int(1) |> Pat.fresh, String("hello") |> Exp.fresh),
-          (Wild |> Pat.fresh, String("world") |> Exp.fresh),
-        ],
-      )
-      |> Exp.fresh,
-      {|case 4
-         | 1 => "hello"
-         | _ => "world"
-        end|},
-    ),
-    full_parser_test(
-      "If",
-      If(Bool(true) |> Exp.fresh, Int(8) |> Exp.fresh, Int(6) |> Exp.fresh)
-      |> Exp.fresh,
-      "if true then 8 else 6",
-    ),
-    full_parser_test(
-      "Deferred Ap",
-      DeferredAp(Var("x") |> Exp.fresh, [Deferral(InAp) |> Exp.fresh])
-      |> Exp.fresh,
-      "x(_)",
-    ),
-    full_parser_test(
-      "Cons",
-      Cons(Int(1) |> Exp.fresh, ListLit([]) |> Exp.fresh) |> Exp.fresh,
-      "1 :: []",
-    ),
-    full_parser_test(
-      "ListLit",
-      ListLit([
-        Int(1) |> Exp.fresh,
-        Int(2) |> Exp.fresh,
-        Int(3) |> Exp.fresh,
-      ])
-      |> Exp.fresh,
-      "[1, 2, 3]",
-    ),
-    menhir_only_test("Unit", Tuple([]) |> Exp.fresh, "()"),
-    menhir_only_test(
-      "Constructor",
-      Constructor("A", None) |> Exp.fresh,
-      "A",
-    ),
-    menhir_only_test(
-      "Constructor cast",
-      Cast(
-        Constructor("A", None) |> Exp.fresh,
-        Unknown(Internal) |> Typ.fresh,
-        Int |> Typ.fresh,
-      )
-      |> Exp.fresh,
-      "A : Int",
-    ),
-    menhir_only_test(
-      "Constructor of specific sum type",
-      Constructor("A", Some(Int |> Typ.fresh)) |> Exp.fresh,
-      "A ~ Int",
-    ),
-    // TODO Fix for the tests below
-    menhir_only_test(
-      "Constructor with Type Variable",
-      Constructor("A", Some(Var("T") |> Typ.fresh)) |> Exp.fresh,
-      "A ~ T",
-    ),
-    full_parser_test(
-      "Type Variable",
-      Let(
-        Cast(
-          Var("x") |> Pat.fresh,
-          Var("T") |> Typ.fresh,
-          Unknown(Internal) |> Typ.fresh,
-        )
-        |> Pat.fresh,
-        EmptyHole |> Exp.fresh,
-        Var("x") |> Exp.fresh,
-      )
-      |> Exp.fresh,
-      "let x : T = ? in x",
-    ),
-    full_parser_test(
-      "Type Alias",
-      TyAlias(Var("x") |> TPat.fresh, Int |> Typ.fresh, Int(1) |> Exp.fresh)
-      |> Exp.fresh,
-      "type x = Int in 1",
-    ),
-    full_parser_test(
-      "Test",
-      Test(
-        BinOp(Int(Equals), Int(3) |> Exp.fresh, Int(3) |> Exp.fresh)
-        |> Exp.fresh,
-      )
-      |> Exp.fresh,
-      "test 3 == 3 end",
-    ),
-    full_parser_test(
-      "Filter",
-      Filter(
-        Filter({act: (Eval, All), pat: Int(3) |> Exp.fresh}),
-        Int(3) |> Exp.fresh,
-      )
-      |> Exp.fresh,
-      "eval 3 in 3" // TODO Use other filter commands
-    ),
-    full_parser_test(
-      "List Concat",
-      ListConcat(
-        ListLit([Int(1) |> Exp.fresh, Int(2) |> Exp.fresh]) |> Exp.fresh,
-        ListLit([Int(3) |> Exp.fresh, Int(4) |> Exp.fresh]) |> Exp.fresh,
-      )
-      |> Exp.fresh,
-      "[1, 2] @ [3, 4]",
-    ),
-    full_parser_test(
-      "times and divide precendence",
-      BinOp(
-        Int(Divide),
-        BinOp(Int(Times), Int(1) |> Exp.fresh, Int(2) |> Exp.fresh)
-        |> Exp.fresh,
-        Int(3) |> Exp.fresh,
-      )
-      |> Exp.fresh,
-      "1 * 2 / 3",
-    ),
-    full_parser_test(
-      "plus and minus precendence",
-      BinOp(
-        Int(Plus),
-        BinOp(Int(Minus), Int(1) |> Exp.fresh, Int(2) |> Exp.fresh)
-        |> Exp.fresh,
-        Int(3) |> Exp.fresh,
-      )
-      |> Exp.fresh,
-      "1 - 2 + 3",
-    ),
-    full_parser_test(
-      "Integer Ops",
-      BinOp(
-        Int(GreaterThanOrEqual),
-        BinOp(
-          Int(Minus),
-          BinOp(
-            Int(Plus),
-            UnOp(Int(Minus), Int(1) |> Exp.fresh) |> Exp.fresh,
-            Int(2) |> Exp.fresh,
-          )
-          |> Exp.fresh,
-          BinOp(
-            Int(Times),
-            BinOp(Int(Divide), Int(3) |> Exp.fresh, Int(4) |> Exp.fresh)
-            |> Exp.fresh,
-            BinOp(Int(Power), Int(5) |> Exp.fresh, Int(6) |> Exp.fresh)
-            |> Exp.fresh,
-          )
-          |> Exp.fresh,
-        )
-        |> Exp.fresh,
-        Int(8) |> Exp.fresh,
-      )
-      |> Exp.fresh,
-      "-1 + 2 - 3 / 4 * 5 ** 6 >= 8",
-    ),
-    full_parser_test("Float", Float(1.) |> Exp.fresh, "1."),
-    full_parser_test(
-      "Float Ops",
-      BinOp(
-        Float(LessThan),
-        BinOp(
-          Float(Minus),
-          Float(2.) |> Exp.fresh,
-          BinOp(
-            Float(Times),
-            BinOp(
-              Float(Divide),
-              Float(3.) |> Exp.fresh,
-              Float(4.) |> Exp.fresh,
-            )
-            |> Exp.fresh,
-            BinOp(
-              Float(Power),
-              Float(5.) |> Exp.fresh,
-              Float(6.) |> Exp.fresh,
-            )
-            |> Exp.fresh,
-          )
-          |> Exp.fresh,
-        )
-        |> Exp.fresh,
-        Float(8.) |> Exp.fresh,
-      )
-      |> Exp.fresh,
-      "2. -. 3. /. 4. *. 5. **. 6. <. 8.",
-    ),
-    full_parser_test(
-      "Let binding with type ascription",
-      Let(
-        Cast(
-          Var("x") |> Pat.fresh,
-          Int |> Typ.fresh,
-          Unknown(Internal) |> Typ.fresh,
-        )
-        |> Pat.fresh,
-        Int(5) |> Exp.fresh,
-        Var("x") |> Exp.fresh,
-      )
-      |> Exp.fresh,
-      "let (x: Int) = 5 in x",
-    ),
-    menhir_only_test(
-      "named_function",
-      Fun(
-        (Var("x"): Pat.term) |> Pat.fresh,
-        BinOp(Int(Plus), Var("x") |> Exp.fresh, Int(5) |> Exp.fresh)
-        |> Exp.fresh,
-        None,
-        Some("f"),
-      )
-      |> Exp.fresh,
-      "named_fun f x -> x + 5",
-    ),
-    full_parser_test(
-      "basic sum type",
-      Let(
-        Cast(
-          Var("x") |> Pat.fresh,
-          Sum([
-            Variant("A", [], None),
-            Variant("B", [], None),
-            Variant("C", [], Some(Int |> Typ.fresh)),
-          ])
-          |> Typ.fresh,
-          Unknown(Internal) |> Typ.fresh,
-        )
-        |> Pat.fresh,
-        Ap(
-          Forward,
-          Constructor("C", None) |> Exp.fresh,
-          Int(7) |> Exp.fresh,
-        )
-        |> Exp.fresh,
-        Var("x") |> Exp.fresh,
-      )
-      |> Exp.fresh,
-      "let x : +A +B +C(Int) = C(7) in x",
-    ),
-    menhir_maketerm_equivalent_test("Empty Type Hole", "let g: ? = 7 in g"),
-    menhir_maketerm_equivalent_test(
-      "Pattern with type ascription",
-      "fun (b : Bool) -> b",
-    ),
-    full_parser_test(
-      "Type Hole in arrow cast",
-      Fun(
-        Cast(
-          Var("b") |> Pat.fresh,
-          Parens(
-            Arrow(
-              Unknown(Hole(EmptyHole)) |> Typ.fresh,
-              Unknown(Hole(EmptyHole)) |> Typ.fresh,
-            )
-            |> Typ.fresh,
-          )
-          |> Typ.fresh,
-          Unknown(Internal) |> Typ.fresh,
-        )
-        |> Pat.fresh,
-        EmptyHole |> Exp.fresh,
-        None,
-        None,
-      )
-      |> Exp.fresh,
-      "fun (b : ? -> ?) -> ?",
-    ),
-    full_parser_test(
-      "multiargument function",
-      Ap(
-        Forward,
-        Var("f") |> Exp.fresh,
-        Tuple([Int(1) |> Exp.fresh, Int(2) |> Exp.fresh]) |> Exp.fresh,
-      )
-      |> Exp.fresh,
-      "f(1, 2)",
-    ),
-    menhir_maketerm_equivalent_test(
-      "partial sum type",
-      "type Partial = +Ok(?) + ? in ?",
-    ),
-    menhir_maketerm_equivalent_test(
-      "Function with type variable",
-      "fun (x : a) -> x",
-    ),
-    menhir_maketerm_equivalent_test("Sequence addition precedence", "1+2;3"),
-    menhir_maketerm_equivalent_test(
-      "And app precedence",
-      "exp_equal(e1, e3) && exp_equal(e2, e4)",
-    ),
-    menhir_maketerm_equivalent_test(
-      "Negation precedence with multiplication",
-      "-num*1",
-    ),
-    menhir_maketerm_equivalent_test(
-      "Concatenation association",
-      "1::2::3::[]",
-    ),
-    menhir_maketerm_equivalent_test(
-      "and less than precedence",
-      "true && 23 < int_of_float(51.00)" // TODO This looks like a bug in MakeTerm
-    ),
-    menhir_maketerm_equivalent_test("Singleton labeled tuple", {|(h = 1)|}),
-    menhir_maketerm_equivalent_test(
-      ~speed_level=`Slow,
-      "Altered Documentation Buffer: Basic Reference",
-      {|
+let tests =
+  Fresh.(
+    "MenhirParser",
+    Exp.[
+      full_parser_test("Integer Literal", int(8), "8"),
+      full_parser_test(
+        "Fun",
+        fn(Pat.var("x"), var("x"), None, None),
+        "fun x -> x",
+      ),
+      full_parser_test(
+        "String Literal",
+        string("Hello World"),
+        {|"Hello World"|},
+      ),
+      full_parser_test("Bool Literal", bool(true), "true"),
+      full_parser_test("Empty Hole", empty_hole(), "?"),
+      full_parser_test("Var", var("x"), "x"),
+      full_parser_test("Parens", parens(var("y")), "(y)"),
+      full_parser_test(
+        "bin_op",
+        bin_op(Int(Plus), int(4), int(5)),
+        "4 + 5",
+      ),
+      full_parser_test(
+        "Let",
+        let_(Fresh.Pat.var("x"), int(5), var("x")),
+        "let x = 5 in x",
+      ),
+      full_parser_test("Tuple", tuple([int(4), int(5)]), "(4, 5)"),
+      full_parser_test(
+        "Match",
+        match(
+          int(4),
+          [(Pat.int(1), string("hello")), (Pat.wild(), string("world"))],
+        ),
+        {|case 4
+       | 1 => "hello"
+       | _ => "world"
+      end|},
+      ),
+      full_parser_test(
+        "If",
+        if_(bool(true), int(8), int(6)),
+        "if true then 8 else 6",
+      ),
+      full_parser_test(
+        "Deferred Ap",
+        deferred_ap(var("x"), [deferral(InAp)]),
+        "x(_)",
+      ),
+      full_parser_test("Cons", cons(int(1), list_lit([])), "1 :: []"),
+      full_parser_test(
+        "ListLit",
+        list_lit([int(1), int(2), int(3)]),
+        "[1, 2, 3]",
+      ),
+      menhir_only_test("Unit", tuple([]), "()"),
+      menhir_only_test("Constructor", constructor("A", None), "A"),
+      menhir_only_test(
+        "Constructor cast",
+        cast(constructor("A", None), Typ.unknown(Internal), Typ.int()),
+        "A : Int",
+      ),
+      menhir_only_test(
+        "Constructor of specific sum type",
+        constructor("A", Some(Typ.int())),
+        "A ~ Int",
+      ),
+      // TODO Fix for the tests below
+      menhir_only_test(
+        "Constructor with Type Variable",
+        constructor("A", Some(Typ.var("T"))),
+        "A ~ T",
+      ),
+      full_parser_test(
+        "Type Variable",
+        let_(
+          Pat.cast(Pat.var("x"), Typ.var("T"), Typ.unknown(Internal)),
+          empty_hole(),
+          var("x"),
+        ),
+        "let x : T = ? in x",
+      ),
+      full_parser_test(
+        "Type Alias",
+        ty_alias(TPat.var("x"), Typ.int(), int(1)),
+        "type x = Int in 1",
+      ),
+      full_parser_test(
+        "Test",
+        test(bin_op(Int(Equals), int(3), int(3))),
+        "test 3 == 3 end",
+      ),
+      full_parser_test(
+        "Filter",
+        filter(Filter({act: (Eval, All), pat: int(3)}), int(3)),
+        "eval 3 in 3" // TODO Use other filter commands
+      ),
+      full_parser_test(
+        "List Concat",
+        list_concat(
+          list_lit([int(1), int(2)]),
+          list_lit([int(3), int(4)]),
+        ),
+        "[1, 2] @ [3, 4]",
+      ),
+      full_parser_test(
+        "times and divide precendence",
+        bin_op(Int(Divide), bin_op(Int(Times), int(1), int(2)), int(3)),
+        "1 * 2 / 3",
+      ),
+      full_parser_test(
+        "plus and minus precendence",
+        bin_op(Int(Plus), bin_op(Int(Minus), int(1), int(2)), int(3)),
+        "1 - 2 + 3",
+      ),
+      full_parser_test(
+        "Integer Ops",
+        bin_op(
+          Int(GreaterThanOrEqual),
+          bin_op(
+            Int(Minus),
+            bin_op(Int(Plus), un_op(Int(Minus), int(1)), int(2)),
+            bin_op(
+              Int(Times),
+              bin_op(Int(Divide), int(3), int(4)),
+              bin_op(Int(Power), int(5), int(6)),
+            ),
+          ),
+          int(8),
+        ),
+        "-1 + 2 - 3 / 4 * 5 ** 6 >= 8",
+      ),
+      full_parser_test("Float", float(1.), "1."),
+      full_parser_test(
+        "Float Ops",
+        bin_op(
+          Float(LessThan),
+          bin_op(
+            Float(Minus),
+            float(2.),
+            bin_op(
+              Float(Times),
+              bin_op(Float(Divide), float(3.), float(4.)),
+              bin_op(Float(Power), float(5.), float(6.)),
+            ),
+          ),
+          float(8.),
+        ),
+        "2. -. 3. /. 4. *. 5. **. 6. <. 8.",
+      ),
+      full_parser_test(
+        "Let binding with type ascription",
+        let_(
+          Pat.cast(Pat.var("x"), Typ.int(), Typ.unknown(Internal)),
+          int(5),
+          var("x"),
+        ),
+        "let (x: Int) = 5 in x",
+      ),
+      menhir_only_test(
+        "named_function",
+        fn(
+          Pat.var("x"),
+          bin_op(Int(Plus), var("x"), int(5)),
+          None,
+          Some("f"),
+        ),
+        "named_fun f x -> x + 5",
+      ),
+      full_parser_test(
+        "basic sum type",
+        let_(
+          Pat.cast(
+            Pat.var("x"),
+            Typ.sum([
+              Variant("A", [], None),
+              Variant("B", [], None),
+              Variant("C", [], Some(Typ.int())),
+            ]),
+            Typ.unknown(Internal),
+          ),
+          ap(Forward, constructor("C", None), int(7)),
+          var("x"),
+        ),
+        "let x : +A +B +C(Int) = C(7) in x",
+      ),
+      menhir_maketerm_equivalent_test("Empty Type Hole", "let g: ? = 7 in g"),
+      menhir_maketerm_equivalent_test(
+        "Pattern with type ascription",
+        "fun (b : Bool) -> b",
+      ),
+      full_parser_test(
+        "Type Hole in arrow cast",
+        fn(
+          Pat.cast(
+            Pat.var("b"),
+            Typ.(
+              parens(
+                arrow(
+                  unknown(TypeProvenance.hole(EmptyHole)),
+                  unknown(TypeProvenance.hole(EmptyHole)),
+                ),
+              )
+            ),
+            Typ.unknown(Internal),
+          ),
+          empty_hole(),
+          None,
+          None,
+        ),
+        "fun (b : ? -> ?) -> ?",
+      ),
+      full_parser_test(
+        "multiargument function",
+        ap(Forward, var("f"), tuple([int(1), int(2)])),
+        "f(1, 2)",
+      ),
+      menhir_maketerm_equivalent_test(
+        "partial sum type",
+        "type Partial = +Ok(?) + ? in ?",
+      ),
+      menhir_maketerm_equivalent_test(
+        "Function with type variable",
+        "fun (x : a) -> x",
+      ),
+      menhir_maketerm_equivalent_test(
+        "Sequence addition precedence",
+        "1+2;3",
+      ),
+      menhir_maketerm_equivalent_test(
+        "And app precedence",
+        "exp_equal(e1, e3) && exp_equal(e2, e4)",
+      ),
+      menhir_maketerm_equivalent_test(
+        "Negation precedence with multiplication",
+        "-num*1",
+      ),
+      menhir_maketerm_equivalent_test(
+        "Concatenation association",
+        "1::2::3::[]",
+      ),
+      menhir_maketerm_equivalent_test(
+        "and less than precedence",
+        "true && 23 < int_of_float(51.00)" // TODO This looks like a bug in MakeTerm
+      ),
+      menhir_maketerm_equivalent_test("Singleton labeled tuple", {|(h = 1)|}),
+      menhir_maketerm_equivalent_test(
+        ~speed_level=`Slow,
+        "Altered Documentation Buffer: Basic Reference",
+        {|
 let empty_hole = ? in
 
 let non_empty_hole : Int = true in
@@ -636,11 +533,11 @@ test 2 + 2 == 5 end;
 
 2 + 2
     |},
-    ),
-    menhir_maketerm_equivalent_test(
-      ~speed_level=`Slow,
-      "Altered Documentation Buffer: Projectors",
-      {|
+      ),
+      menhir_maketerm_equivalent_test(
+        ~speed_level=`Slow,
+        "Altered Documentation Buffer: Projectors",
+        {|
 let fold = (((((((((((()))))))))))) in
 let folds: (Int -> Bool) = ? in
 let guard: Bool = true in
@@ -656,11 +553,11 @@ let ______ = "a shift   malicious" in
 let box: Int = "malicious" in
 if true && (23 < int_of_float(51.00))
 then ______ else "its: " ++ box    |},
-    ),
-    menhir_maketerm_equivalent_test(
-      ~speed_level=`Slow,
-      "Altered Documentation Buffer: Types & Static Errors",
-      {|
+      ),
+      menhir_maketerm_equivalent_test(
+        ~speed_level=`Slow,
+        "Altered Documentation Buffer: Types & Static Errors",
+        {|
 let _ = unbound in
 let Undefined = Undefined in
 let true = 2 in
@@ -705,11 +602,11 @@ let _: [Int] = 1.0::[2] in
 let _: [Int] = 1::[2.0] in
 "BYE"
 |},
-    ),
-    menhir_maketerm_equivalent_test(
-      ~speed_level=`Slow,
-      "Altered Documentation Buffer: adt dynamics",
-      {|
+      ),
+      menhir_maketerm_equivalent_test(
+        ~speed_level=`Slow,
+        "Altered Documentation Buffer: adt dynamics",
+        {|
 type Exp =
   + Var(String)
   + Lam(String, Exp)
@@ -774,12 +671,12 @@ test result_equal(
   go(Ap(Lam("yo", Var("yo")), Lam("bro", Var("bro")))),
 Ok(Lam("bro", Var("bro")))) end
 |},
-    ),
-    menhir_maketerm_equivalent_test(
-      // Variable names are renamed due to lexing overtaking e, t, p, and tp
-      ~speed_level=`Slow,
-      "Altered Documentation Buffer: Polymorphism",
-      {|let id = typfun A -> (fun (x : A) -> x) in
+      ),
+      menhir_maketerm_equivalent_test(
+        // Variable names are renamed due to lexing overtaking e, t, p, and tp
+        ~speed_level=`Slow,
+        "Altered Documentation Buffer: Polymorphism",
+        {|let id = typfun A -> (fun (x : A) -> x) in
 let ex1 = id@<Int>(1) in
 let const : forall A -> (forall B -> (A -> B -> A)) =
 typfun A -> (typfun B -> (fun x -> fun y -> x)) in
@@ -807,29 +704,29 @@ end in
 let ex5 = list_of_mylist(x) in
 (ex1, ex2, ex3, ex4, ex5)
     |},
-    ),
-    // This fails because MakeTerm can't handle left to right keyword prefixes.
-    skip_menhir_maketerm_equivalent_test(
-      "Prefixed keyword parses",
-      {|let ? = ina in ?|},
-    ),
-    skip_menhir_maketerm_equivalent_test(
-      "Sum type messed up in make term",
-      {|type ? = rec ? -> + Aramj -> Bool in ?|},
-    ),
-    skip_menhir_maketerm_equivalent_test(
-      "List concat and typap",
-      {|type ? = (+ Ulog, () -> Float) in let (()) = (()) in 0.001536|},
-    ),
-    skip_menhir_maketerm_equivalent_test(
-      "Sum in product in typeap",
-      {|((fun _ -> b)) @< [(+ Kfgii, Float)] >|},
-    ),
-    skip_menhir_maketerm_equivalent_test(
-      "Non-unique constructors currently throws in equality",
-      {|type ? = ((+ ? + ?)) in []|},
-    ),
-    QCheck_alcotest.to_alcotest(qcheck_menhir_maketerm_equivalent_test),
-    QCheck_alcotest.to_alcotest(qcheck_menhir_serialized_equivalent_test),
-  ],
-);
+      ),
+      // This fails because MakeTerm can't handle left to right keyword prefixes.
+      skip_menhir_maketerm_equivalent_test(
+        "Prefixed keyword parses",
+        {|let ? = ina in ?|},
+      ),
+      skip_menhir_maketerm_equivalent_test(
+        "Sum type messed up in make term",
+        {|type ? = rec ? -> + Aramj -> Bool in ?|},
+      ),
+      skip_menhir_maketerm_equivalent_test(
+        "List concat and typap",
+        {|type ? = (+ Ulog, () -> Float) in let (()) = (()) in 0.001536|},
+      ),
+      skip_menhir_maketerm_equivalent_test(
+        "Sum in product in typeap",
+        {|((fun _ -> b)) @< [(+ Kfgii, Float)] >|},
+      ),
+      skip_menhir_maketerm_equivalent_test(
+        "Non-unique constructors currently throws in equality",
+        {|type ? = ((+ ? + ?)) in []|},
+      ),
+      QCheck_alcotest.to_alcotest(qcheck_menhir_maketerm_equivalent_test),
+      QCheck_alcotest.to_alcotest(qcheck_menhir_serialized_equivalent_test),
+    ],
+  );
diff --git a/test/Test_Statics.re b/test/Test_Statics.re
index ccb7e34bee..61f2d15fd2 100644
--- a/test/Test_Statics.re
+++ b/test/Test_Statics.re
@@ -48,16 +48,7 @@ let testable_info_error_exp =
 
 let testable_error: testable(Info.error) =
   testable(Fmt.using(Info.show_error, Fmt.string), (==));
-module FreshId = {
-  let arrow = (a, b) => Arrow(a, b) |> Typ.fresh;
-  let unknown = a => Unknown(a) |> Typ.fresh;
-  let int = Typ.fresh(Int);
-  let float = Typ.fresh(Float);
-  let prod = a => Prod(a) |> Typ.fresh;
-  let label = a => Label(a) |> Typ.fresh;
-  let tup_label = (a, b) => TupLabel(a, b) |> Typ.fresh;
-  let string = Typ.fresh(String);
-};
+
 let statics = Statics.mk(CoreSettings.on, Builtins.ctx_init);
 
 let parse_exp = (s: string) => {
@@ -85,26 +76,7 @@ let annotated_exp: testable(Grammar.exp_t(option(Info.error))) =
     ),
     Grammar.equal_exp_t(Option.equal(eq_info_error)),
   );
-let no_error_exp =
-    (e: Grammar.exp_term(option(Info.error)))
-    : Grammar.exp_t(option(Info.error)) => {
-  {term: e, annotation: None};
-};
-let no_error_pat =
-    (p: Grammar.pat_term(option(Info.error)))
-    : Grammar.pat_t(option(Info.error)) => {
-  {term: p, annotation: None};
-};
-let no_error_typ =
-    (t: Grammar.typ_term(option(Info.error)))
-    : Grammar.typ_t(option(Info.error)) => {
-  {term: t, annotation: None};
-};
-let error_exp =
-    (err, e: Grammar.exp_term(option(Info.error)))
-    : Grammar.exp_t(option(Info.error)) => {
-  {term: e, annotation: Some(err)};
-};
+
 let fresh = (exp: Grammar.exp_t(unit)): TermBase.exp_t => {
   Grammar.map_exp_annotation(
     (_annotation): IdTagged.IdTag.t => {
@@ -171,932 +143,833 @@ let fully_consistent_typecheck = (name, serialized, expected) => {
     },
   );
 };
-
+module FIError =
+  Grammar.Factory({
+    type t = option(Info.error);
+    let default_value = () => None;
+  });
+module FTemp =
+  Grammar.Factory({
+    type t = IdTagged.IdTag.t;
+    let default_value = (): IdTagged.IdTag.t => {
+      ids: [Id.invalid],
+      copied: false,
+    };
+  });
 let tests = (
   "Statics",
-  FreshId.[
-    fully_consistent_typecheck(
-      "Function with unknown param",
-      "fun x -> 4 + 5",
-      Some(arrow(unknown(Internal), int)),
-    ),
-    fully_consistent_typecheck(
-      "Function with known param",
-      "fun x : Int -> 4 + 5",
-      Some(arrow(int, int)),
-    ),
-    fully_consistent_typecheck(
-      "Function with labeled param",
-      "fun (a=x) -> 4",
-      Some(arrow(prod([tup_label(label("a"), unknown(Internal))]), int)),
-    ),
-    fully_consistent_typecheck(
-      "bifunction",
-      "fun x : Int, y: Int -> x + y",
-      Some(arrow(prod([int, int]), int)),
-    ),
-    fully_consistent_typecheck(
-      "bifunction",
-      "fun x : Int, y: Int -> x + y",
-      Some(arrow(prod([int, int]), int)),
-    ),
-    fully_consistent_typecheck(
-      "function application",
-      "float_of_int(1)",
-      Some(float),
-    ),
-    fully_consistent_typecheck(
-      "function deferral",
-      "string_sub(\"hello\", 1, _)",
-      Some(arrow(int, string)),
-    ),
-    test_case(
-      "Typechecking fails for unlabeled variable being assigned to labeled tuple",
-      `Quick,
-      () => {
-      annotated_tree_test(
-        "let x = (1, 2) in let y : (a=Int, b=Int) = x in y",
-        no_error_exp(
-          Let(
-            no_error_pat(Var("x")),
-            no_error_exp(
-              Parens(
-                Tuple([Int(1) |> no_error_exp, Int(2) |> no_error_exp])
-                |> no_error_exp,
-              ),
-            ),
-            no_error_exp(
-              Let(
-                no_error_pat(
-                  Cast(
-                    no_error_pat(Var("y")),
-                    no_error_typ(
-                      Parens(
-                        Prod([
-                          no_error_typ(
-                            TupLabel(
-                              Label("a") |> no_error_typ,
-                              Int |> no_error_typ,
+  FTemp.(
+    Typ.[
+      fully_consistent_typecheck(
+        "Function with unknown param",
+        "fun x -> 4 + 5",
+        Some(Typ.(arrow(unknown(Internal), int()))),
+      ),
+      fully_consistent_typecheck(
+        "Function with known param",
+        "fun x : Int -> 4 + 5",
+        Some(arrow(int(), int())),
+      ),
+      fully_consistent_typecheck(
+        "Function with labeled param",
+        "fun (a=x) -> 4",
+        Some(
+          arrow(prod([tup_label(label("a"), unknown(Internal))]), int()),
+        ),
+      ),
+      fully_consistent_typecheck(
+        "bifunction",
+        "fun x : Int, y: Int -> x + y",
+        Some(arrow(prod([int(), int()]), int())),
+      ),
+      fully_consistent_typecheck(
+        "bifunction",
+        "fun x : Int, y: Int -> x + y",
+        Some(arrow(prod([int(), int()]), int())),
+      ),
+      fully_consistent_typecheck(
+        "function application",
+        "float_of_int(1)",
+        Some(float()),
+      ),
+      fully_consistent_typecheck(
+        "function deferral",
+        "string_sub(\"hello\", 1, _)",
+        Some(arrow(int(), string())),
+      ),
+      test_case(
+        "Typechecking fails for unlabeled variable being assigned to labeled tuple",
+        `Quick,
+        () => {
+        annotated_tree_test(
+          "let x = (1, 2) in let y : (a=Int, b=Int) = x in y",
+          FIError.(
+            Exp.(
+              let_(
+                Pat.(var("x")),
+                parens(tuple([int(1), int(2)])),
+                let_(
+                  Pat.(
+                    cast(
+                      var("y"),
+                      Typ.(
+                        parens(
+                          prod([
+                            tup_label(label("a"), int()),
+                            tup_label(label("b"), int()),
+                          ]),
+                        )
+                      ),
+                      Typ.unknown(Internal),
+                    )
+                  ),
+                  var(
+                    ~ann=
+                      Some(
+                        FTemp.Typ.(
+                          Exp(
+                            Common(
+                              Inconsistent(
+                                Expectation({
+                                  ana:
+                                    parens(
+                                      prod([
+                                        tup_label(label("a"), int()),
+                                        tup_label(label("b"), int()),
+                                      ]),
+                                    ),
+                                  syn: prod([int(), int()]),
+                                }),
+                              ),
                             ),
-                          ),
-                          TupLabel(
-                            Label("b") |> no_error_typ,
-                            Int |> no_error_typ,
                           )
-                          |> no_error_typ,
-                        ])
-                        |> no_error_typ,
+                        ),
                       ),
-                    ),
-                    Unknown(Internal) |> no_error_typ,
+                    "x",
                   ),
+                  var("y"),
                 ),
-                error_exp(
-                  Exp(
-                    Common(
-                      Inconsistent(
-                        Expectation({
-                          ana:
-                            Parens(
-                              Prod([
-                                TupLabel(
-                                  Label("a") |> Typ.fresh,
-                                  Int |> Typ.fresh,
-                                )
-                                |> Typ.fresh,
-                                TupLabel(
-                                  Label("b") |> Typ.fresh,
-                                  Int |> Typ.fresh,
-                                )
-                                |> Typ.fresh,
-                              ])
-                              |> Typ.fresh,
-                            )
-                            |> Typ.fresh,
-                          syn:
-                            Prod([Int |> Typ.fresh, Int |> Typ.fresh])
-                            |> Typ.fresh,
-                        }),
+              )
+            )
+          ),
+        )
+      }),
+      test_case(
+        "Typechecking fails for unlabeled variable being assigned to labeled tuple",
+        `Quick,
+        () => {
+        annotated_tree_test(
+          "let y : String = true",
+          FIError.(
+            Exp.(
+              let_(
+                Pat.(
+                  cast(var("y"), Typ.(string()), Typ.(unknown(Internal)))
+                ),
+                bool(
+                  ~ann=
+                    Some(
+                      FTemp.Typ.(
+                        Exp(
+                          Common(
+                            Inconsistent(
+                              Expectation({ana: string(), syn: bool()}),
+                            ),
+                          ),
+                        )
                       ),
                     ),
-                  ),
-                  Var("x"),
+                  true,
                 ),
-                no_error_exp(Var("y")),
-              ),
-            ),
-          ),
-        ),
-      )
-    }),
-    test_case(
-      "Typechecking fails for unlabeled variable being assigned to labeled tuple",
-      `Quick,
-      () => {
-      annotated_tree_test(
-        "let y : String = true",
-        no_error_exp(
-          Let(
-            Cast(
-              Var("y") |> no_error_pat,
-              String |> no_error_typ,
-              Unknown(Internal) |> no_error_typ,
+                var("y"),
+              )
             )
-            |> no_error_pat,
-            error_exp(
-              Exp(
-                Common(
-                  Inconsistent(
-                    Expectation({
-                      ana: String |> Typ.fresh,
-                      syn: Bool |> Typ.fresh,
-                    }),
-                  ),
-                ),
-              ),
-              Bool(true),
-            ),
-            Var("y") |> no_error_exp,
           ),
-        ),
-      )
-    }),
-    fully_consistent_typecheck(
-      "Assigning labeled tuple to variable",
-      "let x = (l=32) in let y : (l=Int) = x in y",
-      Some(
-        Prod([
-          TupLabel(Label("l") |> Typ.fresh, Int |> Typ.fresh) |> Typ.fresh,
-        ])
-        |> Typ.fresh,
+        )
+      }),
+      fully_consistent_typecheck(
+        "Assigning labeled tuple to variable",
+        "let x = (l=32) in let y : (l=Int) = x in y",
+        Some(prod([tup_label(label("l"), int())])),
       ),
-    ),
-    fully_consistent_typecheck(
-      "Singleton Labled Tuple ascription in let",
-      "let x : (l=String) = (\"a\") in x",
-      Some(
-        Prod([
-          TupLabel(Label("l") |> Typ.fresh, String |> Typ.fresh) |> Typ.fresh,
-        ])
-        |> Typ.fresh,
+      fully_consistent_typecheck(
+        "Singleton Labled Tuple ascription in let",
+        "let x : (l=String) = (\"a\") in x",
+        Some(prod([tup_label(label("l"), string())])),
       ),
-    ),
-    test_case(
-      "Singleton Labled Tuple ascription in let with wrong type should fail",
-      `Quick,
-      () => {
-      annotated_tree_test(
-        "",
-        Let(
-          Cast(
-            Var("x") |> no_error_pat,
-            Parens(
-              Prod([
-                TupLabel(Label("l") |> no_error_typ, String |> no_error_typ)
-                |> no_error_typ,
-              ])
-              |> no_error_typ,
-            )
-            |> no_error_typ,
-            Unknown(Internal) |> no_error_typ,
-          )
-          |> no_error_pat,
-          error_exp(
-            Exp(
-              Common(
-                Inconsistent(
-                  Expectation({
-                    ana: String |> Typ.fresh,
-                    syn: Int |> Typ.fresh,
-                  }),
+      test_case(
+        "Singleton Labled Tuple ascription in let with wrong type should fail",
+        `Quick,
+        () => {
+        annotated_tree_test(
+          "",
+          FIError.(
+            Exp.(
+              let_(
+                Pat.(
+                  cast(
+                    var("x"),
+                    Typ.(parens(prod([tup_label(label("l"), string())]))),
+                    Typ.unknown(Internal),
+                  )
                 ),
-              ),
-            ),
-            Int(1),
+                int(
+                  ~ann=
+                    Some(
+                      FTemp.Typ.(
+                        Exp(
+                          Common(
+                            Inconsistent(
+                              Expectation({ana: string(), syn: int()}),
+                            ),
+                          ),
+                        )
+                      ),
+                    ),
+                  1,
+                ),
+                var("x"),
+              )
+            )
           ),
-          Var("x") |> no_error_exp,
         )
-        |> no_error_exp,
-      )
-    }),
-    fully_consistent_typecheck(
-      "Singleton Labled Tuple with specified label",
-      "let x : (l=String) = (l=\"a\") in x",
-      Some(
-        Prod([
-          TupLabel(Label("l") |> Typ.fresh, String |> Typ.fresh) |> Typ.fresh,
-        ])
-        |> Typ.fresh,
+      }),
+      fully_consistent_typecheck(
+        "Singleton Labled Tuple with specified label",
+        "let x : (l=String) = (l=\"a\") in x",
+        Some(prod([tup_label(label("l"), string())])),
       ),
-    ),
-    fully_consistent_typecheck(
-      "Labeled tuple with multiple labels",
-      {|(l=32, l2="")|},
-      Some(
-        Prod([
-          TupLabel(Label("l") |> Typ.fresh, Int |> Typ.fresh) |> Typ.fresh,
-          TupLabel(Label("l2") |> Typ.fresh, String |> Typ.fresh)
-          |> Typ.fresh,
-        ])
-        |> Typ.fresh,
+      fully_consistent_typecheck(
+        "Labeled tuple with multiple labels",
+        {|(l=32, l2="")|},
+        Some(
+          prod([
+            tup_label(label("l"), int()),
+            tup_label(label("l2"), string()),
+          ]),
+        ),
       ),
-    ),
-    fully_consistent_typecheck(
-      "Let statement that adds labels during elaboration",
-      {|let x : (name=String, age=Int)= ("Bob", 20) in x|},
-      Some(
-        Prod([
-          TupLabel(Label("name") |> Typ.fresh, String |> Typ.fresh)
-          |> Typ.fresh,
-          TupLabel(Label("age") |> Typ.fresh, Int |> Typ.fresh) |> Typ.fresh,
-        ])
-        |> Typ.fresh,
+      fully_consistent_typecheck(
+        "Let statement that adds labels during elaboration",
+        {|let x : (name=String, age=Int)= ("Bob", 20) in x|},
+        Some(
+          prod([
+            tup_label(label("name"), string()),
+            tup_label(label("age"), int()),
+          ]),
+        ),
       ),
-    ),
-    fully_consistent_typecheck(
-      "Duplicate singleton labels",
-      {|let y : (l=(l=Int)) = (l=1) in y|},
-      Some(
-        Prod([
-          TupLabel(
-            Label("l") |> Typ.fresh,
-            Parens(
-              Prod([
-                TupLabel(Label("l") |> Typ.fresh, Int |> Typ.fresh)
-                |> Typ.fresh,
-              ])
-              |> Typ.fresh,
-            )
-            |> Typ.fresh,
-          )
-          |> Typ.fresh,
-        ])
-        |> Typ.fresh,
+      fully_consistent_typecheck(
+        "Duplicate singleton labels",
+        {|let y : (l=(l=Int)) = (l=1) in y|},
+        Some(
+          prod([
+            tup_label(
+              label("l"),
+              parens(prod([tup_label(label("l"), int())])),
+            ),
+          ]),
+        ),
       ),
-    ),
-    fully_consistent_typecheck(
-      "Reconstructed labeled tuple without values",
-      {|let x : (l=|},
-      Some(Unknown(Internal) |> Typ.fresh),
-    ),
-    fully_consistent_typecheck(
-      "Singleton labeled argument let with unknown type",
-      {|let x : (a=?) = (a=1) in x|},
-      Some(
-        Prod([
-          TupLabel(
-            Label("a") |> Typ.fresh,
-            Unknown(Hole(EmptyHole)) |> Typ.fresh,
-          )
-          |> Typ.fresh,
-        ])
-        |> Typ.fresh,
+      fully_consistent_typecheck(
+        "Reconstructed labeled tuple without values",
+        {|let x : (l=|},
+        Some(unknown(Internal)),
       ),
-    ),
-    fully_consistent_typecheck(
-      "nested different singleton labeled arguments",
-      {|let x : (b=c=String) = b="" in x|},
-      Some(
-        Prod([
-          TupLabel(
-            Label("b") |> Typ.fresh,
-            Prod([
-              TupLabel(Label("c") |> Typ.fresh, String |> Typ.fresh)
-              |> Typ.fresh,
-            ])
-            |> Typ.fresh,
-          )
-          |> Typ.fresh,
-        ])
-        |> Typ.fresh,
+      fully_consistent_typecheck(
+        "Singleton labeled argument let with unknown type",
+        {|let x : (a=?) = (a=1) in x|},
+        Some(prod([tup_label(label("a"), unknown(Hole(EmptyHole)))])),
       ),
-    ),
-    fully_consistent_typecheck(
-      "nested different singleton labeled arguments",
-      {|let x : (a=b=c=?) = b=? in x|},
-      Some(
-        Prod([
-          TupLabel(
-            Label("a") |> Typ.fresh,
-            Prod([
-              TupLabel(
-                Label("b") |> Typ.fresh,
-                Prod([
-                  TupLabel(
-                    Label("c") |> Typ.fresh,
-                    Unknown(Hole(EmptyHole)) |> Typ.fresh,
-                  )
-                  |> Typ.fresh,
-                ])
-                |> Typ.fresh,
-              )
-              |> Typ.fresh,
-            ])
-            |> Typ.fresh,
-          )
-          |> Typ.fresh,
-        ])
-        |> Typ.fresh,
+      fully_consistent_typecheck(
+        "nested different singleton labeled arguments",
+        {|let x : (b=c=String) = b="" in x|},
+        Some(
+          prod([
+            tup_label(
+              label("b"),
+              prod([tup_label(label("c"), string())]),
+            ),
+          ]),
+        ),
       ),
-    ),
-    fully_consistent_typecheck(
-      "Singleton labeled argument function application with unknown type",
-      {|(fun a=x->x)(a=1)|},
-      Some(unknown(Internal)),
-    ),
-    fully_consistent_typecheck(
-      "Singleton labeled argument function application with no labeled param",
-      {|(fun a=x->x)(1)|},
-      Some(unknown(Internal)),
-    ),
-    fully_consistent_typecheck(
-      "Singleton labeled argument not labeled in pattern",
-      {|let x : (a=Int) -> Int = fun a -> a in x(2)|},
-      Some(int),
-    ),
-    test_case("Unknown label in last position", `Quick, () => {
-      annotated_tree_test(
-        {|(1, 1.2, z="hello") : (a=Int, b=Float, String)|},
-        no_error_exp(
-          Cast(
-            error_exp(
-              Exp(
-                Common(
-                  Inconsistent(
-                    Expectation({
-                      ana:
-                        Prod([
-                          TupLabel(Typ.temp(Label("a")), Typ.temp(Int))
-                          |> Typ.temp,
-                          TupLabel(Typ.temp(Label("b")), Typ.temp(Float))
-                          |> Typ.temp,
-                          Typ.temp(String),
-                        ])
-                        |> Typ.temp,
-                      syn:
-                        Prod([
-                          TupLabel(Label("a") |> Typ.temp, Int |> Typ.temp)
-                          |> Typ.temp,
-                          TupLabel(Label("b") |> Typ.temp, Float |> Typ.temp)
-                          |> Typ.temp,
-                          TupLabel(
-                            Label("z") |> Typ.temp,
-                            String |> Typ.temp,
-                          )
-                          |> Typ.temp,
-                        ])
-                        |> Typ.temp,
-                    }),
-                  ),
+      fully_consistent_typecheck(
+        "nested different singleton labeled arguments",
+        {|let x : (a=b=c=?) = b=? in x|},
+        Some(
+          prod([
+            tup_label(
+              label("a"),
+              prod([
+                tup_label(
+                  label("b"),
+                  prod([tup_label(label("c"), unknown(Hole(EmptyHole)))]),
                 ),
-              ),
-              Parens(
-                error_exp(
-                  Exp(
-                    Common(
-                      TupleLabelError({
-                        malformed_labels: [],
-                        duplicate_labels: [],
-                        invalid_labels: ["z"],
-                        typ:
-                          Prod([
-                            TupLabel(Label("a") |> Typ.temp, Int |> Typ.temp)
-                            |> Typ.temp,
-                            TupLabel(
-                              Label("b") |> Typ.temp,
-                              Float |> Typ.temp,
-                            )
-                            |> Typ.temp,
-                            TupLabel(
-                              Label("z") |> Typ.temp,
-                              String |> Typ.temp,
-                            )
-                            |> Typ.temp,
-                          ])
-                          |> Typ.temp,
-                      }),
+              ]),
+            ),
+          ]),
+        ),
+      ),
+      fully_consistent_typecheck(
+        "Singleton labeled argument function application with unknown type",
+        {|(fun a=x->x)(a=1)|},
+        Some(unknown(Internal)),
+      ),
+      fully_consistent_typecheck(
+        "Singleton labeled argument function application with no labeled param",
+        {|(fun a=x->x)(1)|},
+        Some(unknown(Internal)),
+      ),
+      fully_consistent_typecheck(
+        "Singleton labeled argument not labeled in pattern",
+        {|let x : (a=Int) -> Int = fun a -> a in x(2)|},
+        Some(int()),
+      ),
+      test_case("Unknown label in last position", `Quick, () => {
+        annotated_tree_test(
+          {|(1, 1.2, z="hello") : (a=Int, b=Float, String)|},
+          FIError.(
+            Exp.(
+              cast(
+                parens(
+                  ~ann=
+                    Some(
+                      FTemp.Typ.(
+                        Exp(
+                          Common(
+                            Inconsistent(
+                              Expectation({
+                                ana:
+                                  prod([
+                                    tup_label(label("a"), int()),
+                                    tup_label(label("b"), float()),
+                                    string(),
+                                  ]),
+                                syn:
+                                  prod([
+                                    tup_label(label("a"), int()),
+                                    tup_label(label("b"), float()),
+                                    tup_label(label("z"), string()),
+                                  ]),
+                              }),
+                            ),
+                          ),
+                        )
+                      ),
                     ),
-                  ),
-                  Tuple([
-                    no_error_exp(Int(1)),
-                    no_error_exp(Float(1.2)),
-                    error_exp(
-                      Exp(
-                        Common(
-                          TupleLabelError({
-                            malformed_labels: [],
-                            duplicate_labels: [],
-                            invalid_labels: ["z"],
-                            typ:
-                              TupLabel(
-                                Label("z") |> Typ.temp,
-                                String |> Typ.temp,
-                              )
-                              |> Typ.temp,
-                          }),
+                  tuple(
+                    ~ann=
+                      Some(
+                        Exp(
+                          Common(
+                            TupleLabelError({
+                              malformed_labels: [],
+                              duplicate_labels: [],
+                              invalid_labels: ["z"],
+                              typ:
+                                FTemp.Typ.(
+                                  prod([
+                                    tup_label(label("a"), int()),
+                                    tup_label(label("b"), float()),
+                                    tup_label(label("z"), string()),
+                                  ])
+                                ),
+                            }),
+                          ),
                         ),
                       ),
-                      TupLabel(
-                        error_exp(
-                          Exp(Common(NoType(InvalidLabel("z")))),
-                          Label("z"),
+                    [
+                      int(1),
+                      float(1.2),
+                      tup_label(
+                        ~ann=
+                          Some(
+                            FTemp.Typ.(
+                              Exp(
+                                Common(
+                                  TupleLabelError({
+                                    malformed_labels: [],
+                                    duplicate_labels: [],
+                                    invalid_labels: ["z"],
+                                    typ: tup_label(label("z"), string()),
+                                  }),
+                                ),
+                              )
+                            ),
+                          ),
+                        label(
+                          ~ann=
+                            Some(Exp(Common(NoType(InvalidLabel("z"))))),
+                          "z",
                         ),
-                        no_error_exp(String("hello")),
+                        string("hello"),
                       ),
-                    ),
-                  ]),
+                    ],
+                  ),
                 ),
-              ),
-            ),
-            no_error_typ(Unknown(Internal)),
-            no_error_typ(
-              Parens(
-                no_error_typ(
-                  Prod([
-                    TupLabel(no_error_typ(Label("a")), no_error_typ(Int))
-                    |> no_error_typ,
-                    TupLabel(no_error_typ(Label("b")), no_error_typ(Float))
-                    |> no_error_typ,
-                    no_error_typ(String),
-                  ]),
+                Typ.unknown(Internal),
+                Typ.(
+                  parens(
+                    prod([
+                      tup_label(label("a"), int()),
+                      tup_label(label("b"), float()),
+                      string(),
+                    ]),
+                  )
                 ),
-              ),
-            ),
+              )
+            )
           ),
-        ),
-      )
-    }),
-    test_case("Duplicate label synthesis", `Quick, () => {
-      annotated_tree_test(
-        {|(a="hello", a=3)|},
-        no_error_exp(
-          Parens(
-            error_exp(
-              Exp(
-                Common(
-                  TupleLabelError({
-                    malformed_labels: [],
-                    duplicate_labels: ["a", "a"],
-                    invalid_labels: [],
-                    typ:
-                      Prod([
-                        TupLabel(
-                          Label("a") |> Typ.temp,
-                          Unknown(Internal) |> Typ.temp,
+        )
+      }),
+      test_case("Duplicate label synthesis", `Quick, () => {
+        annotated_tree_test(
+          {|(a="hello", a=3)|},
+          FIError.(
+            Exp.(
+              parens(
+                tuple(
+                  ~ann=
+                    Some(
+                      FTemp.Typ.(
+                        Exp(
+                          Common(
+                            TupleLabelError({
+                              malformed_labels: [],
+                              duplicate_labels: ["a", "a"],
+                              invalid_labels: [],
+                              typ:
+                                prod([
+                                  tup_label(label("a"), unknown(Internal)),
+                                ]),
+                            }),
+                          ),
                         )
-                        |> Typ.temp,
-                      ])
-                      |> Typ.temp,
-                  }),
-                ),
-              ),
-              Tuple([
-                error_exp(
-                  Exp(
-                    Common(
-                      TupleLabelError({
-                        malformed_labels: [],
-                        duplicate_labels: ["a"],
-                        invalid_labels: [],
-                        typ:
-                          TupLabel(
-                            Label("a") |> Typ.temp,
-                            String |> Typ.temp,
-                          )
-                          |> Typ.temp,
-                      }),
-                    ),
-                  ),
-                  TupLabel(
-                    error_exp(
-                      Exp(
-                        Common(DuplicateLabel("a", Label("a") |> Typ.temp)),
                       ),
-                      Label("a"),
                     ),
-                    no_error_exp(String("hello")),
-                  ),
-                ),
-                error_exp(
-                  Exp(
-                    Common(
-                      TupleLabelError({
-                        malformed_labels: [],
-                        duplicate_labels: ["a"],
-                        invalid_labels: [],
-                        typ:
-                          TupLabel(Label("a") |> Typ.temp, Int |> Typ.temp)
-                          |> Typ.temp,
-                      }),
+                  [
+                    tup_label(
+                      ~ann=
+                        Some(
+                          FTemp.Typ.(
+                            Exp(
+                              Common(
+                                TupleLabelError({
+                                  malformed_labels: [],
+                                  duplicate_labels: ["a"],
+                                  invalid_labels: [],
+                                  typ: tup_label(label("a"), string()),
+                                }),
+                              ),
+                            )
+                          ),
+                        ),
+                      label(
+                        ~ann=
+                          Some(
+                            FTemp.Typ.(
+                              Exp(Common(DuplicateLabel("a", label("a"))))
+                            ),
+                          ),
+                        "a",
+                      ),
+                      string("hello"),
                     ),
-                  ),
-                  TupLabel(
-                    error_exp(
-                      Exp(
-                        Common(DuplicateLabel("a", Label("a") |> Typ.temp)),
+                    tup_label(
+                      ~ann=
+                        Some(
+                          FTemp.Typ.(
+                            Exp(
+                              Common(
+                                TupleLabelError({
+                                  malformed_labels: [],
+                                  duplicate_labels: ["a"],
+                                  invalid_labels: [],
+                                  typ: tup_label(label("a"), int()),
+                                }),
+                              ),
+                            )
+                          ),
+                        ),
+                      label(
+                        ~ann=
+                          Some(
+                            FTemp.Typ.(
+                              Exp(Common(DuplicateLabel("a", label("a"))))
+                            ),
+                          ),
+                        "a",
                       ),
-                      Label("a"),
+                      int(3),
                     ),
-                    no_error_exp(Int(3)),
-                  ),
-                ),
-              ]),
-            ),
-          ),
-        ),
-      )
-    }),
-    test_case("Bad label projection", `Quick, () => {
-      annotated_tree_test(
-        {|(1, 2) . 1|},
-        error_exp(
-          Exp(
-            Common(
-              NoType(
-                BadLabel(
-                  Exp(MultiHole([Exp(Int(1) |> Exp.fresh)]) |> Exp.fresh),
+                  ],
                 ),
-              ),
-            ),
-          ),
-          Dot(
-            Tuple([no_error_exp(Int(1)), no_error_exp(Int(2))])
-            |> no_error_exp,
-            no_error_exp(MultiHole([Exp(no_error_exp(Int(1)))])),
+              )
+            )
           ),
-        ),
-      )
-    }),
-    test_case("Singleton Bad label synthesis", `Quick, () => {
-      annotated_tree_test(
-        {|(1="hello")|},
-        no_error_exp(
-          Parens(
-            error_exp(
-              Exp(
-                Common(
-                  TupleLabelError({
-                    malformed_labels: [
-                      Exp(
-                        MultiHole([Exp(Exp.fresh(Label("1")))])
-                        |> Exp.fresh,
-                      ),
-                    ],
-                    duplicate_labels: [],
-                    invalid_labels: [],
-                    typ:
-                      Prod([
-                        TupLabel(
-                          Unknown(Internal) |> Typ.temp,
-                          String |> Typ.temp,
-                        )
-                        |> Typ.temp,
-                      ])
-                      |> Typ.temp,
-                  }),
-                ),
-              ),
-              Tuple([
-                error_exp(
-                  Exp(
-                    Common(
-                      TupleLabelError({
-                        malformed_labels: [
-                          Exp(
-                            MultiHole([Exp(Exp.fresh(Label("1")))])
-                            |> Exp.fresh,
+        )
+      }),
+      test_case("Bad label projection", `Quick, () => {
+        annotated_tree_test(
+          {|(1, 2) . 1|},
+          FIError.(
+            Exp.(
+              dot(
+                ~ann=
+                  Some(
+                    Exp(
+                      Common(
+                        NoType(
+                          BadLabel(
+                            Exp(FTemp.Exp.(multi_hole([Exp(int(1))]))),
                           ),
-                        ],
-                        duplicate_labels: [],
-                        invalid_labels: [],
-                        typ:
-                          TupLabel(
-                            Unknown(Internal) |> Typ.temp,
-                            String |> Typ.temp,
-                          )
-                          |> Typ.temp,
-                      }),
+                        ),
+                      ),
                     ),
                   ),
-                  TupLabel(
-                    error_exp(
-                      Exp(
-                        Common(
-                          NoType(
-                            BadLabel(
-                              Exp(
-                                MultiHole([Exp(Exp.fresh(Label("1")))])
-                                |> Exp.fresh,
+                tuple([int(1), int(2)]),
+                multi_hole([Exp(int(1))]),
+              )
+            )
+          ),
+        )
+      }),
+      test_case("Singleton Bad label synthesis", `Quick, () => {
+        annotated_tree_test(
+          {|(1="hello")|},
+          FIError.(
+            Exp.(
+              parens(
+                tuple(
+                  ~ann=
+                    Some(
+                      FTemp.(
+                        Exp(
+                          Common(
+                            TupleLabelError({
+                              malformed_labels: [
+                                Exp.(Exp(multi_hole([Exp(label("1"))]))),
+                              ],
+                              duplicate_labels: [],
+                              invalid_labels: [],
+                              typ:
+                                Typ.(
+                                  prod([
+                                    tup_label(unknown(Internal), string()),
+                                  ])
+                                ),
+                            }),
+                          ),
+                        )
+                      ),
+                    ),
+                  [
+                    tup_label(
+                      ~ann=
+                        Some(
+                          FTemp.(
+                            Exp(
+                              Common(
+                                TupleLabelError({
+                                  malformed_labels: [
+                                    Exp.(
+                                      Exp(multi_hole([Exp(label("1"))]))
+                                    ),
+                                  ],
+                                  duplicate_labels: [],
+                                  invalid_labels: [],
+                                  typ:
+                                    Typ.(
+                                      tup_label(unknown(Internal), string())
+                                    ),
+                                }),
                               ),
-                            ),
+                            )
                           ),
                         ),
+                      multi_hole(
+                        ~ann=
+                          Some(
+                            Exp(
+                              Common(
+                                NoType(
+                                  BadLabel(
+                                    FTemp.Exp.(
+                                      Exp(multi_hole([Exp(label("1"))]))
+                                    ),
+                                  ),
+                                ),
+                              ),
+                            ),
+                          ),
+                        [Exp(label("1"))],
                       ),
-                      MultiHole([Exp(no_error_exp(Label("1")))]),
+                      string("hello"),
                     ),
-                    no_error_exp(String("hello")),
-                  ),
+                  ],
                 ),
-              ]),
-            ),
+              )
+            )
           ),
-        ),
-      )
-    }),
-    test_case("Bad label synthesis", `Quick, () => {
-      annotated_tree_test(
-        {|(1="hello", a=3)|},
-        no_error_exp(
-          Parens(
-            error_exp(
-              Exp(
-                Common(
-                  TupleLabelError({
-                    malformed_labels: [
-                      Exp(
-                        MultiHole([Exp(Int(1) |> Exp.fresh)]) |> Exp.fresh,
-                      ),
-                    ],
-                    duplicate_labels: [],
-                    invalid_labels: [],
-                    typ:
-                      Prod([
-                        TupLabel(
-                          Unknown(Internal) |> Typ.temp,
-                          String |> Typ.temp,
-                        )
-                        |> Typ.temp,
-                        TupLabel(Label("a") |> Typ.temp, Int |> Typ.temp)
-                        |> Typ.temp,
-                      ])
-                      |> Typ.temp,
-                  }),
-                ),
-              ),
-              Tuple([
-                error_exp(
-                  Exp(
-                    Common(
-                      TupleLabelError({
-                        malformed_labels: [
-                          Exp(
-                            MultiHole([Exp(Int(1) |> Exp.fresh)])
-                            |> Exp.fresh,
+        )
+      }),
+      test_case("Bad label synthesis", `Quick, () => {
+        annotated_tree_test(
+          {|(1="hello", a=3)|},
+          FIError.(
+            Exp.(
+              parens(
+                tuple(
+                  ~ann=
+                    Some(
+                      FTemp.(
+                        Exp(
+                          Common(
+                            TupleLabelError({
+                              malformed_labels: [
+                                Exp.(Exp(multi_hole([Exp(int(1))]))),
+                              ],
+                              duplicate_labels: [],
+                              invalid_labels: [],
+                              typ:
+                                Typ.(
+                                  prod([
+                                    tup_label(unknown(Internal), string()),
+                                    tup_label(label("a"), int()),
+                                  ])
+                                ),
+                            }),
                           ),
-                        ],
-                        duplicate_labels: [],
-                        invalid_labels: [],
-                        typ:
-                          TupLabel(
-                            Unknown(Internal) |> Typ.temp,
-                            String |> Typ.temp,
-                          )
-                          |> Typ.temp,
-                      }),
+                        )
+                      ),
                     ),
-                  ),
-                  TupLabel(
-                    error_exp(
-                      Exp(
-                        Common(
-                          NoType(
-                            BadLabel(
-                              Exp(
-                                MultiHole([Exp(Int(1) |> Exp.fresh)])
-                                |> Exp.fresh,
+                  [
+                    tup_label(
+                      ~ann=
+                        Some(
+                          FTemp.(
+                            Exp(
+                              Common(
+                                TupleLabelError({
+                                  malformed_labels: [
+                                    Exp.(Exp(multi_hole([Exp(int(1))]))),
+                                  ],
+                                  duplicate_labels: [],
+                                  invalid_labels: [],
+                                  typ:
+                                    Typ.(
+                                      tup_label(unknown(Internal), string())
+                                    ),
+                                }),
                               ),
-                            ),
+                            )
                           ),
                         ),
+                      multi_hole(
+                        ~ann=
+                          FTemp.(
+                            Some(
+                              Exp(
+                                Common(
+                                  NoType(
+                                    BadLabel(
+                                      Exp.(Exp(multi_hole([Exp(int(1))]))),
+                                    ),
+                                  ),
+                                ),
+                              ),
+                            )
+                          ),
+                        [Exp(int(1))],
                       ),
-                      MultiHole([Exp(no_error_exp(Int(1)))]),
+                      string("hello"),
                     ),
-                    no_error_exp(String("hello")),
-                  ),
-                ),
-                no_error_exp(
-                  TupLabel(
-                    no_error_exp(Label("a")),
-                    no_error_exp(Int(3)),
-                  ),
+                    tup_label(label("a"), int(3)),
+                  ],
                 ),
-              ]),
-            ),
+              )
+            )
           ),
-        ),
-      )
-    }),
-    test_case("Extra Label", `Quick, () => {
-      annotated_tree_test(
-        {|let extra_label : (Int, a=String) = (c=1, a="hello") in true|},
-        no_error_exp(
-          Let(
-            no_error_pat(
-              Cast(
-                no_error_pat(Var("extra_label")),
-                no_error_typ(
-                  Parens(
-                    no_error_typ(
-                      Prod([
-                        no_error_typ(Int),
-                        no_error_typ(
-                          TupLabel(
-                            no_error_typ(Label("a")),
-                            no_error_typ(String),
-                          ),
-                        ),
-                      ]),
+        )
+      }),
+      test_case("Extra Label", `Quick, () => {
+        annotated_tree_test(
+          {|let extra_label : (Int, a=String) = (c=1, a="hello") in true|},
+          FIError.(
+            Exp.(
+              let_(
+                Pat.(
+                  cast(
+                    var("extra_label"),
+                    Typ.(
+                      parens(
+                        prod([int(), tup_label(label("a"), string())]),
+                      )
                     ),
-                  ),
-                ),
-                no_error_typ(Unknown(Internal)),
-              ),
-            ),
-            error_exp(
-              Exp(
-                Common(
-                  Inconsistent(
-                    Expectation({
-                      ana:
-                        Parens(
-                          Prod([
-                            Int |> Typ.fresh,
-                            TupLabel(
-                              Label("a") |> Typ.fresh,
-                              String |> Typ.fresh,
-                            )
-                            |> Typ.fresh,
-                          ])
-                          |> Typ.fresh,
-                        )
-                        |> Typ.fresh,
-                      syn:
-                        Prod([
-                          TupLabel(Label("c") |> Typ.fresh, Int |> Typ.fresh)
-                          |> Typ.fresh,
-                          TupLabel(
-                            Label("a") |> Typ.fresh,
-                            String |> Typ.fresh,
-                          )
-                          |> Typ.fresh,
-                        ])
-                        |> Typ.fresh,
-                    }),
-                  ),
+                    Typ.unknown(Internal),
+                  )
                 ),
-              ),
-              Parens(
-                error_exp(
-                  Exp(
-                    Common(
-                      TupleLabelError({
-                        malformed_labels: [],
-                        duplicate_labels: [],
-                        invalid_labels: ["c"],
-                        typ:
-                          Prod([
-                            TupLabel(
-                              Label("c") |> Typ.fresh,
-                              Int |> Typ.fresh,
-                            )
-                            |> Typ.fresh,
-                            TupLabel(
-                              Label("a") |> Typ.fresh,
-                              String |> Typ.fresh,
-                            )
-                            |> Typ.fresh,
-                          ])
-                          |> Typ.fresh,
-                      }),
-                    ),
-                  ),
-                  Tuple([
-                    error_exp(
+                parens(
+                  ~ann=
+                    Some(
                       Exp(
                         Common(
-                          TupleLabelError({
-                            malformed_labels: [],
-                            duplicate_labels: [],
-                            invalid_labels: ["c"],
-                            typ:
-                              TupLabel(
-                                Label("c") |> Typ.fresh,
-                                Int |> Typ.fresh,
-                              )
-                              |> Typ.fresh,
-                          }),
-                        ),
-                      ),
-                      TupLabel(
-                        error_exp(
-                          Exp(Common(NoType(InvalidLabel("c")))),
-                          Label("c"),
+                          Inconsistent(
+                            FTemp.Typ.(
+                              Expectation({
+                                ana:
+                                  parens(
+                                    prod([
+                                      int(),
+                                      tup_label(label("a"), string()),
+                                    ]),
+                                  ),
+                                syn:
+                                  prod([
+                                    tup_label(label("c"), int()),
+                                    tup_label(label("a"), string()),
+                                  ]),
+                              })
+                            ),
+                          ),
                         ),
-                        no_error_exp(Int(1)),
                       ),
                     ),
-                    no_error_exp(
-                      TupLabel(
-                        no_error_exp(Label("a")),
-                        no_error_exp(String("hello")),
+                  tuple(
+                    ~ann=
+                      Some(
+                        Exp(
+                          Common(
+                            TupleLabelError({
+                              malformed_labels: [],
+                              duplicate_labels: [],
+                              invalid_labels: ["c"],
+                              typ:
+                                FTemp.Typ.(
+                                  prod([
+                                    tup_label(label("c"), int()),
+                                    tup_label(label("a"), string()),
+                                  ])
+                                ),
+                            }),
+                          ),
+                        ),
                       ),
-                    ),
-                  ]),
+                    [
+                      {
+                        tup_label(
+                          ~ann=
+                            Some(
+                              Exp(
+                                Common(
+                                  TupleLabelError({
+                                    malformed_labels: [],
+                                    duplicate_labels: [],
+                                    invalid_labels: ["c"],
+                                    typ:
+                                      FTemp.Typ.(
+                                        tup_label(label("c"), int())
+                                      ),
+                                  }),
+                                ),
+                              ),
+                            ),
+                          label(
+                            ~ann=
+                              Some(
+                                Exp(Common(NoType(InvalidLabel("c")))),
+                              ),
+                            "c",
+                          ),
+                          int(1),
+                        );
+                      },
+                      tup_label(label("a"), string("hello")),
+                    ],
+                  ),
                 ),
-              ),
-            ),
-            no_error_exp(Bool(true)),
+                bool(true),
+              )
+            )
           ),
-        ),
-      )
-    }),
-    test_case("tuple with cast to non-tuple", `Quick, () => {
-      annotated_tree_test(
-        {|(a=1, b=2) : Int|},
-        no_error_exp(
-          Cast(
-            no_error_exp(
-              Parens(
-                error_exp(
-                  Exp(
-                    Common(
-                      Inconsistent(
-                        Expectation({
-                          ana: Int |> Typ.temp,
-                          syn:
-                            Prod([
-                              TupLabel(
-                                Label("a") |> Typ.temp,
-                                Int |> Typ.temp,
-                              )
-                              |> Typ.temp,
-                              TupLabel(
-                                Label("b") |> Typ.temp,
-                                Int |> Typ.temp,
-                              )
-                              |> Typ.temp,
-                            ])
-                            |> Typ.temp,
-                        }),
+        )
+      }),
+      test_case("tuple with cast to non-tuple", `Quick, () => {
+        annotated_tree_test(
+          {|(a=1, b=2) : Int|},
+          FIError.(
+            Exp.(
+              cast(
+                parens(
+                  tuple(
+                    ~ann=
+                      Some(
+                        Exp(
+                          Common(
+                            Inconsistent(
+                              FTemp.Typ.(
+                                Expectation({
+                                  ana: int(),
+                                  syn:
+                                    prod([
+                                      tup_label(label("a"), int()),
+                                      tup_label(label("b"), int()),
+                                    ]),
+                                })
+                              ),
+                            ),
+                          ),
+                        ),
                       ),
-                    ),
+                    [
+                      tup_label(label("a"), int(1)),
+                      tup_label(label("b"), int(2)),
+                    ],
                   ),
-                  Tuple([
-                    TupLabel(
-                      no_error_exp(Label("a")),
-                      no_error_exp(Int(1)),
-                    )
-                    |> no_error_exp,
-                    TupLabel(
-                      no_error_exp(Label("b")),
-                      no_error_exp(Int(2)),
-                    )
-                    |> no_error_exp,
-                  ]),
                 ),
-              ),
-            ),
-            Unknown(Internal) |> no_error_typ,
-            Int |> no_error_typ,
+                Typ.unknown(Internal),
+                Typ.int(),
+              )
+            )
           ),
-        ),
-      )
-    }),
-    test_case("Example error annotations", `Quick, () => {
-      annotated_tree_test(
-        "Inconsistent expectation on plus",
-        no_error_exp(
-          BinOp(
-            Int(Plus),
-            no_error_exp(Int(1)),
-            error_exp(
-              Exp(
-                Common(
-                  Inconsistent(
-                    Expectation({
-                      ana: Int |> Typ.fresh,
-                      syn: String |> Typ.fresh,
-                    }),
+        )
+      }),
+      test_case("Example error annotations", `Quick, () => {
+        annotated_tree_test(
+          "Inconsistent expectation on plus",
+          FIError.Exp.(
+            bin_op(
+              Int(Plus),
+              int(1),
+              string(
+                ~ann=
+                  Some(
+                    FTemp.Typ.(
+                      Exp(
+                        Common(
+                          Inconsistent(
+                            Expectation({ana: int(), syn: string()}),
+                          ),
+                        ),
+                      )
+                    ),
                   ),
-                ),
+                "hello",
               ),
-              String("hello"),
-            ),
+            )
           ),
-        ),
-      )
-    }),
-    fully_consistent_typecheck(
-      "Forall alpha equivalent in cast",
-      {|let x : forall a -> a = in (x : forall b -> b)|},
-      Some(
-        Forall(Var("b") |> TPat.fresh, Var("b") |> Typ.fresh) |> Typ.fresh,
+        )
+      }),
+      fully_consistent_typecheck(
+        "Forall alpha equivalent in cast",
+        {|let x : forall a -> a = in (x : forall b -> b)|},
+        FTemp.Typ.(Some(forall(TPat.var("b"), var("b")))),
       ),
-    ),
-    fully_consistent_typecheck(
-      "Forall alpha equivalent in let",
-      {|let x : forall a -> a = in let y : forall b -> b = x in 1|},
-      Some(int),
-    ),
-  ],
+      fully_consistent_typecheck(
+        "Forall alpha equivalent in let",
+        {|let x : forall a -> a = in let y : forall b -> b = x in 1|},
+        Some(int()),
+      ),
+    ]
+  ),
 );