diff --git a/src/CLI/Print.re b/src/CLI/Print.re
index 8802b66f76..df351d3cc3 100644
--- a/src/CLI/Print.re
+++ b/src/CLI/Print.re
@@ -10,6 +10,7 @@ let exp_to_segment_settings: ExpToSegment.Settings.t = {
   hide_fixpoints: false,
   show_filters: true,
   show_unknown_as_hole: true,
+  raise_if_padding: false,
 };
 
 let segmentize =
diff --git a/src/haz3lcore/pretty/ExpToSegment.re b/src/haz3lcore/pretty/ExpToSegment.re
index d28d36e017..9d3e42a2fe 100644
--- a/src/haz3lcore/pretty/ExpToSegment.re
+++ b/src/haz3lcore/pretty/ExpToSegment.re
@@ -43,6 +43,7 @@ module Settings = {
     hide_fixpoints: bool,
     show_filters: bool,
     show_unknown_as_hole: bool,
+    raise_if_padding: bool,
   };
 
   let of_core = (~inline, ~fold_fn_bodies=?, settings: CoreSettings.t) => {
@@ -59,6 +60,7 @@ module Settings = {
     hide_fixpoints: !settings.evaluation.show_fixpoints,
     show_filters: settings.evaluation.show_stepper_filters,
     show_unknown_as_hole: true,
+    raise_if_padding: false,
   };
 
   let editable = (~inline) => {
@@ -72,6 +74,7 @@ module Settings = {
       hide_fixpoints: false,
       show_filters: true,
       show_unknown_as_hole: true,
+      raise_if_padding: false,
     };
   };
 };
@@ -966,9 +969,12 @@ let mk_form =
 
 /* HACK[Matt]: Sometimes terms that should have multiple ids won't because
    evaluation only ever gives them one */
-let pad_ids = (n: int, ids: list(Id.t)): list(Id.t) => {
+let pad_ids = (~settings: Settings.t, n: int, ids: list(Id.t)): list(Id.t) => {
   let len = List.length(ids);
   if (len < n) {
+    if (settings.raise_if_padding) {
+      raise(Failure("Padding required but not enough ids provided."));
+    };
     ids @ List.init(n - len, _ => Id.mk());
   } else {
     ListUtil.split_n(n, ids) |> fst;
@@ -1060,6 +1066,7 @@ let fold_fun_if = (condition, f_name: string, pieces, exp) =>
       that the expression has no Closures or DynamicErrorHoles
    */
 let rec exp_to_pretty = (~settings: Settings.t, exp: Exp.t): pretty => {
+  let pad_ids = pad_ids(~settings);
   let go = (~inline=settings.inline) =>
     exp_to_pretty(
       ~settings={
@@ -1607,6 +1614,7 @@ let rec exp_to_pretty = (~settings: Settings.t, exp: Exp.t): pretty => {
 }
 and pat_to_pretty = (~settings: Settings.t, pat: Pat.t): pretty => {
   let go = pat_to_pretty(~settings: Settings.t);
+  let pad_ids = pad_ids(~settings);
   let wrap = wrap_with_secondary(~secondary=settings.secondary);
   /* Use settings-aware concatenation and form building */
   let (@) = concat_segment(~secondary=settings.secondary);
@@ -1777,6 +1785,7 @@ and pat_to_pretty = (~settings: Settings.t, pat: Pat.t): pretty => {
 }
 and typ_to_pretty = (~settings: Settings.t, typ: Typ.t): pretty => {
   let go = typ_to_pretty(~settings: Settings.t);
+  let pad_ids = pad_ids(~settings);
   let wrap = wrap_with_secondary(~secondary=settings.secondary);
   /* Use settings-aware concatenation and form building */
   let (@) = concat_segment(~secondary=settings.secondary);
@@ -2020,6 +2029,7 @@ and typ_to_pretty = (~settings: Settings.t, typ: Typ.t): pretty => {
 }
 and tpat_to_pretty = (~settings: Settings.t, tpat: TPat.t): pretty => {
   let wrap = wrap_with_secondary(~secondary=settings.secondary);
+  let pad_ids = pad_ids(~settings);
   /* Use settings-aware concatenation and form building */
   switch (tpat |> IdTagged.term_of) {
   | Invalid(t) =>
diff --git a/src/haz3lcore/pretty/PadIds.re b/src/haz3lcore/pretty/PadIds.re
new file mode 100644
index 0000000000..daa7377a74
--- /dev/null
+++ b/src/haz3lcore/pretty/PadIds.re
@@ -0,0 +1,38 @@
+open Language;
+
+/* Number of IDs required for ExpToSegment compatibility per type constructor */
+let necessary_ids: Typ.t => int =
+  ty => {
+    switch (ty.term) {
+    | Prod([]) => 1 /* Empty product (unit-like) */
+    | Prod(tys) => List.length(tys) - 1 /* One ID per separator */
+    | Sum(tys) => List.length(tys) + 1 /* Constructors + prefix */
+    | _ => 1 /* Default for other type constructors */
+    };
+  };
+
+/**
+ * Pads type IDs to ensure ExpToSegment uses them instead of creating new ones,
+ * preserving ID correspondence for styling. Test_PadIds property test that checks
+ *  ExpToSegment compatibility and padding equivalence.
+ */
+let pad_typ_ids = (ty: Typ.t): Typ.t => {
+  Typ.map_term(
+    ~f_typ=
+      (cont, ty) => {
+        let current_ids = ty.annotation.ids;
+        let needed_ids = necessary_ids(ty);
+        let ids =
+          current_ids
+          @ List.init(needed_ids - List.length(current_ids), _ => Id.mk());
+        cont({
+          ...ty,
+          annotation: {
+            ids,
+            secondary: ty.annotation.secondary,
+          },
+        });
+      },
+    ty,
+  );
+};
diff --git a/src/haz3lcore/projectors/ProjectorBase.re b/src/haz3lcore/projectors/ProjectorBase.re
index a3c99da93c..04da9a882b 100644
--- a/src/haz3lcore/projectors/ProjectorBase.re
+++ b/src/haz3lcore/projectors/ProjectorBase.re
@@ -120,6 +120,7 @@ module View = {
     (
       ~single_line: bool=?,
       ~background: bool=?,
+      ~is_dynamic: Id.t => bool=?,
       ~text_only: bool=?,
       Sort.t,
       list(syntax)
diff --git a/src/haz3lcore/projectors/implementations/TypeProj.re b/src/haz3lcore/projectors/implementations/TypeProj.re
index 48043175fd..8ae6e7f182 100644
--- a/src/haz3lcore/projectors/implementations/TypeProj.re
+++ b/src/haz3lcore/projectors/implementations/TypeProj.re
@@ -24,11 +24,44 @@ let totalize_ty = (expected_ty: option(Typ.t)): Typ.t =>
   | None => Typ.fresh(Unknown(Internal))
   };
 
+let get_dynamic_typ = (info: info): Typ.t => {
+  let dynamic_typ =
+    info.dynamics
+    |> Option.bind(
+         _,
+         (d: Dynamics.Info.t) => {
+           let statics =
+             Statics.mk(CoreSettings.on, Builtins.ctx_init(Some(Int)));
+           let type_of = (c: Sample.t) => {
+             IdTagged.rep_id(c.value)
+             |> Id.Map.find_opt(_, statics(c.value))
+             |> Option.bind(
+                  _,
+                  fun
+                  | InfoExp(e) => {
+                      Some(e.ty);
+                    }
+                  | _ => None,
+                );
+           };
+           let types = List.map(type_of, d.samples) |> Util.OptUtil.sequence;
+
+           Option.bind(
+             types,
+             Typ.meet_all(~empty=Typ.fresh(Unknown(Internal)), Ctx.empty),
+           );
+         },
+       )
+    |> Option.value(~default=Typ.fresh(Unknown(Internal)));
+  dynamic_typ;
+};
+
 module M: Projector = {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type model =
     | Expected
-    | Self;
+    | Self
+    | Dynamic;
 
   [@deriving (show({with_path: false}), sexp, yojson)]
   type action =
@@ -37,54 +70,90 @@ module M: Projector = {
   let init = (any: Any.t): option(model) => {
     switch (any) {
     | Exp(_)
-    | Pat(_) => Some(Expected)
+    | Pat(_)
+    | Typ(_) => Some(Expected)
     | Any () => Some(Expected) /* Grout don't have sorts rn */
     | _ => None
     };
   };
 
-  let dynamics = false;
+  let dynamics = true;
   let focusable = Focusable.non;
 
-  let display_ty = (model, statics): option(Typ.t) =>
-    switch (model) {
-    | _ when expected_ty(statics) |> totalize_ty |> Typ.is_syn =>
-      statics |> self_ty
-    | Self => statics |> self_ty
-    | Expected => statics |> expected_ty
-    };
-
-  let display_mode = (model: model, statics: option(Language.Info.t)): string =>
+  let display_mode = (model: model, statics: option(Language.Info.t)): string => {
     switch (model) {
+    | Dynamic => "⇓"
     | _ when self_ty(statics) == expected_ty(statics) => "⇔"
     | _ when expected_ty(statics) |> totalize_ty |> Typ.is_syn => "⇒"
     | Self => "⇒"
     | Expected => "⇐"
     };
+  };
+  let mode_description =
+      (model: model, statics: option(Language.Info.t)): string => {
+    switch (model) {
+    | Dynamic => "Dynamic type (from runtime values)"
+    | _ when self_ty(statics) == expected_ty(statics) => "Self type matches expected type"
+    | _ when expected_ty(statics) |> totalize_ty |> Typ.is_syn => "Self type"
+    | Self => "Self type"
+    | Expected => "Expected type"
+    };
+  };
 
   let mode_view = (model, info) =>
     div(
-      ~attrs=[Attr.classes(["mode"])],
+      ~attrs=[
+        Attr.classes(["mode"]),
+        Attr.title(mode_description(model, info)),
+      ],
       [text(display_mode(model, info))],
     );
 
   let typ_view = (model, info: info, utility, view_seg: View.seg) => {
-    let typ = display_ty(model, info.statics) |> totalize_ty;
+    let (is_dynamic, typ) =
+      switch (model) {
+      | Dynamic =>
+        let dyn_typ =
+          get_dynamic_typ(info)
+          |> Grammar.map_typ_annotation(_ => IdTagged.IdTag.fresh())
+          |> PadIds.pad_typ_ids;
+        let self_ty =
+          Option.value(
+            ~default=Typ.fresh(Unknown(Internal)),
+            self_ty(info.statics),
+          );
+        let dynamic_ids: list(Id.t) = Typ.diff(self_ty, dyn_typ);
+        (List.mem(_, dynamic_ids), dyn_typ);
+      | Expected when expected_ty(info.statics) |> totalize_ty |> Typ.is_syn => (
+          (_ => false),
+          self_ty(info.statics) |> totalize_ty,
+        )
+      | Expected => ((_ => false), expected_ty(info.statics) |> totalize_ty)
+      | Self => ((_ => false), self_ty(info.statics) |> totalize_ty)
+      };
+
     div(
       ~attrs=[Attr.classes(["type-cell"])],
       [
         Typ(typ)
         |> utility.term_to_seg
-        |> view_seg(~single_line=true, Sort.Typ),
+        |> view_seg(~single_line=true, ~is_dynamic, Sort.Typ),
       ],
     );
   };
 
-  let update = (model, _, a: action) =>
+  let update = (model, info, a: action) => {
+    let has_expected =
+      switch (expected_ty(info.statics)) {
+      | Some(ty) => !Typ.is_syn(ty)
+      | None => false
+      };
     switch (a, model) {
-    | (ToggleDisplay, Expected) => Self
-    | (ToggleDisplay, Self) => Expected
+    | (ToggleDisplay, Expected) => if (has_expected) {Self} else {Dynamic}
+    | (ToggleDisplay, Self) => Dynamic
+    | (ToggleDisplay, Dynamic) => if (has_expected) {Expected} else {Self}
     };
+  };
 
   let placeholder = (_, _) => ProjectorCore.Shape.default;
 
diff --git a/src/haz3lcore/zipper/action/Introduce.re b/src/haz3lcore/zipper/action/Introduce.re
index 4f2a3665cb..30457638c5 100644
--- a/src/haz3lcore/zipper/action/Introduce.re
+++ b/src/haz3lcore/zipper/action/Introduce.re
@@ -249,6 +249,7 @@ module Make =
           hide_fixpoints: false,
           show_filters: true,
           show_unknown_as_hole: true,
+          raise_if_padding: false,
         },
         term,
         already_parenthesized(z),
diff --git a/src/language/ProjectorKind.re b/src/language/ProjectorKind.re
index 1a2f3e010f..bfcd2f9473 100644
--- a/src/language/ProjectorKind.re
+++ b/src/language/ProjectorKind.re
@@ -53,22 +53,18 @@ let name = (p: t): string =>
   | Csv => "csv"
   };
 
-/* This must be updated and kept 1-to-1 with the above
- * name function in order to be able to select the
- * projector in the projector panel menu */
+module StringMap = Map.Make(String);
+let name_to_kind: StringMap.t(t) =
+  List.fold_left(
+    (map, kind) => StringMap.add(name(kind), kind, map),
+    StringMap.empty,
+    all,
+  );
+
 let of_name = (p: string): t =>
-  switch (p) {
-  | "fold" => Fold
-  | "probe" => Probe
-  | "statics" => Statics
-  | "check" => Checkbox
-  | "slider" => Slider
-  | "sliderf" => SliderF
-  | "text" => TextArea
-  | "livelit" => Livelit
-  | "card" => Card
-  | "csv" => Csv
-  | _ => failwith("Unknown projector kind")
+  switch (StringMap.find_opt(p, name_to_kind)) {
+  | Some(k) => k
+  | None => failwith("Unknown projector kind")
   };
 
-let is_name = str => List.mem(str, List.map(name, all));
+let is_name = StringMap.mem(_, name_to_kind);
diff --git a/src/language/statics/Elaborator.re b/src/language/statics/Elaborator.re
index a24eac1224..3c93722a22 100644
--- a/src/language/statics/Elaborator.re
+++ b/src/language/statics/Elaborator.re
@@ -457,21 +457,13 @@ let rec elaborate = (m: Statics.Map.t, uexp: Exp.t): (DHExp.t, Typ.t) => {
         );
       Match(e', List.combine(ps', es')) |> rewrap;
     };
+
   (dhexp, elaborated_type);
 };
 
-//let dhexp_of_uexp = Core.Memo.general(~cache_size_bound=1000, dhexp_of_uexp);
-
-/* This function gives a new id to all the types
-   in the expression. It does this to get rid of
-   all the invalid ids we added to prevent generating
-   too many new ids */
-let fix_typ_ids =
-  Exp.map_term(~f_typ=(cont, e) => e |> IdTagged.new_ids |> cont);
-
 let uexp_elab = (m: Statics.Map.t, uexp: Exp.t): ElaborationResult.t => {
   switch (elaborate(m, uexp)) {
   | exception MissingTypeInfo => DoesNotElaborate
-  | (d, ty) => Elaborates(d |> fix_typ_ids, ty)
+  | (d, ty) => Elaborates(d, ty)
   };
 };
diff --git a/src/language/term/IdTagged.re b/src/language/term/IdTagged.re
index 5d5baa36b6..c4f8fe54e6 100644
--- a/src/language/term/IdTagged.re
+++ b/src/language/term/IdTagged.re
@@ -44,6 +44,8 @@ module IdTag = {
     ids,
     secondary,
   };
+
+  let rep_id = ({ids, _}: t) => List.hd(ids);
 };
 
 [@deriving (show({with_path: false}), sexp, yojson)]
diff --git a/src/language/term/Typ.re b/src/language/term/Typ.re
index 12cc42c4a9..056b8e9519 100644
--- a/src/language/term/Typ.re
+++ b/src/language/term/Typ.re
@@ -1135,3 +1135,63 @@ and paren_pretty_print = typ =>
  * @return A product type representing the combination of the input types
  */
 let to_product = (tys: list(t)): t => TempGrammar.Typ.(prod(tys));
+
+/* Computes the list of ids in t' that are not in t. Assumes initial ids are distinct otherwise you may get incorrect ids. */
+let rec diff = (ty: t, ty': t): list(Id.t) => {
+  let get_ids = () => {
+    let ids = ref([]);
+    let _ =
+      Grammar.map_typ_annotation(
+        (t: IdTagged.IdTag.t) => {
+          ids := t.ids @ ids^;
+          t;
+        },
+        ty': t,
+      );
+    ids^;
+  };
+  switch (term_of(ty), term_of(ty')) {
+  | (Parens(t1), Parens(t2)) => diff(t1, t2)
+  | (Parens(t1), _) => diff(t1, ty')
+  | (_, Projector(_, t2)) => diff(ty, t2)
+  | (Projector(_, t1), _) => diff(t1, ty')
+  | (_, Parens(t2)) => diff(ty, t2)
+  | (Unknown(_), Unknown(_)) => []
+  | (Unknown(_), _) => get_ids()
+  | (Atom(c1), Atom(c2)) when c1 == c2 => []
+  | (Atom(_), _) => get_ids()
+  | (Label(l1), Label(l2)) when l1 == l2 => []
+  | (Label(_), _) => get_ids()
+  | (ExplicitNonlabel, ExplicitNonlabel) => []
+  | (ExplicitNonlabel, _) => get_ids()
+  | (Var(v1), Var(v2)) when v1 == v2 => []
+  | (Var(_), _) => get_ids()
+  | (Rec(tp1, t1), Rec(tp2, t2)) when Equality.syntactic.tpat(tp1, tp2) =>
+    diff(t1, t2)
+  | (Rec(_), _) => get_ids()
+  | (Poly(tp1, t1), Poly(tp2, t2)) when Equality.syntactic.tpat(tp1, tp2) =>
+    diff(t1, t2)
+  | (Poly(_), _) => get_ids()
+  | (ProofOf(e1), ProofOf(e2)) =>
+    Equality.syntactic.exp(e1, e2) ? [] : get_ids()
+  | (ProofOf(_), _) => get_ids()
+  | (Arrow(t1a, t1b), Arrow(t2a, t2b)) => diff(t1a, t2a) @ diff(t1b, t2b)
+  | (Arrow(_), _) => get_ids()
+  | (Prod(tys1), Prod(tys2)) when List.length(tys1) == List.length(tys2) =>
+    List.map2(diff, tys1, tys2) |> List.concat
+  | (Prod(_), _) => get_ids()
+  | (TupLabel(l1, t1), TupLabel(l2, t2)) => diff(l1, l2) @ diff(t1, t2)
+  | (TupLabel(_, _), _) => get_ids()
+  | (List(t1), List(t2)) => diff(t1, t2)
+  | (List(_), _) => get_ids()
+  | (ProdProjection(t1, t2), ProdProjection(t1', t2')) =>
+    diff(t1, t1') @ diff(t2, t2')
+  | (ProdProjection(_, _), _) => get_ids()
+  | (ProdExtension(t1, t2), ProdExtension(t1', t2')) =>
+    diff(t1, t1') @ diff(t2, t2')
+  | (ProdExtension(_, _), _) => get_ids()
+  | (Sum(sm1), Sum(sm2)) when ConstructorMap.equal(fast_equal, sm1, sm2) =>
+    []
+  | (Sum(_), _) => get_ids()
+  };
+};
diff --git a/src/util/Id.re b/src/util/Id.re
index c661ffce0a..cf80efa150 100644
--- a/src/util/Id.re
+++ b/src/util/Id.re
@@ -68,6 +68,11 @@ let mk_str: string => t = s => Uuidm.v5(namespace_uuid, s);
 let compare: (t, t) => int = Uuidm.compare;
 let to_string: (~upper: bool=?, t) => string = Uuidm.to_string;
 let of_string: (~pos: int=?, string) => option(t) = Uuidm.of_string;
+
+let str3 = (id: t) => id |> to_string |> String.sub(_, 0, 3);
+let str8 = (id: t) => id |> to_string |> String.sub(_, 0, 8);
+let cls = (id: t) => "id" ++ str8(id);
+
 let pp: (Format.formatter, t) => unit =
   (f, id) =>
     Format.fprintf(
@@ -81,10 +86,6 @@ let show = id =>
     to_string(id),
   );
 
-let str3 = (id: t) => id |> to_string |> String.sub(_, 0, 3);
-let str8 = (id: t) => id |> to_string |> String.sub(_, 0, 8);
-let cls = (id: t) => "id" ++ str8(id);
-
 [@deriving (sexp, yojson)]
 type binding('v) = (t, 'v);
 
diff --git a/src/util/Monads.re b/src/util/Monads.re
index 89756c915a..dea4a3f872 100644
--- a/src/util/Monads.re
+++ b/src/util/Monads.re
@@ -7,7 +7,6 @@
    In any case, that's a good reference. */
 
 module type MONAD_BASIC = {
-  [@deriving sexp]
   type t('a);
   let return: 'a => t('a);
   let bind: (t('a), 'a => t('b)) => t('b);
diff --git a/src/util/Monads.rei b/src/util/Monads.rei
index 81a6c66969..fa26667425 100644
--- a/src/util/Monads.rei
+++ b/src/util/Monads.rei
@@ -2,7 +2,6 @@
  * https://ocaml.janestreet.com/ocaml-core/v0.13/doc/base/Base__/Monad_intf/index.html */
 
 module type MONAD_BASIC = {
-  [@deriving sexp]
   type t('a);
   let return: 'a => t('a);
   let bind: (t('a), 'a => t('b)) => t('b);
diff --git a/src/web/app/Cursor.re b/src/web/app/Cursor.re
index 915ea5741f..e982190b2f 100644
--- a/src/web/app/Cursor.re
+++ b/src/web/app/Cursor.re
@@ -1,11 +1,14 @@
+open Haz3lcore;
+open Language;
 type cursor('update) = {
-  info: option(Language.Info.t),
+  info: option(Info.t),
+  dynamics: option(list(Sample.t)),
   selected_text: option(unit => string),
-  selection: option(Haz3lcore.Segment.t),
-  indicated_piece: option(Haz3lcore.Piece.t),
-  editor: option(Haz3lcore.Editor.t),
+  selection: option(Segment.t),
+  indicated_piece: option(Piece.t),
+  editor: option(Editor.t),
   editor_read_only: bool,
-  editor_action: Haz3lcore.Action.t => option('update),
+  editor_action: Action.t => option('update),
   undo_action: option('update),
   redo_action: option('update),
   /* Global statics summary for status indicator */
@@ -28,6 +31,7 @@ let map_opt = (f: 'a => option('b), cursor) => {
 
 let empty = {
   info: None,
+  dynamics: None,
   selected_text: None,
   selection: None,
   indicated_piece: None,
diff --git a/src/web/app/common/ProjectorView.re b/src/web/app/common/ProjectorView.re
index 03cd9b0793..b9e4b2197a 100644
--- a/src/web/app/common/ProjectorView.re
+++ b/src/web/app/common/ProjectorView.re
@@ -211,7 +211,14 @@ let offside_wrapper =
   );
 
 let simple_code =
-    (~background=false, ~is_single_line=false, font_metrics, _sort, segment)
+    (
+      ~background=false,
+      ~is_dynamic=(_: Id.t) => false,
+      ~is_single_line=false,
+      font_metrics,
+      _sort,
+      segment,
+    )
     : Node.t => {
   let shape_map = ProjectorCore.Shape.Map.empty; /* Assume this doesn't contain projectors */
   let refractor_shape_map = Id.Map.empty; /* Assume this doesn't contain refractors (probes) */
@@ -219,6 +226,7 @@ let simple_code =
     Measured.of_segment(~is_single_line, segment, shape_map, Id.Map.empty);
   let code =
     Code.view(
+      ~is_dynamic,
       ~measured,
       ~settings=Settings.Model.init,
       ~shape_map,
@@ -283,18 +291,22 @@ let flex_code =
       ~single_line=false, /* Perf optimization if you promise it's single-line */
       ~background=?,
       ~text_only=false,
+      ~is_dynamic=?,
       sort,
       segment,
-    ) =>
+    ) => {
+  let is_dynamic = Option.value(~default=(_: Id.t) => false, is_dynamic);
   text_only
     ? text_code(segment)
     : simple_code(
         ~background?,
+        ~is_dynamic,
         ~is_single_line=single_line,
         font_metrics,
         sort,
         segment,
       );
+};
 
 /* Route top-level metadata to the projector view function. */
 let mk_view =
@@ -315,12 +327,21 @@ let mk_view =
       inject(Project(SetModel(idx, p.kind, new_model)));
     },
     parent: a => inject(handle(idx, a)),
-    view_seg: (~single_line=?, ~background=?, ~text_only=?, sort, segment) =>
+    view_seg:
+      (
+        ~single_line=?,
+        ~background=?,
+        ~is_dynamic=?,
+        ~text_only=?,
+        sort,
+        segment,
+      ) =>
       flex_code(
         ~font_metrics,
         ~single_line?,
         ~background?,
         ~text_only?,
+        ~is_dynamic?,
         sort,
         segment,
       ),
diff --git a/src/web/app/editors/code/Code.re b/src/web/app/editors/code/Code.re
index 309c5f4b93..25426ebce5 100644
--- a/src/web/app/editors/code/Code.re
+++ b/src/web/app/editors/code/Code.re
@@ -66,6 +66,7 @@ let whitespace_token =
 
 let view =
     (
+      ~is_dynamic=(_: Id.t) => false,
       ~measured: Measured.t,
       ~settings: Settings.Model.t,
       ~shape_map: ProjectorCore.Shape.Map.t,
@@ -149,9 +150,17 @@ let view =
               ();
             | None => ()
             };
-          Aba.mk(t.shards, t.children)
-          |> Aba.join(i => [of_delim(t, i)], of_segment)
-          |> List.concat;
+
+          [
+            span(
+              ~attrs=[
+                Attr.classes(Tile.id(t) |> is_dynamic ? ["dynamic"] : []),
+              ],
+              Aba.mk(t.shards, t.children)
+              |> Aba.join(i => [of_delim(t, i)], of_segment)
+              |> List.concat,
+            ),
+          ];
         }
       | Grout(g) => [of_grout(g)]
       | Secondary(s) => [of_secondary(s)]
diff --git a/src/web/app/editors/code/CodeWithStatics.re b/src/web/app/editors/code/CodeWithStatics.re
index f281467114..0f466c68ab 100644
--- a/src/web/app/editors/code/CodeWithStatics.re
+++ b/src/web/app/editors/code/CodeWithStatics.re
@@ -57,6 +57,7 @@ module Model = {
 
   let get_cursor_info = (model: t): Cursor.cursor(Action.t) => {
     info: Indicated.ci_of(model.editor.state.zipper, model.statics.info_map),
+    dynamics: None,
     indicated_piece:
       Indicated.piece''(model.editor.state.zipper)
       |> Option.map(((p, _, _)) => p),
diff --git a/src/web/app/editors/code/ContextMenu.re b/src/web/app/editors/code/ContextMenu.re
index b640b02fcc..c0d80cefc9 100644
--- a/src/web/app/editors/code/ContextMenu.re
+++ b/src/web/app/editors/code/ContextMenu.re
@@ -279,10 +279,10 @@ let type_annotation_data =
       {
         name:
           switch (probe_status) {
-          | Statics(_) => "Remove statics"
+          | Statics(_) => "Remove type probe"
           | Manual(_)
-          | Auto => "Switch to statics"
-          | Non => "Add statics"
+          | Auto => "Switch to type probe"
+          | Non => "Add type probe"
           },
         shortcut: Some(Shortcuts.type_annotation()),
         action: Probe(ToggleStatics),
diff --git a/src/web/app/inspector/CursorInspector.re b/src/web/app/inspector/CursorInspector.re
index 08c9135b1c..65b5c49060 100644
--- a/src/web/app/inspector/CursorInspector.re
+++ b/src/web/app/inspector/CursorInspector.re
@@ -85,6 +85,7 @@ let code_view_settings: Haz3lcore.ExpToSegment.Settings.t = {
   hide_fixpoints: false,
   show_filters: false,
   show_unknown_as_hole: true,
+  raise_if_padding: false,
 };
 
 let view_any = (~globals, any: Any.t) =>
diff --git a/src/web/app/probesystem/ProbeSidebar.re b/src/web/app/probesystem/ProbeSidebar.re
index 5ac220d61e..b2914e4045 100644
--- a/src/web/app/probesystem/ProbeSidebar.re
+++ b/src/web/app/probesystem/ProbeSidebar.re
@@ -173,6 +173,7 @@ let legend_sample_view =
         ~single_line=true,
         ~background=false,
         ~text_only,
+        ~is_dynamic=?None,
       ),
     _ => Effect.Ignore,
     _ => Effect.Ignore,
diff --git a/src/web/init/docs/Probes.ml b/src/web/init/docs/Probes.ml
index 7d2f9c9553..c5f2b33d13 100644
--- a/src/web/init/docs/Probes.ml
+++ b/src/web/init/docs/Probes.ml
@@ -2022,10 +2022,14 @@ let out : string * Haz3lcore.PersistentSegment.t =
          716774da-818d-43e5-8fea-14f8a9566587)(content(Comment\"# STATICS \
          PROBES: These show inferred type information. #\"))))(Secondary((id \
          d4bd4767-725a-4208-a7a6-636d4ecc41c3)(content(Whitespace\"\\n\"))))(Secondary((id \
-         d4c05b17-0a5f-4775-9866-71a91a92bb06)(content(Comment\"# Double \
-         clicking toggles from analytic to synthetic type. \
+         8b88339d-6aba-4f4d-adc5-118affc27855)(content(Comment\"# Double \
+         clicking toggles between analytic type, synthetic type, \
          #\"))))(Secondary((id \
          9062ef1a-3700-4912-9897-3b3c45829642)(content(Whitespace\"\\n\"))))(Secondary((id \
+         7b692ad2-7f24-4e98-8400-1b313aef30f6)(content(Comment\"# and dynamic \
+         type. For dynamic type the dynamic component is shown in green. \
+         #\"))))(Secondary((id \
+         4be2eff9-0ea6-46a9-8ab9-22cac9029cec)(content(Whitespace\"\\n\"))))(Secondary((id \
          59ed61a7-31b6-4d83-bca7-ac30c1302de7)(content(Whitespace\"\\n\"))))(Tile((id \
          b026144b-b546-4411-8c42-b00c63cfce83)(label(let = in))(mold((out \
          Exp)(in_(Pat Exp))(nibs(((shape Convex)(sort Exp))((shape(Concave \
@@ -2128,6 +2132,118 @@ let out : string * Haz3lcore.PersistentSegment.t =
          Exp))))))(shards(0))(children()))))))))(Secondary((id \
          0ecbef06-b1e6-4ec1-afcb-10a9b52a5b5d)(content(Whitespace\" \
          \")))))))))(Secondary((id \
+         0e1b0f10-8f5b-45db-bf0a-63a30095c9be)(content(Whitespace\"\\n\"))))(Tile((id \
+         8766e1a8-42fa-4d1c-9569-1ad816a791da)(label(let = in))(mold((out \
+         Exp)(in_(Pat Exp))(nibs(((shape Convex)(sort Exp))((shape(Concave \
+         45))(sort Exp))))))(shards(0 1 2))(children(((Secondary((id \
+         a005db8f-10e1-47c4-b3d7-1233cd3273ab)(content(Whitespace\" \
+         \"))))(Tile((id \
+         aa00b5ea-0a31-47fc-a45d-560a32bbfeab)(label(d))(mold((out \
+         Pat)(in_())(nibs(((shape Convex)(sort Pat))((shape Convex)(sort \
+         Pat))))))(shards(0))(children())))(Secondary((id \
+         7c03a3ad-c7e2-4b2c-a133-060410a805c9)(content(Whitespace\" \
+         \")))))((Secondary((id \
+         aa0bc12f-4fdb-4488-b467-ab7bfcedaa4e)(content(Whitespace\" \
+         \"))))(Tile((id \
+         ccb5478b-987f-4364-8290-873db5c6ce1b)(label(from_lvs))(mold((out \
+         Exp)(in_())(nibs(((shape Convex)(sort Exp))((shape Convex)(sort \
+         Exp))))))(shards(0))(children())))(Tile((id \
+         ce8d0375-c6b7-4735-b875-0beaba96612b)(label(\"(\"\")\"))(mold((out \
+         Exp)(in_(Exp))(nibs(((shape(Concave 23))(sort Exp))((shape \
+         Convex)(sort Exp))))))(shards(0 1))(children(((Tile((id \
+         eb0d87d8-aed0-4f1f-b079-a6aecd5474f5)(label([ ]))(mold((out \
+         Exp)(in_(Exp))(nibs(((shape Convex)(sort Exp))((shape Convex)(sort \
+         Exp))))))(shards(0 1))(children(((Tile((id \
+         1939e804-2b76-4677-a72d-783de0df6c08)(label(\"(\"\")\"))(mold((out \
+         Exp)(in_(Exp))(nibs(((shape Convex)(sort Exp))((shape Convex)(sort \
+         Exp))))))(shards(0 1))(children(((Tile((id \
+         47a93940-5640-4da6-af49-40b527626208)(label(label))(mold((out \
+         Exp)(in_())(nibs(((shape Convex)(sort Exp))((shape Convex)(sort \
+         Exp))))))(shards(0))(children())))(Tile((id \
+         088c26b1-f774-42e8-8e19-1e2798fb18d8)(label(=))(mold((out \
+         Exp)(in_())(nibs(((shape(Concave 39))(sort Exp))((shape(Concave \
+         39))(sort Exp))))))(shards(0))(children())))(Tile((id \
+         ec28e481-eb56-4282-b236-23e09e7a1e72)(label(\"\\\"a\\\"\"))(mold((out \
+         Exp)(in_())(nibs(((shape Convex)(sort Exp))((shape Convex)(sort \
+         Exp))))))(shards(0))(children())))(Tile((id \
+         db6c6eed-9645-4331-ac34-72c9e9b8d3e7)(label(,))(mold((out \
+         Exp)(in_())(nibs(((shape(Concave 44))(sort Exp))((shape(Concave \
+         44))(sort Exp))))))(shards(0))(children())))(Secondary((id \
+         d6b8fe43-d30f-48e7-a5a2-faa94665fb8d)(content(Whitespace\" \
+         \"))))(Tile((id \
+         9ae68c01-bfa9-40da-a68d-8804cc0b1977)(label(value))(mold((out \
+         Exp)(in_())(nibs(((shape Convex)(sort Exp))((shape Convex)(sort \
+         Exp))))))(shards(0))(children())))(Tile((id \
+         b63751c0-397d-4445-a1a7-02cbf98800bd)(label(=))(mold((out \
+         Exp)(in_())(nibs(((shape(Concave 39))(sort Exp))((shape(Concave \
+         39))(sort Exp))))))(shards(0))(children())))(Tile((id \
+         27635fe8-33ea-4242-bd06-716d93017e57)(label(a))(mold((out \
+         Exp)(in_())(nibs(((shape Convex)(sort Exp))((shape Convex)(sort \
+         Exp))))))(shards(0))(children()))))))))(Tile((id \
+         5af1b488-24e3-4efe-9106-0624bb514b47)(label(,))(mold((out \
+         Exp)(in_())(nibs(((shape(Concave 44))(sort Exp))((shape(Concave \
+         44))(sort Exp))))))(shards(0))(children())))(Secondary((id \
+         85372a1f-9c71-47a8-9ffb-0ebca6237106)(content(Whitespace\"\\n\"))))(Secondary((id \
+         e9f33122-bbb9-403d-8074-b50a784352da)(content(Whitespace\" \
+         \"))))(Secondary((id \
+         0cde39bc-5fb3-4b16-8c5e-f3c39f4278e6)(content(Whitespace\" \
+         \"))))(Secondary((id \
+         dd3bcbe8-73dd-4147-a3b6-14af740e3c8f)(content(Whitespace\" \
+         \"))))(Secondary((id \
+         14c6bfcd-5eb2-45ea-9e29-977d17fa78b4)(content(Whitespace\" \
+         \"))))(Secondary((id \
+         caced31d-22ce-4aa9-9e89-3f41a43defe9)(content(Whitespace\" \
+         \"))))(Secondary((id \
+         82afef74-1241-4ff7-87d6-14cf403aaa46)(content(Whitespace\" \
+         \"))))(Secondary((id \
+         78f8a0d0-f346-46cf-b1bf-795c1617c4df)(content(Whitespace\" \
+         \"))))(Secondary((id \
+         e972d74c-6279-4fc4-b2e0-04c7413df24d)(content(Whitespace\" \
+         \"))))(Secondary((id \
+         ab49805c-087f-4498-809d-1f363cbdd90b)(content(Whitespace\" \
+         \"))))(Secondary((id \
+         f80a1b2e-2bef-46ad-b59f-9418e6136672)(content(Whitespace\" \
+         \"))))(Secondary((id \
+         4bac5aa5-68c2-4620-abe3-9e67287e2dcf)(content(Whitespace\" \
+         \"))))(Secondary((id \
+         b77ec293-d674-4e42-bee3-9cfabb88d4b6)(content(Whitespace\" \
+         \"))))(Secondary((id \
+         c3d49f6d-6add-4406-9647-f5e1873c4c45)(content(Whitespace\" \
+         \"))))(Secondary((id \
+         d7a9e69b-9c95-4b7b-8cca-4238fec1a828)(content(Whitespace\" \
+         \"))))(Secondary((id \
+         07d338d0-c882-46ce-b769-5424ae49d1ab)(content(Whitespace\" \
+         \"))))(Secondary((id \
+         8eca16ec-40f5-46f0-abe7-7f3d42168cd5)(content(Whitespace\" \
+         \"))))(Tile((id \
+         c06c19bf-6643-470e-a231-f61b9d0cd45d)(label(\"(\"\")\"))(mold((out \
+         Exp)(in_(Exp))(nibs(((shape Convex)(sort Exp))((shape Convex)(sort \
+         Exp))))))(shards(0 1))(children(((Tile((id \
+         c6e2b858-df98-4198-b6af-9e072575cc94)(label(label))(mold((out \
+         Exp)(in_())(nibs(((shape Convex)(sort Exp))((shape Convex)(sort \
+         Exp))))))(shards(0))(children())))(Tile((id \
+         1605e2b8-9895-489f-87a7-45dda5b024bd)(label(=))(mold((out \
+         Exp)(in_())(nibs(((shape(Concave 39))(sort Exp))((shape(Concave \
+         39))(sort Exp))))))(shards(0))(children())))(Tile((id \
+         bdd44f66-5f25-4492-88b8-8cd8e96d0969)(label(\"\\\"b\\\"\"))(mold((out \
+         Exp)(in_())(nibs(((shape Convex)(sort Exp))((shape Convex)(sort \
+         Exp))))))(shards(0))(children())))(Tile((id \
+         3cfac31e-124c-4889-b4b0-2a924c705a43)(label(,))(mold((out \
+         Exp)(in_())(nibs(((shape(Concave 44))(sort Exp))((shape(Concave \
+         44))(sort Exp))))))(shards(0))(children())))(Secondary((id \
+         81561d5b-83a9-474b-9061-87f6987ac236)(content(Whitespace\" \
+         \"))))(Tile((id \
+         a5c7f241-2cb5-439d-92da-5f2219faa388)(label(value))(mold((out \
+         Exp)(in_())(nibs(((shape Convex)(sort Exp))((shape Convex)(sort \
+         Exp))))))(shards(0))(children())))(Tile((id \
+         beafa075-68be-47fa-a508-e7d24b671f72)(label(=))(mold((out \
+         Exp)(in_())(nibs(((shape(Concave 39))(sort Exp))((shape(Concave \
+         39))(sort Exp))))))(shards(0))(children())))(Tile((id \
+         dadcc25f-887f-440b-aca4-69eb1ea74396)(label(b))(mold((out \
+         Exp)(in_())(nibs(((shape Convex)(sort Exp))((shape Convex)(sort \
+         Exp))))))(shards(0))(children()))))))))))))))))))(Secondary((id \
+         c93065af-c949-4c8d-b96e-e32a41432bdc)(content(Whitespace\" \
+         \")))))))))(Secondary((id \
          fc419efe-9b69-43d5-a8ec-2711a99cef14)(content(Whitespace\"\\n\"))))(Tile((id \
          35a67ab1-de80-4647-8ff3-35d78ece4ac1)(label(b))(mold((out \
          Exp)(in_())(nibs(((shape Convex)(sort Exp))((shape Convex)(sort \
@@ -2306,13 +2422,18 @@ let out : string * Haz3lcore.PersistentSegment.t =
          test ^^probe(new_frunk(4)) == 314 end;\n\
          test ^^probe(new_frunk(6)) == 330 end;\n\n\
          # STATICS PROBES: These show inferred type information. #\n\
-         # Double clicking toggles from analytic to synthetic type. #\n\n\
+         # Double clicking toggles between analytic type, synthetic type, #\n\
+         # and dynamic type. For dynamic type the dynamic component is shown \
+         in green. #\n\n\
          let a: Bool = ^^statics(1) in\n\
          let b: Bool = ^^statics(true) in \n\
          let c: (String, ?) = ^^statics((?, 1)) in\n\
+         let d = ^^statics(from_lvs([(label=\"a\", value=a),\n\
+        \                (label=\"b\", value=b)])) in\n\
          b";
       refractors =
-        "((01b8885d-2bb0-4d1b-89df-d1723fcc919f((kind \
+        "((ce8d0375-c6b7-4735-b875-0beaba96612b((kind Statics)(model \
+         Dynamic)))(01b8885d-2bb0-4d1b-89df-d1723fcc919f((kind \
          Probe)(model\"()\")))(0626cd00-4c2d-426c-988a-ff577e24b50c((kind \
          Probe)(model\"()\")))(07e0c1c5-957e-4eaa-8ec8-187588fc3595((kind \
          Statics)(model Self)))(161e5fc2-1c02-4cf6-b2bc-88aa38334dbe((kind \
diff --git a/src/web/view/ContextInspector.re b/src/web/view/ContextInspector.re
index 179b72cd68..f1ced55fbe 100644
--- a/src/web/view/ContextInspector.re
+++ b/src/web/view/ContextInspector.re
@@ -21,6 +21,7 @@ let context_entry_view = (~globals, entry: Language.Ctx.entry): Node.t => {
         hide_fixpoints: false,
         show_filters: false,
         show_unknown_as_hole: true,
+        raise_if_padding: false,
       },
     );
   let div_name = div(~attrs=[clss(["name"])]);
diff --git a/src/web/view/Kind.re b/src/web/view/Kind.re
index 6ad892b5d3..6e72610fae 100644
--- a/src/web/view/Kind.re
+++ b/src/web/view/Kind.re
@@ -20,6 +20,7 @@ let view = (~globals, kind: Language.Ctx.kind): Node.t =>
             hide_fixpoints: false,
             show_filters: false,
             show_unknown_as_hole: true,
+            raise_if_padding: false,
           },
           ty,
         ),
diff --git a/src/web/www/style/projectors/proj-type.css b/src/web/www/style/projectors/proj-type.css
index b382205963..fcc4c37ecb 100644
--- a/src/web/www/style/projectors/proj-type.css
+++ b/src/web/www/style/projectors/proj-type.css
@@ -96,6 +96,11 @@
   color: white;
 }
 
+/* Display live typing part of type as green */
+.dynamic > .token.Typ {
+  color: green;
+}
+
 /* REFRACTOR MODE */
 /* When Type is used as a refractor (skip_inline=true), hide backing */
 .refractors .base .projector.statics > svg {
diff --git a/test/Test_ExpToSegment.re b/test/Test_ExpToSegment.re
index b9cd5d3bc2..f8727478ea 100644
--- a/test/Test_ExpToSegment.re
+++ b/test/Test_ExpToSegment.re
@@ -14,6 +14,7 @@ let exp_to_segment_settings: ExpToSegment.Settings.t = {
   hide_fixpoints: false,
   show_filters: true,
   show_unknown_as_hole: true,
+  raise_if_padding: false,
 };
 
 let exp_to_segment =
@@ -440,6 +441,7 @@ let exp_to_segment_roundtrip_settings: ExpToSegment.Settings.t = {
   hide_fixpoints: false,
   show_filters: true,
   show_unknown_as_hole: true,
+  raise_if_padding: false,
 };
 
 let exp_to_segment_roundtrip =
@@ -1018,6 +1020,7 @@ let grout_structural_settings: ExpToSegment.Settings.t = {
   hide_fixpoints: false,
   show_filters: true,
   show_unknown_as_hole: true,
+  raise_if_padding: false,
 };
 
 /* String-to-string grout tests: parse strings, verify round-trip preserves text.
diff --git a/test/Test_Menhir.re b/test/Test_Menhir.re
index 53ccbbb96b..07a94877d3 100644
--- a/test/Test_Menhir.re
+++ b/test/Test_Menhir.re
@@ -171,6 +171,7 @@ let qcheck_menhir_serialized_equivalent_test =
             hide_fixpoints: false,
             show_filters: true,
             show_unknown_as_hole: true,
+            raise_if_padding: false,
           },
           core_exp,
         );
diff --git a/test/Test_PadIds.re b/test/Test_PadIds.re
new file mode 100644
index 0000000000..fa0437ceba
--- /dev/null
+++ b/test/Test_PadIds.re
@@ -0,0 +1,35 @@
+open Haz3lcore;
+
+let qcheck_pads_typ_for_exp_to_segment =
+  QCheck.Test.make(
+    ~name="No ids are needed to be padded during ExpToSegment",
+    ~count=1000,
+    QCheck_Util.arb_typ(~minimal_idents=false, 30),
+    typ => {
+      let padded = PadIds.pad_typ_ids(typ);
+      let _ =
+        ExpToSegment.typ_to_segment(
+          ~settings={
+            secondary: AutoFormat,
+            parenthesization: Defensive,
+            label_format: QuoteWhenNecessary,
+            inline: false,
+            fold_case_clauses: false,
+            fold_fn_bodies: `NoFold,
+            hide_fixpoints: false,
+            show_filters: true,
+            show_unknown_as_hole: true,
+            raise_if_padding: true // Will raise an exception if padding
+          },
+          padded,
+        );
+      Language.Equality.syntactic.typ(padded, PadIds.pad_typ_ids(padded));
+    },
+  );
+
+let tests = [
+  (
+    "PadIds",
+    [QCheck_alcotest.to_alcotest(qcheck_pads_typ_for_exp_to_segment)],
+  ),
+];
diff --git a/test/Test_Typ.re b/test/Test_Typ.re
index c23ff83b8b..63cab7b44c 100644
--- a/test/Test_Typ.re
+++ b/test/Test_Typ.re
@@ -195,5 +195,161 @@ let fast_equal_tests = (
     ),
   ],
 );
+let testable_id = testable(Fmt.using(Id.show, Fmt.string), (==));
+let diff_tests = (
+  "Typ.diff",
+  [
+    QCheck_alcotest.to_alcotest(
+      QCheck.Test.make(
+        ~name="diff identity",
+        ~count=1000,
+        QCheck_Util.arb_typ(~minimal_idents=true, 7),
+        typ =>
+        Typ.diff(typ, typ) == []
+      ),
+    ),
+    test_case(
+      "diff root different atom types",
+      `Quick,
+      () => {
+        let int_typ = Typ.fresh(Atom(Atom.Int));
+        let float_typ = Typ.fresh(Atom(Atom.Float));
+        let expected = [Typ.rep_id(float_typ)];
+        check(
+          list(testable_id),
+          "diff on different atom types",
+          expected,
+          Typ.diff(int_typ, float_typ),
+        );
+      },
+    ),
+    test_case(
+      "diff arrow different codomain",
+      `Quick,
+      () => {
+        let int_typ = Typ.fresh(Atom(Atom.Int));
+        let float_typ = Typ.fresh(Atom(Atom.Float));
+        let arrow1 = Typ.fresh(Arrow(int_typ, int_typ));
+        let arrow2 = Typ.fresh(Arrow(int_typ, float_typ));
+        let expected = [Typ.rep_id(float_typ)];
+        check(
+          list(testable_id),
+          "diff on arrows with different codomains",
+          expected,
+          Typ.diff(arrow1, arrow2),
+        );
+      },
+    ),
+    test_case(
+      "diff list different element",
+      `Quick,
+      () => {
+        let int_typ = Typ.fresh(Atom(Atom.Int));
+        let float_typ = Typ.fresh(Atom(Atom.Float));
+        let list1 = Typ.fresh(List(int_typ));
+        let list2 = Typ.fresh(List(float_typ));
+        let expected = [Typ.rep_id(float_typ)];
+        check(
+          list(testable_id),
+          "diff on lists with different elements",
+          expected,
+          Typ.diff(list1, list2),
+        );
+      },
+    ),
+    test_case(
+      "diff arrow different domain",
+      `Quick,
+      () => {
+        let int_typ = Typ.fresh(Atom(Atom.Int));
+        let float_typ = Typ.fresh(Atom(Atom.Float));
+        let string_typ = Typ.fresh(Atom(Atom.String));
+        let arrow1 = Typ.fresh(Arrow(int_typ, string_typ));
+        let arrow2 = Typ.fresh(Arrow(float_typ, string_typ));
+        let expected = [Typ.rep_id(float_typ)];
+        check(
+          list(testable_id),
+          "diff on arrows with different domains",
+          expected,
+          Typ.diff(arrow1, arrow2),
+        );
+      },
+    ),
+    test_case(
+      "(Int, a) ~ (Int, String)",
+      `Quick,
+      () => {
+        let int_typ = Typ.fresh(Atom(Atom.Int));
+        let string_typ = Typ.fresh(Atom(Atom.String));
+        let var_a = Typ.fresh(Var("a"));
+        let expected = [Typ.rep_id(string_typ)];
+        check(
+          list(testable_id),
+          "diff on (Int, a) ~ (Int, String)",
+          expected,
+          Typ.diff(
+            Typ.fresh(Prod([int_typ, var_a])),
+            Typ.fresh(Prod([int_typ, string_typ])),
+          ),
+        );
+      },
+    ),
+    test_case(
+      "diff var different names",
+      `Quick,
+      () => {
+        let var1 = Typ.fresh(Var("x"));
+        let var2 = Typ.fresh(Var("y"));
+        let expected = [Typ.rep_id(var2)];
+        check(
+          list(testable_id),
+          "diff on vars with different names",
+          expected,
+          Typ.diff(var1, var2),
+        );
+      },
+    ),
+    test_case(
+      "Recursive types with same tpat and type",
+      `Quick,
+      () => {
+        let tpat_x = TPat.fresh(Var("x"));
+        let var_x = Typ.fresh(Var("x"));
+        let rec1 = Typ.fresh(Rec(tpat_x, var_x));
+        let rec2 = Typ.fresh(Rec(tpat_x, var_x));
+        let expected = [];
+        check(
+          list(testable_id),
+          "diff on recursive types with same tpats",
+          expected,
+          Typ.diff(rec1, rec2),
+        );
+      },
+    ),
+    test_case(
+      "Recursive types with different tpats",
+      `Quick,
+      () => {
+        let rec1 =
+          Typ.fresh(Rec(TPat.fresh(Var("x")), Typ.fresh(Var("x"))));
+        let tpat_y = TPat.fresh(Var("y"));
+        let var_y = Typ.fresh(Var("y"));
+        let rec2 = Typ.fresh(Rec(tpat_y, var_y));
+
+        let expected = [
+          TPat.rep_id(tpat_y),
+          Typ.rep_id(var_y),
+          Typ.rep_id(rec2),
+        ];
+        check(
+          list(testable_id),
+          "diff on recursive types with different tpats",
+          expected,
+          Typ.diff(rec1, rec2),
+        );
+      },
+    ),
+  ],
+);
 
-let tests = [meet_tests, fast_equal_tests];
+let tests = [meet_tests, fast_equal_tests, diff_tests];
diff --git a/test/dune b/test/dune
index 7c65972125..39ba484629 100644
--- a/test/dune
+++ b/test/dune
@@ -5,4 +5,4 @@
  (libraries web menhirParser junit_alcotest bisect_ppx.runtime)
  (modes js)
  (preprocess
-  (pps ppx_deriving.show)))
+  (pps ppx_deriving.show ppx_sexp_conv)))
diff --git a/test/haz3ltest.re b/test/haz3ltest.re
index 07ed85106b..158559f46a 100644
--- a/test/haz3ltest.re
+++ b/test/haz3ltest.re
@@ -34,6 +34,7 @@ let (suite, _) =
     @ Test_Elaboration.tests
     @ Test_Evaluator.tests
     @ Test_Editing.tests
+    @ Test_PadIds.tests
     @ Test_AutoProbe.tests
     @ Test_Indentation.tests
     @ [Test_Coverage.tests, Test_Unboxing.tests]