Try declaring a regular recursive type for exp as opposed to the recursive modules

src/haz3lcore/dynamics/FilterEnvironment.re

@@ -1,2 +1,2 @@
-type t = list(TermBase.StepperFilterKind.filter);
+type t = list(TermBase.filter);
 let extends = (flt, env) => [flt, ...env];

src/haz3lcore/lang/term/TPat.re

@@ -10,7 +10,7 @@ include TermBase.TPat;
 let rep_id: t => Id.t = IdTagged.rep_id;
 let fresh: term => t = IdTagged.fresh;
 
-let hole = (tms: list(TermBase.Any.t)) =>
+let hole = (tms: list(TermBase.Any.t)): TermBase.TPat.term =>
   switch (tms) {
   | [] => EmptyHole
   | [_, ..._] => MultiHole(tms)

src/haz3lcore/lang/term/Typ.re

@@ -34,7 +34,7 @@ let fresh: term => t = IdTagged.fresh;
 let temp: term => t = term => {term, ids: [Id.invalid], copied: false};
 let rep_id: t => Id.t = IdTagged.rep_id;
 
-let hole = (tms: list(TermBase.Any.t)) =>
+let hole = (tms: list(TermBase.Any.t)): TermBase.Typ.term =>
   switch (tms) {
   | [] => Unknown(Hole(EmptyHole))
   | [_, ..._] => Unknown(Hole(MultiHole(tms)))
@@ -137,7 +137,8 @@ let of_source = List.map((source: source) => source.ty);
    but right now TypeHole strictly predominates over Internal
    which strictly predominates over SynSwitch. */
 let join_type_provenance =
-    (p1: type_provenance, p2: type_provenance): type_provenance =>
+    (p1: TermBase.type_provenance, p2: TermBase.type_provenance)
+    : TermBase.type_provenance =>
   switch (p1, p2) {
   | (Hole(h1), Hole(h2)) when h1 == h2 => Hole(h1)
   | (Hole(EmptyHole), Hole(EmptyHole) | SynSwitch)

src/haz3lcore/statics/Ctx.re

@@ -2,14 +2,14 @@ open Util;
 
 [@deriving (show({with_path: false}), sexp, yojson)]
 type kind =
-  | Singleton(TermBase.Typ.t)
+  | Singleton(TermBase.typ_t)
   | Abstract;
 
 [@deriving (show({with_path: false}), sexp, yojson)]
 type var_entry = {
   name: Var.t,
   id: Id.t,
-  typ: TermBase.Typ.t,
+  typ: TermBase.typ_t,
 };
 
 [@deriving (show({with_path: false}), sexp, yojson)]
@@ -99,7 +99,9 @@ let lookup_alias = (ctx: t, name: string): option(TermBase.Typ.t) =>
   | Some(Singleton(ty)) => Some(ty)
   | Some(Abstract) => None
   | None =>
-    Some(TermBase.Typ.Unknown(Hole(Invalid(name))) |> IdTagged.fresh)
+    Some(
+      (Unknown(Hole(Invalid(name))): TermBase.Typ.term) |> IdTagged.fresh,
+    )
   };
 
 let add_ctrs = (ctx: t, name: string, id: Id.t, ctrs: TermBase.Typ.sum_map): t =>
@@ -112,11 +114,10 @@ let add_ctrs = (ctx: t, name: string, id: Id.t, ctrs: TermBase.Typ.sum_map): t =
           id,
           typ:
             switch (typ) {
-            | None => TermBase.Typ.Var(name) |> IdTagged.fresh
+            | None => (Var(name): TermBase.typ_term) |> IdTagged.fresh
             | Some(typ) =>
-              TermBase.Typ.Arrow(
-                typ,
-                TermBase.Typ.Var(name) |> IdTagged.fresh,
+              (
+                Arrow(typ, (Var(name): TermBase.typ_term) |> IdTagged.fresh): TermBase.typ_term
               )
               |> IdTagged.fresh
             },

src/haz3lcore/statics/Term.re

@@ -31,7 +31,7 @@ module Pat = {
 
   let fresh: term => t = IdTagged.fresh;
 
-  let hole = (tms: list(TermBase.Any.t)) =>
+  let hole = (tms: list(TermBase.Any.t)): TermBase.Pat.term =>
     switch (tms) {
     | [] => EmptyHole
     | [_, ..._] => MultiHole(tms)
@@ -597,7 +597,7 @@ module Any = {
     | Typ(t) => Some(t)
     | _ => None;
 
-  let rec ids =
+  let rec ids: TermBase.any_t => list(Id.t) =
     fun
     | Exp(tm) => tm.ids
     | Pat(tm) => tm.ids
@@ -620,7 +620,7 @@ module Any = {
   // (This would change for n-tuples if we decided parentheses are necessary.)
   let rep_id =
     fun
-    | Exp(tm) => Exp.rep_id(tm)
+    | (Exp(tm): TermBase.any_t) => Exp.rep_id(tm)
     | Pat(tm) => Pat.rep_id(tm)
     | Typ(tm) => Typ.rep_id(tm)
     | TPat(tm) => TPat.rep_id(tm)