Type Hole Inference (post merge)

note.txt

@@ -0,0 +1 @@
+Note: this push is a test to reactivate the GitHub Action and rerun test cases, in case there was a collision during the last push. 

src/haz3lcore/Measured.re

@@ -267,9 +267,15 @@ let is_indented_map = (seg: Segment.t) => {
   go(seg);
 };
 
-let of_segment = (~old: t=empty, ~touched=Touched.empty, seg: Segment.t): t => {
+let of_segment =
+    (
+      ~old: t=empty,
+      ~touched=Touched.empty,
+      ~global_inference_info=InferenceResult.empty_info(),
+      seg: Segment.t,
+    )
+    : t => {
   let is_indented = is_indented_map(seg);
-
   // recursive across seg's bidelimited containers
   let rec go_nested =
           (
@@ -356,7 +362,22 @@ let of_segment = (~old: t=empty, ~touched=Touched.empty, seg: Segment.t): t => {
             let map = map |> add_w(w, {origin, last});
             (contained_indent, last, map);
           | Grout(g) =>
-            let last = {...origin, col: origin.col + 1};
+            let annotation_offset =
+              switch (
+                InferenceResult.get_suggestion_text_for_id(
+                  g.id,
+                  global_inference_info,
+                )
+              ) {
+              | (Solvable(suggestion_string), TypHole)
+              | (NestedInconsistency(suggestion_string), TypHole) =>
+                String.length(suggestion_string)
+              | (_, ExpHole)
+              | (_, None)
+              | (NoSuggestion(_), _) => 1
+              };
+
+            let last = {...origin, col: origin.col + annotation_offset};
             let map = map |> add_g(g, {origin, last});
             (contained_indent, last, map);
           | Tile(t) =>

src/haz3lcore/assistant/AssistantCtx.re

@@ -92,14 +92,30 @@ let suggest_variable = (ci: Info.t): list(Suggestion.t) => {
   let ctx = Info.ctx_of(ci);
   switch (ci) {
   | InfoExp({mode, _}) =>
-    bound_variables(Mode.ty_of(mode), ctx)
-    @ bound_aps(Mode.ty_of(mode), ctx)
-    @ bound_constructors(x => Exp(Common(x)), Mode.ty_of(mode), ctx)
-    @ bound_constructor_aps(x => Exp(Common(x)), Mode.ty_of(mode), ctx)
+    bound_variables(Mode.assistant_ty_of(mode), ctx)
+    @ bound_aps(Mode.assistant_ty_of(mode), ctx)
+    @ bound_constructors(
+        x => Exp(Common(x)),
+        Mode.assistant_ty_of(mode),
+        ctx,
+      )
+    @ bound_constructor_aps(
+        x => Exp(Common(x)),
+        Mode.assistant_ty_of(mode),
+        ctx,
+      )
   | InfoPat({mode, co_ctx, _}) =>
-    free_variables(Mode.ty_of(mode), ctx, co_ctx)
-    @ bound_constructors(x => Pat(Common(x)), Mode.ty_of(mode), ctx)
-    @ bound_constructor_aps(x => Pat(Common(x)), Mode.ty_of(mode), ctx)
+    free_variables(Mode.assistant_ty_of(mode), ctx, co_ctx)
+    @ bound_constructors(
+        x => Pat(Common(x)),
+        Mode.assistant_ty_of(mode),
+        ctx,
+      )
+    @ bound_constructor_aps(
+        x => Pat(Common(x)),
+        Mode.assistant_ty_of(mode),
+        ctx,
+      )
   | InfoTyp(_) => typ_context_entries(ctx)
   | _ => []
   };
@@ -141,7 +157,7 @@ let suggest_lookahead_variable = (ci: Info.t): list(Suggestion.t) => {
     let exp_aps = ty =>
       bound_aps(ty, ctx)
       @ bound_constructor_aps(x => Exp(Common(x)), ty, ctx);
-    switch (Mode.ty_of(mode)) {
+    switch (Mode.assistant_ty_of(mode)) {
     | List(ty) =>
       List.map(restrategize(" )::"), exp_aps(ty))
       @ List.map(restrategize("::"), exp_refs(ty))
@@ -165,7 +181,7 @@ let suggest_lookahead_variable = (ci: Info.t): list(Suggestion.t) => {
       free_variables(ty, ctx, co_ctx)
       @ bound_constructors(x => Pat(Common(x)), ty, ctx);
     let pat_aps = ty => bound_constructor_aps(x => Pat(Common(x)), ty, ctx);
-    switch (Mode.ty_of(mode)) {
+    switch (Mode.assistant_ty_of(mode)) {
     | List(ty) =>
       List.map(restrategize(" )::"), pat_aps(ty))
       @ List.map(restrategize("::"), pat_refs(ty))

src/haz3lcore/assistant/AssistantForms.re

@@ -11,7 +11,7 @@ let leading_expander = " " ++ AssistantExpander.c;
  * running Statics, but for now, new forms e.g. operators must be added
  * below manually.  */
 module Typ = {
-  let unk: Typ.t = Unknown(Internal);
+  let unk: Typ.t = Unknown(NoProvenance, false);
 
   let of_const_mono_delim: list((Token.t, Typ.t)) = [
     ("true", Bool),
@@ -70,8 +70,8 @@ module Typ = {
   let expected: Info.t => Typ.t =
     fun
     | InfoExp({mode, _})
-    | InfoPat({mode, _}) => Mode.ty_of(mode)
-    | _ => Unknown(Internal);
+    | InfoPat({mode, _}) => Mode.assistant_ty_of(mode)
+    | _ => Unknown(NoProvenance, false);
 
   let filter_by =
       (

src/haz3lcore/assistant/TyDi.re

@@ -95,6 +95,10 @@ let set_buffer = (~settings, ~ctx: Ctx.t, z: Zipper.t): option(Zipper.t) => {
     suggestions
     |> List.filter(({content, _}: Suggestion.t) =>
          String.starts_with(~prefix=tok_to_left, content)
+         /* HACK(andrew): Below filtering of cons suggestion
+          * should be done in a more principled way when a
+          * ranker is implemented */
+         && !(Info.sort_of(ci) == Pat && content == "::")
        );
   let* top_suggestion = suggestions |> Util.ListUtil.hd_opt;
   let* suggestion_suffix = suffix_of(top_suggestion.content, tok_to_left);

src/haz3lcore/dynamics/DH.re

@@ -141,8 +141,13 @@ module rec DHExp: {
     | [_] => failwith("mk_tuple: expected at least 2 elements")
     | xs => Tuple(xs);
 
+  let is_any_synswitch: Typ.t => bool =
+    fun
+    | Unknown(_, s) => s
+    | _ => false;
+
   let cast = (d: t, t1: Typ.t, t2: Typ.t): t =>
-    if (Typ.eq(t1, t2) || t2 == Unknown(SynSwitch)) {
+    if (Typ.eq(t1, t2) || is_any_synswitch(t2)) {
       d;
     } else {
       Cast(d, t1, t2);

src/haz3lcore/dynamics/Elaborator.re

@@ -27,13 +27,17 @@ let fixed_pat_typ = (m: Statics.Map.t, p: Term.UPat.t): option(Typ.t) =>
   | _ => None
   };
 
-let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) =>
+let cast = (ctx: Ctx.t, id: Id.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) =>
   switch (mode) {
   | Syn => d
   | SynFun =>
     switch (self_ty) {
-    | Unknown(prov) =>
-      DHExp.cast(d, Unknown(prov), Arrow(Unknown(prov), Unknown(prov)))
+    | Unknown(prov, s) =>
+      DHExp.cast(
+        d,
+        Unknown(prov, s),
+        Arrow(Unknown(prov, s), Unknown(prov, s)),
+      )
     | Arrow(_) => d
     | _ => failwith("Elaborator.wrap: SynFun non-arrow-type")
     }
@@ -45,26 +49,28 @@ let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) =>
     | ListConcat(_)
     | Cons(_) =>
       switch (ana_ty) {
-      | Unknown(prov) => DHExp.cast(d, List(Unknown(prov)), Unknown(prov))
+      | Unknown(prov, s) =>
+        DHExp.cast(d, List(Unknown(prov, s)), Unknown(prov, s))
       | _ => d
       }
     | Fun(_) =>
       /* See regression tests in Examples/Dynamics */
-      let (_, ana_out) = Typ.matched_arrow(ctx, ana_ty);
-      let (self_in, _) = Typ.matched_arrow(ctx, self_ty);
+      let ((_, ana_out), _) = Typ.matched_arrow(ctx, id, ana_ty);
+      let ((self_in, _), _) = Typ.matched_arrow(ctx, id, self_ty);
       DHExp.cast(d, Arrow(self_in, ana_out), ana_ty);
     | Tuple(ds) =>
       switch (ana_ty) {
-      | Unknown(prov) =>
-        let us = List.init(List.length(ds), _ => Typ.Unknown(prov));
-        DHExp.cast(d, Prod(us), Unknown(prov));
+      | Unknown(prov, s) =>
+        let us = List.init(List.length(ds), _ => Typ.Unknown(prov, s));
+        DHExp.cast(d, Prod(us), Unknown(prov, s));
       | _ => d
       }
     | Ap(Constructor(_), _)
     | Constructor(_) =>
       switch (ana_ty, self_ty) {
-      | (Unknown(prov), Rec(_, Sum(_)))
-      | (Unknown(prov), Sum(_)) => DHExp.cast(d, self_ty, Unknown(prov))
+      | (Unknown(prov, s), Rec(_, Sum(_)))
+      | (Unknown(prov, s), Sum(_)) =>
+        DHExp.cast(d, self_ty, Unknown(prov, s))
       | _ => d
       }
     /* Forms with special ana rules but no particular typing requirements */
@@ -104,24 +110,24 @@ let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) =>
 
 /* Handles cast insertion and non-empty-hole wrapping
    for elaborated expressions */
-let wrap = (ctx: Ctx.t, u: Id.t, mode: Mode.t, self, d: DHExp.t): DHExp.t =>
+let wrap = (ctx: Ctx.t, id: Id.t, mode: Mode.t, self, d: DHExp.t): DHExp.t =>
   switch (Info.status_exp(ctx, mode, self)) {
   | NotInHole(_) =>
     let self_ty =
       switch (Self.typ_of_exp(ctx, self)) {
       | Some(self_ty) => Typ.normalize(ctx, self_ty)
-      | None => Unknown(Internal)
+      | None => Unknown(NoProvenance, false)
       };
-    cast(ctx, mode, self_ty, d);
-  | InHole(_) => NonEmptyHole(TypeInconsistent, u, 0, d)
+    cast(ctx, id, mode, self_ty, d);
+  | InHole(_) => NonEmptyHole(TypeInconsistent, id, 0, d)
   };
 
 let rec dhexp_of_uexp =
         (m: Statics.Map.t, uexp: Term.UExp.t): option(DHExp.t) => {
-  switch (Id.Map.find_opt(Term.UExp.rep_id(uexp), m)) {
+  let id = Term.UExp.rep_id(uexp); /* NOTE: using term uids for hole ids */
+  switch (Id.Map.find_opt(id, m)) {
   | Some(InfoExp({mode, self, ctx, _})) =>
     let err_status = Info.status_exp(ctx, mode, self);
-    let id = Term.UExp.rep_id(uexp); /* NOTE: using term uids for hole ids */
     let+ d: DHExp.t =
       switch (uexp.term) {
       | Invalid(t) => Some(DHExp.InvalidText(id, 0, t))
@@ -139,7 +145,7 @@ let rec dhexp_of_uexp =
       | ListLit(es) =>
         let* ds = es |> List.map(dhexp_of_uexp(m)) |> OptUtil.sequence;
         let+ ty = fixed_exp_typ(m, uexp);
-        let ty = Typ.matched_list(ctx, ty);
+        let (ty, _) = Typ.matched_list(ctx, id, ty);
         DHExp.ListLit(id, 0, ty, ds);
       | Fun(p, body) =>
         let* dp = dhpat_of_upat(m, p);
@@ -281,26 +287,26 @@ let rec dhexp_of_uexp =
   };
 }
 and dhpat_of_upat = (m: Statics.Map.t, upat: Term.UPat.t): option(DHPat.t) => {
-  switch (Id.Map.find_opt(Term.UPat.rep_id(upat), m)) {
+  let id = Term.UPat.rep_id(upat); /* NOTE: using term uids for hole ids */
+  switch (Id.Map.find_opt(id, m)) {
   | Some(InfoPat({mode, self, ctx, _})) =>
     let err_status = Info.status_pat(ctx, mode, self);
     let maybe_reason: option(ErrStatus.HoleReason.t) =
       switch (err_status) {
       | NotInHole(_) => None
       | InHole(_) => Some(TypeInconsistent)
       };
-    let u = Term.UPat.rep_id(upat); /* NOTE: using term uids for hole ids */
     let wrap = (d: DHPat.t): option(DHPat.t) =>
       switch (maybe_reason) {
       | None => Some(d)
-      | Some(reason) => Some(NonEmptyHole(reason, u, 0, d))
+      | Some(reason) => Some(NonEmptyHole(reason, id, 0, d))
       };
     switch (upat.term) {
-    | Invalid(t) => Some(DHPat.InvalidText(u, 0, t))
-    | EmptyHole => Some(EmptyHole(u, 0))
+    | Invalid(t) => Some(DHPat.InvalidText(id, 0, t))
+    | EmptyHole => Some(EmptyHole(id, 0))
     | MultiHole(_) =>
       // TODO: dhexp, eval for multiholes
-      Some(EmptyHole(u, 0))
+      Some(EmptyHole(id, 0))
     | Wild => wrap(Wild)
     | Bool(b) => wrap(BoolLit(b))
     | Int(n) => wrap(IntLit(n))
@@ -310,11 +316,12 @@ and dhpat_of_upat = (m: Statics.Map.t, upat: Term.UPat.t): option(DHPat.t) => {
     | ListLit(ps) =>
       let* ds = ps |> List.map(dhpat_of_upat(m)) |> OptUtil.sequence;
       let* ty = fixed_pat_typ(m, upat);
-      wrap(ListLit(Typ.matched_list(ctx, ty), ds));
+      let (ty', _) = Typ.matched_list(ctx, id, ty);
+      wrap(ListLit(ty', ds));
     | Constructor(name) =>
       switch (err_status) {
       | InHole(Common(NoType(FreeConstructor(_)))) =>
-        Some(BadConstructor(u, 0, name))
+        Some(BadConstructor(id, 0, name))
       | _ => wrap(Constructor(name))
       }
     | Cons(hd, tl) =>
@@ -349,7 +356,7 @@ let uexp_elab = (m: Statics.Map.t, uexp: Term.UExp.t): ElaborationResult.t =>
     let ty =
       switch (fixed_exp_typ(m, uexp)) {
       | Some(ty) => ty
-      | None => Typ.Unknown(Internal)
+      | None => Typ.Unknown(NoProvenance, false)
       };
     Elaborates(d, ty, Delta.empty);
   };

src/haz3lcore/dynamics/PatternMatch.re

@@ -5,7 +5,7 @@ type match_result =
   | DoesNotMatch
   | IndetMatch;
 
-let const_unknown: 'a => Typ.t = _ => Unknown(Internal);
+let const_unknown: 'a => Typ.t = _ => Unknown(NoProvenance, false);
 
 let cast_sum_maps =
     (sm1: Typ.sum_map, sm2: Typ.sum_map)
@@ -191,9 +191,9 @@ let rec matches = (dp: DHPat.t, d: DHExp.t): match_result =>
   | (Cons(_) | ListLit(_), Cast(d, List(ty1), List(ty2))) =>
     matches_cast_Cons(dp, d, [(ty1, ty2)])
   | (Cons(_) | ListLit(_), Cast(d, Unknown(_), List(ty2))) =>
-    matches_cast_Cons(dp, d, [(Unknown(Internal), ty2)])
+    matches_cast_Cons(dp, d, [(Unknown(NoProvenance, false), ty2)])
   | (Cons(_) | ListLit(_), Cast(d, List(ty1), Unknown(_))) =>
-    matches_cast_Cons(dp, d, [(ty1, Unknown(Internal))])
+    matches_cast_Cons(dp, d, [(ty1, Unknown(NoProvenance, false))])
   | (Cons(_, _), Cons(_, _))
   | (ListLit(_, _), Cons(_, _))
   | (Cons(_, _), ListLit(_))
@@ -459,9 +459,17 @@ and matches_cast_Cons =
   | Cast(d', List(ty1), List(ty2)) =>
     matches_cast_Cons(dp, d', [(ty1, ty2), ...elt_casts])
   | Cast(d', List(ty1), Unknown(_)) =>
-    matches_cast_Cons(dp, d', [(ty1, Unknown(Internal)), ...elt_casts])
+    matches_cast_Cons(
+      dp,
+      d',
+      [(ty1, Unknown(NoProvenance, false)), ...elt_casts],
+    )
   | Cast(d', Unknown(_), List(ty2)) =>
-    matches_cast_Cons(dp, d', [(Unknown(Internal), ty2), ...elt_casts])
+    matches_cast_Cons(
+      dp,
+      d',
+      [(Unknown(NoProvenance, false), ty2), ...elt_casts],
+    )
   | Cast(_, _, _) => DoesNotMatch
   | BoundVar(_) => DoesNotMatch
   | FreeVar(_) => IndetMatch

src/haz3lcore/dynamics/Transition.re

@@ -74,19 +74,21 @@ module CastHelpers = {
     | Ground
     | NotGroundOrHole(Typ.t) /* the argument is the corresponding ground type */;
 
-  let const_unknown: 'a => Typ.t = _ => Unknown(Internal);
+  let const_unknown: 'a => Typ.t = _ => Unknown(NoProvenance, false);
 
   let grounded_Arrow =
-    NotGroundOrHole(Arrow(Unknown(Internal), Unknown(Internal)));
+    NotGroundOrHole(
+      Arrow(Unknown(NoProvenance, false), Unknown(NoProvenance, false)),
+    );
   let grounded_Prod = length =>
     NotGroundOrHole(
-      Prod(ListUtil.replicate(length, Typ.Unknown(Internal))),
+      Prod(ListUtil.replicate(length, Typ.Unknown(NoProvenance, false))),
     );
   let grounded_Sum = (sm: Typ.sum_map): ground_cases => {
     let sm' = sm |> ConstructorMap.map(Option.map(const_unknown));
     NotGroundOrHole(Sum(sm'));
   };
-  let grounded_List = NotGroundOrHole(List(Unknown(Internal)));
+  let grounded_List = NotGroundOrHole(List(Unknown(NoProvenance, false)));
 
   let rec ground_cases_of = (ty: Typ.t): ground_cases => {
     let is_ground_arg: option(Typ.t) => bool =