diff --git a/src/haz3lcore/assistant/AssistantForms.re b/src/haz3lcore/assistant/AssistantForms.re
index f3551ac0eb..a66d711787 100644
--- a/src/haz3lcore/assistant/AssistantForms.re
+++ b/src/haz3lcore/assistant/AssistantForms.re
@@ -27,7 +27,7 @@ module Typ = {
     ("fun" ++ leading_expander, Arrow(unk, unk) |> Typ.fresh),
     (
       "typfun" ++ leading_expander,
-      Forall(Var("") |> TPat.fresh, unk) |> Typ.fresh,
+      Forall(VarTPat("") |> TPat.fresh, unk) |> Typ.fresh,
     ),
     ("if" ++ leading_expander, unk),
     ("let" ++ leading_expander, unk),
diff --git a/src/haz3lcore/dynamics/Builtins.re b/src/haz3lcore/dynamics/Builtins.re
index c47617edc6..bf383eb9b8 100644
--- a/src/haz3lcore/dynamics/Builtins.re
+++ b/src/haz3lcore/dynamics/Builtins.re
@@ -41,13 +41,13 @@ let fn =
 module Pervasives = {
   module Impls = {
     /* constants */
-    let infinity = 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 = FloatLit(Float.infinity) |> fresh;
+    let neg_infinity = FloatLit(Float.neg_infinity) |> fresh;
+    let nan = FloatLit(Float.nan) |> fresh;
+    let epsilon_float = FloatLit(epsilon_float) |> fresh;
+    let pi = FloatLit(Float.pi) |> fresh;
+    let max_int = IntLit(Int.max_int) |> fresh;
+    let min_int = IntLit(Int.min_int) |> fresh;
 
     let unary = (f: DHExp.t => result, d: DHExp.t) => {
       switch (f(d)) {
@@ -81,7 +81,7 @@ module Pervasives = {
     let is_finite =
       unary(d =>
         switch (term_of(d)) {
-        | Float(f) => Ok(fresh(Bool(Float.is_finite(f))))
+        | FloatLit(f) => Ok(fresh(BoolLit(Float.is_finite(f))))
         | _ => Error(InvalidBoxedFloatLit(d))
         }
       );
@@ -89,7 +89,7 @@ module Pervasives = {
     let is_infinite =
       unary(d =>
         switch (term_of(d)) {
-        | Float(f) => Ok(fresh(Bool(Float.is_infinite(f))))
+        | FloatLit(f) => Ok(fresh(BoolLit(Float.is_infinite(f))))
         | _ => Error(InvalidBoxedFloatLit(d))
         }
       );
@@ -97,7 +97,7 @@ module Pervasives = {
     let is_nan =
       unary(d =>
         switch (term_of(d)) {
-        | Float(f) => Ok(fresh(Bool(Float.is_nan(f))))
+        | FloatLit(f) => Ok(fresh(BoolLit(Float.is_nan(f))))
         | _ => Error(InvalidBoxedFloatLit(d))
         }
       );
@@ -105,7 +105,7 @@ module Pervasives = {
     let string_of_int =
       unary(d =>
         switch (term_of(d)) {
-        | Int(n) => Ok(fresh(String(string_of_int(n))))
+        | IntLit(n) => Ok(fresh(StringLit(string_of_int(n))))
         | _ => Error(InvalidBoxedIntLit(d))
         }
       );
@@ -113,7 +113,7 @@ module Pervasives = {
     let string_of_float =
       unary(d =>
         switch (term_of(d)) {
-        | Float(f) => Ok(fresh(String(string_of_float(f))))
+        | FloatLit(f) => Ok(fresh(StringLit(string_of_float(f))))
         | _ => Error(InvalidBoxedFloatLit(d))
         }
       );
@@ -121,7 +121,7 @@ module Pervasives = {
     let string_of_bool =
       unary(d =>
         switch (term_of(d)) {
-        | Bool(b) => Ok(fresh(String(string_of_bool(b))))
+        | BoolLit(b) => Ok(fresh(StringLit(string_of_bool(b))))
         | _ => Error(InvalidBoxedBoolLit(d))
         }
       );
@@ -129,7 +129,7 @@ module Pervasives = {
     let int_of_float =
       unary(d =>
         switch (term_of(d)) {
-        | Float(f) => Ok(fresh(Int(int_of_float(f))))
+        | FloatLit(f) => Ok(fresh(IntLit(int_of_float(f))))
         | _ => Error(InvalidBoxedFloatLit(d))
         }
       );
@@ -137,7 +137,7 @@ module Pervasives = {
     let float_of_int =
       unary(d =>
         switch (term_of(d)) {
-        | Int(n) => Ok(fresh(Float(float_of_int(n))))
+        | IntLit(n) => Ok(fresh(FloatLit(float_of_int(n))))
         | _ => Error(InvalidBoxedIntLit(d))
         }
       );
@@ -145,7 +145,7 @@ module Pervasives = {
     let abs =
       unary(d =>
         switch (term_of(d)) {
-        | Int(n) => Ok(fresh(Int(abs(n))))
+        | IntLit(n) => Ok(fresh(IntLit(abs(n))))
         | _ => Error(InvalidBoxedIntLit(d))
         }
       );
@@ -153,7 +153,7 @@ module Pervasives = {
     let float_op = fn =>
       unary(d =>
         switch (term_of(d)) {
-        | Float(f) => Ok(fresh(Float(fn(f))))
+        | FloatLit(f) => Ok(fresh(FloatLit(fn(f))))
         | _ => Error(InvalidBoxedFloatLit(d))
         }
       );
@@ -176,7 +176,7 @@ module Pervasives = {
         (convert: string => option('a), wrap: 'a => DHExp.t, name: string) =>
       unary(d =>
         switch (term_of(d)) {
-        | String(s) =>
+        | StringLit(s) =>
           switch (convert(s)) {
           | Some(n) => Ok(wrap(n))
           | None =>
@@ -190,17 +190,17 @@ module Pervasives = {
       );
 
     let int_of_string =
-      of_string(int_of_string_opt, n => Int(n) |> DHExp.fresh);
+      of_string(int_of_string_opt, n => IntLit(n) |> DHExp.fresh);
     let float_of_string =
-      of_string(float_of_string_opt, f => Float(f) |> DHExp.fresh);
+      of_string(float_of_string_opt, f => FloatLit(f) |> DHExp.fresh);
     let bool_of_string =
-      of_string(bool_of_string_opt, b => Bool(b) |> DHExp.fresh);
+      of_string(bool_of_string_opt, b => BoolLit(b) |> DHExp.fresh);
 
     let int_mod = (name, d1) =>
       binary(
         (d1, d2) =>
           switch (term_of(d1), term_of(d2)) {
-          | (Int(_), Int(0)) =>
+          | (IntLit(_), IntLit(0)) =>
             Ok(
               fresh(
                 DynamicErrorHole(
@@ -209,8 +209,8 @@ module Pervasives = {
                 ),
               ),
             )
-          | (Int(n), Int(m)) => Ok(Int(n mod m) |> fresh)
-          | (Int(_), _) =>
+          | (IntLit(n), IntLit(m)) => Ok(IntLit(n mod m) |> fresh)
+          | (IntLit(_), _) =>
             raise(EvaluatorError.Exception(InvalidBoxedIntLit(d2)))
           | (_, _) =>
             raise(EvaluatorError.Exception(InvalidBoxedIntLit(d1)))
@@ -221,7 +221,7 @@ module Pervasives = {
     let string_length =
       unary(d =>
         switch (term_of(d)) {
-        | String(s) => Ok(Int(String.length(s)) |> fresh)
+        | StringLit(s) => Ok(IntLit(String.length(s)) |> fresh)
         | _ => Error(InvalidBoxedStringLit(d))
         }
       );
@@ -229,9 +229,9 @@ module Pervasives = {
     let string_compare =
       binary((d1, d2) =>
         switch (term_of(d1), term_of(d2)) {
-        | (String(s1), String(s2)) =>
-          Ok(Int(String.compare(s1, s2)) |> fresh)
-        | (String(_), _) => Error(InvalidBoxedStringLit(d2))
+        | (StringLit(s1), StringLit(s2)) =>
+          Ok(IntLit(String.compare(s1, s2)) |> fresh)
+        | (StringLit(_), _) => Error(InvalidBoxedStringLit(d2))
         | (_, _) => Error(InvalidBoxedStringLit(d1))
         }
       );
@@ -239,7 +239,7 @@ module Pervasives = {
     let string_trim =
       unary(d =>
         switch (term_of(d)) {
-        | String(s) => Ok(String(String.trim(s)) |> fresh)
+        | StringLit(s) => Ok(StringLit(String.trim(s)) |> fresh)
         | _ => Error(InvalidBoxedStringLit(d))
         }
       );
@@ -247,19 +247,19 @@ module Pervasives = {
     let string_of: DHExp.t => option(string) =
       d =>
         switch (term_of(d)) {
-        | String(s) => Some(s)
+        | StringLit(s) => Some(s)
         | _ => None
         };
 
     let string_concat =
       binary((d1, d2) =>
         switch (term_of(d1), term_of(d2)) {
-        | (String(s1), ListLit(xs)) =>
+        | (StringLit(s1), ListLit(xs)) =>
           switch (xs |> List.map(string_of) |> Util.OptUtil.sequence) {
           | None => Error(InvalidBoxedStringLit(List.hd(xs)))
-          | Some(xs) => Ok(String(String.concat(s1, xs)) |> fresh)
+          | Some(xs) => Ok(StringLit(String.concat(s1, xs)) |> fresh)
           }
-        | (String(_), _) => Error(InvalidBoxedListLit(d2))
+        | (StringLit(_), _) => Error(InvalidBoxedListLit(d2))
         | (_, _) => Error(InvalidBoxedStringLit(d1))
         }
       );
@@ -267,14 +267,14 @@ module Pervasives = {
     let string_sub = _ =>
       ternary((d1, d2, d3) =>
         switch (term_of(d1), term_of(d2), term_of(d3)) {
-        | (String(s), Int(idx), Int(len)) =>
-          try(Ok(String(String.sub(s, idx, len)) |> fresh)) {
+        | (StringLit(s), IntLit(idx), IntLit(len)) =>
+          try(Ok(StringLit(String.sub(s, idx, len)) |> fresh)) {
           | _ =>
             // TODO: make it clear that the problem could be with d3 too
             Ok(DynamicErrorHole(d2, IndexOutOfBounds) |> fresh)
           }
-        | (String(_), Int(_), _) => Error(InvalidBoxedIntLit(d3))
-        | (String(_), _, _) => Error(InvalidBoxedIntLit(d2))
+        | (StringLit(_), IntLit(_), _) => Error(InvalidBoxedIntLit(d3))
+        | (StringLit(_), _, _) => Error(InvalidBoxedIntLit(d2))
         | (_, _, _) => Error(InvalidBoxedIntLit(d1))
         }
       );
diff --git a/src/haz3lcore/dynamics/Casts.re b/src/haz3lcore/dynamics/Casts.re
index a69f560dd5..9f0a8ead4e 100644
--- a/src/haz3lcore/dynamics/Casts.re
+++ b/src/haz3lcore/dynamics/Casts.re
@@ -34,7 +34,7 @@ let grounded_Arrow =
   );
 let grounded_Forall =
   NotGroundOrHole(
-    Forall(EmptyHole |> TPat.fresh, Unknown(Internal) |> Typ.temp)
+    Forall(EmptyHoleTPat |> TPat.fresh, Unknown(Internal) |> Typ.temp)
     |> Typ.temp,
   );
 let grounded_Prod = length =>
@@ -58,12 +58,12 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => {
   | Int
   | Float
   | String
-  | Var(_)
+  | TypVar(_)
   | Rec(_)
   | Forall(_, {term: Unknown(_), _})
   | Arrow({term: Unknown(_), _}, {term: Unknown(_), _})
   | List({term: Unknown(_), _}) => Ground
-  | Parens(ty) => ground_cases_of(ty)
+  | TypParens(ty) => ground_cases_of(ty)
   | Prod(tys) =>
     if (List.for_all(
           fun
@@ -81,7 +81,7 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => {
   | Arrow(_, _) => grounded_Arrow
   | Forall(_) => grounded_Forall
   | List(_) => grounded_List
-  | Ap(_) => failwith("type application in dynamics")
+  | ApTyp(_) => failwith("type application in dynamics")
   };
 };
 
@@ -183,7 +183,7 @@ let hole = EmptyHole |> DHExp.fresh;
 let pattern_fixup = (p: DHPat.t): DHPat.t => {
   let rec unwrap_casts = (p: DHPat.t): (DHPat.t, DHExp.t) => {
     switch (DHPat.term_of(p)) {
-    | Cast(p1, t1, t2) =>
+    | CastPat(p1, t1, t2) =>
       let (p1, d1) = unwrap_casts(p1);
       (
         p1,
@@ -198,13 +198,13 @@ let pattern_fixup = (p: DHPat.t): DHPat.t => {
     | EmptyHole => p
     | Cast(d1, t1, t2) =>
       let p1 = rewrap_casts((p, d1));
-      {term: Cast(p1, t1, t2), copied: d.copied, ids: d.ids};
+      {term: CastPat(p1, t1, t2), copied: d.copied, ids: d.ids};
     | FailedCast(d1, t1, t2) =>
       let p1 = rewrap_casts((p, d1));
       {
         term:
-          Cast(
-            Cast(p1, t1, Typ.fresh(Unknown(Internal))) |> DHPat.fresh,
+          CastPat(
+            CastPat(p1, t1, Typ.fresh(Unknown(Internal))) |> DHPat.fresh,
             Typ.fresh(Unknown(Internal)),
             t2,
           ),
diff --git a/src/haz3lcore/dynamics/DHExp.re b/src/haz3lcore/dynamics/DHExp.re
index f7651ba963..ad9bd015b2 100644
--- a/src/haz3lcore/dynamics/DHExp.re
+++ b/src/haz3lcore/dynamics/DHExp.re
@@ -67,10 +67,10 @@ let rec strip_casts =
         | EmptyHole
         | Invalid(_)
         | Var(_)
-        | Bool(_)
-        | Int(_)
-        | Float(_)
-        | String(_)
+        | BoolLit(_)
+        | IntLit(_)
+        | FloatLit(_)
+        | StringLit(_)
         | Constructor(_)
         | DynamicErrorHole(_)
         | Closure(_)
@@ -135,10 +135,10 @@ let ty_subst = (s: Typ.t, tpat: TPat.t, exp: t): t => {
           | Undefined
           | Constructor(_)
           | Var(_)
-          | Bool(_)
-          | Int(_)
-          | Float(_)
-          | String(_)
+          | BoolLit(_)
+          | IntLit(_)
+          | FloatLit(_)
+          | StringLit(_)
           | FailedCast(_, _, _)
           | MultiHole(_)
           | Deferral(_)
diff --git a/src/haz3lcore/dynamics/DHPat.re b/src/haz3lcore/dynamics/DHPat.re
index f9e4adbddb..c7e18cca3d 100644
--- a/src/haz3lcore/dynamics/DHPat.re
+++ b/src/haz3lcore/dynamics/DHPat.re
@@ -12,43 +12,43 @@ let rec binds_var = (m: Statics.Map.t, x: Var.t, dp: t): bool =>
   | Some(_) => false
   | None =>
     switch (dp |> term_of) {
-    | EmptyHole
-    | MultiHole(_)
+    | EmptyHolePat
+    | MultiHolePat(_)
     | Wild
-    | Invalid(_)
-    | Int(_)
-    | Float(_)
-    | Bool(_)
-    | String(_)
-    | Constructor(_) => false
-    | Cast(y, _, _)
-    | Parens(y) => binds_var(m, x, y)
-    | Var(y) => Var.eq(x, y)
-    | Tuple(dps) => dps |> List.exists(binds_var(m, x))
-    | Cons(dp1, dp2) => binds_var(m, x, dp1) || binds_var(m, x, dp2)
-    | ListLit(d_list) =>
+    | InvalidPat(_)
+    | IntPat(_)
+    | FloatPat(_)
+    | BoolPat(_)
+    | StringPat(_)
+    | ConstructorPat(_) => false
+    | CastPat(y, _, _)
+    | ParensPat(y) => binds_var(m, x, y)
+    | VarPat(y) => Var.eq(x, y)
+    | TuplePat(dps) => dps |> List.exists(binds_var(m, x))
+    | ConsPat(dp1, dp2) => binds_var(m, x, dp1) || binds_var(m, x, dp2)
+    | ListLitPat(d_list) =>
       let new_list = List.map(binds_var(m, x), d_list);
       List.fold_left((||), false, new_list);
-    | Ap(_, _) => false
+    | ApPat(_, _) => false
     }
   };
 
 let rec bound_vars = (dp: t): list(Var.t) =>
   switch (dp |> term_of) {
-  | EmptyHole
-  | MultiHole(_)
+  | EmptyHolePat
+  | MultiHolePat(_)
   | Wild
-  | Invalid(_)
-  | Int(_)
-  | Float(_)
-  | Bool(_)
-  | String(_)
-  | Constructor(_) => []
-  | Cast(y, _, _)
-  | Parens(y) => bound_vars(y)
-  | Var(y) => [y]
-  | Tuple(dps) => List.flatten(List.map(bound_vars, dps))
-  | Cons(dp1, dp2) => bound_vars(dp1) @ bound_vars(dp2)
-  | ListLit(dps) => List.flatten(List.map(bound_vars, dps))
-  | Ap(_, dp1) => bound_vars(dp1)
+  | InvalidPat(_)
+  | IntPat(_)
+  | FloatPat(_)
+  | BoolPat(_)
+  | StringPat(_)
+  | ConstructorPat(_) => []
+  | CastPat(y, _, _)
+  | ParensPat(y) => bound_vars(y)
+  | VarPat(y) => [y]
+  | TuplePat(dps) => List.flatten(List.map(bound_vars, dps))
+  | ConsPat(dp1, dp2) => bound_vars(dp1) @ bound_vars(dp2)
+  | ListLitPat(dps) => List.flatten(List.map(bound_vars, dps))
+  | ApPat(_, dp1) => bound_vars(dp1)
   };
diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
index d50d462064..c4a571e93c 100644
--- a/src/haz3lcore/dynamics/Elaborator.re
+++ b/src/haz3lcore/dynamics/Elaborator.re
@@ -36,8 +36,8 @@ let fresh_pat_cast = (p: DHPat.t, t1: Typ.t, t2: Typ.t): DHPat.t => {
   Typ.eq(t1, t2)
     ? p
     : {
-      Cast(
-        DHPat.fresh(Cast(p, t1, Typ.temp(Unknown(Internal))))
+      CastPat(
+        DHPat.fresh(CastPat(p, t1, Typ.temp(Unknown(Internal))))
         |> Casts.pattern_fixup,
         Typ.temp(Unknown(Internal)),
         t2,
@@ -66,7 +66,7 @@ let elaborated_type = (m: Statics.Map.t, uexp: UExp.t): (Typ.t, Ctx.t, 'a) => {
       Arrow(ty1, ty2) |> Typ.temp;
     | SynTypFun =>
       let (tpat, ty) = Typ.matched_forall(ctx, self_ty);
-      let tpat = Option.value(tpat, ~default=TPat.fresh(EmptyHole));
+      let tpat = Option.value(tpat, ~default=TPat.fresh(EmptyHoleTPat));
       Forall(tpat, ty) |> Typ.temp;
     // We need to remove the synswitches from this type.
     | Ana(ana_ty) => Typ.match_synswitch(ana_ty, self_ty)
@@ -93,7 +93,7 @@ let elaborated_pat_type = (m: Statics.Map.t, upat: UPat.t): (Typ.t, Ctx.t) => {
       Arrow(ty1, ty2) |> Typ.temp;
     | SynTypFun =>
       let (tpat, ty) = Typ.matched_forall(ctx, self_ty);
-      let tpat = Option.value(tpat, ~default=TPat.fresh(EmptyHole));
+      let tpat = Option.value(tpat, ~default=TPat.fresh(EmptyHoleTPat));
       Forall(tpat, ty) |> Typ.temp;
     | Ana(ana_ty) =>
       switch (prev_synswitch) {
@@ -111,11 +111,11 @@ let rec elaborate_pattern =
   let (term, rewrap) = UPat.unwrap(upat);
   let dpat =
     switch (term) {
-    | Int(_) => upat |> cast_from(Int |> Typ.temp)
-    | Bool(_) => upat |> cast_from(Bool |> Typ.temp)
-    | Float(_) => upat |> cast_from(Float |> Typ.temp)
-    | String(_) => upat |> cast_from(String |> Typ.temp)
-    | ListLit(ps) =>
+    | IntPat(_) => upat |> cast_from(Int |> Typ.temp)
+    | BoolPat(_) => upat |> cast_from(Bool |> Typ.temp)
+    | FloatPat(_) => upat |> cast_from(Float |> Typ.temp)
+    | StringPat(_) => upat |> cast_from(String |> Typ.temp)
+    | ListLitPat(ps) =>
       let (ps, tys) = List.map(elaborate_pattern(m), ps) |> ListUtil.unzip;
       let inner_type =
         tys
@@ -125,9 +125,11 @@ let rec elaborate_pattern =
       |> List.map2((p, t) => fresh_pat_cast(p, t, inner_type), _, tys)
       |> (
         ps' =>
-          ListLit(ps') |> rewrap |> cast_from(List(inner_type) |> Typ.temp)
+          ListLitPat(ps')
+          |> rewrap
+          |> cast_from(List(inner_type) |> Typ.temp)
       );
-    | Cons(p1, p2) =>
+    | ConsPat(p1, p2) =>
       let (p1', ty1) = elaborate_pattern(m, p1);
       let (p2', ty2) = elaborate_pattern(m, p2);
       let ty2_inner = Typ.matched_list(ctx, ty2);
@@ -136,22 +138,22 @@ let rec elaborate_pattern =
         |> Option.value(~default=Typ.temp(Unknown(Internal)));
       let p1'' = fresh_pat_cast(p1', ty1, ty_inner);
       let p2'' = fresh_pat_cast(p2', ty2, List(ty_inner) |> Typ.temp);
-      Cons(p1'', p2'') |> rewrap |> cast_from(List(ty_inner) |> Typ.temp);
-    | Tuple(ps) =>
+      ConsPat(p1'', p2'') |> rewrap |> cast_from(List(ty_inner) |> Typ.temp);
+    | TuplePat(ps) =>
       let (ps', tys) = List.map(elaborate_pattern(m), ps) |> ListUtil.unzip;
-      Tuple(ps') |> rewrap |> cast_from(Prod(tys) |> Typ.temp);
-    | Ap(p1, p2) =>
+      TuplePat(ps') |> rewrap |> cast_from(Prod(tys) |> Typ.temp);
+    | ApPat(p1, p2) =>
       let (p1', ty1) = elaborate_pattern(m, p1);
       let (p2', ty2) = elaborate_pattern(m, p2);
       let (ty1l, ty1r) = Typ.matched_arrow(ctx, ty1);
       let p1'' = fresh_pat_cast(p1', ty1, Arrow(ty1l, ty1r) |> Typ.temp);
       let p2'' = fresh_pat_cast(p2', ty2, ty1l);
-      Ap(p1'', p2'') |> rewrap |> cast_from(ty1r);
-    | Invalid(_)
-    | EmptyHole
-    | MultiHole(_)
+      ApPat(p1'', p2'') |> rewrap |> cast_from(ty1r);
+    | InvalidPat(_)
+    | EmptyHolePat
+    | MultiHolePat(_)
     | Wild => upat |> cast_from(Typ.temp(Unknown(Internal)))
-    | Var(v) =>
+    | VarPat(v) =>
       upat
       |> cast_from(
            Ctx.lookup_var(ctx, v)
@@ -159,11 +161,11 @@ let rec elaborate_pattern =
            |> Option.value(~default=Typ.temp(Unknown(Internal))),
          )
     // Type annotations should already appear
-    | Parens(p)
-    | Cast(p, _, _) =>
+    | ParensPat(p)
+    | CastPat(p, _, _) =>
       let (p', ty) = elaborate_pattern(m, p);
       p' |> cast_from(ty |> Typ.normalize(ctx));
-    | Constructor(c, _) =>
+    | ConstructorPat(c, _) =>
       let mode =
         switch (Id.Map.find_opt(Pat.rep_id(upat), m)) {
         | Some(Info.InfoPat({mode, _})) => mode
@@ -176,7 +178,7 @@ let rec elaborate_pattern =
         | _ => Unknown(Internal) |> Typ.temp
         };
       let t = t |> Typ.normalize(ctx);
-      Constructor(c, t) |> rewrap |> cast_from(t);
+      ConstructorPat(c, t) |> rewrap |> cast_from(t);
     };
   (dpat, elaborated_type);
 };
@@ -234,10 +236,10 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
       let (e', ty) = elaborate(m, e);
       e' |> cast_from(ty);
     | Deferral(_) => uexp
-    | Int(_) => uexp |> cast_from(Int |> Typ.temp)
-    | Bool(_) => uexp |> cast_from(Bool |> Typ.temp)
-    | Float(_) => uexp |> cast_from(Float |> Typ.temp)
-    | String(_) => uexp |> cast_from(String |> Typ.temp)
+    | IntLit(_) => uexp |> cast_from(Int |> Typ.temp)
+    | BoolLit(_) => uexp |> cast_from(Bool |> Typ.temp)
+    | FloatLit(_) => uexp |> cast_from(Float |> Typ.temp)
+    | StringLit(_) => uexp |> cast_from(String |> Typ.temp)
     | ListLit(es) =>
       let (ds, tys) = List.map(elaborate(m), es) |> ListUtil.unzip;
       let inner_type =
@@ -353,7 +355,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
       let tye'' =
         Typ.subst(
           ut',
-          tpat |> Option.value(~default=TPat.fresh(EmptyHole)),
+          tpat |> Option.value(~default=TPat.fresh(EmptyHoleTPat)),
           tye',
         );
       TypAp(e', ut) |> rewrap |> cast_from(tye'');
@@ -382,7 +384,8 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
       let kind' =
         switch (kind) {
         | Residue(_) => kind
-        | Filter({act, pat}) => Filter({act, pat: elaborate(m, pat) |> fst})
+        | FilterStepper({act, pat}) =>
+          FilterStepper({act, pat: elaborate(m, pat) |> fst})
         };
       Filter(kind', e') |> rewrap |> cast_from(t);
     | Closure(env, e) =>
diff --git a/src/haz3lcore/dynamics/EvaluatorStep.re b/src/haz3lcore/dynamics/EvaluatorStep.re
index f25f25603f..008541b676 100644
--- a/src/haz3lcore/dynamics/EvaluatorStep.re
+++ b/src/haz3lcore/dynamics/EvaluatorStep.re
@@ -243,10 +243,10 @@ let rec matches =
       | Closure(env, ctx) =>
         let+ ctx = matches(env, flt, ctx, exp, act, idx);
         Closure(env, ctx) |> wrap_ids(ids);
-      | Filter(Filter(flt'), ctx) =>
+      | Filter(FilterStepper(flt'), ctx) =>
         let flt = flt |> FilterEnvironment.extends(flt');
         let+ ctx = matches(env, flt, ctx, exp, act, idx);
-        Filter(Filter(flt'), ctx) |> wrap_ids(ids);
+        Filter(FilterStepper(flt'), ctx) |> wrap_ids(ids);
       | Filter(Residue(idx', act'), ctx) =>
         let (ract, ridx, rctx) =
           if (idx > idx') {
diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re
index 61fd72f1bd..dcb3d324ef 100644
--- a/src/haz3lcore/dynamics/FilterMatcher.re
+++ b/src/haz3lcore/dynamics/FilterMatcher.re
@@ -202,17 +202,17 @@ let rec matches_exp =
       TermBase.StepperFilterKind.fast_equal(df, ff) && matches_exp(dd, fd)
     | (Filter(_), _) => false
 
-    | (Bool(dv), Bool(fv)) => dv == fv
-    | (Bool(_), _) => false
+    | (BoolLit(dv), BoolLit(fv)) => dv == fv
+    | (BoolLit(_), _) => false
 
-    | (Int(dv), Int(fv)) => dv == fv
-    | (Int(_), _) => false
+    | (IntLit(dv), IntLit(fv)) => dv == fv
+    | (IntLit(_), _) => false
 
-    | (Float(dv), Float(fv)) => dv == fv
-    | (Float(_), _) => false
+    | (FloatLit(dv), FloatLit(fv)) => dv == fv
+    | (FloatLit(_), _) => false
 
-    | (String(dv), String(fv)) => dv == fv
-    | (String(_), _) => false
+    | (StringLit(dv), StringLit(fv)) => dv == fv
+    | (StringLit(_), _) => false
 
     | (
         Constructor(_),
@@ -377,11 +377,12 @@ and matches_typ = (d: Typ.t, f: Typ.t) => {
 
 and matches_utpat = (d: TPat.t, f: TPat.t): bool => {
   switch (d.term, f.term) {
-  | (Invalid(_), _) => false
-  | (_, Invalid(_)) => false
-  | (_, EmptyHole) => true
-  | (MultiHole(l1), MultiHole(l2)) => List.length(l1) == List.length(l2) /* TODO: probably should define a matches_any and recurse in here...? */
-  | (Var(t1), Var(t2)) => t1 == t2
+  | (InvalidTPat(_), _) => false
+  | (_, InvalidTPat(_)) => false
+  | (_, EmptyHoleTPat) => true
+  | (MultiHoleTPat(l1), MultiHoleTPat(l2)) =>
+    List.length(l1) == List.length(l2) /* TODO: probably should define a matches_any and recurse in here...? */
+  | (VarTPat(t1), VarTPat(t2)) => t1 == t2
   | _ => false
   };
 };
diff --git a/src/haz3lcore/dynamics/PatternMatch.re b/src/haz3lcore/dynamics/PatternMatch.re
index 329ca1efd8..2f282d88e1 100644
--- a/src/haz3lcore/dynamics/PatternMatch.re
+++ b/src/haz3lcore/dynamics/PatternMatch.re
@@ -13,23 +13,23 @@ let combine_result = (r1: match_result, r2: match_result): match_result =>
 
 let rec matches = (dp: Pat.t, d: DHExp.t): match_result =>
   switch (DHPat.term_of(dp)) {
-  | Invalid(_)
-  | EmptyHole
-  | MultiHole(_)
+  | InvalidPat(_)
+  | EmptyHolePat
+  | MultiHolePat(_)
   | Wild => Matches(Environment.empty)
-  | Int(n) =>
+  | IntPat(n) =>
     let* n' = Unboxing.unbox(Int, d);
     n == n' ? Matches(Environment.empty) : DoesNotMatch;
-  | Float(n) =>
+  | FloatPat(n) =>
     let* n' = Unboxing.unbox(Float, d);
     n == n' ? Matches(Environment.empty) : DoesNotMatch;
-  | Bool(b) =>
+  | BoolPat(b) =>
     let* b' = Unboxing.unbox(Bool, d);
     b == b' ? Matches(Environment.empty) : DoesNotMatch;
-  | String(s) =>
+  | StringPat(s) =>
     let* s' = Unboxing.unbox(String, d);
     s == s' ? Matches(Environment.empty) : DoesNotMatch;
-  | ListLit(xs) =>
+  | ListLitPat(xs) =>
     let* s' = Unboxing.unbox(List, d);
     if (List.length(xs) == List.length(s')) {
       List.map2(matches, xs, s')
@@ -37,24 +37,24 @@ let rec matches = (dp: Pat.t, d: DHExp.t): match_result =>
     } else {
       DoesNotMatch;
     };
-  | Cons(x, xs) =>
+  | ConsPat(x, xs) =>
     let* (x', xs') = Unboxing.unbox(Cons, d);
     let* m_x = matches(x, x');
     let* m_xs = matches(xs, xs');
     Matches(Environment.union(m_x, m_xs));
-  | Constructor(ctr, _) =>
+  | ConstructorPat(ctr, _) =>
     let* () = Unboxing.unbox(SumNoArg(ctr), d);
     Matches(Environment.empty);
-  | Ap({term: Constructor(ctr, _), _}, p2) =>
+  | ApPat({term: ConstructorPat(ctr, _), _}, p2) =>
     let* d2 = Unboxing.unbox(SumWithArg(ctr), d);
     matches(p2, d2);
-  | Ap(_, _) => IndetMatch // TODO: should this fail?
-  | Var(x) => Matches(Environment.singleton((x, d)))
-  | Tuple(ps) =>
+  | ApPat(_, _) => IndetMatch // TODO: should this fail?
+  | VarPat(x) => Matches(Environment.singleton((x, d)))
+  | TuplePat(ps) =>
     let* ds = Unboxing.unbox(Tuple(List.length(ps)), d);
     List.map2(matches, ps, ds)
     |> List.fold_left(combine_result, Matches(Environment.empty));
-  | Parens(p) => matches(p, d)
-  | Cast(p, t1, t2) =>
+  | ParensPat(p) => matches(p, d)
+  | CastPat(p, t1, t2) =>
     matches(p, Cast(d, t2, t1) |> DHExp.fresh |> Casts.transition_multiple)
   };
diff --git a/src/haz3lcore/dynamics/Stepper.re b/src/haz3lcore/dynamics/Stepper.re
index 8b977cdf5f..34184941cb 100644
--- a/src/haz3lcore/dynamics/Stepper.re
+++ b/src/haz3lcore/dynamics/Stepper.re
@@ -52,10 +52,10 @@ let rec matches =
       | Closure(env, ctx) =>
         let+ ctx = matches(env, flt, ctx, exp, act, idx);
         Closure(env, ctx) |> rewrap;
-      | Filter(Filter(flt'), ctx) =>
+      | Filter(FilterStepper(flt'), ctx) =>
         let flt = flt |> FilterEnvironment.extends(flt');
         let+ ctx = matches(env, flt, ctx, exp, act, idx);
-        Filter(Filter(flt'), ctx) |> rewrap;
+        Filter(FilterStepper(flt'), ctx) |> rewrap;
       | Filter(Residue(idx', act'), ctx) =>
         let (ract, ridx, rctx) =
           if (idx > idx') {
diff --git a/src/haz3lcore/dynamics/Substitution.re b/src/haz3lcore/dynamics/Substitution.re
index 5d918e520b..492e7c9ac8 100644
--- a/src/haz3lcore/dynamics/Substitution.re
+++ b/src/haz3lcore/dynamics/Substitution.re
@@ -60,10 +60,10 @@ let rec subst_var = (m, d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t => {
     Ap(dir, d3, d4) |> rewrap;
   | BuiltinFun(_) => d2
   | Test(d3) => Test(subst_var(m, d1, x, d3)) |> rewrap
-  | Bool(_)
-  | Int(_)
-  | Float(_)
-  | String(_)
+  | BoolLit(_)
+  | IntLit(_)
+  | FloatLit(_)
+  | StringLit(_)
   | Constructor(_) => d2
   | ListLit(ds) => ListLit(List.map(subst_var(m, d1, x), ds)) |> rewrap
   | Cons(d3, d4) =>
diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re
index a54c9d18d8..30393b8e2b 100644
--- a/src/haz3lcore/dynamics/Transition.re
+++ b/src/haz3lcore/dynamics/Transition.re
@@ -442,10 +442,10 @@ module Transition = (EV: EV_MODE) => {
     | Deferral(_) =>
       let. _ = otherwise(env, d);
       Indet;
-    | Bool(_)
-    | Int(_)
-    | Float(_)
-    | String(_)
+    | BoolLit(_)
+    | IntLit(_)
+    | FloatLit(_)
+    | StringLit(_)
     | Constructor(_)
     | BuiltinFun(_) =>
       let. _ = otherwise(env, d);
@@ -477,7 +477,7 @@ module Transition = (EV: EV_MODE) => {
         );
       let-unbox n = (Int, d1');
       Step({
-        expr: Int(- n) |> fresh,
+        expr: IntLit(- n) |> fresh,
         state_update,
         kind: UnOp(Int(Minus)),
         is_value: true,
@@ -492,7 +492,7 @@ module Transition = (EV: EV_MODE) => {
         );
       let-unbox b = (Bool, d1');
       Step({
-        expr: Bool(!b) |> fresh,
+        expr: BoolLit(!b) |> fresh,
         state_update,
         kind: UnOp(Bool(Not)),
         is_value: true,
@@ -507,7 +507,7 @@ module Transition = (EV: EV_MODE) => {
         );
       let-unbox b1 = (Bool, d1');
       Step({
-        expr: b1 ? d2 : Bool(false) |> fresh,
+        expr: b1 ? d2 : BoolLit(false) |> fresh,
         state_update,
         kind: BinBoolOp(And),
         is_value: false,
@@ -522,7 +522,7 @@ module Transition = (EV: EV_MODE) => {
         );
       let-unbox b1 = (Bool, d1');
       Step({
-        expr: b1 ? Bool(true) |> fresh : d2,
+        expr: b1 ? BoolLit(true) |> fresh : d2,
         state_update,
         kind: BinBoolOp(Or),
         is_value: false,
@@ -547,27 +547,27 @@ module Transition = (EV: EV_MODE) => {
         expr:
           (
             switch (op) {
-            | Plus => Int(n1 + n2)
-            | Minus => Int(n1 - n2)
+            | Plus => IntLit(n1 + n2)
+            | Minus => IntLit(n1 - n2)
             | Power when n2 < 0 =>
               DynamicErrorHole(
                 BinOp(Int(op), d1', d2') |> rewrap,
                 NegativeExponent,
               )
-            | Power => Int(IntUtil.ipow(n1, n2))
-            | Times => Int(n1 * n2)
+            | Power => IntLit(IntUtil.ipow(n1, n2))
+            | Times => IntLit(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)
+            | Divide => IntLit(n1 / n2)
+            | LessThan => BoolLit(n1 < n2)
+            | LessThanOrEqual => BoolLit(n1 <= n2)
+            | GreaterThan => BoolLit(n1 > n2)
+            | GreaterThanOrEqual => BoolLit(n1 >= n2)
+            | Equals => BoolLit(n1 == n2)
+            | NotEquals => BoolLit(n1 != n2)
             }
           )
           |> fresh,
@@ -597,17 +597,17 @@ module Transition = (EV: EV_MODE) => {
         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)
+            | Plus => FloatLit(n1 +. n2)
+            | Minus => FloatLit(n1 -. n2)
+            | Power => FloatLit(n1 ** n2)
+            | Times => FloatLit(n1 *. n2)
+            | Divide => FloatLit(n1 /. n2)
+            | LessThan => BoolLit(n1 < n2)
+            | LessThanOrEqual => BoolLit(n1 <= n2)
+            | GreaterThan => BoolLit(n1 > n2)
+            | GreaterThanOrEqual => BoolLit(n1 >= n2)
+            | Equals => BoolLit(n1 == n2)
+            | NotEquals => BoolLit(n1 != n2)
             }
           )
           |> fresh,
@@ -635,8 +635,8 @@ module Transition = (EV: EV_MODE) => {
       Step({
         expr:
           switch (op) {
-          | Concat => String(s1 ++ s2) |> fresh
-          | Equals => Bool(s1 == s2) |> fresh
+          | Concat => StringLit(s1 ++ s2) |> fresh
+          | Equals => BoolLit(s1 == s2) |> fresh
           },
         state_update,
         kind: BinStringOp(op),
diff --git a/src/haz3lcore/dynamics/TypeAssignment.re b/src/haz3lcore/dynamics/TypeAssignment.re
index 59b58aa56f..88da409502 100644
--- a/src/haz3lcore/dynamics/TypeAssignment.re
+++ b/src/haz3lcore/dynamics/TypeAssignment.re
@@ -34,43 +34,43 @@ let dhpat_extend_ctx = (dhpat: DHPat.t, ty: Typ.t, ctx: Ctx.t): option(Ctx.t) =>
   let rec dhpat_var_entry =
           (dhpat: DHPat.t, ty: Typ.t): option(list(Ctx.entry)) => {
     switch (dhpat |> Pat.term_of) {
-    | Var(name) =>
+    | VarPat(name) =>
       let entry = Ctx.VarEntry({name, id: Id.invalid, typ: ty});
       Some([entry]);
-    | Tuple(l1) =>
+    | TuplePat(l1) =>
       let* ts = Typ.matched_prod_strict(ctx, List.length(l1), ty);
       let* l =
         List.map2((dhp, typ) => {dhpat_var_entry(dhp, typ)}, l1, ts)
         |> OptUtil.sequence;
       Some(List.concat(l));
-    | Cons(dhp1, dhp2) =>
+    | ConsPat(dhp1, dhp2) =>
       let* t = Typ.matched_list_strict(ctx, ty);
       let* l1 = dhpat_var_entry(dhp1, t);
       let* l2 = dhpat_var_entry(dhp2, List(t) |> Typ.temp);
       Some(l1 @ l2);
-    | ListLit(l) =>
+    | ListLitPat(l) =>
       let* t = Typ.matched_list_strict(ctx, ty);
       let* l =
         List.map(dhp => {dhpat_var_entry(dhp, t)}, l) |> OptUtil.sequence;
       Some(List.concat(l));
-    | Ap({term: Constructor(name, _), _}, dhp) =>
+    | ApPat({term: ConstructorPat(name, _), _}, dhp) =>
       // TODO: make this stricter
       let* ctrs = Typ.get_sum_constructors(ctx, ty);
       let* typ = ConstructorMap.get_entry(name, ctrs);
       let* (ty1, ty2) = Typ.matched_arrow_strict(ctx, typ);
       Typ.eq(ty2, ty) ? dhpat_var_entry(dhp, ty1) : None;
-    | Ap(_) => None
-    | EmptyHole
+    | ApPat(_) => None
+    | EmptyHolePat
     | Wild
-    | Invalid(_)
-    | MultiHole(_) => Some([])
-    | Parens(dhp) => dhpat_var_entry(dhp, ty)
-    | Int(_) => Typ.eq(ty, Int |> Typ.temp) ? Some([]) : None
-    | Float(_) => Typ.eq(ty, Float |> Typ.temp) ? Some([]) : None
-    | Bool(_) => Typ.eq(ty, Bool |> Typ.temp) ? Some([]) : None
-    | String(_) => Typ.eq(ty, String |> Typ.temp) ? Some([]) : None
-    | Constructor(_) => Some([]) // TODO: make this stricter
-    | Cast(dhp, ty1, ty2) =>
+    | InvalidPat(_)
+    | MultiHolePat(_) => Some([])
+    | ParensPat(dhp) => dhpat_var_entry(dhp, ty)
+    | IntPat(_) => Typ.eq(ty, Int |> Typ.temp) ? Some([]) : None
+    | FloatPat(_) => Typ.eq(ty, Float |> Typ.temp) ? Some([]) : None
+    | BoolPat(_) => Typ.eq(ty, Bool |> Typ.temp) ? Some([]) : None
+    | StringPat(_) => Typ.eq(ty, String |> Typ.temp) ? Some([]) : None
+    | ConstructorPat(_) => Some([]) // TODO: make this stricter
+    | CastPat(dhp, ty1, ty2) =>
       Typ.eq(ty, ty2) ? dhpat_var_entry(dhp, ty1) : None
     };
   };
@@ -81,29 +81,29 @@ let dhpat_extend_ctx = (dhpat: DHPat.t, ty: Typ.t, ctx: Ctx.t): option(Ctx.t) =>
 /* patterns in functions and fixpoints must have a synthesizable type */
 let rec dhpat_synthesize = (dhpat: DHPat.t, ctx: Ctx.t): option(Typ.t) => {
   switch (dhpat |> Pat.term_of) {
-  | Var(_)
-  | Constructor(_)
-  | Ap(_) => None
-  | Tuple(dhs) =>
+  | VarPat(_)
+  | ConstructorPat(_)
+  | ApPat(_) => None
+  | TuplePat(dhs) =>
     let* l = List.map(dhpat_synthesize(_, ctx), dhs) |> OptUtil.sequence;
     Some(Prod(l) |> Typ.temp);
-  | Cons(dhp1, _) =>
+  | ConsPat(dhp1, _) =>
     let* t = dhpat_synthesize(dhp1, ctx);
     Some(List(t) |> Typ.temp);
-  | ListLit([]) => Some(List(Unknown(Internal) |> Typ.temp) |> Typ.temp)
-  | ListLit([x, ..._]) =>
+  | ListLitPat([]) => Some(List(Unknown(Internal) |> Typ.temp) |> Typ.temp)
+  | ListLitPat([x, ..._]) =>
     let* t_x = dhpat_synthesize(x, ctx);
     Some(List(t_x) |> Typ.temp);
-  | EmptyHole => Some(Unknown(Internal) |> Typ.temp)
+  | EmptyHolePat => Some(Unknown(Internal) |> Typ.temp)
   | Wild => Some(Unknown(Internal) |> Typ.temp)
-  | Invalid(_)
-  | MultiHole(_) => Some(Unknown(Internal) |> Typ.temp)
-  | Parens(dhp) => dhpat_synthesize(dhp, ctx)
-  | Int(_) => Some(Int |> Typ.temp)
-  | Float(_) => Some(Float |> Typ.temp)
-  | Bool(_) => Some(Bool |> Typ.temp)
-  | String(_) => Some(String |> Typ.temp)
-  | Cast(_, _, ty) => Some(ty)
+  | InvalidPat(_)
+  | MultiHolePat(_) => Some(Unknown(Internal) |> Typ.temp)
+  | ParensPat(dhp) => dhpat_synthesize(dhp, ctx)
+  | IntPat(_) => Some(Int |> Typ.temp)
+  | FloatPat(_) => Some(Float |> Typ.temp)
+  | BoolPat(_) => Some(Bool |> Typ.temp)
+  | StringPat(_) => Some(String |> Typ.temp)
+  | CastPat(_, _, ty) => Some(ty)
   };
 };
 
@@ -162,7 +162,7 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) =>
     let* ctx = dhpat_extend_ctx(dhp, ty_p, ctx);
     let* ty2 = typ_of_dhexp(ctx, m, d);
     Some(Arrow(ty_p, ty2) |> Typ.temp);
-  | TypFun({term: Var(name), _} as utpat, d, _)
+  | TypFun({term: VarTPat(name), _} as utpat, d, _)
       when !Ctx.shadows_typ(ctx, name) =>
     let ctx =
       Ctx.extend_tvar(ctx, {name, id: TPat.rep_id(utpat), kind: Abstract});
@@ -170,7 +170,7 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) =>
     Some(Forall(utpat, ty) |> Typ.temp);
   | TypFun(_, d, _) =>
     let* ty = typ_of_dhexp(ctx, m, d);
-    Some(Forall(Var("?") |> TPat.fresh, ty) |> Typ.temp);
+    Some(Forall(VarTPat("?") |> TPat.fresh, ty) |> Typ.temp);
   | TypAp(d, ty1) =>
     let* ty = typ_of_dhexp(ctx, m, d);
     let* (name, ty2) = Typ.matched_forall_strict(ctx, ty);
@@ -222,10 +222,10 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) =>
   | Test(dtest) =>
     let* ty = typ_of_dhexp(ctx, m, dtest);
     Typ.eq(ty, Bool |> Typ.temp) ? Some(Prod([]) |> Typ.temp) : None;
-  | Bool(_) => Some(Bool |> Typ.temp)
-  | Int(_) => Some(Int |> Typ.temp)
-  | Float(_) => Some(Float |> Typ.temp)
-  | String(_) => Some(String |> Typ.temp)
+  | BoolLit(_) => Some(Bool |> Typ.temp)
+  | IntLit(_) => Some(Int |> Typ.temp)
+  | FloatLit(_) => Some(Float |> Typ.temp)
+  | StringLit(_) => Some(String |> Typ.temp)
   | BinOp(Bool(_), d1, d2) =>
     let* ty1 = typ_of_dhexp(ctx, m, d1);
     let* ty2 = typ_of_dhexp(ctx, m, d2);
diff --git a/src/haz3lcore/dynamics/Unboxing.re b/src/haz3lcore/dynamics/Unboxing.re
index 400620026c..6cbad137c9 100644
--- a/src/haz3lcore/dynamics/Unboxing.re
+++ b/src/haz3lcore/dynamics/Unboxing.re
@@ -49,15 +49,15 @@ let rec unbox: type a. (unbox_request(a), DHExp.t) => unboxed(a) =
   (request, expr) => {
     switch (request, DHExp.term_of(expr)) {
     /* Remove parentheses from casts */
-    | (_, Cast(d, {term: Parens(x), _}, y))
-    | (_, Cast(d, x, {term: Parens(y), _})) =>
+    | (_, Cast(d, {term: TypParens(x), _}, y))
+    | (_, Cast(d, x, {term: TypParens(y), _})) =>
       unbox(request, Cast(d, x, y) |> DHExp.fresh)
 
     /* Base types are always already unboxed because of the ITCastID rule*/
-    | (Bool, Bool(b)) => Matches(b)
-    | (Int, Int(i)) => Matches(i)
-    | (Float, Float(f)) => Matches(f)
-    | (String, String(s)) => Matches(s)
+    | (Bool, BoolLit(b)) => Matches(b)
+    | (Int, IntLit(i)) => Matches(i)
+    | (Float, FloatLit(f)) => Matches(f)
+    | (String, StringLit(s)) => Matches(s)
 
     /* Lists can be either lists or list casts */
     | (List, ListLit(l)) => Matches(l)
@@ -145,7 +145,7 @@ let rec unbox: type a. (unbox_request(a), DHExp.t) => unboxed(a) =
        in elaboration or in the cast calculus. */
     | (
         _,
-        Bool(_) | Int(_) | Float(_) | String(_) | Constructor(_) |
+        BoolLit(_) | IntLit(_) | FloatLit(_) | StringLit(_) | Constructor(_) |
         BuiltinFun(_) |
         Deferral(_) |
         DeferredAp(_) |
diff --git a/src/haz3lcore/lang/term/TPat.re b/src/haz3lcore/lang/term/TPat.re
index 583f805851..6a359be59d 100644
--- a/src/haz3lcore/lang/term/TPat.re
+++ b/src/haz3lcore/lang/term/TPat.re
@@ -12,16 +12,16 @@ let fresh: term => t = IdTagged.fresh;
 
 let hole = (tms: list(TermBase.Any.t)): TermBase.TPat.term =>
   switch (tms) {
-  | [] => EmptyHole
-  | [_, ..._] => MultiHole(tms)
+  | [] => EmptyHoleTPat
+  | [_, ..._] => MultiHoleTPat(tms)
   };
 
 let cls_of_term: term => cls =
   fun
-  | Invalid(_) => Invalid
-  | EmptyHole => EmptyHole
-  | MultiHole(_) => MultiHole
-  | Var(_) => Var;
+  | InvalidTPat(_) => Invalid
+  | EmptyHoleTPat => EmptyHole
+  | MultiHoleTPat(_) => MultiHole
+  | VarTPat(_) => Var;
 
 let show_cls: cls => string =
   fun
diff --git a/src/haz3lcore/lang/term/Typ.re b/src/haz3lcore/lang/term/Typ.re
index c9a6f0c204..d7936efb29 100644
--- a/src/haz3lcore/lang/term/Typ.re
+++ b/src/haz3lcore/lang/term/Typ.re
@@ -36,15 +36,15 @@ let rep_id: t => Id.t = IdTagged.rep_id;
 
 let hole = (tms: list(TermBase.Any.t)): TermBase.Typ.term =>
   switch (tms) {
-  | [] => Unknown(Hole(EmptyHole))
-  | [_, ..._] => Unknown(Hole(MultiHole(tms)))
+  | [] => Unknown(HoleProvenance(EmptyTypeHole))
+  | [_, ..._] => Unknown(HoleProvenance(MultiTypeHole(tms)))
   };
 
 let cls_of_term: term => cls =
   fun
-  | Unknown(Hole(Invalid(_))) => Invalid
-  | Unknown(Hole(EmptyHole)) => EmptyHole
-  | Unknown(Hole(MultiHole(_))) => MultiHole
+  | Unknown(HoleProvenance(InvalidTypeHole(_))) => Invalid
+  | Unknown(HoleProvenance(EmptyTypeHole)) => EmptyHole
+  | Unknown(HoleProvenance(MultiTypeHole(_))) => MultiHole
   | Unknown(SynSwitch) => SynSwitch
   | Unknown(Internal) => Internal
   | Int => Int
@@ -53,10 +53,10 @@ let cls_of_term: term => cls =
   | String => String
   | List(_) => List
   | Arrow(_) => Arrow
-  | Var(_) => Var
+  | TypVar(_) => Var
   | Prod(_) => Prod
-  | Parens(_) => Parens
-  | Ap(_) => Ap
+  | TypParens(_) => Parens
+  | ApTyp(_) => Ap
   | Sum(_) => Sum
   | Rec(_) => Rec
   | Forall(_) => Forall;
@@ -85,7 +85,7 @@ let show_cls: cls => string =
 
 let rec is_arrow = (typ: t) => {
   switch (typ.term) {
-  | Parens(typ) => is_arrow(typ)
+  | TypParens(typ) => is_arrow(typ)
   | Arrow(_) => true
   | Unknown(_)
   | Int
@@ -94,8 +94,8 @@ let rec is_arrow = (typ: t) => {
   | String
   | List(_)
   | Prod(_)
-  | Var(_)
-  | Ap(_)
+  | TypVar(_)
+  | ApTyp(_)
   | Sum(_)
   | Forall(_)
   | Rec(_) => false
@@ -104,7 +104,7 @@ let rec is_arrow = (typ: t) => {
 
 let rec is_forall = (typ: t) => {
   switch (typ.term) {
-  | Parens(typ) => is_forall(typ)
+  | TypParens(typ) => is_forall(typ)
   | Forall(_) => true
   | Unknown(_)
   | Int
@@ -114,8 +114,8 @@ let rec is_forall = (typ: t) => {
   | Arrow(_)
   | List(_)
   | Prod(_)
-  | Var(_)
-  | Ap(_)
+  | TypVar(_)
+  | ApTyp(_)
   | Sum(_)
   | Rec(_) => false
   };
@@ -140,13 +140,18 @@ let join_type_provenance =
     (p1: TermBase.type_provenance, p2: TermBase.type_provenance)
     : TermBase.type_provenance =>
   switch (p1, p2) {
-  | (Hole(h1), Hole(h2)) when h1 == h2 => Hole(h1)
-  | (Hole(EmptyHole), Hole(EmptyHole) | SynSwitch)
-  | (SynSwitch, Hole(EmptyHole)) => Hole(EmptyHole)
+  | (HoleProvenance(h1), HoleProvenance(h2)) when h1 == h2 =>
+    HoleProvenance(h1)
+  | (
+      HoleProvenance(EmptyTypeHole),
+      HoleProvenance(EmptyTypeHole) | SynSwitch,
+    )
+  | (SynSwitch, HoleProvenance(EmptyTypeHole)) =>
+    HoleProvenance(EmptyTypeHole)
   | (SynSwitch, Internal)
   | (Internal, SynSwitch) => SynSwitch
-  | (Internal | Hole(_), _)
-  | (_, Hole(_)) => Internal
+  | (Internal | HoleProvenance(_), _)
+  | (_, HoleProvenance(_)) => Internal
   | (SynSwitch, SynSwitch) => SynSwitch
   };
 
@@ -157,9 +162,9 @@ let rec free_vars = (~bound=[], ty: t): list(Var.t) =>
   | Float
   | Bool
   | String => []
-  | Ap(t1, t2) => free_vars(~bound, t1) @ free_vars(~bound, t2)
-  | Var(v) => List.mem(v, bound) ? [] : [v]
-  | Parens(ty) => free_vars(~bound, ty)
+  | ApTyp(t1, t2) => free_vars(~bound, t1) @ free_vars(~bound, t2)
+  | TypVar(v) => List.mem(v, bound) ? [] : [v]
+  | TypParens(ty) => free_vars(~bound, ty)
   | List(ty) => free_vars(~bound, ty)
   | Arrow(t1, t2) => free_vars(~bound, t1) @ free_vars(~bound, t2)
   | Sum(sm) => ConstructorMap.free_variables(free_vars(~bound), sm)
@@ -194,9 +199,9 @@ let eq = (t1: t, t2: t): bool => fast_equal(t1, t2);
 let rec join = (~resolve=false, ~fix, ctx: Ctx.t, ty1: t, ty2: t): option(t) => {
   let join' = join(~resolve, ~fix, ctx);
   switch (term_of(ty1), term_of(ty2)) {
-  | (_, Parens(ty2)) => join'(ty1, ty2)
-  | (Parens(ty1), _) => join'(ty1, ty2)
-  | (_, Unknown(Hole(_))) when fix =>
+  | (_, TypParens(ty2)) => join'(ty1, ty2)
+  | (TypParens(ty1), _) => join'(ty1, ty2)
+  | (_, Unknown(HoleProvenance(_))) when fix =>
     /* NOTE(andrew): This is load bearing
        for ensuring that function literals get appropriate
        casts. Documentation/Dynamics has regression tests */
@@ -205,7 +210,7 @@ let rec join = (~resolve=false, ~fix, ctx: Ctx.t, ty1: t, ty2: t): option(t) =>
     Some(Unknown(join_type_provenance(p1, p2)) |> temp)
   | (Unknown(_), _) => Some(ty2)
   | (_, Unknown(Internal | SynSwitch)) => Some(ty1)
-  | (Var(n1), Var(n2)) =>
+  | (TypVar(n1), TypVar(n2)) =>
     if (n1 == n2) {
       Some(ty1);
     } else {
@@ -214,11 +219,11 @@ let rec join = (~resolve=false, ~fix, ctx: Ctx.t, ty1: t, ty2: t): option(t) =>
       let+ ty_join = join'(ty1, ty2);
       !resolve && eq(ty1, ty_join) ? ty1 : ty_join;
     }
-  | (Var(name), _) =>
+  | (TypVar(name), _) =>
     let* ty_name = Ctx.lookup_alias(ctx, name);
     let+ ty_join = join'(ty_name, ty2);
     !resolve && eq(ty_name, ty_join) ? ty1 : ty_join;
-  | (_, Var(name)) =>
+  | (_, TypVar(name)) =>
     let* ty_name = Ctx.lookup_alias(ctx, name);
     let+ ty_join = join'(ty_name, ty1);
     !resolve && eq(ty_name, ty_join) ? ty2 : ty_join;
@@ -227,7 +232,7 @@ let rec join = (~resolve=false, ~fix, ctx: Ctx.t, ty1: t, ty2: t): option(t) =>
     let ctx = Ctx.extend_dummy_tvar(ctx, tp1);
     let ty1' =
       switch (TPat.tyvar_of_utpat(tp2)) {
-      | Some(x2) => subst(Var(x2) |> temp, tp1, ty1)
+      | Some(x2) => subst(TypVar(x2) |> temp, tp1, ty1)
       | None => ty1
       };
     let+ ty_body = join(~resolve, ~fix, ctx, ty1', ty2);
@@ -237,7 +242,7 @@ let rec join = (~resolve=false, ~fix, ctx: Ctx.t, ty1: t, ty2: t): option(t) =>
     let ctx = Ctx.extend_dummy_tvar(ctx, x1);
     let ty1' =
       switch (TPat.tyvar_of_utpat(x2)) {
-      | Some(x2) => subst(Var(x2) |> temp, x1, ty1)
+      | Some(x2) => subst(TypVar(x2) |> temp, x1, ty1)
       | None => ty1
       };
     let+ ty_body = join(~resolve, ~fix, ctx, ty1', ty2);
@@ -275,7 +280,7 @@ let rec join = (~resolve=false, ~fix, ctx: Ctx.t, ty1: t, ty2: t): option(t) =>
     let+ ty = join'(ty1, ty2);
     List(ty) |> temp;
   | (List(_), _) => None
-  | (Ap(_), _) => failwith("Type join of ap")
+  | (ApTyp(_), _) => failwith("Type join of ap")
   };
 };
 
@@ -284,7 +289,7 @@ let rec join = (~resolve=false, ~fix, ctx: Ctx.t, ty1: t, ty2: t): option(t) =>
 let rec match_synswitch = (t1: t, t2: t) => {
   let (term1, rewrap1) = unwrap(t1);
   switch (term1, term_of(t2)) {
-  | (Parens(t1), _) => Parens(match_synswitch(t1, t2)) |> rewrap1
+  | (TypParens(t1), _) => TypParens(match_synswitch(t1, t2)) |> rewrap1
   | (Unknown(SynSwitch), _) => t2
   // These cases can't have a synswitch inside
   | (Unknown(_), _)
@@ -292,8 +297,8 @@ let rec match_synswitch = (t1: t, t2: t) => {
   | (Float, _)
   | (Bool, _)
   | (String, _)
-  | (Var(_), _)
-  | (Ap(_), _)
+  | (TypVar(_), _)
+  | (ApTyp(_), _)
   | (Rec(_), _)
   | (Forall(_), _) => t1
   // These might
@@ -327,8 +332,8 @@ let is_consistent = (ctx: Ctx.t, ty1: t, ty2: t): bool =>
 
 let rec weak_head_normalize = (ctx: Ctx.t, ty: t): t =>
   switch (term_of(ty)) {
-  | Parens(t) => weak_head_normalize(ctx, t)
-  | Var(x) =>
+  | TypParens(t) => weak_head_normalize(ctx, t)
+  | TypVar(x) =>
     switch (Ctx.lookup_alias(ctx, x)) {
     | Some(ty) => weak_head_normalize(ctx, ty)
     | None => ty
@@ -339,7 +344,7 @@ let rec weak_head_normalize = (ctx: Ctx.t, ty: t): t =>
 let rec normalize = (ctx: Ctx.t, ty: t): t => {
   let (term, rewrap) = unwrap(ty);
   switch (term) {
-  | Var(x) =>
+  | TypVar(x) =>
     switch (Ctx.lookup_alias(ctx, x)) {
     | Some(ty) => normalize(ctx, ty)
     | None => ty
@@ -349,9 +354,10 @@ let rec normalize = (ctx: Ctx.t, ty: t): t => {
   | Float
   | Bool
   | String => ty
-  | Parens(t) => Parens(normalize(ctx, t)) |> rewrap
+  | TypParens(t) => TypParens(normalize(ctx, t)) |> rewrap
   | List(t) => List(normalize(ctx, t)) |> rewrap
-  | Ap(t1, t2) => Ap(normalize(ctx, t1), normalize(ctx, t2)) |> rewrap
+  | ApTyp(t1, t2) =>
+    ApTyp(normalize(ctx, t1), normalize(ctx, t2)) |> rewrap
   | Arrow(t1, t2) =>
     Arrow(normalize(ctx, t1), normalize(ctx, t2)) |> rewrap
   | Prod(ts) => Prod(List.map(normalize(ctx), ts)) |> rewrap
@@ -369,7 +375,7 @@ let rec normalize = (ctx: Ctx.t, ty: t): t => {
 
 let rec matched_arrow_strict = (ctx, ty) =>
   switch (term_of(weak_head_normalize(ctx, ty))) {
-  | Parens(ty) => matched_arrow_strict(ctx, ty)
+  | TypParens(ty) => matched_arrow_strict(ctx, ty)
   | Arrow(ty_in, ty_out) => Some((ty_in, ty_out))
   | Unknown(SynSwitch) =>
     Some((Unknown(SynSwitch) |> temp, Unknown(SynSwitch) |> temp))
@@ -384,7 +390,7 @@ let matched_arrow = (ctx, ty) =>
 
 let rec matched_forall_strict = (ctx, ty) =>
   switch (term_of(weak_head_normalize(ctx, ty))) {
-  | Parens(ty) => matched_forall_strict(ctx, ty)
+  | TypParens(ty) => matched_forall_strict(ctx, ty)
   | Forall(t, ty) => Some((Some(t), ty))
   | Unknown(SynSwitch) => Some((None, Unknown(SynSwitch) |> temp))
   | _ => None // (None, Unknown(Internal) |> temp)
@@ -396,7 +402,7 @@ let matched_forall = (ctx, ty) =>
 
 let rec matched_prod_strict = (ctx, length, ty) =>
   switch (term_of(weak_head_normalize(ctx, ty))) {
-  | Parens(ty) => matched_prod_strict(ctx, length, ty)
+  | TypParens(ty) => matched_prod_strict(ctx, length, ty)
   | Prod(tys) when List.length(tys) == length => Some(tys)
   | Unknown(SynSwitch) =>
     Some(List.init(length, _ => Unknown(SynSwitch) |> temp))
@@ -409,7 +415,7 @@ let matched_prod = (ctx, length, ty) =>
 
 let rec matched_list_strict = (ctx, ty) =>
   switch (term_of(weak_head_normalize(ctx, ty))) {
-  | Parens(ty) => matched_list_strict(ctx, ty)
+  | TypParens(ty) => matched_list_strict(ctx, ty)
   | List(ty) => Some(ty)
   | Unknown(SynSwitch) => Some(Unknown(SynSwitch) |> temp)
   | _ => None
@@ -422,7 +428,7 @@ let matched_list = (ctx, ty) =>
 let rec matched_args = (ctx, default_arity, ty) => {
   let ty' = weak_head_normalize(ctx, ty);
   switch (term_of(ty')) {
-  | Parens(ty) => matched_args(ctx, default_arity, ty)
+  | TypParens(ty) => matched_args(ctx, default_arity, ty)
   | Prod([_, ..._] as tys) => tys
   | Unknown(_) => List.init(default_arity, _ => ty')
   | _ => [ty']
@@ -432,7 +438,7 @@ let rec matched_args = (ctx, default_arity, ty) => {
 let rec get_sum_constructors = (ctx: Ctx.t, ty: t): option(sum_map) => {
   let ty = weak_head_normalize(ctx, ty);
   switch (term_of(ty)) {
-  | Parens(ty) => get_sum_constructors(ctx, ty)
+  | TypParens(ty) => get_sum_constructors(ctx, ty)
   | Sum(sm) => Some(sm)
   | Rec(_) =>
     /* Note: We must unroll here to get right ctr types;
@@ -447,7 +453,7 @@ let rec get_sum_constructors = (ctx: Ctx.t, ty: t): option(sum_map) => {
        the below code will be incorrect! */
     let ty =
       switch (ty |> term_of) {
-      | Rec({term: Var(x), _}, ty_body) =>
+      | Rec({term: VarTPat(x), _}, ty_body) =>
         switch (Ctx.lookup_alias(ctx, x)) {
         | None => unroll(ty)
         | Some(_) => ty_body
@@ -464,7 +470,7 @@ let rec get_sum_constructors = (ctx: Ctx.t, ty: t): option(sum_map) => {
 
 let rec is_unknown = (ty: t): bool =>
   switch (ty |> term_of) {
-  | Parens(x) => is_unknown(x)
+  | TypParens(x) => is_unknown(x)
   | Unknown(_) => true
   | _ => false
   };
@@ -472,14 +478,14 @@ let rec is_unknown = (ty: t): bool =>
 /* Does the type require parentheses when on the left of an arrow for printing? */
 let rec needs_parens = (ty: t): bool =>
   switch (term_of(ty)) {
-  | Parens(ty) => needs_parens(ty)
-  | Ap(_)
+  | TypParens(ty) => needs_parens(ty)
+  | ApTyp(_)
   | Unknown(_)
   | Int
   | Float
   | String
   | Bool
-  | Var(_) => false
+  | TypVar(_) => false
   | Rec(_, _)
   | Forall(_, _) => true
   | List(_) => false /* is already wrapped in [] */
@@ -490,23 +496,23 @@ let rec needs_parens = (ty: t): bool =>
 
 let pretty_print_tvar = (tv: TPat.t): string =>
   switch (IdTagged.term_of(tv)) {
-  | Var(x) => x
-  | Invalid(_)
-  | EmptyHole
-  | MultiHole(_) => "?"
+  | VarTPat(x) => x
+  | InvalidTPat(_)
+  | EmptyHoleTPat
+  | MultiHoleTPat(_) => "?"
   };
 
 /* Essentially recreates haz3lweb/view/Type.re's view_ty but with string output */
 let rec pretty_print = (ty: t): string =>
   switch (term_of(ty)) {
-  | Parens(ty) => pretty_print(ty)
-  | Ap(_)
+  | TypParens(ty) => pretty_print(ty)
+  | ApTyp(_)
   | Unknown(_) => "?"
   | Int => "Int"
   | Float => "Float"
   | Bool => "Bool"
   | String => "String"
-  | Var(tvar) => tvar
+  | TypVar(tvar) => tvar
   | List(t) => "[" ++ pretty_print(t) ++ "]"
   | Arrow(t1, t2) => paren_pretty_print(t1) ++ " -> " ++ pretty_print(t2)
   | Sum(sm) =>
diff --git a/src/haz3lcore/statics/Ctx.re b/src/haz3lcore/statics/Ctx.re
index f213a18cb7..ecbe752d36 100644
--- a/src/haz3lcore/statics/Ctx.re
+++ b/src/haz3lcore/statics/Ctx.re
@@ -100,7 +100,8 @@ let lookup_alias = (ctx: t, name: string): option(TermBase.Typ.t) =>
   | Some(Abstract) => None
   | None =>
     Some(
-      (Unknown(Hole(Invalid(name))): TermBase.Typ.term) |> IdTagged.fresh,
+      (Unknown(HoleProvenance(InvalidTypeHole(name))): TermBase.Typ.term)
+      |> IdTagged.fresh,
     )
   };
 
@@ -114,10 +115,13 @@ let add_ctrs = (ctx: t, name: string, id: Id.t, ctrs: TermBase.Typ.sum_map): t =
           id,
           typ:
             switch (typ) {
-            | None => (Var(name): TermBase.typ_term) |> IdTagged.fresh
+            | None => (TypVar(name): TermBase.typ_term) |> IdTagged.fresh
             | Some(typ) =>
               (
-                Arrow(typ, (Var(name): TermBase.typ_term) |> IdTagged.fresh): TermBase.typ_term
+                Arrow(
+                  typ,
+                  (TypVar(name): TermBase.typ_term) |> IdTagged.fresh,
+                ): TermBase.typ_term
               )
               |> IdTagged.fresh
             },
diff --git a/src/haz3lcore/statics/Info.re b/src/haz3lcore/statics/Info.re
index 8aaaeaae3d..38e9180a00 100644
--- a/src/haz3lcore/statics/Info.re
+++ b/src/haz3lcore/statics/Info.re
@@ -339,7 +339,7 @@ let rec status_common =
     switch (
       Typ.join_fix(
         ctx,
-        Forall(Var("?") |> TPat.fresh, Unknown(Internal) |> Typ.temp)
+        Forall(VarTPat("?") |> TPat.fresh, Unknown(Internal) |> Typ.temp)
         |> Typ.temp,
         ty,
       )
@@ -454,9 +454,10 @@ let rec status_exp = (ctx: Ctx.t, mode: Mode.t, self: Self.exp): status_exp =>
    free, and whether a ctr name is a dupe. */
 let status_typ = (ctx: Ctx.t, expects: typ_expects, ty: Typ.t): status_typ =>
   switch (ty.term) {
-  | Unknown(Hole(Invalid(token))) => InHole(BadToken(token))
-  | Unknown(Hole(EmptyHole)) => NotInHole(Type(ty))
-  | Var(name) =>
+  | Unknown(HoleProvenance(InvalidTypeHole(token))) =>
+    InHole(BadToken(token))
+  | Unknown(HoleProvenance(EmptyTypeHole)) => NotInHole(Type(ty))
+  | TypVar(name) =>
     switch (expects) {
     | VariantExpected(Unique, sum_ty)
     | ConstructorExpected(Unique, sum_ty) =>
@@ -469,16 +470,16 @@ let status_typ = (ctx: Ctx.t, expects: typ_expects, ty: Typ.t): status_typ =>
       | false =>
         switch (Ctx.is_abstract(ctx, name)) {
         | false => InHole(FreeTypeVariable(name))
-        | true => NotInHole(Type(Var(name) |> Typ.temp))
+        | true => NotInHole(Type(TypVar(name) |> Typ.temp))
         }
       | true => NotInHole(TypeAlias(name, Typ.weak_head_normalize(ctx, ty)))
       }
     }
-  | Ap(t1, ty_in) =>
+  | ApTyp(t1, ty_in) =>
     switch (expects) {
     | VariantExpected(status_variant, ty_variant) =>
       switch (status_variant, t1.term) {
-      | (Unique, Var(name)) =>
+      | (Unique, TypVar(name)) =>
         NotInHole(Variant(name, Arrow(ty_in, ty_variant) |> Typ.temp))
       | _ =>
         NotInHole(VariantIncomplete(Arrow(ty_in, ty_variant) |> Typ.temp))
@@ -496,8 +497,8 @@ let status_typ = (ctx: Ctx.t, expects: typ_expects, ty: Typ.t): status_typ =>
 
 let status_tpat = (ctx: Ctx.t, utpat: TPat.t): status_tpat =>
   switch (utpat.term) {
-  | EmptyHole => NotInHole(Empty)
-  | Var(name) when Ctx.shadows_typ(ctx, name) =>
+  | EmptyHoleTPat => NotInHole(Empty)
+  | VarTPat(name) when Ctx.shadows_typ(ctx, name) =>
     let f = src => InHole(ShadowsType(name, src));
     if (Form.is_base_typ(name)) {
       f(BaseTyp);
@@ -506,9 +507,9 @@ let status_tpat = (ctx: Ctx.t, utpat: TPat.t): status_tpat =>
     } else {
       f(TyVar);
     };
-  | Var(name) => NotInHole(Var(name))
-  | Invalid(_) => InHole(NotAVar(NotCapitalized))
-  | MultiHole(_) => InHole(NotAVar(Other))
+  | VarTPat(name) => NotInHole(Var(name))
+  | InvalidTPat(_) => InHole(NotAVar(NotCapitalized))
+  | MultiHoleTPat(_) => InHole(NotAVar(Other))
   };
 
 /* Determines whether any term is in an error hole. */
@@ -593,7 +594,7 @@ let fixed_constraint_pat =
     )
     : Constraint.t =>
   switch (upat.term) {
-  | Cast(_) => constraint_
+  | CastPat(_) => constraint_
   | _ =>
     switch (fixed_typ_pat(ctx, mode, self) |> Typ.term_of) {
     | Unknown(_) => Constraint.Hole
@@ -677,10 +678,10 @@ let get_binding_site = (info: t): option(Id.t) => {
     let+ entry = Ctx.lookup_var(ctx, name);
     entry.id;
   | InfoExp({term: {term: Constructor(name, _), _}, ctx, _})
-  | InfoPat({term: {term: Constructor(name, _), _}, ctx, _}) =>
+  | InfoPat({term: {term: ConstructorPat(name, _), _}, ctx, _}) =>
     let+ entry = Ctx.lookup_ctr(ctx, name);
     entry.id;
-  | InfoTyp({term: {term: Var(name), _}, ctx, _}) =>
+  | InfoTyp({term: {term: TypVar(name), _}, ctx, _}) =>
     Ctx.lookup_tvar_id(ctx, name)
   | _ => None
   };
diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re
index d1edb9d16a..ba5049547e 100644
--- a/src/haz3lcore/statics/MakeTerm.re
+++ b/src/haz3lcore/statics/MakeTerm.re
@@ -126,16 +126,16 @@ let rm_and_log_projectors = (seg: Segment.t): Segment.t =>
 
 let parse_sum_term: UTyp.t => ConstructorMap.variant(UTyp.t) =
   fun
-  | {term: Var(ctr), ids, _} => Variant(ctr, ids, None)
-  | {term: Ap({term: Var(ctr), ids: ids_ctr, _}, u), ids: ids_ap, _} =>
+  | {term: TypVar(ctr), ids, _} => Variant(ctr, ids, None)
+  | {term: ApTyp({term: TypVar(ctr), ids: ids_ctr, _}, u), ids: ids_ap, _} =>
     Variant(ctr, ids_ctr @ ids_ap, Some(u))
   | t => BadEntry(t);
 
 let mk_bad = (ctr, ids, value) => {
-  let t: Typ.t = {ids, copied: false, term: Var(ctr)};
+  let t: Typ.t = {ids, copied: false, term: TypVar(ctr)};
   switch (value) {
   | None => t
-  | Some(u) => Ap(t, u) |> Typ.fresh
+  | Some(u) => ApTyp(t, u) |> Typ.fresh
   };
 };
 
@@ -182,12 +182,13 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = {
       | ([t], []) when Form.is_empty_tuple(t) => ret(Tuple([]))
       | ([t], []) when Form.is_wild(t) => ret(Deferral(OutsideAp))
       | ([t], []) when Form.is_empty_list(t) => ret(ListLit([]))
-      | ([t], []) when Form.is_bool(t) => ret(Bool(bool_of_string(t)))
+      | ([t], []) when Form.is_bool(t) => ret(BoolLit(bool_of_string(t)))
       | ([t], []) when Form.is_undefined(t) => ret(Undefined)
-      | ([t], []) when Form.is_int(t) => ret(Int(int_of_string(t)))
+      | ([t], []) when Form.is_int(t) => ret(IntLit(int_of_string(t)))
       | ([t], []) when Form.is_string(t) =>
-        ret(String(Form.strip_quotes(t)))
-      | ([t], []) when Form.is_float(t) => ret(Float(float_of_string(t)))
+        ret(StringLit(Form.strip_quotes(t)))
+      | ([t], []) when Form.is_float(t) =>
+        ret(FloatLit(float_of_string(t)))
       | ([t], []) when Form.is_var(t) => ret(Var(t))
       | ([t], []) when Form.is_ctr(t) =>
         ret(Constructor(t, Unknown(Internal) |> Typ.temp))
@@ -221,13 +222,13 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = {
         | (["typfun", "->"], [TPat(tpat)]) => TypFun(tpat, r, None)
         | (["let", "=", "in"], [Pat(pat), Exp(def)]) => Let(pat, def, r)
         | (["hide", "in"], [Exp(filter)]) =>
-          Filter(Filter({act: (Eval, One), pat: filter}), r)
+          Filter(FilterStepper({act: (Eval, One), pat: filter}), r)
         | (["eval", "in"], [Exp(filter)]) =>
-          Filter(Filter({act: (Eval, All), pat: filter}), r)
+          Filter(FilterStepper({act: (Eval, All), pat: filter}), r)
         | (["pause", "in"], [Exp(filter)]) =>
-          Filter(Filter({act: (Step, One), pat: filter}), r)
+          Filter(FilterStepper({act: (Step, One), pat: filter}), r)
         | (["debug", "in"], [Exp(filter)]) =>
-          Filter(Filter({act: (Step, All), pat: filter}), r)
+          Filter(FilterStepper({act: (Step, All), pat: filter}), r)
         | (["type", "=", "in"], [TPat(tpat), Typ(def)]) =>
           TyAlias(tpat, def, r)
         | (["if", "then", "else"], [Exp(cond), Exp(conseq)]) =>
@@ -335,23 +336,24 @@ and pat_term: unsorted => (UPat.term, list(Id.t)) = {
     | ([(_id, tile)], []) =>
       ret(
         switch (tile) {
-        | ([t], []) when Form.is_empty_tuple(t) => Tuple([])
-        | ([t], []) when Form.is_empty_list(t) => ListLit([])
-        | ([t], []) when Form.is_bool(t) => Bool(bool_of_string(t))
-        | ([t], []) when Form.is_float(t) => Float(float_of_string(t))
-        | ([t], []) when Form.is_int(t) => Int(int_of_string(t))
-        | ([t], []) when Form.is_string(t) => String(Form.strip_quotes(t))
-        | ([t], []) when Form.is_var(t) => Var(t)
+        | ([t], []) when Form.is_empty_tuple(t) => TuplePat([])
+        | ([t], []) when Form.is_empty_list(t) => ListLitPat([])
+        | ([t], []) when Form.is_bool(t) => BoolPat(bool_of_string(t))
+        | ([t], []) when Form.is_float(t) => FloatPat(float_of_string(t))
+        | ([t], []) when Form.is_int(t) => IntPat(int_of_string(t))
+        | ([t], []) when Form.is_string(t) =>
+          StringPat(Form.strip_quotes(t))
+        | ([t], []) when Form.is_var(t) => VarPat(t)
         | ([t], []) when Form.is_wild(t) => Wild
         | ([t], []) when Form.is_ctr(t) =>
-          Constructor(t, Unknown(Internal) |> Typ.fresh)
+          ConstructorPat(t, Unknown(Internal) |> Typ.fresh)
         | ([t], []) when t != " " && !Form.is_explicit_hole(t) =>
-          Invalid(t)
-        | (["(", ")"], [Pat(body)]) => Parens(body)
+          InvalidPat(t)
+        | (["(", ")"], [Pat(body)]) => ParensPat(body)
         | (["[", "]"], [Pat(body)]) =>
           switch (body) {
-          | {term: Tuple(ps), _} => ListLit(ps)
-          | term => ListLit([term])
+          | {term: TuplePat(ps), _} => ListLitPat(ps)
+          | term => ListLitPat([term])
           }
         | _ => hole(tm)
         },
@@ -363,7 +365,7 @@ and pat_term: unsorted => (UPat.term, list(Id.t)) = {
     | ([(_id, t)], []) =>
       ret(
         switch (t) {
-        | (["(", ")"], [Pat(arg)]) => Ap(l, arg)
+        | (["(", ")"], [Pat(arg)]) => ApPat(l, arg)
         | _ => hole(tm)
         },
       )
@@ -373,15 +375,15 @@ and pat_term: unsorted => (UPat.term, list(Id.t)) = {
   | Bin(Pat(p), tiles, Typ(ty)) as tm =>
     switch (tiles) {
     | ([(_id, ([":"], []))], []) =>
-      ret(Cast(p, ty, Unknown(Internal) |> Typ.fresh))
+      ret(CastPat(p, ty, Unknown(Internal) |> Typ.fresh))
     | _ => ret(hole(tm))
     }
   | Bin(Pat(l), tiles, Pat(r)) as tm =>
     switch (is_tuple_pat(tiles)) {
-    | Some(between_kids) => ret(Tuple([l] @ between_kids @ [r]))
+    | Some(between_kids) => ret(TuplePat([l] @ between_kids @ [r]))
     | None =>
       switch (tiles) {
-      | ([(_id, (["::"], []))], []) => ret(Cons(l, r))
+      | ([(_id, (["::"], []))], []) => ret(ConsPat(l, r))
       | _ => ret(hole(tm))
       }
     }
@@ -406,11 +408,11 @@ and typ_term: unsorted => (UTyp.term, list(Id.t)) = {
         | (["Int"], []) => Int
         | (["Float"], []) => Float
         | (["String"], []) => String
-        | ([t], []) when Form.is_typ_var(t) => Var(t)
-        | (["(", ")"], [Typ(body)]) => Parens(body)
+        | ([t], []) when Form.is_typ_var(t) => TypVar(t)
+        | (["(", ")"], [Typ(body)]) => TypParens(body)
         | (["[", "]"], [Typ(body)]) => List(body)
         | ([t], []) when t != " " && !Form.is_explicit_hole(t) =>
-          Unknown(Hole(Invalid(t)))
+          Unknown(HoleProvenance(InvalidTypeHole(t)))
         | _ => hole(tm)
         },
       )
@@ -418,7 +420,7 @@ and typ_term: unsorted => (UTyp.term, list(Id.t)) = {
     }
   | Post(Typ(t), tiles) as tm =>
     switch (tiles) {
-    | ([(_, (["(", ")"], [Typ(typ)]))], []) => ret(Ap(t, typ))
+    | ([(_, (["(", ")"], [Typ(typ)]))], []) => ret(ApTyp(t, typ))
     | _ => ret(hole(tm))
     }
   /* forall and rec have to be before sum so that they bind tighter.
@@ -476,9 +478,9 @@ and tpat_term: unsorted => TPat.term = {
     | ([(_id, tile)], []) =>
       ret(
         switch (tile) {
-        | ([t], []) when Form.is_typ_var(t) => Var(t)
+        | ([t], []) when Form.is_typ_var(t) => VarTPat(t)
         | ([t], []) when t != " " && !Form.is_explicit_hole(t) =>
-          Invalid(t)
+          InvalidTPat(t)
         | _ => hole(tm)
         },
       )
diff --git a/src/haz3lcore/statics/Mode.re b/src/haz3lcore/statics/Mode.re
index 2415399627..645f6f5556 100644
--- a/src/haz3lcore/statics/Mode.re
+++ b/src/haz3lcore/statics/Mode.re
@@ -35,7 +35,10 @@ let ty_of: t => Typ.t =
     Arrow(Unknown(SynSwitch) |> Typ.temp, Unknown(SynSwitch) |> Typ.temp)
     |> Typ.temp
   | SynTypFun =>
-    Forall(Var("syntypfun") |> TPat.fresh, Unknown(SynSwitch) |> Typ.temp)
+    Forall(
+      VarTPat("syntypfun") |> TPat.fresh,
+      Unknown(SynSwitch) |> Typ.temp,
+    )
     |> Typ.temp; /* TODO: naming the type variable? */
 
 let of_arrow = (ctx: Ctx.t, mode: t): (t, t) =>
@@ -55,7 +58,7 @@ let of_forall = (ctx: Ctx.t, name_opt: option(string), mode: t): t =>
     let (name_expected_opt, item) = Typ.matched_forall(ctx, ty);
     switch (name_opt, name_expected_opt) {
     | (Some(name), Some(name_expected)) =>
-      Ana(Typ.subst(Var(name) |> Typ.temp, name_expected, item))
+      Ana(Typ.subst(TypVar(name) |> Typ.temp, name_expected, item))
     | _ => Ana(item)
     };
   };
diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
index 443c94155b..e198f7bc04 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -120,7 +120,7 @@ let typ_exp_binop: Operators.op_bin => (Typ.t, Typ.t, Typ.t) =
 let typ_exp_unop: Operators.op_un => (Typ.t, Typ.t) =
   fun
   | Meta(Unquote) => (
-      Var("$Meta") |> Typ.temp,
+      TypVar("$Meta") |> Typ.temp,
       Unknown(Internal) |> Typ.temp,
     )
   | Bool(Not) => (Bool |> Typ.temp, Bool |> Typ.temp)
@@ -226,11 +226,12 @@ and uexp_to_info_map =
   | EmptyHole => atomic(Just(Unknown(Internal) |> Typ.temp))
   | Deferral(position) =>
     add'(~self=IsDeferral(position), ~co_ctx=CoCtx.empty, m)
-  | Undefined => atomic(Just(Unknown(Hole(EmptyHole)) |> Typ.temp))
-  | Bool(_) => atomic(Just(Bool |> Typ.temp))
-  | Int(_) => atomic(Just(Int |> Typ.temp))
-  | Float(_) => atomic(Just(Float |> Typ.temp))
-  | String(_) => atomic(Just(String |> Typ.temp))
+  | Undefined =>
+    atomic(Just(Unknown(HoleProvenance(EmptyTypeHole)) |> Typ.temp))
+  | BoolLit(_) => atomic(Just(Bool |> Typ.temp))
+  | IntLit(_) => atomic(Just(Int |> Typ.temp))
+  | FloatLit(_) => atomic(Just(Float |> Typ.temp))
+  | StringLit(_) => atomic(Just(String |> Typ.temp))
   | ListLit(es) =>
     let ids = List.map(UExp.rep_id, es);
     let modes = Mode.of_list_lit(ctx, List.length(es), mode);
@@ -281,7 +282,7 @@ and uexp_to_info_map =
         | _ => e.term
         },
     };
-    let ty_in = Var("$Meta") |> Typ.temp;
+    let ty_in = TypVar("$Meta") |> Typ.temp;
     let ty_out = Unknown(Internal) |> Typ.temp;
     let (e, m) = go(~mode=Ana(ty_in), e, m);
     add(~self=Just(ty_out), ~co_ctx=e.co_ctx, m);
@@ -311,7 +312,7 @@ and uexp_to_info_map =
   | Test(e) =>
     let (e, m) = go(~mode=Ana(Bool |> Typ.temp), e, m);
     add(~self=Just(Prod([]) |> Typ.temp), ~co_ctx=e.co_ctx, m);
-  | Filter(Filter({pat: cond, _}), body) =>
+  | Filter(FilterStepper({pat: cond, _}), body) =>
     let (cond, m) = go(~mode=Syn, cond, m, ~is_in_filter=true);
     let (body, m) = go(~mode, body, m);
     add(
@@ -373,7 +374,7 @@ and uexp_to_info_map =
     let self =
       is_exhaustive ? unwrapped_self : InexhaustiveMatch(unwrapped_self);
     add'(~self, ~co_ctx=CoCtx.mk(ctx, p.ctx, e.co_ctx), m);
-  | TypFun({term: Var(name), _} as utpat, body, _)
+  | TypFun({term: VarTPat(name), _} as utpat, body, _)
       when !Ctx.shadows_typ(ctx, name) =>
     let mode_body = Mode.of_forall(ctx, Some(name), mode);
     let m = utpat_to_info_map(~ctx, ~ancestors, utpat, m) |> snd;
@@ -600,7 +601,7 @@ and uexp_to_info_map =
   | TyAlias(typat, utyp, body) =>
     let m = utpat_to_info_map(~ctx, ~ancestors, typat, m) |> snd;
     switch (typat.term) {
-    | Var(name) when !Ctx.shadows_typ(ctx, name) =>
+    | VarTPat(name) when !Ctx.shadows_typ(ctx, name) =>
       /* Currently we disallow all type shadowing */
       /* NOTE(andrew): Currently, UTyp.to_typ returns Unknown(TypeHole)
          for any type variable reference not in its ctx. So any free variables
@@ -615,7 +616,8 @@ and uexp_to_info_map =
              use a different name than the alias for the recursive parameter */
           //let ty_rec = Typ.Rec("α", Typ.subst(Var("α"), name, ty_pre));
           let ty_rec =
-            Rec((Var(name): TPat.term) |> IdTagged.fresh, utyp) |> Typ.temp;
+            Rec((VarTPat(name): TPat.term) |> IdTagged.fresh, utyp)
+            |> Typ.temp;
           let ctx_def =
             Ctx.extend_alias(ctx, name, TPat.rep_id(typat), ty_rec);
           (ty_rec, ctx_def, ctx_def);
@@ -650,10 +652,10 @@ and uexp_to_info_map =
       let ty_escape = Typ.subst(ty_def, typat, ty_body);
       let m = utyp_to_info_map(~ctx=ctx_def, ~ancestors, utyp, m) |> snd;
       add(~self=Just(ty_escape), ~co_ctx, m);
-    | Var(_)
-    | Invalid(_)
-    | EmptyHole
-    | MultiHole(_) =>
+    | VarTPat(_)
+    | InvalidTPat(_)
+    | EmptyHoleTPat
+    | MultiHoleTPat(_) =>
       let ({co_ctx, ty: ty_body, _}: Info.exp, m) =
         go'(~ctx, ~mode, body, m);
       let m = utyp_to_info_map(~ctx, ~ancestors, utyp, m) |> snd;
@@ -713,25 +715,25 @@ and upat_to_info_map =
     );
   let hole = self => atomic(self, Constraint.Hole);
   switch (term) {
-  | MultiHole(tms) =>
+  | MultiHolePat(tms) =>
     let (_, m) = multi(~ctx, ~ancestors, m, tms);
     add(~self=IsMulti, ~ctx, ~constraint_=Constraint.Hole, m);
-  | Invalid(token) => hole(BadToken(token))
-  | EmptyHole => hole(Just(unknown))
-  | Int(int) => atomic(Just(Int |> Typ.temp), Constraint.Int(int))
-  | Float(float) =>
+  | InvalidPat(token) => hole(BadToken(token))
+  | EmptyHolePat => hole(Just(unknown))
+  | IntPat(int) => atomic(Just(Int |> Typ.temp), Constraint.Int(int))
+  | FloatPat(float) =>
     atomic(Just(Float |> Typ.temp), Constraint.Float(float))
-  | Tuple([]) => atomic(Just(Prod([]) |> Typ.temp), Constraint.Truth)
-  | Bool(bool) =>
+  | TuplePat([]) => atomic(Just(Prod([]) |> Typ.temp), Constraint.Truth)
+  | BoolPat(bool) =>
     atomic(
       Just(Bool |> Typ.temp),
       bool
         ? Constraint.InjL(Constraint.Truth)
         : Constraint.InjR(Constraint.Truth),
     )
-  | String(string) =>
+  | StringPat(string) =>
     atomic(Just(String |> Typ.temp), Constraint.String(string))
-  | ListLit(ps) =>
+  | ListLitPat(ps) =>
     let ids = List.map(UPat.rep_id, ps);
     let modes = Mode.of_list_lit(ctx, List.length(ps), mode);
     let (ctx, tys, cons, m) = ctx_fold(ctx, m, ps, modes);
@@ -747,7 +749,7 @@ and upat_to_info_map =
       ~constraint_=cons_fold_list(cons),
       m,
     );
-  | Cons(hd, tl) =>
+  | ConsPat(hd, tl) =>
     let (hd, m) = go(~ctx, ~mode=Mode.of_cons_hd(ctx, mode), hd, m);
     let (tl, m) =
       go(~ctx=hd.ctx, ~mode=Mode.of_cons_tl(ctx, mode, hd.ty), tl, m);
@@ -759,7 +761,7 @@ and upat_to_info_map =
       m,
     );
   | Wild => atomic(Just(unknown), Constraint.Truth)
-  | Var(name) =>
+  | VarPat(name) =>
     /* NOTE: The self type assigned to pattern variables (Unknown)
        may be SynSwitch, but SynSwitch is never added to the context;
        Unknown(Internal) is used in this case */
@@ -776,7 +778,7 @@ and upat_to_info_map =
       ~constraint_=Constraint.Truth,
       m,
     );
-  | Tuple(ps) =>
+  | TuplePat(ps) =>
     let modes = Mode.of_prod(ctx, mode, List.length(ps));
     let (ctx, tys, cons, m) = ctx_fold(ctx, m, ps, modes);
     let rec cons_fold_tuple = cs =>
@@ -791,13 +793,13 @@ and upat_to_info_map =
       ~constraint_=cons_fold_tuple(cons),
       m,
     );
-  | Parens(p) =>
+  | ParensPat(p) =>
     let (p, m) = go(~ctx, ~mode, p, m);
     add(~self=Just(p.ty), ~ctx=p.ctx, ~constraint_=p.constraint_, m);
-  | Constructor(ctr, _) =>
+  | ConstructorPat(ctr, _) =>
     let self = Self.of_ctr(ctx, ctr);
     atomic(self, Constraint.of_ctr(ctx, mode, ctr, self));
-  | Ap(fn, arg) =>
+  | ApPat(fn, arg) =>
     let ctr = UPat.ctr_name(fn);
     let fn_mode = Mode.of_ap(ctx, mode, ctr);
     let (fn, m) = go(~ctx, ~mode=fn_mode, fn, m);
@@ -810,7 +812,7 @@ and upat_to_info_map =
         Constraint.of_ap(ctx, mode, ctr, arg.constraint_, Some(ty_out)),
       m,
     );
-  | Cast(p, ann, _) =>
+  | CastPat(p, ann, _) =>
     let (ann, m) = utyp_to_info_map(~ctx, ~ancestors, ann, m);
     let (p, m) = go(~ctx, ~mode=Ana(ann.term), p, m);
     add(~self=Just(ann.term), ~ctx=p.ctx, ~constraint_=p.constraint_, m);
@@ -833,7 +835,7 @@ and utyp_to_info_map =
   let go' = utyp_to_info_map(~ctx, ~ancestors);
   let go = go'(~expects=TypeExpected);
   switch (term) {
-  | Unknown(Hole(MultiHole(tms))) =>
+  | Unknown(HoleProvenance(MultiTypeHole(tms))) =>
     let (_, m) = multi(~ctx, ~ancestors, m, tms);
     add(m);
   | Unknown(_)
@@ -841,11 +843,11 @@ and utyp_to_info_map =
   | Float
   | Bool
   | String => add(m)
-  | Var(_) =>
+  | TypVar(_) =>
     /* Names are resolved in Info.status_typ */
     add(m)
   | List(t)
-  | Parens(t) => add(go(t, m) |> snd)
+  | TypParens(t) => add(go(t, m) |> snd)
   | Arrow(t1, t2) =>
     let m = go(t1, m) |> snd;
     let m = go(t2, m) |> snd;
@@ -853,7 +855,7 @@ and utyp_to_info_map =
   | Prod(ts) =>
     let m = map_m(go, ts, m) |> snd;
     add(m);
-  | Ap(t1, t2) =>
+  | ApTyp(t1, t2) =>
     let t1_mode: Info.typ_expects =
       switch (expects) {
       | VariantExpected(m, sum_ty) =>
@@ -875,7 +877,7 @@ and utyp_to_info_map =
         variants,
       );
     add(m);
-  | Forall({term: Var(name), _} as utpat, tbody) =>
+  | Forall({term: VarTPat(name), _} as utpat, tbody) =>
     let body_ctx =
       Ctx.extend_tvar(ctx, {name, id: TPat.rep_id(utpat), kind: Abstract});
     let m =
@@ -895,7 +897,7 @@ and utyp_to_info_map =
       |> snd;
     let m = utpat_to_info_map(~ctx, ~ancestors, utpat, m) |> snd;
     add(m); // TODO: check with andrew
-  | Rec({term: Var(name), _} as utpat, tbody) =>
+  | Rec({term: VarTPat(name), _} as utpat, tbody) =>
     let body_ctx =
       Ctx.extend_tvar(ctx, {name, id: TPat.rep_id(utpat), kind: Abstract});
     let m =
@@ -926,12 +928,12 @@ and utpat_to_info_map =
   };
   let ancestors = [TPat.rep_id(utpat)] @ ancestors;
   switch (term) {
-  | MultiHole(tms) =>
+  | MultiHoleTPat(tms) =>
     let (_, m) = multi(~ctx, ~ancestors, m, tms);
     add(m);
-  | Invalid(_)
-  | EmptyHole
-  | Var(_) => add(m)
+  | InvalidTPat(_)
+  | EmptyHoleTPat
+  | VarTPat(_) => add(m)
   };
 }
 and variant_to_info_map =
@@ -954,7 +956,7 @@ and variant_to_info_map =
           List.mem(ctr, ctrs) ? Duplicate : Unique,
           ty_sum,
         ),
-        {term: Var(ctr), ids, copied: false},
+        {term: TypVar(ctr), ids, copied: false},
         m,
       )
       |> snd;
diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re
index 92eef8161e..18584ced4e 100644
--- a/src/haz3lcore/statics/Term.re
+++ b/src/haz3lcore/statics/Term.re
@@ -33,28 +33,28 @@ module Pat = {
 
   let hole = (tms: list(TermBase.Any.t)): TermBase.Pat.term =>
     switch (tms) {
-    | [] => EmptyHole
-    | [_, ..._] => MultiHole(tms)
+    | [] => EmptyHolePat
+    | [_, ..._] => MultiHolePat(tms)
     };
 
   let cls_of_term: term => cls =
     fun
-    | Invalid(_) => Invalid
-    | EmptyHole => EmptyHole
-    | MultiHole(_) => MultiHole
+    | InvalidPat(_) => Invalid
+    | EmptyHolePat => EmptyHole
+    | MultiHolePat(_) => MultiHole
     | Wild => Wild
-    | Int(_) => Int
-    | Float(_) => Float
-    | Bool(_) => Bool
-    | String(_) => String
-    | ListLit(_) => ListLit
-    | Constructor(_) => Constructor
-    | Cons(_) => Cons
-    | Var(_) => Var
-    | Tuple(_) => Tuple
-    | Parens(_) => Parens
-    | Ap(_) => Ap
-    | Cast(_) => Cast;
+    | IntPat(_) => Int
+    | FloatPat(_) => Float
+    | BoolPat(_) => Bool
+    | StringPat(_) => String
+    | ListLitPat(_) => ListLit
+    | ConstructorPat(_) => Constructor
+    | ConsPat(_) => Cons
+    | VarPat(_) => Var
+    | TuplePat(_) => Tuple
+    | ParensPat(_) => Parens
+    | ApPat(_) => Ap
+    | CastPat(_) => Cast;
 
   let show_cls: cls => string =
     fun
@@ -77,44 +77,44 @@ module Pat = {
 
   let rec is_var = (pat: t) => {
     switch (pat.term) {
-    | Parens(pat)
-    | Cast(pat, _, _) => is_var(pat)
-    | Var(_) => true
-    | Invalid(_)
-    | EmptyHole
-    | MultiHole(_)
+    | ParensPat(pat)
+    | CastPat(pat, _, _) => is_var(pat)
+    | VarPat(_) => true
+    | InvalidPat(_)
+    | EmptyHolePat
+    | MultiHolePat(_)
     | Wild
-    | Int(_)
-    | Float(_)
-    | Bool(_)
-    | String(_)
-    | ListLit(_)
-    | Cons(_, _)
-    | Tuple(_)
-    | Constructor(_)
-    | Ap(_) => false
+    | IntPat(_)
+    | FloatPat(_)
+    | BoolPat(_)
+    | StringPat(_)
+    | ListLitPat(_)
+    | ConsPat(_, _)
+    | TuplePat(_)
+    | ConstructorPat(_)
+    | ApPat(_) => false
     };
   };
 
   let rec is_fun_var = (pat: t) => {
     switch (pat.term) {
-    | Parens(pat) => is_fun_var(pat)
-    | Cast(pat, typ, _) =>
+    | ParensPat(pat) => is_fun_var(pat)
+    | CastPat(pat, typ, _) =>
       is_var(pat) && (UTyp.is_arrow(typ) || Typ.is_forall(typ))
-    | Invalid(_)
-    | EmptyHole
-    | MultiHole(_)
+    | InvalidPat(_)
+    | EmptyHolePat
+    | MultiHolePat(_)
     | Wild
-    | Int(_)
-    | Float(_)
-    | Bool(_)
-    | String(_)
-    | ListLit(_)
-    | Cons(_, _)
-    | Var(_)
-    | Tuple(_)
-    | Constructor(_)
-    | Ap(_) => false
+    | IntPat(_)
+    | FloatPat(_)
+    | BoolPat(_)
+    | StringPat(_)
+    | ListLitPat(_)
+    | ConsPat(_, _)
+    | VarPat(_)
+    | TuplePat(_)
+    | ConstructorPat(_)
+    | ApPat(_) => false
     };
   };
 
@@ -122,22 +122,22 @@ module Pat = {
     is_fun_var(pat)
     || (
       switch (pat.term) {
-      | Parens(pat) => is_tuple_of_arrows(pat)
-      | Tuple(pats) => pats |> List.for_all(is_fun_var)
-      | Invalid(_)
-      | EmptyHole
-      | MultiHole(_)
+      | ParensPat(pat) => is_tuple_of_arrows(pat)
+      | TuplePat(pats) => pats |> List.for_all(is_fun_var)
+      | InvalidPat(_)
+      | EmptyHolePat
+      | MultiHolePat(_)
       | Wild
-      | Int(_)
-      | Float(_)
-      | Bool(_)
-      | String(_)
-      | ListLit(_)
-      | Cons(_, _)
-      | Var(_)
-      | Cast(_)
-      | Constructor(_)
-      | Ap(_) => false
+      | IntPat(_)
+      | FloatPat(_)
+      | BoolPat(_)
+      | StringPat(_)
+      | ListLitPat(_)
+      | ConsPat(_, _)
+      | VarPat(_)
+      | CastPat(_)
+      | ConstructorPat(_)
+      | ApPat(_) => false
       }
     );
 
@@ -145,69 +145,69 @@ module Pat = {
     is_var(pat)
     || (
       switch (pat.term) {
-      | Parens(pat)
-      | Cast(pat, _, _) => is_tuple_of_vars(pat)
-      | Tuple(pats) => pats |> List.for_all(is_var)
-      | Invalid(_)
-      | EmptyHole
-      | MultiHole(_)
+      | ParensPat(pat)
+      | CastPat(pat, _, _) => is_tuple_of_vars(pat)
+      | TuplePat(pats) => pats |> List.for_all(is_var)
+      | InvalidPat(_)
+      | EmptyHolePat
+      | MultiHolePat(_)
       | Wild
-      | Int(_)
-      | Float(_)
-      | Bool(_)
-      | String(_)
-      | ListLit(_)
-      | Cons(_, _)
-      | Var(_)
-      | Constructor(_)
-      | Ap(_) => false
+      | IntPat(_)
+      | FloatPat(_)
+      | BoolPat(_)
+      | StringPat(_)
+      | ListLitPat(_)
+      | ConsPat(_, _)
+      | VarPat(_)
+      | ConstructorPat(_)
+      | ApPat(_) => false
       }
     );
 
   let rec get_var = (pat: t) => {
     switch (pat.term) {
-    | Parens(pat) => get_var(pat)
-    | Var(x) => Some(x)
-    | Cast(x, _, _) => get_var(x)
-    | Invalid(_)
-    | EmptyHole
-    | MultiHole(_)
+    | ParensPat(pat) => get_var(pat)
+    | VarPat(x) => Some(x)
+    | CastPat(x, _, _) => get_var(x)
+    | InvalidPat(_)
+    | EmptyHolePat
+    | MultiHolePat(_)
     | Wild
-    | Int(_)
-    | Float(_)
-    | Bool(_)
-    | String(_)
-    | ListLit(_)
-    | Cons(_, _)
-    | Tuple(_)
-    | Constructor(_)
-    | Ap(_) => None
+    | IntPat(_)
+    | FloatPat(_)
+    | BoolPat(_)
+    | StringPat(_)
+    | ListLitPat(_)
+    | ConsPat(_, _)
+    | TuplePat(_)
+    | ConstructorPat(_)
+    | ApPat(_) => None
     };
   };
 
   let rec get_fun_var = (pat: t) => {
     switch (pat.term) {
-    | Parens(pat) => get_fun_var(pat)
-    | Cast(pat, t1, _) =>
+    | ParensPat(pat) => get_fun_var(pat)
+    | CastPat(pat, t1, _) =>
       if (Typ.is_arrow(t1) || UTyp.is_forall(t1)) {
         get_var(pat) |> Option.map(var => var);
       } else {
         None;
       }
-    | Invalid(_)
-    | EmptyHole
-    | MultiHole(_)
+    | InvalidPat(_)
+    | EmptyHolePat
+    | MultiHolePat(_)
     | Wild
-    | Int(_)
-    | Float(_)
-    | Bool(_)
-    | String(_)
-    | ListLit(_)
-    | Cons(_, _)
-    | Var(_)
-    | Tuple(_)
-    | Constructor(_)
-    | Ap(_) => None
+    | IntPat(_)
+    | FloatPat(_)
+    | BoolPat(_)
+    | StringPat(_)
+    | ListLitPat(_)
+    | ConsPat(_, _)
+    | VarPat(_)
+    | TuplePat(_)
+    | ConstructorPat(_)
+    | ApPat(_) => None
     };
   };
 
@@ -216,28 +216,28 @@ module Pat = {
     | Some(x) => Some([x])
     | None =>
       switch (pat.term) {
-      | Parens(pat)
-      | Cast(pat, _, _) => get_bindings(pat)
-      | Tuple(pats) =>
+      | ParensPat(pat)
+      | CastPat(pat, _, _) => get_bindings(pat)
+      | TuplePat(pats) =>
         let vars = pats |> List.map(get_var);
         if (List.exists(Option.is_none, vars)) {
           None;
         } else {
           Some(List.map(Option.get, vars));
         };
-      | Invalid(_)
-      | EmptyHole
-      | MultiHole(_)
+      | InvalidPat(_)
+      | EmptyHolePat
+      | MultiHolePat(_)
       | Wild
-      | Int(_)
-      | Float(_)
-      | Bool(_)
-      | String(_)
-      | ListLit(_)
-      | Cons(_, _)
-      | Var(_)
-      | Constructor(_)
-      | Ap(_) => None
+      | IntPat(_)
+      | FloatPat(_)
+      | BoolPat(_)
+      | StringPat(_)
+      | ListLitPat(_)
+      | ConsPat(_, _)
+      | VarPat(_)
+      | ConstructorPat(_)
+      | ApPat(_) => None
       }
     };
 
@@ -246,29 +246,29 @@ module Pat = {
       Some(1);
     } else {
       switch (pat.term) {
-      | Parens(pat)
-      | Cast(pat, _, _) => get_num_of_vars(pat)
-      | Tuple(pats) =>
+      | ParensPat(pat)
+      | CastPat(pat, _, _) => get_num_of_vars(pat)
+      | TuplePat(pats) =>
         is_tuple_of_vars(pat) ? Some(List.length(pats)) : None
-      | Invalid(_)
-      | EmptyHole
-      | MultiHole(_)
+      | InvalidPat(_)
+      | EmptyHolePat
+      | MultiHolePat(_)
       | Wild
-      | Int(_)
-      | Float(_)
-      | Bool(_)
-      | String(_)
-      | ListLit(_)
-      | Cons(_, _)
-      | Var(_)
-      | Constructor(_)
-      | Ap(_) => None
+      | IntPat(_)
+      | FloatPat(_)
+      | BoolPat(_)
+      | StringPat(_)
+      | ListLitPat(_)
+      | ConsPat(_, _)
+      | VarPat(_)
+      | ConstructorPat(_)
+      | ApPat(_) => None
       };
     };
 
   let ctr_name = (p: t): option(Constructor.t) =>
     switch (p.term) {
-    | Constructor(name, _) => Some(name)
+    | ConstructorPat(name, _) => Some(name)
     | _ => None
     };
 };
@@ -337,10 +337,10 @@ module Exp = {
     | FailedCast(_) => FailedCast
     | Deferral(_) => Deferral
     | Undefined => Undefined
-    | Bool(_) => Bool
-    | Int(_) => Int
-    | Float(_) => Float
-    | String(_) => String
+    | BoolLit(_) => Bool
+    | IntLit(_) => Int
+    | FloatLit(_) => Float
+    | StringLit(_) => String
     | ListLit(_) => ListLit
     | Constructor(_) => Constructor
     | Fun(_) => Fun
@@ -425,10 +425,10 @@ module Exp = {
     | FailedCast(_)
     | Deferral(_)
     | Undefined
-    | Bool(_)
-    | Int(_)
-    | Float(_)
-    | String(_)
+    | BoolLit(_)
+    | IntLit(_)
+    | FloatLit(_)
+    | StringLit(_)
     | ListLit(_)
     | Tuple(_)
     | Var(_)
@@ -466,10 +466,10 @@ module Exp = {
       | FailedCast(_)
       | Deferral(_)
       | Undefined
-      | Bool(_)
-      | Int(_)
-      | Float(_)
-      | String(_)
+      | BoolLit(_)
+      | IntLit(_)
+      | FloatLit(_)
+      | StringLit(_)
       | ListLit(_)
       | Fun(_)
       | TypFun(_)
@@ -526,10 +526,10 @@ module Exp = {
       | Cast(_)
       | Deferral(_)
       | Undefined
-      | Bool(_)
-      | Int(_)
-      | Float(_)
-      | String(_)
+      | BoolLit(_)
+      | IntLit(_)
+      | FloatLit(_)
+      | StringLit(_)
       | ListLit(_)
       | Fun(_)
       | TypFun(_)
diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re
index 02bd8400d4..0c888d8ef7 100644
--- a/src/haz3lcore/statics/TermBase.re
+++ b/src/haz3lcore/statics/TermBase.re
@@ -63,10 +63,10 @@ and exp_term =
   | FailedCast(exp_t, typ_t, typ_t)
   | Deferral(deferral_position_t)
   | Undefined
-  | Bool(bool)
-  | Int(int)
-  | Float(float)
-  | String(string)
+  | BoolLit(bool)
+  | IntLit(int)
+  | FloatLit(float)
+  | StringLit(string)
   | ListLit(list(exp_t))
   | Constructor(string, typ_t) // Typ.t field is only meaningful in dynamic expressions
   | Fun(
@@ -102,22 +102,22 @@ and exp_term =
   | Cast(exp_t, typ_t, typ_t)
 and exp_t = IdTagged.t(exp_term)
 and pat_term =
-  | Invalid(string)
-  | EmptyHole
-  | MultiHole(list(any_t))
+  | InvalidPat(string)
+  | EmptyHolePat
+  | MultiHolePat(list(any_t))
   | Wild
-  | Int(int)
-  | Float(float)
-  | Bool(bool)
-  | String(string)
-  | ListLit(list(pat_t))
-  | Constructor(string, typ_t) // Typ.t field is only meaningful in dynamic patterns
-  | Cons(pat_t, pat_t)
-  | Var(Var.t)
-  | Tuple(list(pat_t))
-  | Parens(pat_t)
-  | Ap(pat_t, pat_t)
-  | Cast(pat_t, typ_t, typ_t)
+  | IntPat(int)
+  | FloatPat(float)
+  | BoolPat(bool)
+  | StringPat(string)
+  | ListLitPat(list(pat_t))
+  | ConstructorPat(string, typ_t) // Typ.t field is only meaningful in dynamic patterns
+  | ConsPat(pat_t, pat_t)
+  | VarPat(Var.t)
+  | TuplePat(list(pat_t))
+  | ParensPat(pat_t)
+  | ApPat(pat_t, pat_t)
+  | CastPat(pat_t, typ_t, typ_t)
 and pat_t = IdTagged.t(pat_term)
 and typ_term =
   | Unknown(type_provenance)
@@ -125,39 +125,39 @@ and typ_term =
   | Float
   | Bool
   | String
-  | Var(string)
+  | TypVar(string)
   | List(typ_t)
   | Arrow(typ_t, typ_t)
   | Sum(ConstructorMap.t(typ_t))
   | Prod(list(typ_t))
-  | Parens(typ_t)
-  | Ap(typ_t, typ_t)
+  | TypParens(typ_t)
+  | ApTyp(typ_t, typ_t)
   | Rec(tpat_t, typ_t)
   | Forall(tpat_t, typ_t)
 and typ_t = IdTagged.t(typ_term)
 and tpat_term =
-  | Invalid(string)
-  | EmptyHole
-  | MultiHole(list(any_t))
-  | Var(string)
+  | InvalidTPat(string)
+  | EmptyHoleTPat
+  | MultiHoleTPat(list(any_t))
+  | VarTPat(string)
 and tpat_t = IdTagged.t(tpat_term)
 and rul_term =
-  | Invalid(string)
+  | InvalidRule(string)
   | Hole(list(any_t))
   | Rules(exp_t, list((pat_t, exp_t)))
 and rul_t = IdTagged.t(rul_term)
 and environment_t = VarBstMap.Ordered.t_(exp_t)
 and closure_environment_t = (Id.t, environment_t)
 and stepper_filter_kind_t =
-  | Filter(filter)
+  | FilterStepper(filter)
   | Residue(int, FilterAction.t)
 and type_hole =
-  | Invalid(string)
-  | EmptyHole
-  | MultiHole(list(any_t))
+  | InvalidTypeHole(string)
+  | EmptyTypeHole
+  | MultiTypeHole(list(any_t))
 and type_provenance =
   | SynSwitch
-  | Hole(type_hole)
+  | HoleProvenance(type_hole)
   | Internal
 and filter = {
   pat: exp_t,
@@ -296,11 +296,11 @@ and Exp: {
         switch (term) {
         | EmptyHole
         | Invalid(_)
-        | Bool(_)
-        | Int(_)
-        | Float(_)
+        | BoolLit(_)
+        | IntLit(_)
+        | FloatLit(_)
         | Constructor(_)
-        | String(_)
+        | StringLit(_)
         | Deferral(_)
         | Var(_)
         | Undefined => term
@@ -365,10 +365,10 @@ and Exp: {
       && Typ.fast_equal(t1, t3)
       && Typ.fast_equal(t2, t4)
     | (Deferral(d1), Deferral(d2)) => d1 == d2
-    | (Bool(b1), Bool(b2)) => b1 == b2
-    | (Int(i1), Int(i2)) => i1 == i2
-    | (Float(f1), Float(f2)) => f1 == f2
-    | (String(s1), String(s2)) => s1 == s2
+    | (BoolLit(b1), BoolLit(b2)) => b1 == b2
+    | (IntLit(i1), IntLit(i2)) => i1 == i2
+    | (FloatLit(f1), FloatLit(f2)) => f1 == f2
+    | (StringLit(s1), StringLit(s2)) => s1 == s2
     | (ListLit(xs), ListLit(ys)) =>
       List.length(xs) == List.length(ys) && List.equal(fast_equal, xs, ys)
     | (Constructor(c1, ty1), Constructor(c2, ty2)) =>
@@ -431,10 +431,10 @@ and Exp: {
     | (Invalid(_), _)
     | (FailedCast(_), _)
     | (Deferral(_), _)
-    | (Bool(_), _)
-    | (Int(_), _)
-    | (Float(_), _)
-    | (String(_), _)
+    | (BoolLit(_), _)
+    | (IntLit(_), _)
+    | (FloatLit(_), _)
+    | (StringLit(_), _)
     | (ListLit(_), _)
     | (Constructor(_), _)
     | (Fun(_), _)
@@ -509,23 +509,24 @@ and Pat: {
       ...exp,
       term:
         switch (term) {
-        | EmptyHole
-        | Invalid(_)
+        | EmptyHolePat
+        | InvalidPat(_)
         | Wild
-        | Bool(_)
-        | Int(_)
-        | Float(_)
-        | Constructor(_)
-        | String(_)
-        | Var(_) => term
-        | MultiHole(things) => MultiHole(List.map(any_map_term, things))
-        | ListLit(ts) => ListLit(List.map(pat_map_term, ts))
-        | Ap(e1, e2) => Ap(pat_map_term(e1), pat_map_term(e2))
-        | Cons(e1, e2) => Cons(pat_map_term(e1), pat_map_term(e2))
-        | Tuple(xs) => Tuple(List.map(pat_map_term, xs))
-        | Parens(e) => Parens(pat_map_term(e))
-        | Cast(e, t1, t2) =>
-          Cast(pat_map_term(e), typ_map_term(t1), typ_map_term(t2))
+        | BoolPat(_)
+        | IntPat(_)
+        | FloatPat(_)
+        | ConstructorPat(_)
+        | StringPat(_)
+        | VarPat(_) => term
+        | MultiHolePat(things) =>
+          MultiHolePat(List.map(any_map_term, things))
+        | ListLitPat(ts) => ListLitPat(List.map(pat_map_term, ts))
+        | ApPat(e1, e2) => ApPat(pat_map_term(e1), pat_map_term(e2))
+        | ConsPat(e1, e2) => ConsPat(pat_map_term(e1), pat_map_term(e2))
+        | TuplePat(xs) => TuplePat(List.map(pat_map_term, xs))
+        | ParensPat(e) => ParensPat(pat_map_term(e))
+        | CastPat(e, t1, t2) =>
+          CastPat(pat_map_term(e), typ_map_term(t1), typ_map_term(t2))
         },
     };
     x |> f_pat(rec_call);
@@ -533,45 +534,46 @@ and Pat: {
 
   let rec fast_equal = (p1: t, p2: t) =>
     switch (p1 |> IdTagged.term_of, p2 |> IdTagged.term_of) {
-    | (Parens(x), _) => fast_equal(x, p2)
-    | (_, Parens(x)) => fast_equal(p1, x)
-    | (EmptyHole, EmptyHole) => true
-    | (MultiHole(xs), MultiHole(ys)) =>
+    | (ParensPat(x), _) => fast_equal(x, p2)
+    | (_, ParensPat(x)) => fast_equal(p1, x)
+    | (EmptyHolePat, EmptyHolePat) => true
+    | (MultiHolePat(xs), MultiHolePat(ys)) =>
       List.length(xs) == List.length(ys)
       && List.equal(Any.fast_equal, xs, ys)
-    | (Invalid(s1), Invalid(s2)) => s1 == s2
+    | (InvalidPat(s1), InvalidPat(s2)) => s1 == s2
     | (Wild, Wild) => true
-    | (Bool(b1), Bool(b2)) => b1 == b2
-    | (Int(i1), Int(i2)) => i1 == i2
-    | (Float(f1), Float(f2)) => f1 == f2
-    | (String(s1), String(s2)) => s1 == s2
-    | (Constructor(c1, t1), Constructor(c2, t2)) =>
+    | (BoolPat(b1), BoolPat(b2)) => b1 == b2
+    | (IntPat(i1), IntPat(i2)) => i1 == i2
+    | (FloatPat(f1), FloatPat(f2)) => f1 == f2
+    | (StringPat(s1), StringPat(s2)) => s1 == s2
+    | (ConstructorPat(c1, t1), ConstructorPat(c2, t2)) =>
       c1 == c2 && Typ.fast_equal(t1, t2)
-    | (Var(v1), Var(v2)) => v1 == v2
-    | (ListLit(xs), ListLit(ys)) =>
+    | (VarPat(v1), VarPat(v2)) => v1 == v2
+    | (ListLitPat(xs), ListLitPat(ys)) =>
       List.length(xs) == List.length(ys) && List.equal(fast_equal, xs, ys)
-    | (Cons(x1, y1), Cons(x2, y2)) =>
+    | (ConsPat(x1, y1), ConsPat(x2, y2)) =>
       fast_equal(x1, x2) && fast_equal(y1, y2)
-    | (Tuple(xs), Tuple(ys)) =>
+    | (TuplePat(xs), TuplePat(ys)) =>
       List.length(xs) == List.length(ys) && List.equal(fast_equal, xs, ys)
-    | (Ap(x1, y1), Ap(x2, y2)) => fast_equal(x1, x2) && fast_equal(y1, y2)
-    | (Cast(x1, t1, t2), Cast(x2, u1, u2)) =>
+    | (ApPat(x1, y1), ApPat(x2, y2)) =>
+      fast_equal(x1, x2) && fast_equal(y1, y2)
+    | (CastPat(x1, t1, t2), CastPat(x2, u1, u2)) =>
       fast_equal(x1, x2) && Typ.fast_equal(t1, u1) && Typ.fast_equal(t2, u2)
-    | (EmptyHole, _)
-    | (MultiHole(_), _)
-    | (Invalid(_), _)
+    | (EmptyHolePat, _)
+    | (MultiHolePat(_), _)
+    | (InvalidPat(_), _)
     | (Wild, _)
-    | (Bool(_), _)
-    | (Int(_), _)
-    | (Float(_), _)
-    | (String(_), _)
-    | (ListLit(_), _)
-    | (Constructor(_), _)
-    | (Cons(_), _)
-    | (Var(_), _)
-    | (Tuple(_), _)
-    | (Ap(_), _)
-    | (Cast(_), _) => false
+    | (BoolPat(_), _)
+    | (IntPat(_), _)
+    | (FloatPat(_), _)
+    | (StringPat(_), _)
+    | (ListLitPat(_), _)
+    | (ConstructorPat(_), _)
+    | (ConsPat(_), _)
+    | (VarPat(_), _)
+    | (TuplePat(_), _)
+    | (ApPat(_), _)
+    | (CastPat(_), _) => false
     };
 }
 and Typ: {
@@ -625,21 +627,23 @@ and Typ: {
       ...exp,
       term:
         switch (term) {
-        | Unknown(Hole(EmptyHole))
-        | Unknown(Hole(Invalid(_)))
+        | Unknown(HoleProvenance(EmptyTypeHole))
+        | Unknown(HoleProvenance(InvalidTypeHole(_)))
         | Unknown(SynSwitch)
         | Unknown(Internal)
         | Bool
         | Int
         | Float
         | String
-        | Var(_) => term
+        | TypVar(_) => term
         | List(t) => List(typ_map_term(t))
-        | Unknown(Hole(MultiHole(things))) =>
-          Unknown(Hole(MultiHole(List.map(any_map_term, things))))
-        | Ap(e1, e2) => Ap(typ_map_term(e1), typ_map_term(e2))
+        | Unknown(HoleProvenance(MultiTypeHole(things))) =>
+          Unknown(
+            HoleProvenance(MultiTypeHole(List.map(any_map_term, things))),
+          )
+        | ApTyp(e1, e2) => ApTyp(typ_map_term(e1), typ_map_term(e2))
         | Prod(xs) => Prod(List.map(typ_map_term, xs))
-        | Parens(e) => Parens(typ_map_term(e))
+        | TypParens(e) => TypParens(typ_map_term(e))
         | Arrow(t1, t2) => Arrow(typ_map_term(t1), typ_map_term(t2))
         | Sum(variants) =>
           Sum(
@@ -682,9 +686,9 @@ and Typ: {
         Rec(tp2, ty) |> rewrap
       | Rec(tp2, ty) => Rec(tp2, subst(s, x, ty)) |> rewrap
       | List(ty) => List(subst(s, x, ty)) |> rewrap
-      | Var(y) => str == y ? s : Var(y) |> rewrap
-      | Parens(ty) => Parens(subst(s, x, ty)) |> rewrap
-      | Ap(t1, t2) => Ap(subst(s, x, t1), subst(s, x, t2)) |> rewrap
+      | TypVar(y) => str == y ? s : TypVar(y) |> rewrap
+      | TypParens(ty) => TypParens(subst(s, x, ty)) |> rewrap
+      | ApTyp(t1, t2) => ApTyp(subst(s, x, t1), subst(s, x, t2)) |> rewrap
       };
     | None => ty
     };
@@ -695,13 +699,13 @@ and Typ: {
 
   let rec eq_internal = (n: int, t1: t, t2: t) => {
     switch (IdTagged.term_of(t1), IdTagged.term_of(t2)) {
-    | (Parens(t1), _) => eq_internal(n, t1, t2)
-    | (_, Parens(t2)) => eq_internal(n, t1, t2)
+    | (TypParens(t1), _) => eq_internal(n, t1, t2)
+    | (_, TypParens(t2)) => eq_internal(n, t1, t2)
     | (Rec(x1, t1), Rec(x2, t2))
     | (Forall(x1, t1), Forall(x2, t2)) =>
       let alpha_subst =
         subst({
-          term: Var("=" ++ string_of_int(n)),
+          term: TypVar("=" ++ string_of_int(n)),
           copied: false,
           ids: [Id.invalid],
         });
@@ -716,9 +720,9 @@ and Typ: {
     | (Bool, _) => false
     | (String, String) => true
     | (String, _) => false
-    | (Ap(t1, t2), Ap(t1', t2')) =>
+    | (ApTyp(t1, t2), ApTyp(t1', t2')) =>
       eq_internal(n, t1, t1') && eq_internal(n, t2, t2')
-    | (Ap(_), _) => false
+    | (ApTyp(_), _) => false
     | (Unknown(_), Unknown(_)) => true
     | (Unknown(_), _) => false
     | (Arrow(t1, t2), Arrow(t1', t2')) =>
@@ -732,8 +736,8 @@ and Typ: {
       /* Does not normalize the types. */
       ConstructorMap.equal(eq_internal(n), sm1, sm2)
     | (Sum(_), _) => false
-    | (Var(n1), Var(n2)) => n1 == n2
-    | (Var(_), _) => false
+    | (TypVar(n1), TypVar(n2)) => n1 == n2
+    | (TypVar(_), _) => false
     };
   };
 
@@ -782,10 +786,11 @@ and TPat: {
       ...exp,
       term:
         switch (term) {
-        | EmptyHole
-        | Invalid(_)
-        | Var(_) => term
-        | MultiHole(things) => MultiHole(List.map(any_map_term, things))
+        | EmptyHoleTPat
+        | InvalidTPat(_)
+        | VarTPat(_) => term
+        | MultiHoleTPat(things) =>
+          MultiHoleTPat(List.map(any_map_term, things))
         },
     };
     x |> f_tpat(rec_call);
@@ -793,22 +798,22 @@ and TPat: {
 
   let tyvar_of_utpat = ({term, _}: t) =>
     switch (term) {
-    | Var(x) => Some(x)
+    | VarTPat(x) => Some(x)
     | _ => None
     };
 
   let fast_equal = (tp1: t, tp2: t) =>
     switch (tp1 |> IdTagged.term_of, tp2 |> IdTagged.term_of) {
-    | (EmptyHole, EmptyHole) => true
-    | (Invalid(s1), Invalid(s2)) => s1 == s2
-    | (MultiHole(xs), MultiHole(ys)) =>
+    | (EmptyHoleTPat, EmptyHoleTPat) => true
+    | (InvalidTPat(s1), InvalidTPat(s2)) => s1 == s2
+    | (MultiHoleTPat(xs), MultiHoleTPat(ys)) =>
       List.length(xs) == List.length(ys)
       && List.equal(Any.fast_equal, xs, ys)
-    | (Var(x), Var(y)) => x == y
-    | (EmptyHole, _)
-    | (Invalid(_), _)
-    | (MultiHole(_), _)
-    | (Var(_), _) => false
+    | (VarTPat(x), VarTPat(y)) => x == y
+    | (EmptyHoleTPat, _)
+    | (InvalidTPat(_), _)
+    | (MultiHoleTPat(_), _)
+    | (VarTPat(_), _) => false
     };
 }
 and Rul: {
@@ -856,7 +861,7 @@ and Rul: {
       ...exp,
       term:
         switch (term) {
-        | Invalid(_) => term
+        | InvalidRule(_) => term
         | Hole(things) => Hole(List.map(any_map_term, things))
         | Rules(e, rls) =>
           Rules(
@@ -873,7 +878,7 @@ and Rul: {
 
   let fast_equal = (r1: t, r2: t) =>
     switch (r1 |> IdTagged.term_of, r2 |> IdTagged.term_of) {
-    | (Invalid(s1), Invalid(s2)) => s1 == s2
+    | (InvalidRule(s1), InvalidRule(s2)) => s1 == s2
     | (Hole(xs), Hole(ys)) =>
       List.length(xs) == List.length(ys)
       && List.equal(Any.fast_equal, xs, ys)
@@ -886,7 +891,7 @@ and Rul: {
            rls1,
            rls2,
          )
-    | (Invalid(_), _)
+    | (InvalidRule(_), _)
     | (Hole(_), _)
     | (Rules(_), _) => false
     };
@@ -1041,7 +1046,7 @@ and StepperFilterKind: {
 
   let map = (mapper, filter: t): t => {
     switch (filter) {
-    | Filter({act, pat}) => Filter({act, pat: mapper(pat)})
+    | FilterStepper({act, pat}) => FilterStepper({act, pat: mapper(pat)})
     | Residue(idx, act) => Residue(idx, act)
     };
   };
@@ -1059,7 +1064,8 @@ and StepperFilterKind: {
       Exp.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any);
     (
       fun
-      | Filter({pat: e, act}) => Filter({pat: exp_map_term(e), act})
+      | FilterStepper({pat: e, act}) =>
+        FilterStepper({pat: exp_map_term(e), act})
       | Residue(i, a) => Residue(i, a):
         t => t
     );
@@ -1067,10 +1073,10 @@ and StepperFilterKind: {
 
   let fast_equal = (f1: t, f2: t) =>
     switch (f1, f2) {
-    | (Filter({pat: e1, act: a1}), Filter({pat: e2, act: a2})) =>
+    | (FilterStepper({pat: e1, act: a1}), FilterStepper({pat: e2, act: a2})) =>
       Exp.fast_equal(e1, e2) && a1 == a2
     | (Residue(i1, a1), Residue(i2, a2)) => i1 == i2 && a1 == a2
-    | (Filter(_), _)
+    | (FilterStepper(_), _)
     | (Residue(_), _) => false
     };
 };
diff --git a/src/haz3lcore/zipper/EditorUtil.re b/src/haz3lcore/zipper/EditorUtil.re
index 23265f8a2a..6617e036ed 100644
--- a/src/haz3lcore/zipper/EditorUtil.re
+++ b/src/haz3lcore/zipper/EditorUtil.re
@@ -7,10 +7,10 @@ let rec append_exp = (e1: Exp.t, e2: Exp.t): Exp.t => {
   | FailedCast(_)
   | Undefined
   | Deferral(_)
-  | Bool(_)
-  | Int(_)
-  | Float(_)
-  | String(_)
+  | BoolLit(_)
+  | IntLit(_)
+  | FloatLit(_)
+  | StringLit(_)
   | ListLit(_)
   | Constructor(_)
   | Closure(_)
diff --git a/src/haz3lschool/Exercise.re b/src/haz3lschool/Exercise.re
index 01050d5e7b..04d742d3a3 100644
--- a/src/haz3lschool/Exercise.re
+++ b/src/haz3lschool/Exercise.re
@@ -571,7 +571,7 @@ module F = (ExerciseEnv: ExerciseEnv) => {
   let wrap_filter = (act: FilterAction.action, term: UExp.t): UExp.t => {
     term:
       Filter(
-        Filter({
+        FilterStepper({
           act: FilterAction.(act, One),
           pat: {
             term: Constructor("$e", Unknown(Internal) |> Typ.temp),
diff --git a/src/haz3lschool/SyntaxTest.re b/src/haz3lschool/SyntaxTest.re
index 23dff72251..a1722fbb6d 100644
--- a/src/haz3lschool/SyntaxTest.re
+++ b/src/haz3lschool/SyntaxTest.re
@@ -16,23 +16,24 @@ type syntax_result = {
 
 let rec find_var_upat = (name: string, upat: Pat.t): bool => {
   switch (upat.term) {
-  | Var(x) => x == name
-  | EmptyHole
+  | VarPat(x) => x == name
+  | EmptyHolePat
   | Wild
-  | Invalid(_)
-  | MultiHole(_)
-  | Int(_)
-  | Float(_)
-  | Bool(_)
-  | String(_)
-  | Constructor(_) => false
-  | Cons(up1, up2) => find_var_upat(name, up1) || find_var_upat(name, up2)
-  | ListLit(l)
-  | Tuple(l) =>
+  | InvalidPat(_)
+  | MultiHolePat(_)
+  | IntPat(_)
+  | FloatPat(_)
+  | BoolPat(_)
+  | StringPat(_)
+  | ConstructorPat(_) => false
+  | ConsPat(up1, up2) =>
+    find_var_upat(name, up1) || find_var_upat(name, up2)
+  | ListLitPat(l)
+  | TuplePat(l) =>
     List.fold_left((acc, up) => {acc || find_var_upat(name, up)}, false, l)
-  | Parens(up) => find_var_upat(name, up)
-  | Ap(up1, up2) => find_var_upat(name, up1) || find_var_upat(name, up2)
-  | Cast(up, _, _) => find_var_upat(name, up)
+  | ParensPat(up) => find_var_upat(name, up)
+  | ApPat(up1, up2) => find_var_upat(name, up1) || find_var_upat(name, up2)
+  | CastPat(up, _, _) => find_var_upat(name, up)
   };
 };
 
@@ -47,12 +48,12 @@ let rec find_in_let =
         (name: string, upat: UPat.t, def: UExp.t, l: list(UExp.t))
         : list(UExp.t) => {
   switch (upat.term, def.term) {
-  | (Parens(up), Parens(ue)) => find_in_let(name, up, ue, l)
-  | (Parens(up), _) => find_in_let(name, up, def, l)
+  | (ParensPat(up), Parens(ue)) => find_in_let(name, up, ue, l)
+  | (ParensPat(up), _) => find_in_let(name, up, def, l)
   | (_, Parens(ue)) => find_in_let(name, upat, ue, l)
-  | (Cast(up, _, _), _) => find_in_let(name, up, def, l)
-  | (Var(x), Fun(_)) => x == name ? [def, ...l] : l
-  | (Tuple(pl), Tuple(ul)) =>
+  | (CastPat(up, _, _), _) => find_in_let(name, up, def, l)
+  | (VarPat(x), Fun(_)) => x == name ? [def, ...l] : l
+  | (TuplePat(pl), Tuple(ul)) =>
     if (List.length(pl) != List.length(ul)) {
       l;
     } else {
@@ -63,15 +64,17 @@ let rec find_in_let =
         ul,
       );
     }
-  | (Var(_), _)
-  | (Tuple(_), _)
+  | (VarPat(_), _)
+  | (TuplePat(_), _)
   | (
-      EmptyHole | Wild | Invalid(_) | MultiHole(_) | Int(_) | Float(_) | Bool(_) |
-      String(_) |
-      ListLit(_) |
-      Constructor(_) |
-      Cons(_, _) |
-      Ap(_, _),
+      EmptyHolePat | Wild | InvalidPat(_) | MultiHolePat(_) | IntPat(_) |
+      FloatPat(_) |
+      BoolPat(_) |
+      StringPat(_) |
+      ListLitPat(_) |
+      ConstructorPat(_) |
+      ConsPat(_, _) |
+      ApPat(_, _),
       _,
     ) => l
   };
@@ -122,10 +125,10 @@ let rec find_fn =
   | MultiHole(_)
   | DynamicErrorHole(_)
   | FailedCast(_)
-  | Bool(_)
-  | Int(_)
-  | Float(_)
-  | String(_)
+  | BoolLit(_)
+  | IntLit(_)
+  | FloatLit(_)
+  | StringLit(_)
   | Constructor(_)
   | Undefined
   | BuiltinFun(_)
@@ -138,29 +141,29 @@ let rec find_fn =
  */
 let rec var_mention_upat = (name: string, upat: Pat.t): bool => {
   switch (upat.term) {
-  | Var(x) => x == name
-  | EmptyHole
+  | VarPat(x) => x == name
+  | EmptyHolePat
   | Wild
-  | Invalid(_)
-  | MultiHole(_)
-  | Int(_)
-  | Float(_)
-  | Bool(_)
-  | String(_)
-  | Constructor(_) => false
-  | Cons(up1, up2) =>
+  | InvalidPat(_)
+  | MultiHolePat(_)
+  | IntPat(_)
+  | FloatPat(_)
+  | BoolPat(_)
+  | StringPat(_)
+  | ConstructorPat(_) => false
+  | ConsPat(up1, up2) =>
     var_mention_upat(name, up1) || var_mention_upat(name, up2)
-  | ListLit(l)
-  | Tuple(l) =>
+  | ListLitPat(l)
+  | TuplePat(l) =>
     List.fold_left(
       (acc, up) => {acc || var_mention_upat(name, up)},
       false,
       l,
     )
-  | Parens(up) => var_mention_upat(name, up)
-  | Ap(up1, up2) =>
+  | ParensPat(up) => var_mention_upat(name, up)
+  | ApPat(up1, up2) =>
     var_mention_upat(name, up1) || var_mention_upat(name, up2)
-  | Cast(up, _, _) => var_mention_upat(name, up)
+  | CastPat(up, _, _) => var_mention_upat(name, up)
   };
 };
 
@@ -173,10 +176,10 @@ let rec var_mention = (name: string, uexp: Exp.t): bool => {
   | EmptyHole
   | Invalid(_)
   | MultiHole(_)
-  | Bool(_)
-  | Int(_)
-  | Float(_)
-  | String(_)
+  | BoolLit(_)
+  | IntLit(_)
+  | FloatLit(_)
+  | StringLit(_)
   | Constructor(_)
   | Undefined
   | Deferral(_) => false
@@ -234,10 +237,10 @@ let rec var_applied = (name: string, uexp: Exp.t): bool => {
   | EmptyHole
   | Invalid(_)
   | MultiHole(_)
-  | Bool(_)
-  | Int(_)
-  | Float(_)
-  | String(_)
+  | BoolLit(_)
+  | IntLit(_)
+  | FloatLit(_)
+  | StringLit(_)
   | Constructor(_)
   | Undefined
   | Deferral(_) => false
@@ -325,10 +328,10 @@ let rec tail_check = (name: string, uexp: Exp.t): bool => {
   | MultiHole(_)
   | DynamicErrorHole(_)
   | FailedCast(_)
-  | Bool(_)
-  | Int(_)
-  | Float(_)
-  | String(_)
+  | BoolLit(_)
+  | IntLit(_)
+  | FloatLit(_)
+  | StringLit(_)
   | Constructor(_)
   | Undefined
   | Var(_)
diff --git a/src/haz3lweb/view/Cell.re b/src/haz3lweb/view/Cell.re
index ba06d2a29e..55ded0cdfc 100644
--- a/src/haz3lweb/view/Cell.re
+++ b/src/haz3lweb/view/Cell.re
@@ -409,7 +409,7 @@ let locked =
           statics.info_map,
           statics.term,
         )
-      : Bool(true) |> DHExp.fresh;
+      : BoolLit(true) |> DHExp.fresh;
   let elab: Elaborator.Elaboration.t = {d: elab};
   let result: ModelResult.t =
     settings.core.dynamics
diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re
index 879b355999..1b38b6fdf3 100644
--- a/src/haz3lweb/view/CursorInspector.re
+++ b/src/haz3lweb/view/CursorInspector.re
@@ -142,12 +142,12 @@ let typ_ok_view = (cls: Cls.t, ok: Info.ok_typ) =>
   | Type(_) when cls == Typ(EmptyHole) => [text("Fillable by any type")]
   | Type(ty) => [Type.view(ty), text("is a type")]
   | TypeAlias(name, ty_lookup) => [
-      Type.view(Var(name) |> Typ.fresh),
+      Type.view(TypVar(name) |> Typ.fresh),
       text("is an alias for"),
       Type.view(ty_lookup),
     ]
   | Variant(name, sum_ty) => [
-      Type.view(Var(name) |> Typ.fresh),
+      Type.view(TypVar(name) |> Typ.fresh),
       text("is a sum type constuctor of type"),
       Type.view(sum_ty),
     ]
@@ -160,7 +160,7 @@ let typ_ok_view = (cls: Cls.t, ok: Info.ok_typ) =>
 let typ_err_view = (ok: Info.error_typ) =>
   switch (ok) {
   | FreeTypeVariable(name) => [
-      Type.view(Var(name) |> Typ.fresh),
+      Type.view(TypVar(name) |> Typ.fresh),
       text("not found"),
     ]
   | BadToken(token) => [
@@ -171,7 +171,7 @@ let typ_err_view = (ok: Info.error_typ) =>
   | WantConstructorFoundType(_) => [text("Expected a constructor")]
   | WantTypeFoundAp => [text("Must be part of a sum type")]
   | DuplicateConstructor(name) => [
-      Type.view(Var(name) |> Typ.fresh),
+      Type.view(TypVar(name) |> Typ.fresh),
       text("already used in this sum"),
     ]
   };
@@ -242,17 +242,17 @@ let tpat_view = (_: Cls.t, status: Info.status_tpat) =>
   | InHole(ShadowsType(name, BaseTyp)) =>
     div_err([
       text("Can't shadow base type"),
-      Type.view(Var(name) |> Typ.fresh),
+      Type.view(TypVar(name) |> Typ.fresh),
     ])
   | InHole(ShadowsType(name, TyAlias)) =>
     div_err([
       text("Can't shadow existing alias"),
-      Type.view(Var(name) |> Typ.fresh),
+      Type.view(TypVar(name) |> Typ.fresh),
     ])
   | InHole(ShadowsType(name, TyVar)) =>
     div_err([
       text("Can't shadow existing type variable"),
-      Type.view(Var(name) |> Typ.fresh),
+      Type.view(TypVar(name) |> Typ.fresh),
     ])
   };
 
diff --git a/src/haz3lweb/view/ExplainThis.re b/src/haz3lweb/view/ExplainThis.re
index a74a5187d8..7bea3e5041 100644
--- a/src/haz3lweb/view/ExplainThis.re
+++ b/src/haz3lweb/view/ExplainThis.re
@@ -394,15 +394,15 @@ let example_view =
 
 let rec bypass_parens_and_annot_pat = (pat: Pat.t) => {
   switch (pat.term) {
-  | Parens(p)
-  | Cast(p, _, _) => bypass_parens_and_annot_pat(p)
+  | ParensPat(p)
+  | CastPat(p, _, _) => bypass_parens_and_annot_pat(p)
   | _ => pat
   };
 };
 
 let rec bypass_parens_pat = (pat: Pat.t) => {
   switch (pat.term) {
-  | Parens(p) => bypass_parens_pat(p)
+  | ParensPat(p) => bypass_parens_pat(p)
   | _ => pat
   };
 };
@@ -416,7 +416,7 @@ let rec bypass_parens_exp = (exp: Exp.t) => {
 
 let rec bypass_parens_typ = (typ: Typ.t) => {
   switch (typ.term) {
-  | Parens(t) => bypass_parens_typ(t)
+  | TypParens(t) => bypass_parens_typ(t)
   | _ => typ
   };
 };
@@ -560,10 +560,10 @@ let get_doc =
         );
       | Undefined => get_message(UndefinedExp.undefined_exps)
       | Deferral(_) => get_message(TerminalExp.deferral_exps)
-      | Bool(b) => get_message(TerminalExp.bool_exps(b))
-      | Int(i) => get_message(TerminalExp.int_exps(i))
-      | Float(f) => get_message(TerminalExp.float_exps(f))
-      | String(s) => get_message(TerminalExp.string_exps(s))
+      | BoolLit(b) => get_message(TerminalExp.bool_exps(b))
+      | IntLit(i) => get_message(TerminalExp.int_exps(i))
+      | FloatLit(f) => get_message(TerminalExp.float_exps(f))
+      | StringLit(s) => get_message(TerminalExp.string_exps(s))
       | ListLit(terms) =>
         get_message(
           ~format=
@@ -623,7 +623,7 @@ let get_doc =
         let pat_id = List.nth(pat.ids, 0);
         let body_id = List.nth(body.ids, 0);
         switch (pat.term) {
-        | EmptyHole =>
+        | EmptyHolePat =>
           if (FunctionExp.function_empty_hole_exp.id
               == get_specificity_level(FunctionExp.functions_empty_hole)) {
             get_message(
@@ -647,7 +647,7 @@ let get_doc =
           } else {
             basic(FunctionExp.functions_empty_hole);
           }
-        | MultiHole(_) =>
+        | MultiHolePat(_) =>
           if (FunctionExp.function_multi_hole_exp.id
               == get_specificity_level(FunctionExp.functions_multi_hole)) {
             get_message(
@@ -689,7 +689,7 @@ let get_doc =
           } else {
             basic(FunctionExp.functions_wild);
           }
-        | Int(i) =>
+        | IntPat(i) =>
           if (FunctionExp.function_intlit_exp.id
               == get_specificity_level(FunctionExp.functions_int)) {
             get_message(
@@ -714,7 +714,7 @@ let get_doc =
           } else {
             basic(FunctionExp.functions_int);
           }
-        | Float(f) =>
+        | FloatPat(f) =>
           if (FunctionExp.function_floatlit_exp.id
               == get_specificity_level(FunctionExp.functions_float)) {
             get_message(
@@ -739,7 +739,7 @@ let get_doc =
           } else {
             basic(FunctionExp.functions_float);
           }
-        | Bool(b) =>
+        | BoolPat(b) =>
           if (FunctionExp.function_boollit_exp.id
               == get_specificity_level(FunctionExp.functions_bool)) {
             get_message(
@@ -764,7 +764,7 @@ let get_doc =
           } else {
             basic(FunctionExp.functions_bool);
           }
-        | String(s) =>
+        | StringPat(s) =>
           if (FunctionExp.function_strlit_exp.id
               == get_specificity_level(FunctionExp.functions_str)) {
             get_message(
@@ -789,7 +789,7 @@ let get_doc =
           } else {
             basic(FunctionExp.functions_str);
           }
-        | Tuple([]) =>
+        | TuplePat([]) =>
           if (FunctionExp.function_triv_exp.id
               == get_specificity_level(FunctionExp.functions_triv)) {
             get_message(
@@ -812,7 +812,7 @@ let get_doc =
           } else {
             basic(FunctionExp.functions_triv);
           }
-        | ListLit(elements) =>
+        | ListLitPat(elements) =>
           if (List.length(elements) == 0) {
             if (FunctionExp.function_listnil_exp.id
                 == get_specificity_level(FunctionExp.functions_listnil)) {
@@ -861,7 +861,7 @@ let get_doc =
           } else {
             basic(FunctionExp.functions_listlit);
           }
-        | Cons(hd, tl) =>
+        | ConsPat(hd, tl) =>
           if (FunctionExp.function_cons_exp.id
               == get_specificity_level(FunctionExp.functions_cons)) {
             let hd_id = List.nth(hd.ids, 0);
@@ -888,7 +888,7 @@ let get_doc =
           } else {
             basic(FunctionExp.functions_cons);
           }
-        | Var(var) =>
+        | VarPat(var) =>
           if (FunctionExp.function_var_exp.id
               == get_specificity_level(FunctionExp.functions_var)) {
             get_message(
@@ -909,7 +909,7 @@ let get_doc =
           } else {
             basic(FunctionExp.functions_var);
           }
-        | Tuple(elements) =>
+        | TuplePat(elements) =>
           let pat_id = List.nth(pat.ids, 0);
           let body_id = List.nth(body.ids, 0);
           let basic_tuple = group_id => {
@@ -1004,7 +1004,7 @@ let get_doc =
               basic(FunctionExp.functions_tuple);
             }
           };
-        | Ap(con, arg) =>
+        | ApPat(con, arg) =>
           if (FunctionExp.function_ap_exp.id
               == get_specificity_level(FunctionExp.functions_ap)) {
             let con_id = List.nth(con.ids, 0);
@@ -1031,7 +1031,7 @@ let get_doc =
           } else {
             basic(FunctionExp.functions_ap);
           }
-        | Constructor(v, _) =>
+        | ConstructorPat(v, _) =>
           if (FunctionExp.function_ctr_exp.id
               == get_specificity_level(FunctionExp.functions_ctr)) {
             let pat_id = List.nth(pat.ids, 0);
@@ -1055,9 +1055,9 @@ let get_doc =
           } else {
             basic(FunctionExp.functions_ctr);
           }
-        | Invalid(_) => default // Shouldn't get hit
-        | Parens(_) => default // Shouldn't get hit?
-        | Cast(_) => default // Shouldn't get hit?
+        | InvalidPat(_) => default // Shouldn't get hit
+        | ParensPat(_) => default // Shouldn't get hit?
+        | CastPat(_) => default // Shouldn't get hit?
         };
       | Tuple(terms) =>
         let basic = group_id =>
@@ -1147,7 +1147,7 @@ let get_doc =
           );
         };
         switch (pat.term) {
-        | EmptyHole =>
+        | EmptyHolePat =>
           if (LetExp.let_empty_hole_exp.id
               == get_specificity_level(LetExp.lets_emptyhole)) {
             get_message(
@@ -1168,7 +1168,7 @@ let get_doc =
           } else {
             basic(LetExp.lets_emptyhole);
           }
-        | MultiHole(_) =>
+        | MultiHolePat(_) =>
           if (LetExp.let_multi_hole_exp.id
               == get_specificity_level(LetExp.lets_mutlihole)) {
             get_message(
@@ -1209,7 +1209,7 @@ let get_doc =
           } else {
             basic(LetExp.lets_wild);
           }
-        | Int(i) =>
+        | IntPat(i) =>
           if (LetExp.let_int_exp.id == get_specificity_level(LetExp.lets_int)) {
             get_message(
               ~colorings=
@@ -1234,7 +1234,7 @@ let get_doc =
               LetExp.lets_int,
             );
           }
-        | Float(f) =>
+        | FloatPat(f) =>
           if (LetExp.let_float_exp.id
               == get_specificity_level(LetExp.lets_float)) {
             // TODO Make sure everywhere printing the float literal print it prettier
@@ -1261,7 +1261,7 @@ let get_doc =
               LetExp.lets_float,
             );
           }
-        | Bool(b) =>
+        | BoolPat(b) =>
           if (LetExp.let_bool_exp.id
               == get_specificity_level(LetExp.lets_bool)) {
             get_message(
@@ -1287,7 +1287,7 @@ let get_doc =
               LetExp.lets_bool,
             );
           }
-        | String(s) =>
+        | StringPat(s) =>
           if (LetExp.let_str_exp.id == get_specificity_level(LetExp.lets_str)) {
             get_message(
               ~colorings=
@@ -1312,7 +1312,7 @@ let get_doc =
               LetExp.lets_str,
             );
           }
-        | Tuple([]) =>
+        | TuplePat([]) =>
           if (LetExp.let_triv_exp.id
               == get_specificity_level(LetExp.lets_triv)) {
             get_message(
@@ -1337,7 +1337,7 @@ let get_doc =
               LetExp.lets_triv,
             );
           }
-        | ListLit(elements) =>
+        | ListLitPat(elements) =>
           if (List.length(elements) == 0) {
             if (LetExp.let_listnil_exp.id
                 == get_specificity_level(LetExp.lets_listnil)) {
@@ -1384,7 +1384,7 @@ let get_doc =
           } else {
             basic(LetExp.lets_listlit);
           }
-        | Cons(hd, tl) =>
+        | ConsPat(hd, tl) =>
           if (LetExp.let_cons_exp.id
               == get_specificity_level(LetExp.lets_cons)) {
             let hd_id = List.nth(hd.ids, 0);
@@ -1407,7 +1407,7 @@ let get_doc =
           } else {
             basic(LetExp.lets_cons);
           }
-        | Var(var) =>
+        | VarPat(var) =>
           if (LetExp.let_var_exp.id == get_specificity_level(LetExp.lets_var)) {
             get_message(
               ~colorings=
@@ -1428,7 +1428,7 @@ let get_doc =
           } else {
             basic(LetExp.lets_var);
           }
-        | Tuple(elements) =>
+        | TuplePat(elements) =>
           let basic_tuple = group_id => {
             get_message(
               ~colorings=LetExp.let_tuple_exp_coloring_ids(~pat_id, ~def_id),
@@ -1517,7 +1517,7 @@ let get_doc =
               basic(LetExp.lets_tuple);
             }
           };
-        | Ap(con, arg) =>
+        | ApPat(con, arg) =>
           if (LetExp.let_ap_exp.id == get_specificity_level(LetExp.lets_ap)) {
             let con_id = List.nth(con.ids, 0);
             let arg_id = List.nth(arg.ids, 0);
@@ -1539,7 +1539,7 @@ let get_doc =
           } else {
             basic(LetExp.lets_ap);
           }
-        | Constructor(v, _) =>
+        | ConstructorPat(v, _) =>
           if (LetExp.let_ctr_exp.id == get_specificity_level(LetExp.lets_ctr)) {
             get_message(
               ~colorings=
@@ -1561,9 +1561,9 @@ let get_doc =
           } else {
             basic(LetExp.lets_ctr);
           }
-        | Invalid(_) => default // Shouldn't get hit
-        | Parens(_) => default // Shouldn't get hit?
-        | Cast(_) => default // Shouldn't get hit?
+        | InvalidPat(_) => default // Shouldn't get hit
+        | ParensPat(_) => default // Shouldn't get hit?
+        | CastPat(_) => default // Shouldn't get hit?
         };
       | FixF(pat, body, _) =>
         message_single(
@@ -1710,28 +1710,28 @@ let get_doc =
             ),
           SeqExp.seqs,
         );
-      | Filter(Filter({act: (Step, One), pat}), body) =>
+      | Filter(FilterStepper({act: (Step, One), pat}), body) =>
         message_single(
           FilterExp.filter_pause(
             ~p_id=UExp.rep_id(pat),
             ~body_id=UExp.rep_id(body),
           ),
         )
-      | Filter(Filter({act: (Step, All), pat}), body) =>
+      | Filter(FilterStepper({act: (Step, All), pat}), body) =>
         message_single(
           FilterExp.filter_debug(
             ~p_id=UExp.rep_id(pat),
             ~body_id=UExp.rep_id(body),
           ),
         )
-      | Filter(Filter({act: (Eval, All), pat}), body) =>
+      | Filter(FilterStepper({act: (Eval, All), pat}), body) =>
         message_single(
           FilterExp.filter_eval(
             ~p_id=UExp.rep_id(pat),
             ~body_id=UExp.rep_id(body),
           ),
         )
-      | Filter(Filter({act: (Eval, One), pat}), body) =>
+      | Filter(FilterStepper({act: (Eval, One), pat}), body) =>
         message_single(
           FilterExp.filter_hide(
             ~p_id=UExp.rep_id(pat),
@@ -1906,10 +1906,10 @@ let get_doc =
     get_message_exp(term.term);
   | Some(InfoPat({term, _})) =>
     switch (bypass_parens_pat(term).term) {
-    | EmptyHole => get_message(HolePat.empty_hole)
-    | MultiHole(_) => get_message(HolePat.multi_hole)
+    | EmptyHolePat => get_message(HolePat.empty_hole)
+    | MultiHolePat(_) => get_message(HolePat.multi_hole)
     | Wild => get_message(TerminalPat.wild)
-    | Int(i) =>
+    | IntPat(i) =>
       get_message(
         ~format=
           Some(
@@ -1918,7 +1918,7 @@ let get_doc =
           ),
         TerminalPat.intlit(i),
       )
-    | Float(f) =>
+    | FloatPat(f) =>
       get_message(
         ~format=
           Some(
@@ -1927,7 +1927,7 @@ let get_doc =
           ),
         TerminalPat.floatlit(f),
       )
-    | Bool(b) =>
+    | BoolPat(b) =>
       get_message(
         ~format=
           Some(
@@ -1936,7 +1936,7 @@ let get_doc =
           ),
         TerminalPat.boollit(b),
       )
-    | String(s) =>
+    | StringPat(s) =>
       get_message(
         ~format=
           Some(
@@ -1945,8 +1945,8 @@ let get_doc =
           ),
         TerminalPat.strlit(s),
       )
-    | Tuple([]) => get_message(TerminalPat.triv)
-    | ListLit(elements) =>
+    | TuplePat([]) => get_message(TerminalPat.triv)
+    | ListLitPat(elements) =>
       if (List.length(elements) == 0) {
         get_message(ListPat.listnil);
       } else {
@@ -1962,7 +1962,7 @@ let get_doc =
           ListPat.listlit,
         );
       }
-    | Cons(hd, tl) =>
+    | ConsPat(hd, tl) =>
       let hd_id = List.nth(hd.ids, 0);
       let tl_id = List.nth(tl.ids, 0);
       let basic = doc =>
@@ -1980,7 +1980,7 @@ let get_doc =
           doc,
         );
       switch (tl.term) {
-      | Cons(hd2, tl2) =>
+      | ConsPat(hd2, tl2) =>
         if (ListPat.cons2_pat.id == get_specificity_level(ListPat.cons2)) {
           let hd2_id = List.nth(hd2.ids, 0);
           let tl2_id = List.nth(tl2.ids, 0);
@@ -2008,7 +2008,7 @@ let get_doc =
         }
       | _ => basic(ListPat.cons)
       };
-    | Var(v) =>
+    | VarPat(v) =>
       get_message(
         ~format=
           Some(
@@ -2016,7 +2016,7 @@ let get_doc =
           ),
         TerminalPat.var(v),
       )
-    | Tuple(elements) =>
+    | TuplePat(elements) =>
       let basic = group =>
         get_message(
           ~format=
@@ -2082,7 +2082,7 @@ let get_doc =
         }
       | _ => basic(TuplePat.tuple)
       };
-    | Ap(con, arg) =>
+    | ApPat(con, arg) =>
       let con_id = List.nth(con.ids, 0);
       let arg_id = List.nth(arg.ids, 0);
       get_message(
@@ -2098,7 +2098,7 @@ let get_doc =
           ),
         AppPat.ap,
       );
-    | Constructor(con, _) =>
+    | ConstructorPat(con, _) =>
       get_message(
         ~format=
           Some(
@@ -2106,7 +2106,7 @@ let get_doc =
           ),
         TerminalPat.ctr(con),
       )
-    | Cast(pat, typ, _) =>
+    | CastPat(pat, typ, _) =>
       let pat_id = List.nth(pat.ids, 0);
       let typ_id = List.nth(typ.ids, 0);
       get_message(
@@ -2122,8 +2122,8 @@ let get_doc =
           ),
         TypAnnPat.typann,
       );
-    | Invalid(_) => simple("Not a valid pattern")
-    | Parens(_) =>
+    | InvalidPat(_) => simple("Not a valid pattern")
+    | ParensPat(_) =>
       // Shouldn't be hit?
       default
     }
@@ -2131,8 +2131,10 @@ let get_doc =
     switch (bypass_parens_typ(term).term) {
     | Unknown(SynSwitch)
     | Unknown(Internal)
-    | Unknown(Hole(EmptyHole)) => get_message(HoleTyp.empty_hole)
-    | Unknown(Hole(MultiHole(_))) => get_message(HoleTyp.multi_hole)
+    | Unknown(HoleProvenance(EmptyTypeHole)) =>
+      get_message(HoleTyp.empty_hole)
+    | Unknown(HoleProvenance(MultiTypeHole(_))) =>
+      get_message(HoleTyp.multi_hole)
     | Int => get_message(TerminalTyp.int)
     | Float => get_message(TerminalTyp.float)
     | Bool => get_message(TerminalTyp.bool)
@@ -2302,9 +2304,9 @@ let get_doc =
         }
       | _ => basic(TupleTyp.tuple)
       };
-    | Var(c) when Info.typ_is_constructor_expected(typ_info) =>
+    | TypVar(c) when Info.typ_is_constructor_expected(typ_info) =>
       get_message(SumTyp.sum_typ_nullary_constructor_defs(c))
-    | Var(v) =>
+    | TypVar(v) =>
       get_message(
         ~format=
           Some(
@@ -2313,18 +2315,19 @@ let get_doc =
         TerminalTyp.var(v),
       )
     | Sum(_) => get_message(SumTyp.labelled_sum_typs)
-    | Ap({term: Var(c), _}, _) =>
+    | ApTyp({term: TypVar(c), _}, _) =>
       get_message(SumTyp.sum_typ_unary_constructor_defs(c))
-    | Unknown(Hole(Invalid(_))) => simple("Not a type or type operator")
-    | Ap(_)
-    | Parens(_) => default // Shouldn't be hit?
+    | Unknown(HoleProvenance(InvalidTypeHole(_))) =>
+      simple("Not a type or type operator")
+    | ApTyp(_)
+    | TypParens(_) => default // Shouldn't be hit?
     }
   | Some(InfoTPat(info)) =>
     switch (info.term.term) {
-    | Invalid(_) => simple("Type names must begin with a capital letter")
-    | EmptyHole => get_message(HoleTPat.empty_hole_tpats)
-    | MultiHole(_) => get_message(HoleTPat.multi_hole_tpats)
-    | Var(v) =>
+    | InvalidTPat(_) => simple("Type names must begin with a capital letter")
+    | EmptyHoleTPat => get_message(HoleTPat.empty_hole_tpats)
+    | MultiHoleTPat(_) => get_message(HoleTPat.multi_hole_tpats)
+    | VarTPat(v) =>
       get_message(
         ~format=
           Some(
diff --git a/src/haz3lweb/view/Type.re b/src/haz3lweb/view/Type.re
index 82dfd0a9e3..325ff58928 100644
--- a/src/haz3lweb/view/Type.re
+++ b/src/haz3lweb/view/Type.re
@@ -5,7 +5,7 @@ open Haz3lcore;
 
 let tpat_view = (tpat: Haz3lcore.TPat.t): string =>
   switch (tpat.term) {
-  | Var(x) => x
+  | VarTPat(x) => x
   | _ => "?"
   };
 
@@ -25,12 +25,12 @@ let rec view_ty = (~strip_outer_parens=false, ty: Haz3lcore.Typ.t): Node.t =>
       ],
       [text("?") /*, prov_view(prov)*/],
     )
-  | Parens(ty) => view_ty(ty)
+  | TypParens(ty) => view_ty(ty)
   | Int => ty_view("Int", "Int")
   | Float => ty_view("Float", "Float")
   | String => ty_view("String", "String")
   | Bool => ty_view("Bool", "Bool")
-  | Var(name) => ty_view("Var", name)
+  | TypVar(name) => ty_view("Var", name)
   | Rec(name, t) =>
     div(
       ~attrs=[clss(["typ-view", "Rec"])],
@@ -94,7 +94,7 @@ let rec view_ty = (~strip_outer_parens=false, ty: Haz3lcore.Typ.t): Node.t =>
         ctr_view(t0) @ ts_views;
       },
     )
-  | Ap(_) =>
+  | ApTyp(_) =>
     div(
       ~attrs=[
         clss(["typ-view", "atom", "unknown"]),
diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
index ffb0eed0c5..d73aafba10 100644
--- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
+++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
@@ -47,12 +47,12 @@ let rec precedence = (~show_function_bodies, ~show_casts: bool, d: DHExp.t) => {
   switch (DHExp.term_of(d)) {
   | Var(_)
   | Invalid(_)
-  | Bool(_)
-  | Int(_)
   | Seq(_)
   | Test(_)
-  | Float(_)
-  | String(_)
+  | BoolLit(_)
+  | IntLit(_)
+  | FloatLit(_)
+  | StringLit(_)
   | ListLit(_)
   | EmptyHole
   | Constructor(_)
@@ -255,7 +255,7 @@ let mk =
       | Filter(flt, d') =>
         if (settings.show_stepper_filters) {
           switch (flt) {
-          | Filter({pat, act}) =>
+          | FilterStepper({pat, act}) =>
             let keyword = FilterAction.string_of_t(act);
             let flt_doc = go_formattable(pat);
             vseps([
@@ -277,7 +277,7 @@ let mk =
         } else {
           switch (flt) {
           | Residue(_) => go'(d')
-          | Filter(_) => go'(d')
+          | FilterStepper(_) => go'(d')
           };
         }
 
@@ -315,10 +315,10 @@ let mk =
         }
       | BuiltinFun(f) => text(f)
       | Constructor(name, _) => DHDoc_common.mk_ConstructorLit(name)
-      | Bool(b) => DHDoc_common.mk_BoolLit(b)
-      | Int(n) => DHDoc_common.mk_IntLit(n)
-      | Float(f) => DHDoc_common.mk_FloatLit(f)
-      | String(s) => DHDoc_common.mk_StringLit(s)
+      | BoolLit(b) => DHDoc_common.mk_BoolLit(b)
+      | IntLit(n) => DHDoc_common.mk_IntLit(n)
+      | FloatLit(f) => DHDoc_common.mk_FloatLit(f)
+      | StringLit(s) => DHDoc_common.mk_StringLit(s)
       | Undefined => DHDoc_common.mk_Undefined()
       | Test(d) => DHDoc_common.mk_Test(go'(d))
       | Deferral(_) => text("_")
diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Pat.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Pat.re
index 8996bd4b03..77f53e41a0 100644
--- a/src/haz3lweb/view/dhcode/layout/DHDoc_Pat.re
+++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Pat.re
@@ -3,22 +3,22 @@ open Haz3lcore;
 
 let precedence = (dp: Pat.t) =>
   switch (DHPat.term_of(dp)) {
-  | EmptyHole
-  | MultiHole(_)
+  | EmptyHolePat
+  | MultiHolePat(_)
   | Wild
-  | Invalid(_)
-  | Var(_)
-  | Int(_)
-  | Float(_)
-  | Bool(_)
-  | String(_)
-  | ListLit(_)
-  | Constructor(_) => DHDoc_common.precedence_const
-  | Tuple(_) => DHDoc_common.precedence_Comma
-  | Cons(_) => DHDoc_common.precedence_Cons
-  | Ap(_) => DHDoc_common.precedence_Ap
-  | Parens(_) => DHDoc_common.precedence_const
-  | Cast(_) => DHDoc_common.precedence_Ap
+  | InvalidPat(_)
+  | VarPat(_)
+  | IntPat(_)
+  | FloatPat(_)
+  | BoolPat(_)
+  | StringPat(_)
+  | ListLitPat(_)
+  | ConstructorPat(_) => DHDoc_common.precedence_const
+  | TuplePat(_) => DHDoc_common.precedence_Comma
+  | ConsPat(_) => DHDoc_common.precedence_Cons
+  | ApPat(_) => DHDoc_common.precedence_Ap
+  | ParensPat(_) => DHDoc_common.precedence_const
+  | CastPat(_) => DHDoc_common.precedence_Ap
   };
 
 let rec mk =
@@ -41,27 +41,27 @@ let rec mk =
   );
   let doc =
     switch (DHPat.term_of(dp)) {
-    | MultiHole(_)
-    | EmptyHole => DHDoc_common.mk_EmptyHole(ClosureEnvironment.empty)
-    | Invalid(t) => DHDoc_common.mk_InvalidText(t)
-    | Var(x) => Doc.text(x)
+    | MultiHolePat(_)
+    | EmptyHolePat => DHDoc_common.mk_EmptyHole(ClosureEnvironment.empty)
+    | InvalidPat(t) => DHDoc_common.mk_InvalidText(t)
+    | VarPat(x) => Doc.text(x)
     | Wild => DHDoc_common.Delim.wild
-    | Constructor(name, _) => DHDoc_common.mk_ConstructorLit(name)
-    | Int(n) => DHDoc_common.mk_IntLit(n)
-    | Float(f) => DHDoc_common.mk_FloatLit(f)
-    | Bool(b) => DHDoc_common.mk_BoolLit(b)
-    | String(s) => DHDoc_common.mk_StringLit(s)
-    | ListLit(d_list) =>
+    | ConstructorPat(name, _) => DHDoc_common.mk_ConstructorLit(name)
+    | IntPat(n) => DHDoc_common.mk_IntLit(n)
+    | FloatPat(f) => DHDoc_common.mk_FloatLit(f)
+    | BoolPat(b) => DHDoc_common.mk_BoolLit(b)
+    | StringPat(s) => DHDoc_common.mk_StringLit(s)
+    | ListLitPat(d_list) =>
       let ol = List.map(mk', d_list);
       DHDoc_common.mk_ListLit(ol);
-    | Cons(dp1, dp2) =>
+    | ConsPat(dp1, dp2) =>
       let (doc1, doc2) =
         mk_right_associative_operands(DHDoc_common.precedence_Cons, dp1, dp2);
       DHDoc_common.mk_Cons(doc1, doc2);
-    | Tuple([]) => DHDoc_common.Delim.triv
-    | Tuple(ds) => DHDoc_common.mk_Tuple(List.map(mk', ds))
+    | TuplePat([]) => DHDoc_common.Delim.triv
+    | TuplePat(ds) => DHDoc_common.mk_Tuple(List.map(mk', ds))
     // TODO: Print type annotations
-    | Cast(dp, t1, t2) when show_casts =>
+    | CastPat(dp, t1, t2) when show_casts =>
       Doc.hcats([
         mk'(dp),
         Doc.annot(
@@ -75,10 +75,10 @@ let rec mk =
           ]),
         ),
       ])
-    | Cast(dp, _, _) => mk'(~parenthesize, dp)
-    | Parens(dp) =>
+    | CastPat(dp, _, _) => mk'(~parenthesize, dp)
+    | ParensPat(dp) =>
       mk(~enforce_inline, ~parenthesize=true, ~infomap, ~show_casts, dp)
-    | Ap(dp1, dp2) =>
+    | ApPat(dp1, dp2) =>
       let (doc1, doc2) =
         mk_left_associative_operands(DHDoc_common.precedence_Ap, dp1, dp2);
       DHDoc_common.mk_Ap(doc1, doc2);
diff --git a/src/haz3lweb/view/dhcode/layout/HTypDoc.re b/src/haz3lweb/view/dhcode/layout/HTypDoc.re
index 996d01f607..b1ad3f746d 100644
--- a/src/haz3lweb/view/dhcode/layout/HTypDoc.re
+++ b/src/haz3lweb/view/dhcode/layout/HTypDoc.re
@@ -19,15 +19,15 @@ let precedence = (ty: Typ.t): int =>
   | Bool
   | String
   | Unknown(_)
-  | Var(_)
+  | TypVar(_)
   | Forall(_)
   | Rec(_)
   | Sum(_) => precedence_Sum
   | List(_) => precedence_Const
   | Prod(_) => precedence_Prod
   | Arrow(_, _) => precedence_Arrow
-  | Parens(_) => precedence_Const
-  | Ap(_) => precedence_Ap
+  | TypParens(_) => precedence_Const
+  | ApTyp(_) => precedence_Ap
   };
 
 let pad_child =
@@ -66,7 +66,7 @@ let rec mk = (~parenthesize=false, ~enforce_inline: bool, ty: Typ.t): t => {
   );
   let (doc, parenthesize) =
     switch (Typ.term_of(ty)) {
-    | Parens(ty) => (mk(~parenthesize=true, ~enforce_inline, ty), false)
+    | TypParens(ty) => (mk(~parenthesize=true, ~enforce_inline, ty), false)
     | Unknown(_) => (
         annot(HTypAnnot.Delim, annot(HTypAnnot.HoleLabel, text("?"))),
         parenthesize,
@@ -75,7 +75,7 @@ let rec mk = (~parenthesize=false, ~enforce_inline: bool, ty: Typ.t): t => {
     | Float => (text("Float"), parenthesize)
     | Bool => (text("Bool"), parenthesize)
     | String => (text("String"), parenthesize)
-    | Var(name) => (text(name), parenthesize)
+    | TypVar(name) => (text(name), parenthesize)
     | List(ty) => (
         hcats([
           mk_delim("["),
@@ -173,7 +173,7 @@ let rec mk = (~parenthesize=false, ~enforce_inline: bool, ty: Typ.t): t => {
            )
         |> hcats;
       (center, true);
-    | Ap(t1, t2) => (
+    | ApTyp(t1, t2) => (
         hcats([mk'(t1), text("("), mk'(t2), text(")")]),
         parenthesize,
       )