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/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/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

src/haz3lcore/dynamics/Builtins.re

@@ -1,4 +1,5 @@
 open DHExp;
+open Sexplib.Conv;
 
 /*
    Built-in functions for Hazel.
@@ -8,28 +9,30 @@ open DHExp;
 
    See the existing ones for reference.
  */
-
+[@deriving (show({with_path: false}), sexp)]
+type foo = DHExp.t(list(Id.t));
 [@deriving (show({with_path: false}), sexp)]
 type builtin =
-  | Const(Typ.t, DHExp.t)
-  | Fn(Typ.t, Typ.t, DHExp.t => DHExp.t);
+  | Const(Typ.t, foo)
+  | Fn(Typ.t, Typ.t, DHExp.t(list(Id.t)) => DHExp.t(list(Id.t)));
 
 [@deriving (show({with_path: false}), sexp)]
 type t = VarMap.t_(builtin);
 
 [@deriving (show({with_path: false}), sexp)]
-type forms = VarMap.t_(DHExp.t => DHExp.t);
+type forms = VarMap.t_(DHExp.t(list(Id.t)) => DHExp.t(list(Id.t)));
 
-type result = Result.t(DHExp.t, EvaluatorError.t);
+type result = Result.t(DHExp.t(list(Id.t)), EvaluatorError.t);
 
-let const = (name: Var.t, typ: Typ.term, v: DHExp.t, builtins: t): t =>
+let const =
+    (name: Var.t, typ: Typ.term, v: DHExp.t(list(Id.t)), builtins: t): t =>
   VarMap.extend(builtins, (name, Const(typ |> Typ.fresh, v)));
 let fn =
     (
       name: Var.t,
       t1: Typ.term,
       t2: Typ.term,
-      impl: DHExp.t => DHExp.t,
+      impl: DHExp.t(list(Id.t)) => DHExp.t(list(Id.t)),
       builtins: t,
     )
     : t =>
@@ -49,14 +52,18 @@ module Pervasives = {
     let max_int = DHExp.Int(Int.max_int) |> fresh;
     let min_int = DHExp.Int(Int.min_int) |> fresh;
 
-    let unary = (f: DHExp.t => result, d: DHExp.t) => {
+    let unary = (f: DHExp.t(list(Id.t)) => result, d: DHExp.t(list(Id.t))) => {
       switch (f(d)) {
       | Ok(r') => r'
       | Error(e) => EvaluatorError.Exception(e) |> raise
       };
     };
 
-    let binary = (f: (DHExp.t, DHExp.t) => result, d: DHExp.t) => {
+    let binary =
+        (
+          f: (DHExp.t(list(Id.t)), DHExp.t(list(Id.t))) => result,
+          d: DHExp.t(list(Id.t)),
+        ) => {
       switch (term_of(d)) {
       | Tuple([d1, d2]) =>
         switch (f(d1, d2)) {
@@ -67,7 +74,17 @@ module Pervasives = {
       };
     };
 
-    let ternary = (f: (DHExp.t, DHExp.t, DHExp.t) => result, d: DHExp.t) => {
+    let ternary =
+        (
+          f:
+            (
+              DHExp.t(list(Id.t)),
+              DHExp.t(list(Id.t)),
+              DHExp.t(list(Id.t))
+            ) =>
+            result,
+          d: DHExp.t(list(Id.t)),
+        ) => {
       switch (term_of(d)) {
       | Tuple([d1, d2, d3]) =>
         switch (f(d1, d2, d3)) {
@@ -173,7 +190,11 @@ module Pervasives = {
     let atan = float_op(atan);
 
     let of_string =
-        (convert: string => option('a), wrap: 'a => DHExp.t, name: string) =>
+        (
+          convert: string => option('a),
+          wrap: 'a => DHExp.t(list(Id.t)),
+          name: string,
+        ) =>
       unary(d =>
         switch (term_of(d)) {
         | String(s) =>
@@ -245,7 +266,7 @@ module Pervasives = {
         }
       );
 
-    let string_of: DHExp.t => option(string) =
+    let string_of: DHExp.t(list(Id.t)) => option(string) =
       d =>
         switch (term_of(d)) {
         | String(s) => Some(s)

src/haz3lcore/dynamics/Casts.re

@@ -90,7 +90,9 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => {
 /* Rules are taken from figure 12 of https://arxiv.org/pdf/1805.00155.pdf  */
 
 /* gives a transition step that can be taken by the cast calculus here if applicable. */
-let rec transition = (~recursive=false, d: DHExp.t): option(DHExp.t) => {
+let rec transition =
+        (~recursive=false, d: DHExp.t(list(Id.t)))
+        : option(DHExp.t(list(Id.t))) => {
   switch (DHExp.term_of(d)) {
   | Cast(d1, t1, t2) =>
     let d1 =
@@ -168,7 +170,8 @@ let rec transition = (~recursive=false, d: DHExp.t): option(DHExp.t) => {
   };
 };
 
-let rec transition_multiple = (d: DHExp.t): DHExp.t => {
+let rec transition_multiple =
+        (d: DHExp.t(list(Id.t))): DHExp.t(list(Id.t)) => {
   switch (transition(~recursive=true, d)) {
   | Some(d'') => transition_multiple(d'')
   | None => d
@@ -181,7 +184,7 @@ let hole = EmptyHole |> DHExp.fresh;
 // Hacky way to do transition_multiple on patterns by transferring
 // the cast to the expression and then back to the pattern.
 let pattern_fixup = (p: DHPat.t): DHPat.t => {
-  let rec unwrap_casts = (p: DHPat.t): (DHPat.t, DHExp.t) => {
+  let rec unwrap_casts = (p: DHPat.t): (DHPat.t, DHExp.t(list(Id.t))) => {
     switch (DHPat.term_of(p)) {
     | Cast(p1, t1, t2) =>
       let (p1, d1) = unwrap_casts(p1);
@@ -193,7 +196,7 @@ let pattern_fixup = (p: DHPat.t): DHPat.t => {
     | _ => (p, hole)
     };
   };
-  let rec rewrap_casts = ((p: DHPat.t, d: DHExp.t)): DHPat.t => {
+  let rec rewrap_casts = ((p: DHPat.t, d: DHExp.t(list(Id.t)))): DHPat.t => {
     switch (DHExp.term_of(d)) {
     | EmptyHole => p
     | Cast(d1, t1, t2) =>

src/haz3lcore/dynamics/DHExp.re

@@ -7,10 +7,10 @@
 
 include Exp;
 
-let term_of: t => term = IdTagged.term_of;
-let fast_copy: (Id.t, t) => t = IdTagged.fast_copy;
+let term_of: t(list(Id.t)) => term(list(Id.t)) = IdTagged.term_of;
+let fast_copy: (Id.t, t(list(Id.t))) => t(list(Id.t)) = IdTagged.fast_copy;
 
-let mk = (ids, term): t => {
+let mk = (ids, term): t(list(Id.t)) => {
   {ids, copied: true, term};
 };
 
@@ -95,7 +95,7 @@ let assign_name_if_none = (t, name) => {
   };
 };
 
-let ty_subst = (s: Typ.t, tpat: TPat.t, exp: t): t => {
+let ty_subst = (s: Typ.t, tpat: TPat.t, exp: t(list(Id.t))): t(list(Id.t)) => {
   switch (TPat.tyvar_of_utpat(tpat)) {
   | None => exp
   | Some(x) =>