Try making all of the ids type parameters

src/haz3lcore/Measured.re

@@ -85,12 +85,12 @@ let add_s = (id: Id.t, i: int, m, map) => {
 };
 
 // assumes tile is single shard
-let add_t = (t: Tile.t, m, map) => {
+let add_t = (t: Tile.t(Id.t), m, map) => {
   ...map,
   tiles:
     map.tiles
     |> Id.Map.update(
-         t.id,
+         t.extra,
          fun
          | None => Some([(Tile.l_shard(t), m)])
          | Some(ms) => Some([(Tile.l_shard(t), m), ...ms]),
@@ -104,11 +104,11 @@ let add_w = (w: Secondary.t, m, map) => {
   ...map,
   secondary: map.secondary |> Id.Map.add(w.id, m),
 };
-let add_pr = (p: Base.projector, m, map) => {
+let add_pr = (p: Base.projector(Id.t), m, map) => {
   ...map,
-  projectors: map.projectors |> Id.Map.add(p.id, m),
+  projectors: map.projectors |> Id.Map.add(p.extra, m),
 };
-let add_p = (p: Piece.t, m, map) =>
+let add_p = (p: Piece.t(Id.t), m, map) =>
   p
   |> Piece.get(
        w => add_w(w, m, map),
@@ -141,9 +141,10 @@ let singleton_g = (g, m) => empty |> add_g(g, m);
 let singleton_s = (id, shard, m) => empty |> add_s(id, shard, m);
 
 // TODO(d) rename
-let find_opt_shards = (t: Tile.t, map) => Id.Map.find_opt(t.id, map.tiles);
-let find_shards = (~msg="", t: Tile.t, map) =>
-  try(Id.Map.find(t.id, map.tiles)) {
+let find_opt_shards = (t: Tile.t(Id.t), map) =>
+  Id.Map.find_opt(t.extra, map.tiles);
+let find_shards = (~msg="", t: Tile.t(Id.t), map) =>
+  try(Id.Map.find(t.extra, map.tiles)) {
   | _ => failwith("find_shards: " ++ msg)
   };
 
@@ -163,15 +164,15 @@ let find_g = (~msg="", g: Grout.t, map): measurement =>
   try(Id.Map.find(g.id, map.grout)) {
   | _ => failwith("find_g: " ++ msg)
   };
-let find_pr = (~msg="", p: Base.projector, map): measurement =>
-  try(Id.Map.find(p.id, map.projectors)) {
+let find_pr = (~msg="", p: Base.projector(Id.t), map): measurement =>
+  try(Id.Map.find(p.extra, map.projectors)) {
   | _ => failwith("find_g: " ++ msg)
   };
-let find_pr_opt = (p: Base.projector, map): option(measurement) =>
-  Id.Map.find_opt(p.id, map.projectors);
+let find_pr_opt = (p: Base.projector(Id.t), map): option(measurement) =>
+  Id.Map.find_opt(p.extra, map.projectors);
 // returns the measurement spanning the whole tile
-let find_t = (t: Tile.t, map): measurement => {
-  let shards = Id.Map.find(t.id, map.tiles);
+let find_t = (t: Tile.t(Id.t), map): measurement => {
+  let shards = Id.Map.find(t.extra, map.tiles);
   let (first, last) =
     try({
       let first = ListUtil.assoc_err(Tile.l_shard(t), shards, "find_t");
@@ -182,7 +183,7 @@ let find_t = (t: Tile.t, map): measurement => {
     };
   {origin: first.origin, last: last.last};
 };
-let find_p = (~msg="", p: Piece.t, map): measurement =>
+let find_p = (~msg="", p: Piece.t(Id.t), map): measurement =>
   try(
     p
     |> Piece.get(
@@ -228,7 +229,7 @@ let find_by_id = (id: Id.t, map: t): option(measurement) => {
   };
 };
 
-let post_tile_indent = (t: Tile.t) => {
+let post_tile_indent = (t: Tile.t(Id.t)) => {
   // hack for indent following fun/if tiles.
   // proper fix involves updating mold datatype
   // to specify whether a right-facing concave
@@ -244,13 +245,13 @@ let post_tile_indent = (t: Tile.t) => {
   complete_fun || missing_right_extreme;
 };
 
-let missing_left_extreme = (t: Tile.t) => Tile.l_shard(t) > 0;
+let missing_left_extreme = (t: Tile.t(Id.t)) => Tile.l_shard(t) > 0;
 
-let is_indented_map = (seg: Segment.t) => {
-  let rec go = (~is_indented=false, ~map=Id.Map.empty, seg: Segment.t) =>
+let is_indented_map = (seg: Segment.t(Id.t)) => {
+  let rec go = (~is_indented=false, ~map=Id.Map.empty, seg: Segment.t(Id.t)) =>
     seg
     |> List.fold_left(
-         ((is_indented, map), p: Piece.t) =>
+         ((is_indented, map), p: Piece.t(Id.t)) =>
            switch (p) {
            | Secondary(w) when Secondary.is_linebreak(w) => (
                false,
@@ -282,7 +283,7 @@ let last_of_token = (token: string, origin: Point.t): Point.t =>
     row: origin.row + StringUtil.num_linebreaks(token),
   };
 
-let of_segment = (seg: Segment.t, info_map: Statics.Map.t): t => {
+let of_segment = (seg: Segment.t(Id.t), info_map: Statics.Map.t): t => {
   let is_indented = is_indented_map(seg);
 
   // recursive across seg's bidelimited containers
@@ -291,7 +292,7 @@ let of_segment = (seg: Segment.t, info_map: Statics.Map.t): t => {
             ~map,
             ~container_indent: abs_indent=0,
             ~origin=Point.zero,
-            seg: Segment.t,
+            seg: Segment.t(Id.t),
           )
           : (Point.t, t) => {
     // recursive across seg's list structure
@@ -300,7 +301,7 @@ let of_segment = (seg: Segment.t, info_map: Statics.Map.t): t => {
               ~map,
               ~contained_indent: rel_indent=0,
               ~origin: Point.t,
-              seg: Segment.t,
+              seg: Segment.t(Id.t),
             )
             : (Point.t, t) =>
       switch (seg) {
@@ -354,7 +355,7 @@ let of_segment = (seg: Segment.t, info_map: Statics.Map.t): t => {
             (contained_indent, last, map);
           | Projector(p) =>
             let token =
-              Projector.placeholder(p, Id.Map.find_opt(p.id, info_map));
+              Projector.placeholder(p, Id.Map.find_opt(p.extra, info_map));
             let last = last_of_token(token, origin);
             let map = extra_rows(token, origin, map);
             let map = add_pr(p, {origin, last}, map);
@@ -364,7 +365,7 @@ let of_segment = (seg: Segment.t, info_map: Statics.Map.t): t => {
               let token = List.nth(t.label, shard);
               let map = extra_rows(token, origin, map);
               let last = last_of_token(token, origin);
-              let map = add_s(t.id, shard, {origin, last}, map);
+              let map = add_s(t.extra, shard, {origin, last}, map);
               (last, map);
             };
             let (last, map) =
@@ -392,7 +393,7 @@ let of_segment = (seg: Segment.t, info_map: Statics.Map.t): t => {
   snd(go_nested(~map=empty, seg));
 };
 
-let length = (seg: Segment.t, map: t): int =>
+let length = (seg: Segment.t(Id.t), map: t): int =>
   switch (seg) {
   | [] => 0
   | [p] =>

src/haz3lcore/TermMap.re

@@ -1,5 +1,5 @@
 include Id.Map;
-type t = Id.Map.t(Any.t);
+type t = Id.Map.t(Any.t(IdTag.t));
 
-let add_all = (ids: list(Id.t), tm: Any.t, map: t) =>
+let add_all = (ids: list(Id.t), tm: Any.t(IdTag.t), map: t) =>
   ids |> List.fold_left((map, id) => add(id, tm, map), map);

src/haz3lcore/TermRanges.re

@@ -1,7 +1,7 @@
 open Util;
 
 include Id.Map;
-type range = (Piece.t, Piece.t);
+type range = (Piece.t(Id.t), Piece.t(Id.t));
 type nonrec t = t(range);
 
 let union = union((_, range, _) => Some(range));
@@ -11,7 +11,7 @@ let union = union((_, range, _) => Some(range));
  * unmemoized traversal building a hashtbl avoiding unioning.
 
    TODO(andrew): Consider setting a limit for the hashtbl size */
-let range_hash: Hashtbl.t(Tile.segment, Id.Map.t(range)) =
+let range_hash: Hashtbl.t(Tile.segment(Id.t), Id.Map.t(range)) =
   Hashtbl.create(1000);
 
 // NOTE: this calculation is out of sync with
@@ -23,7 +23,7 @@ let range_hash: Hashtbl.t(Tile.segment, Id.Map.t(range)) =
 // TODO(d) fix or derive from other info
 //
 // tail-recursive in outer recursion
-let rec mk' = (seg: Segment.t) => {
+let rec mk' = (seg: Segment.t(Id.t)) => {
   let rec go = (skel: Skel.t): (range, t) => {
     let root = Skel.root(skel) |> Aba.map_a(List.nth(seg));
     let root_l = Aba.first_a(root);

src/haz3lcore/TileMap.re

@@ -1,13 +1,16 @@
 include Id.Map;
-type t = Id.Map.t(Tile.t);
+type t = Id.Map.t(Tile.t(Id.t));
 
 // tail-recursive
-let rec mk = (~map=empty, seg: Segment.t): t =>
+let rec mk = (~map=empty, seg: Segment.t(Id.t)): t =>
   Segment.tiles(seg)
   |> List.fold_left(
-       (map, t: Tile.t) => {
+       (map, t: Tile.t(Id.t)) => {
          t.children
-         |> List.fold_left((map, kid) => mk(~map, kid), add(t.id, t, map))
+         |> List.fold_left(
+              (map, kid) => mk(~map, kid),
+              add(t.extra, t, map),
+            )
        },
        map,
      );

src/haz3lcore/assistant/AssistantCtx.re

@@ -3,7 +3,12 @@ open Suggestion;
 /* For suggestions in patterns, suggest variables which
  * occur free in that pattern's scope. */
 let free_variables =
-    (expected_ty: Typ.t, ctx: Ctx.t, co_ctx: CoCtx.t): list(Suggestion.t) => {
+    (
+      expected_ty: Typ.t(IdTag.t),
+      ctx: Ctx.t(IdTag.t),
+      co_ctx: CoCtx.t(IdTag.t),
+    )
+    : list(Suggestion.t) => {
   List.filter_map(
     ((name, entries)) =>
       switch (Ctx.lookup_var(ctx, name)) {
@@ -21,7 +26,8 @@ let free_variables =
 };
 
 /* For suggestsions in expressions, suggest variables from the ctx */
-let bound_variables = (ty_expect: Typ.t, ctx: Ctx.t): list(Suggestion.t) =>
+let bound_variables =
+    (ty_expect: Typ.t(IdTag.t), ctx: Ctx.t(IdTag.t)): list(Suggestion.t) =>
   List.filter_map(
     fun
     | Ctx.VarEntry({typ, name, _})
@@ -32,7 +38,11 @@ let bound_variables = (ty_expect: Typ.t, ctx: Ctx.t): list(Suggestion.t) =>
   );
 
 let bound_constructors =
-    (wrap: strategy_common => strategy, ty: Typ.t, ctx: Ctx.t)
+    (
+      wrap: strategy_common => strategy,
+      ty: Typ.t(IdTag.t),
+      ctx: Ctx.t(IdTag.t),
+    )
     : list(Suggestion.t) =>
   /* get names of all constructor entries consistent with ty */
   List.filter_map(
@@ -45,7 +55,8 @@ let bound_constructors =
   );
 
 /* Suggest applying a function from the ctx which returns an appropriate type */
-let bound_aps = (ty_expect: Typ.t, ctx: Ctx.t): list(Suggestion.t) =>
+let bound_aps =
+    (ty_expect: Typ.t(IdTag.t), ctx: Ctx.t(IdTag.t)): list(Suggestion.t) =>
   List.filter_map(
     fun
     | Ctx.VarEntry({typ: {term: Arrow(_, ty_out), _} as ty_arr, name, _})
@@ -61,7 +72,8 @@ let bound_aps = (ty_expect: Typ.t, ctx: Ctx.t): list(Suggestion.t) =>
     ctx,
   );
 
-let bound_constructor_aps = (wrap, ty: Typ.t, ctx: Ctx.t): list(Suggestion.t) =>
+let bound_constructor_aps =
+    (wrap, ty: Typ.t(IdTag.t), ctx: Ctx.t(IdTag.t)): list(Suggestion.t) =>
   List.filter_map(
     fun
     | Ctx.ConstructorEntry({
@@ -78,7 +90,7 @@ let bound_constructor_aps = (wrap, ty: Typ.t, ctx: Ctx.t): list(Suggestion.t) =>
   );
 
 /* Suggest bound type aliases in type annotations or definitions */
-let typ_context_entries = (ctx: Ctx.t): list(Suggestion.t) =>
+let typ_context_entries = (ctx: Ctx.t(IdTag.t)): list(Suggestion.t) =>
   List.filter_map(
     fun
     | Ctx.TVarEntry({kind: Singleton(_), name, _}) =>

src/haz3lcore/assistant/AssistantForms.re

@@ -11,9 +11,9 @@ let leading_expander = " ";
  * running Statics, but for now, new forms e.g. operators must be added
  * below manually.  */
 module Typ = {
-  let unk: Typ.t = Unknown(Internal) |> Typ.fresh;
+  let unk: Typ.t(IdTag.t) = Unknown(Internal) |> Typ.fresh;
 
-  let of_const_mono_delim: list((Token.t, Typ.t)) = [
+  let of_const_mono_delim: list((Token.t, Typ.t(IdTag.t))) = [
     ("true", Bool |> Typ.fresh),
     ("false", Bool |> Typ.fresh),
     //("[]", List(unk)), / *NOTE: would need to refactor buffer for this to show up */
@@ -22,20 +22,20 @@ module Typ = {
     ("_", unk),
   ];
 
-  let of_leading_delim: list((Token.t, Typ.t)) = [
+  let of_leading_delim: list((Token.t, Typ.t(IdTag.t))) = [
     ("case" ++ leading_expander, unk),
     ("fun" ++ leading_expander, Arrow(unk, unk) |> Typ.fresh),
     (
       "typfun" ++ leading_expander,
-      Forall(Var("") |> TPat.fresh, unk) |> Typ.fresh,
+      Forall((Var(""): TPat.term(IdTag.t)) |> TPat.fresh, unk) |> Typ.fresh,
     ),
     ("if" ++ leading_expander, unk),
     ("let" ++ leading_expander, unk),
     ("test" ++ leading_expander, Prod([]) |> Typ.fresh),
     ("type" ++ leading_expander, unk),
   ];
 
-  let of_infix_delim: list((Token.t, Typ.term)) = [
+  let of_infix_delim: list((Token.t, Typ.term(IdTag.t))) = [
     //("|>", Unknown(Internal)), /* annoying during case rules */
     (",", Prod([unk, unk])), /* NOTE: Current approach doesn't work for this, but irrelevant as 1-char */
     ("::", List(unk)), /* annoying in patterns */
@@ -71,20 +71,20 @@ module Typ = {
     ("++", String),
   ];
 
-  let expected: Info.t => Typ.t =
+  let expected: Info.t => Typ.t(IdTag.t) =
     fun
     | InfoExp({mode, _})
     | InfoPat({mode, _}) => Mode.ty_of(mode)
     | _ => Unknown(Internal) |> Typ.fresh;
 
   let filter_by =
       (
-        ctx: Ctx.t,
-        expected_ty: Typ.t,
-        self_tys: list((Token.t, Typ.t)),
+        ctx: Ctx.t(IdTag.t),
+        expected_ty: Typ.t(IdTag.t),
+        self_tys: list((Token.t, Typ.t(IdTag.t))),
         delims: list(string),
       )
-      : list((Token.t, Typ.t)) =>
+      : list((Token.t, Typ.t(IdTag.t))) =>
     List.filter_map(
       delim => {
         let* self_ty = List.assoc_opt(delim, self_tys);
@@ -198,7 +198,7 @@ let suggest_form = (ty_map, delims_of_sort, ci: Info.t): list(Suggestion.t) => {
 
 let suggest_operator: Info.t => list(Suggestion.t) =
   suggest_form(
-    List.map(((a, b)) => (a, IdTagged.fresh(b)), Typ.of_infix_delim),
+    List.map(((a, b)) => (a, Annotated.fresh(b)), Typ.of_infix_delim),
     Delims.infix,
   );
 

src/haz3lcore/assistant/Suggestion.re

@@ -37,9 +37,9 @@ type strategy_all =
 
 [@deriving (show({with_path: false}), sexp, yojson)]
 type strategy_common =
-  | NewForm(Typ.t)
-  | FromCtx(Typ.t)
-  | FromCtxAp(Typ.t);
+  | NewForm(Typ.t(IdTag.t))
+  | FromCtx(Typ.t(IdTag.t))
+  | FromCtxAp(Typ.t(IdTag.t));
 
 [@deriving (show({with_path: false}), sexp, yojson)]
 type strategy_exp =
@@ -48,7 +48,7 @@ type strategy_exp =
 [@deriving (show({with_path: false}), sexp, yojson)]
 type strategy_pat =
   | Common(strategy_common)
-  | FromCoCtx(Typ.t);
+  | FromCoCtx(Typ.t(IdTag.t));
 
 [@deriving (show({with_path: false}), sexp, yojson)]
 type strategy_typ =

src/haz3lcore/assistant/TyDi.re

@@ -50,9 +50,9 @@ let token_to_left = (z: Zipper.t): option(string) =>
  * holds an unparsed string, which is parsed via the same mechanism as
  * Paste only when a suggestion is accepted. */
 let mk_unparsed_buffer =
-    (~sort: Sort.t, sibs: Siblings.t, t: Token.t): Segment.t => {
+    (~sort: Sort.t, sibs: Siblings.t, t: Token.t): Segment.t(Id.t) => {
   let mold = Siblings.mold_fitting_between(sort, Precedence.max, sibs);
-  [Tile({id: Id.mk(), label: [t], shards: [0], children: [], mold})];
+  [Tile({extra: Id.mk(), label: [t], shards: [0], children: [], mold})];
 };
 
 /* If 'current' is a proper prefix of 'candidate', return the