diff --git a/src/haz3lcore/dynamics/DHExp.re b/src/haz3lcore/dynamics/DHExp.re
index e8b46575d0..8459118a07 100644
--- a/src/haz3lcore/dynamics/DHExp.re
+++ b/src/haz3lcore/dynamics/DHExp.re
@@ -69,7 +69,7 @@ let rec strip_casts =
         | Filter(_)
         | Let(_)
         | FixF(_)
-        | TyAlias(_)
+        | TyDef(_)
         | Fun(_)
         | Ap(_)
         | Deferral(_)
@@ -159,7 +159,7 @@ let ty_subst = (s: Typ.t, tpat: TPat.t, exp: t): t => {
           | FailedCast(_, _, _)
           | MultiHole(_)
           | Deferral(_)
-          | TyAlias(_)
+          | TyDef(_)
           | DeferredAp(_)
           | Parens(_)
           | UnOp(_) => continue(exp)
diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re
index 61fd72f1bd..b4f4f0d7d7 100644
--- a/src/haz3lcore/dynamics/FilterMatcher.re
+++ b/src/haz3lcore/dynamics/FilterMatcher.re
@@ -328,9 +328,9 @@ let rec matches_exp =
 
     | (Undefined, _) => false
 
-    | (TyAlias(dtp, dut, dd), TyAlias(ftp, fut, fd)) =>
+    | (TyDef(dtp, dut, dd), TyDef(ftp, fut, fd)) =>
       dtp == ftp && dut == fut && matches_exp(dd, fd)
-    | (TyAlias(_), _) => false
+    | (TyDef(_), _) => false
     };
   };
 }
diff --git a/src/haz3lcore/dynamics/Substitution.re b/src/haz3lcore/dynamics/Substitution.re
index 73c46ff6f5..43bfa48441 100644
--- a/src/haz3lcore/dynamics/Substitution.re
+++ b/src/haz3lcore/dynamics/Substitution.re
@@ -141,9 +141,9 @@ let rec subst_var = (m, d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t => {
     let d5' = subst_var(m, d1, x, d5);
     let d6' = subst_var(m, d1, x, d6);
     If(d4', d5', d6') |> rewrap;
-  | TyAlias(tp, ut, d4) =>
+  | TyDef(tp, ut, d4) =>
     let d4' = subst_var(m, d1, x, d4);
-    TyAlias(tp, ut, d4') |> rewrap;
+    TyDef(tp, ut, d4') |> rewrap;
   | Parens(d4) =>
     let d4' = subst_var(m, d1, x, d4);
     Parens(d4') |> rewrap;
diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re
index d46b40f7db..a9bcf5b9d6 100644
--- a/src/haz3lcore/dynamics/Transition.re
+++ b/src/haz3lcore/dynamics/Transition.re
@@ -726,7 +726,7 @@ module Transition = (EV: EV_MODE) => {
     | Parens(d) =>
       let. _ = otherwise(env, d);
       Step({expr: d, state_update, kind: RemoveParens, is_value: false});
-    | TyAlias(_, _, d) =>
+    | TyDef(_, _, d) =>
       let. _ = otherwise(env, d);
       Step({expr: d, state_update, kind: RemoveTypeAlias, is_value: false});
     | Filter(f1, d1) =>
diff --git a/src/haz3lcore/dynamics/TypeAssignment.re b/src/haz3lcore/dynamics/TypeAssignment.re
index 59b58aa56f..8b9fe27e44 100644
--- a/src/haz3lcore/dynamics/TypeAssignment.re
+++ b/src/haz3lcore/dynamics/TypeAssignment.re
@@ -343,7 +343,7 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) =>
     } else {
       None;
     };
-  | TyAlias(_, _, d) => typ_of_dhexp(ctx, m, d)
+  | TyDef(_, _, d) => typ_of_dhexp(ctx, m, d)
   | Parens(d) => typ_of_dhexp(ctx, m, d)
   };
 };
diff --git a/src/haz3lcore/dynamics/Unboxing.re b/src/haz3lcore/dynamics/Unboxing.re
index 07bde372b3..ef423f41df 100644
--- a/src/haz3lcore/dynamics/Unboxing.re
+++ b/src/haz3lcore/dynamics/Unboxing.re
@@ -223,7 +223,7 @@ let rec unbox: type a. (unbox_request(a), DHExp.t) => unboxed(a) =
         Let(_) |
         Fun(_, _, _, None) |
         FixF(_) |
-        TyAlias(_) |
+        TyDef(_) |
         Ap(_) |
         If(_) |
         Seq(_) |
diff --git a/src/haz3lcore/lang/term/TPat.re b/src/haz3lcore/lang/term/TPat.re
index 583f805851..17cc97ac66 100644
--- a/src/haz3lcore/lang/term/TPat.re
+++ b/src/haz3lcore/lang/term/TPat.re
@@ -3,6 +3,7 @@ type cls =
   | Invalid
   | EmptyHole
   | MultiHole
+  | Ap
   | Var;
 
 include TermBase.TPat;
@@ -21,11 +22,13 @@ let cls_of_term: term => cls =
   | Invalid(_) => Invalid
   | EmptyHole => EmptyHole
   | MultiHole(_) => MultiHole
-  | Var(_) => Var;
+  | Var(_) => Var
+  | Ap(_, _) => Ap;
 
 let show_cls: cls => string =
   fun
   | Invalid => "Invalid type alias"
   | MultiHole => "Broken type alias"
   | EmptyHole => "Empty type alias hole"
+  | Ap => "Type substitution"
   | Var => "Type alias";
diff --git a/src/haz3lcore/lang/term/Typ.re b/src/haz3lcore/lang/term/Typ.re
index 0647ef1865..3689a46f63 100644
--- a/src/haz3lcore/lang/term/Typ.re
+++ b/src/haz3lcore/lang/term/Typ.re
@@ -514,6 +514,11 @@ let rec needs_parens = (ty: t): bool =>
 let pretty_print_tvar = (tv: TPat.t): string =>
   switch (IdTagged.term_of(tv)) {
   | Var(x) => x
+  | Ap(_, x) =>
+    switch (x) {
+    | Var(y) => y
+    | _ => "?" //double check for doubly recursive types? maybe?
+    }
   | Invalid(_)
   | EmptyHole
   | MultiHole(_) => "?"
diff --git a/src/haz3lcore/pretty/ExpToSegment.re b/src/haz3lcore/pretty/ExpToSegment.re
index a0b185c67e..9196ccf334 100644
--- a/src/haz3lcore/pretty/ExpToSegment.re
+++ b/src/haz3lcore/pretty/ExpToSegment.re
@@ -310,7 +310,7 @@ let rec exp_to_pretty = (~settings: Settings.t, exp: Exp.t): pretty => {
     [mk_form("fix", id, [p])]
     @ e
     |> fold_fun_if(settings.fold_fn_bodies, name);
-  | TyAlias(tp, t, e) =>
+  | TyDef(tp, t, e) =>
     // TODO: Add optional newlines
     let id = exp |> Exp.rep_id;
     let+ tp = tpat_to_pretty(~settings: Settings.t, tp)
@@ -730,7 +730,7 @@ let rec external_precedence = (exp: Exp.t): Precedence.t => {
 
   // Top-level things
   | Filter(_)
-  | TyAlias(_)
+  | TyDef(_)
   | Let(_) => Precedence.let_
 
   // Matt: I think multiholes are min because we don't know the precedence of the `⟩?⟨`s
@@ -885,8 +885,8 @@ let rec parenthesize = (~show_filters: bool, exp: Exp.t): Exp.t => {
       c // TODO: Parenthesize through closure
     )
     |> rewrap
-  | TyAlias(tp, t, e) =>
-    TyAlias(
+  | TyDef(tp, t, e) =>
+    TyDef(
       tp,
       parenthesize_typ(t) |> paren_typ_at(Precedence.min),
       parenthesize(e) |> paren_assoc_at(Precedence.let_),
diff --git a/src/haz3lcore/statics/Elaborator.re b/src/haz3lcore/statics/Elaborator.re
index b46bc6967f..52d67a5501 100644
--- a/src/haz3lcore/statics/Elaborator.re
+++ b/src/haz3lcore/statics/Elaborator.re
@@ -314,7 +314,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: Exp.t): (DHExp.t, Typ.t) => {
       let (p', typ) = elaborate_pattern(m, p);
       let (e', tye) = elaborate(m, e);
       FixF(p', fresh_cast(e', tye, typ), env) |> rewrap |> cast_from(typ);
-    | TyAlias(_, _, e) =>
+    | TyDef(_, _, e) =>
       let (e', tye) = elaborate(m, e);
       e' |> cast_from(tye);
     | Ap(dir, f, a) =>
diff --git a/src/haz3lcore/statics/Info.re b/src/haz3lcore/statics/Info.re
index e8769ac892..26b54390fc 100644
--- a/src/haz3lcore/statics/Info.re
+++ b/src/haz3lcore/statics/Info.re
@@ -170,7 +170,7 @@ type type_var_err =
 [@deriving (show({with_path: false}), sexp, yojson)]
 type shadow_src =
   | BaseTyp
-  | TyAlias
+  | TyDef
   | TyVar;
 
 /* Type pattern term errors */
@@ -183,7 +183,8 @@ type error_tpat =
 [@deriving (show({with_path: false}), sexp, yojson)]
 type ok_tpat =
   | Empty
-  | Var(string);
+  | Var(string)
+  | Ap(string, string);
 
 [@deriving (show({with_path: false}), sexp, yojson)]
 type status_tpat =
@@ -502,13 +503,28 @@ let status_tpat = (ctx: Ctx.t, utpat: TPat.t): status_tpat =>
     if (Form.is_base_typ(name)) {
       f(BaseTyp);
     } else if (Ctx.is_alias(ctx, name)) {
-      f(TyAlias);
+      f(TyDef);
     } else {
       f(TyVar);
     };
   | Var(name) => NotInHole(Var(name))
   | Invalid(_) => InHole(NotAVar(NotCapitalized))
   | MultiHole(_) => InHole(NotAVar(Other))
+  | Ap(arg1, arg2) =>
+    switch (arg1, arg2) {
+    | (Var(name), _)
+        when Form.is_base_typ(name) || Ctx.lookup_alias(ctx, name) != None =>
+      let f = src => InHole(ShadowsType(name, src));
+      if (Form.is_base_typ(name)) {
+        f(BaseTyp);
+      } else if (Ctx.is_alias(ctx, name)) {
+        f(TyDef);
+      } else {
+        f(TyVar);
+      };
+    | (Var(x), Var(y)) => NotInHole(Ap(x, y))
+    | _ => InHole(NotAVar(Other))
+    }
   };
 
 /* Determines whether any term is in an error hole. */
diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re
index 9c28029e00..9f8a8e6520 100644
--- a/src/haz3lcore/statics/MakeTerm.re
+++ b/src/haz3lcore/statics/MakeTerm.re
@@ -229,7 +229,7 @@ and exp_term: unsorted => (Exp.term, list(Id.t)) = {
         | (["debug", "in"], [Exp(filter)]) =>
           Filter(Filter({act: (Step, All), pat: filter}), r)
         | (["type", "=", "in"], [TPat(tpat), Typ(def)]) =>
-          TyAlias(tpat, def, r)
+          TyDef(tpat, def, r)
         | (["if", "then", "else"], [Exp(cond), Exp(conseq)]) =>
           If(cond, conseq, r)
         | _ => hole(tm)
diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
index 7165db11d8..c42db755c1 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -599,7 +599,7 @@ and uexp_to_info_map =
         (unwrapped_self, m);
       };
     add'(~self, ~co_ctx=CoCtx.union([scrut.co_ctx] @ e_co_ctxs), m);
-  | TyAlias(typat, utyp, body) =>
+  | TyDef(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) =>
@@ -660,6 +660,139 @@ and uexp_to_info_map =
         go'(~ctx, ~mode, body, m);
       let m = utyp_to_info_map(~ctx, ~ancestors, utyp, m) |> snd;
       add(~self=Just(ty_body), ~co_ctx, m);
+    | Ap(t1, t2) =>
+      let name =
+        switch (t1) {
+        | Var(s) => s
+        | _ => ""
+        };
+      let arg =
+        switch (t2) {
+        | Var(s) => s
+        | _ => ""
+        };
+      let utyp_without_ap = UTyp.remove_ap_in_def(name, arg, utyp);
+      let (ty_def, ctx_def, ctx_body) = {
+        let ty_pre =
+          UTyp.to_typ(
+            Ctx.extend_dummy_tvar(Ctx.extend_dummy_tvar(ctx, name), arg),
+            utyp,
+          );
+        switch (utyp.term) {
+        | Sum(_) when List.mem(name, Typ.free_vars(ty_pre)) =>
+          let ty_pre =
+            UTyp.to_typ(
+              Ctx.extend_dummy_tvar(Ctx.extend_dummy_tvar(ctx, name), arg),
+              utyp_without_ap,
+            );
+          let ty_rec = Typ.Rec("α", Typ.subst(Var("α"), name, ty_pre));
+          let ctx_def =
+            Ctx.extend_higher_kind(
+              ctx,
+              name,
+              arg,
+              UTPat.rep_id(typat),
+              ty_rec,
+            );
+          (ty_rec, ctx_def, ctx_def);
+        | _ => (
+            ty_pre,
+            Ctx.extend_higher_kind(
+              ctx,
+              name,
+              arg,
+              UTPat.rep_id(typat),
+              ty_pre,
+            ),
+            Ctx.extend_higher_kind(
+              ctx,
+              name,
+              arg,
+              UTPat.rep_id(typat),
+              ty_pre,
+            ),
+          )
+        };
+      };
+      let ctx_body = {
+        let ty_pre =
+          UTyp.to_typ(
+            Ctx.extend_dummy_tvar(Ctx.extend_dummy_tvar(ctx, name), arg),
+            utyp,
+          );
+
+        switch (ty_pre) {
+        | Sum(sm_map) =>
+          Ctx.add_ctr_with_typ_parameter(
+            ctx_body,
+            name,
+            UTyp.rep_id(utyp),
+            sm_map,
+            arg,
+          )
+        | _ => ctx_body
+        };
+      };
+      let ({co_ctx, ty: ty_body, _}: Info.exp, m) =
+        go'(~ctx=ctx_body, ~mode, body, m);
+      /* Make sure types don't escape their scope */
+      let ty_escape = Typ.subst(ty_def, name, ty_body);
+      let m = utyp_to_info_map(~ctx=ctx_def, ~ancestors, utyp, m) |> snd;
+      add(~self=Just(ty_escape), ~co_ctx, m);
+
+      //  let (ty_def, ctx_def, ctx_body) = {
+      //         switch (utyp.term) {
+      //         | Sum(_) when List.mem(name, Typ.free_vars(utyp)) =>
+      //           /* NOTE: When debugging type system issues it may be beneficial to
+      //              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;
+      //           let ctx_def =
+      //             Ctx.extend_alias(ctx, name, TPat.rep_id(typat), ty_rec);
+      //           (ty_rec, ctx_def, ctx_def);
+      //         | _ => (
+      //             utyp,
+      //             ctx,
+      //             Ctx.extend_alias(ctx, name, TPat.rep_id(typat), utyp),
+      //           )
+
+      let (ty_def, ctx_def, ctx_body) = {
+        switch (utyp.term) {
+        | Sum(_) when List.mem(constructor, Typ.free_vars(utyp)) =>
+          let ty_rec =
+            Rec((Var("α"): TPat.term) |> IdTagged.fresh, utyp) |> Typ.temp; //worried because
+          let ctx_def =
+            Ctx.extend_alias(ctx, constructor, TPat.rep_id(typat), ty_rec);
+          (ty_rec, ctx_def, ctx_def);
+
+        | _ =>
+          let ty = Typ.to_typ(ctx, utyp);
+          (
+            utyp, //not sure about the usage of utyp here
+            ctx,
+            Ctx.extend_alias(ctx, constructor, TPat.rep_id(typat), ty),
+          );
+        };
+      };
+      //Printf.printf(
+      //  "ty_def: %s, ctx_def: %s, ctx_body: %s \n",
+      //  Typ.show(ty_def),
+      //  Ctx.show(ctx_def),
+      //  Ctx.show(ctx_body),
+      //);
+      let ctx_body =
+        switch (Typ.get_sum_constructors(ctx, ty_def)) {
+        | Some(sm) =>
+          Ctx.add_ctrs(ctx_body, constructor, UTyp.rep_id(utyp), sm)
+        | None => ctx_body
+        };
+      let ({co_ctx, ty: ty_body, _}: Info.exp, m) =
+        go'(~ctx=ctx_body, ~mode, body, m);
+      /* Make sure types don't escape their scope */
+      let ty_escape = Typ.subst(ty_def, constructor, ty_body);
+      let m = utyp_to_info_map(~ctx=ctx_def, ~ancestors, utyp, m) |> snd;
+      add(~self=Just(ty_escape), ~co_ctx, m);
     };
   };
 }
diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re
index b19a5c73a5..572679eb28 100644
--- a/src/haz3lcore/statics/Term.re
+++ b/src/haz3lcore/statics/Term.re
@@ -317,7 +317,7 @@ module Exp = {
     | MetaVar
     | Let
     | FixF
-    | TyAlias
+    | TyDef
     | Ap
     | TypAp
     | DeferredAp
@@ -370,7 +370,7 @@ module Exp = {
     | Var(_) => Var
     | Let(_) => Let
     | FixF(_) => FixF
-    | TyAlias(_) => TyAlias
+    | TyDef(_) => TyDef
     | Ap(_) => Ap
     | TypAp(_) => TypAp
     | DeferredAp(_) => DeferredAp
@@ -411,7 +411,7 @@ module Exp = {
     | MetaVar => "Meta variable reference"
     | Let => "Let expression"
     | FixF => "Fixpoint operator"
-    | TyAlias => "Type Alias definition"
+    | TyDef => "Type Alias definition"
     | Ap => "Application"
     | TypAp => "Type application"
     | DeferredAp => "Partial Application"
@@ -455,7 +455,7 @@ module Exp = {
     | Var(_)
     | Let(_)
     | FixF(_)
-    | TyAlias(_)
+    | TyDef(_)
     | Ap(_)
     | TypAp(_)
     | DeferredAp(_)
@@ -499,7 +499,7 @@ module Exp = {
       | Var(_)
       | Let(_)
       | FixF(_)
-      | TyAlias(_)
+      | TyDef(_)
       | Ap(_)
       | TypAp(_)
       | DeferredAp(_)
@@ -557,7 +557,7 @@ module Exp = {
       | Var(_)
       | Let(_)
       | Filter(_)
-      | TyAlias(_)
+      | TyDef(_)
       | Ap(_)
       | TypAp(_)
       | DeferredAp(_)
@@ -723,7 +723,7 @@ module Exp = {
           | Constructor(_)
           | TypFun(_)
           | Tuple(_)
-          | TyAlias(_)
+          | TyDef(_)
           | Ap(_)
           | TypAp(_)
           | DeferredAp(_)
diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re
index e8c4b339f3..3ece456387 100644
--- a/src/haz3lcore/statics/TermBase.re
+++ b/src/haz3lcore/statics/TermBase.re
@@ -80,7 +80,7 @@ and exp_term =
   | Var(Var.t)
   | Let(pat_t, exp_t, exp_t)
   | FixF(pat_t, exp_t, option(closure_environment_t))
-  | TyAlias(tpat_t, typ_t, exp_t)
+  | TyDef(tpat_t, typ_t, exp_t)
   | Ap(Operators.ap_direction, exp_t, exp_t)
   | TypAp(exp_t, typ_t)
   | DeferredAp(exp_t, list(exp_t))
@@ -140,6 +140,7 @@ and tpat_term =
   | EmptyHole
   | MultiHole(list(any_t))
   | Var(string)
+  | Ap(tpat_term, tpat_term)
 and tpat_t = IdTagged.t(tpat_term)
 and rul_term =
   | Invalid(string)
@@ -316,8 +317,8 @@ and Exp: {
         | Let(p, e1, e2) =>
           Let(pat_map_term(p), exp_map_term(e1), exp_map_term(e2))
         | FixF(p, e, env) => FixF(pat_map_term(p), exp_map_term(e), env)
-        | TyAlias(tp, t, e) =>
-          TyAlias(tpat_map_term(tp), typ_map_term(t), exp_map_term(e))
+        | TyDef(tp, t, e) =>
+          TyDef(tpat_map_term(tp), typ_map_term(t), exp_map_term(e))
         | Ap(op, e1, e2) => Ap(op, exp_map_term(e1), exp_map_term(e2))
         | TypAp(e, t) => TypAp(exp_map_term(e), typ_map_term(t))
         | DeferredAp(e, es) =>
@@ -390,7 +391,7 @@ and Exp: {
       Pat.fast_equal(p1, p2)
       && fast_equal(e1, e2)
       && Option.equal(ClosureEnvironment.id_equal, c1, c2)
-    | (TyAlias(tp1, t1, e1), TyAlias(tp2, t2, e2)) =>
+    | (TyDef(tp1, t1, e1), TyDef(tp2, t2, e2)) =>
       TPat.fast_equal(tp1, tp2)
       && Typ.fast_equal(t1, t2)
       && fast_equal(e1, e2)
@@ -445,7 +446,7 @@ and Exp: {
     | (Var(_), _)
     | (Let(_), _)
     | (FixF(_), _)
-    | (TyAlias(_), _)
+    | (TyDef(_), _)
     | (Ap(_), _)
     | (TypAp(_), _)
     | (DeferredAp(_), _)
@@ -786,6 +787,7 @@ and TPat: {
         switch (term) {
         | EmptyHole
         | Invalid(_)
+        | Ap(_, _)
         | Var(_) => term
         | MultiHole(things) => MultiHole(List.map(any_map_term, things))
         },
@@ -807,6 +809,8 @@ and TPat: {
       List.length(xs) == List.length(ys)
       && List.equal(Any.fast_equal, xs, ys)
     | (Var(x), Var(y)) => x == y
+    | (Ap(t1, t2), Ap(t3, t4)) => t1 == t3 && t2 == t4
+    | (Ap(_, _), _)
     | (EmptyHole, _)
     | (Invalid(_), _)
     | (MultiHole(_), _)
diff --git a/src/haz3lcore/zipper/EditorUtil.re b/src/haz3lcore/zipper/EditorUtil.re
index a7225fe7c8..1f098fd5fa 100644
--- a/src/haz3lcore/zipper/EditorUtil.re
+++ b/src/haz3lcore/zipper/EditorUtil.re
@@ -41,9 +41,9 @@ let rec append_exp = (e1: Exp.t, e2: Exp.t): Exp.t => {
   | Let(p, edef, ebody) =>
     let ebody' = append_exp(ebody, e2);
     {ids: e1.ids, copied: false, term: Let(p, edef, ebody')};
-  | TyAlias(tp, tdef, ebody) =>
+  | TyDef(tp, tdef, ebody) =>
     let ebody' = append_exp(ebody, e2);
-    {ids: e1.ids, copied: false, term: TyAlias(tp, tdef, ebody')};
+    {ids: e1.ids, copied: false, term: TyDef(tp, tdef, ebody')};
   };
 };
 
diff --git a/src/haz3lcore/zipper/action/Select.re b/src/haz3lcore/zipper/action/Select.re
index f3d24af236..17c267acec 100644
--- a/src/haz3lcore/zipper/action/Select.re
+++ b/src/haz3lcore/zipper/action/Select.re
@@ -151,14 +151,14 @@ module Make = (M: Move.S) => {
       };
     let* ci_parent = statics_of(id);
     switch (Info.cls_of(ci_parent)) {
-    | Exp(Let | TyAlias) =>
+    | Exp(Let | TyDef) =>
       /* For definition-type forms, don't select the body,
        * unless the body is precisely what we're clicking on */
       switch (ci_parent) {
       | InfoExp({term: t, _}) =>
         switch (IdTagged.term_of(t)) {
         | Let(_, _, body)
-        | TyAlias(_, _, body) =>
+        | TyDef(_, _, body) =>
           let body_id = IdTagged.rep_id(body);
           base_id == body_id ? term(id, z) : tile(id, z);
         | _ => tile(id, z)
diff --git a/src/haz3lweb/app/explainthis/Example.re b/src/haz3lweb/app/explainthis/Example.re
index 9408167cf6..4a103fdc6a 100644
--- a/src/haz3lweb/app/explainthis/Example.re
+++ b/src/haz3lweb/app/explainthis/Example.re
@@ -113,7 +113,7 @@ let mk_fix = mk_tile(Form.get("fix"));
 let mk_ap_exp = mk_tile(Form.get("ap_exp"));
 let mk_ap_pat = mk_tile(Form.get("ap_pat"));
 let mk_let = mk_tile(Form.get("let_"));
-let mk_tyalias = mk_tile(Form.get("type_alias"));
+let mk_TyDef = mk_tile(Form.get("type_alias"));
 let mk_if = mk_tile(Form.get("if_"));
 let mk_test = mk_tile(Form.get("test"));
 let mk_case = mk_tile(Form.get("case"));
diff --git a/src/haz3lweb/app/explainthis/ExplainThis.re b/src/haz3lweb/app/explainthis/ExplainThis.re
index 3388bbb3ba..c705baa038 100644
--- a/src/haz3lweb/app/explainthis/ExplainThis.re
+++ b/src/haz3lweb/app/explainthis/ExplainThis.re
@@ -549,12 +549,12 @@ let get_doc =
       | BuiltinFun(_) => simple("Internal expression")
       | EmptyHole => get_message(HoleExp.empty_hole_exps)
       | MultiHole(_children) => get_message(HoleExp.multi_hole_exps)
-      | TyAlias(ty_pat, ty_def, _body) =>
+      | TyDef(ty_pat, ty_def, _body) =>
         let tpat_id = List.nth(ty_pat.ids, 0);
         let def_id = List.nth(ty_def.ids, 0);
         get_message(
           ~colorings=
-            TyAliasExp.tyalias_base_exp_coloring_ids(~tpat_id, ~def_id),
+            TyDefExp.TyDef_base_exp_coloring_ids(~tpat_id, ~def_id),
           ~format=
             Some(
               msg =>
@@ -564,7 +564,7 @@ let get_doc =
                   Id.to_string(tpat_id),
                 ),
             ),
-          TyAliasExp.tyalias_exps,
+          TyDefExp.TyDef_exps,
         );
       | Undefined => get_message(UndefinedExp.undefined_exps)
       | Deferral(_) => get_message(TerminalExp.deferral_exps)
diff --git a/src/haz3lweb/app/explainthis/ExplainThisForm.re b/src/haz3lweb/app/explainthis/ExplainThisForm.re
index a2291253e5..9bf5d0db68 100644
--- a/src/haz3lweb/app/explainthis/ExplainThisForm.re
+++ b/src/haz3lweb/app/explainthis/ExplainThisForm.re
@@ -183,7 +183,7 @@ type form_id =
   | UnOpExp(Operators.op_un)
   | BinOpExp(Operators.op_bin)
   | CaseExp
-  | TyAliasExp
+  | TyDefExp
   | EmptyHolePat
   | MultiHolePat
   | WildPat
@@ -276,7 +276,7 @@ type group_id =
   | UnOpExp(Operators.op_un)
   | BinOpExp(Operators.op_bin)
   | CaseExp
-  | TyAliasExp
+  | TyDefExp
   | PipelineExp
   | EmptyHolePat
   | MultiHolePat
diff --git a/src/haz3lweb/app/explainthis/data/TyAliasExp.re b/src/haz3lweb/app/explainthis/data/TyAliasExp.re
index 65cc234dfd..5237f3459c 100644
--- a/src/haz3lweb/app/explainthis/data/TyAliasExp.re
+++ b/src/haz3lweb/app/explainthis/data/TyAliasExp.re
@@ -4,19 +4,20 @@ open ExplainThisForm;
 
 let _tpat = tpat("p");
 let _typ_def = typ("ty_def");
-let tyalias_base_exp_coloring_ids = (~tpat_id: Id.t, ~def_id: Id.t) => [
-  (Piece.id(_tpat), tpat_id),
-  (Piece.id(_typ_def), def_id),
-];
-let tyalias_exp: form = {
+let TyDef_base_exp_coloring_ids =
+  (~tpat_id: Id.t, ~def_id: Id.t) => [
+    (Piece.id(_tpat), tpat_id),
+    (Piece.id(_typ_def), def_id),
+  ];
+let TyDef_exp: form = {
   let explanation = "The [*type*](%s) is bound to the [*type variable*](%s) in the body.";
   let form = [
-    mk_tyalias([[space(), _tpat, space()], [space(), _typ_def, space()]]),
+    mk_TyDef([[space(), _tpat, space()], [space(), _typ_def, space()]]),
     linebreak(),
     exp("e_body"),
   ];
   {
-    id: TyAliasExp,
+    id: TyDefExp,
     syntactic_form: form,
     expandable_id: None,
     explanation,
@@ -24,4 +25,4 @@ let tyalias_exp: form = {
   };
 };
 
-let tyalias_exps: group = {id: TyAliasExp, forms: [tyalias_exp]};
+let TyDef_exps: group = {id: TyDefExp, forms: [TyDef_exp]};
diff --git a/src/haz3lweb/app/inspector/CursorInspector.re b/src/haz3lweb/app/inspector/CursorInspector.re
index b33aec0586..90e8545c2d 100644
--- a/src/haz3lweb/app/inspector/CursorInspector.re
+++ b/src/haz3lweb/app/inspector/CursorInspector.re
@@ -339,7 +339,7 @@ let tpat_view = (~globals, _: Cls.t, status: Info.status_tpat) => {
       text("Can't shadow base type"),
       view_type(Var(name) |> Typ.fresh) |> code_box_container,
     ])
-  | InHole(ShadowsType(name, TyAlias)) =>
+  | InHole(ShadowsType(name, TyDef)) =>
     div_err([
       text("Can't shadow existing alias"),
       view_type(Var(name) |> Typ.fresh) |> code_box_container,
diff --git a/src/haz3lweb/exercises/SyntaxTest.re b/src/haz3lweb/exercises/SyntaxTest.re
index 9465ac6abf..6d5e5d3d88 100644
--- a/src/haz3lweb/exercises/SyntaxTest.re
+++ b/src/haz3lweb/exercises/SyntaxTest.re
@@ -93,7 +93,7 @@ let rec find_fn = (name: string, uexp: Exp.t, l: list(Exp.t)): list(Exp.t) => {
   | Parens(u1)
   | Cast(u1, _, _)
   | UnOp(_, u1)
-  | TyAlias(_, _, u1)
+  | TyDef(_, _, u1)
   | Test(u1)
   | Closure(_, u1)
   | Filter(_, u1) => l |> find_fn(name, u1)
@@ -191,7 +191,7 @@ let rec var_mention = (name: string, uexp: Exp.t): bool => {
   | Test(u)
   | Parens(u)
   | UnOp(_, u)
-  | TyAlias(_, _, u)
+  | TyDef(_, _, u)
   | Filter(_, u) => var_mention(name, u)
   | DynamicErrorHole(u, _) => var_mention(name, u)
   | FailedCast(u, _, _) => var_mention(name, u)
@@ -252,7 +252,7 @@ let rec var_applied = (name: string, uexp: Exp.t): bool => {
   | Test(u)
   | Parens(u)
   | UnOp(_, u)
-  | TyAlias(_, _, u)
+  | TyDef(_, _, u)
   | Filter(_, u) => var_applied(name, u)
   | TypAp(u, _) =>
     switch (u.term) {
@@ -342,7 +342,7 @@ let rec tail_check = (name: string, uexp: Exp.t): bool => {
     //If l has no recursive calls then true
     !List.fold_left((acc, ue) => {acc || var_mention(name, ue)}, false, l)
   | Test(_) => false
-  | TyAlias(_, _, u)
+  | TyDef(_, _, u)
   | Cast(u, _, _)
   | Filter(_, u)
   | Closure(_, u)
diff --git a/test/Test_MakeTerm.re b/test/Test_MakeTerm.re
index 003ce7ca65..873f609491 100644
--- a/test/Test_MakeTerm.re
+++ b/test/Test_MakeTerm.re
@@ -77,11 +77,7 @@ let tests = (
     }),
     test_case("Type Alias", `Quick, () => {
       exp_check(
-        TyAlias(
-          Var("x") |> TPat.fresh,
-          Int |> Typ.fresh,
-          Int(1) |> Exp.fresh,
-        )
+        TyDef(Var("x") |> TPat.fresh, Int |> Typ.fresh, Int(1) |> Exp.fresh)
         |> Exp.fresh,
         "type x = Int in 1",
       )