Add some information on the lifted type to the cursor inspector

src/haz3lcore/statics/Info.re

@@ -202,7 +202,8 @@ type exp = {
   co_ctx: CoCtx.t, /* Locally free variables */
   cls: Cls.t, /* DERIVED: Syntax class (i.e. form name) */
   status: status_exp, /* DERIVED: Ok/Error statuses for display */
-  ty: Typ.t /* DERIVED: Type after nonempty hole fixing */
+  ty: Typ.t, /* DERIVED: Type after nonempty hole fixing */
+  lifted_ty: option(Typ.t) /* Type static-level elaboration */
 };
 
 [@deriving (show({with_path: false}), sexp, yojson)]
@@ -630,11 +631,31 @@ let fixed_typ_exp = (ctx, mode: Mode.t, self: Self.exp): Typ.t =>
 
 /* Add derivable attributes for expression terms */
 let derived_exp =
-    (~uexp: UExp.t, ~ctx, ~mode, ~ancestors, ~self, ~co_ctx): exp => {
+    (
+      ~uexp: UExp.t,
+      ~ctx,
+      ~mode,
+      ~ancestors,
+      ~self,
+      ~co_ctx,
+      ~lifted_ty: option(Typ.t),
+    )
+    : exp => {
   let cls = Cls.Exp(UExp.cls_of_term(uexp.term));
   let status = status_exp(ctx, mode, self);
   let ty = fixed_typ_exp(ctx, mode, self);
-  {cls, self, ty, mode, status, ctx, co_ctx, ancestors, term: uexp};
+  {
+    cls,
+    self,
+    ty,
+    mode,
+    status,
+    ctx,
+    co_ctx,
+    ancestors,
+    lifted_ty,
+    term: uexp,
+  };
 };
 
 /* Add derivable attributes for pattern terms */

src/haz3lcore/statics/Statics.re

@@ -182,9 +182,17 @@ and uexp_to_info_map =
     | Ana({term: Unknown(SynSwitch), _}) => Mode.Syn
     | _ => mode
     };
-  let add' = (~self, ~co_ctx, m) => {
+  let add' = (~lifted_ty=?, ~self, ~co_ctx, m) => {
     let info =
-      Info.derived_exp(~uexp, ~ctx, ~mode, ~ancestors, ~self, ~co_ctx);
+      Info.derived_exp(
+        ~uexp,
+        ~ctx,
+        ~mode,
+        ~ancestors,
+        ~self,
+        ~co_ctx,
+        ~lifted_ty,
+      );
 
     (info, add_info(ids, InfoExp(info), m));
   };
@@ -249,7 +257,11 @@ and uexp_to_info_map =
       uexp_to_info_map(~ctx, ~mode, ~ancestors, elaborated_exp, m);
 
     // We need to keep the original status of the expression to get error messages on the unelaborated expression
-    let info = {...info, status: original_info.status};
+    let info = {
+      ...info,
+      status: original_info.status,
+      lifted_ty: Some(info.ty),
+    };
 
     (info, add_info(elaborated_exp.ids, InfoExp(info), m));
   };

src/haz3lweb/view/CursorInspector.re

@@ -66,7 +66,8 @@ let elements_noun: Cls.t => string =
   | Exp(ListConcat) => "Operands"
   | _ => failwith("elements_noun: Cls doesn't have elements");
 
-let common_err_view = (cls: Cls.t, err: Info.error_common) =>
+let common_err_view =
+    (~lifted_ty: option(Typ.t)=?, cls: Cls.t, err: Info.error_common) =>
   switch (err) {
   | NoType(BadToken(token)) =>
     switch (Form.bad_token_cls(token)) {
@@ -85,19 +86,27 @@ let common_err_view = (cls: Cls.t, err: Info.error_common) =>
       Type.view(typ),
       text("inconsistent with arrow type"),
     ]
-  | Inconsistent(Expectation({ana, syn})) => [
+  | Inconsistent(Expectation({ana, syn})) =>
+    [
       text(":"),
       Type.view(syn),
       text("inconsistent with expected type"),
       Type.view(ana),
     ]
+    @ (
+      switch (lifted_ty) {
+      | None => []
+      | Some(lifted) => [text("lifted to"), Type.view(lifted)]
+      }
+    )
   | Inconsistent(Internal(tys)) => [
       text(elements_noun(cls) ++ " have inconsistent types:"),
       ...ListUtil.join(text(","), List.map(Type.view, tys)),
     ]
   };
 
-let common_ok_view = (cls: Cls.t, ok: Info.ok_pat) => {
+let common_ok_view =
+    (~lifted_ty: option(Typ.t)=?, cls: Cls.t, ok: Info.ok_common) => {
   switch (cls, ok) {
   | (Exp(MultiHole) | Pat(MultiHole), _) => [
       text("Expecting operator or delimiter"),
@@ -122,12 +131,20 @@ let common_ok_view = (cls: Cls.t, ok: Info.ok_pat) => {
       Type.view(syn),
       text("equals expected type"),
     ]
-  | (_, Ana(Consistent({ana, syn, _}))) => [
+  | (_, Ana(Consistent({ana, syn, _}))) =>
+    // print_endline("Id: " ++)
+    [
       text(":"),
       Type.view(syn),
       text("consistent with expected type"),
       Type.view(ana),
     ]
+    @ (
+      switch (lifted_ty) {
+      | None => []
+      | Some(lifted) => [text("lifted to"), Type.view(lifted)]
+      }
+    )
   | (_, Ana(InternallyInconsistent({ana, nojoin: tys}))) =>
     [
       text(elements_noun(cls) ++ " have inconsistent types:"),
@@ -177,7 +194,7 @@ let typ_err_view = (ok: Info.error_typ) =>
     ]
   };
 
-let rec exp_view = (cls: Cls.t, status: Info.status_exp) =>
+let rec exp_view = (cls: Cls.t, status: Info.status_exp, info: Info.exp) =>
   switch (status) {
   | InHole(FreeVariable(name)) =>
     div_err([code_err(name), text("not found")])
@@ -188,7 +205,7 @@ let rec exp_view = (cls: Cls.t, status: Info.status_exp) =>
     | Some(err) =>
       let cls_str = String.uncapitalize_ascii(cls_str);
       div_err([
-        exp_view(cls, InHole(Common(err))),
+        exp_view(cls, InHole(Common(err)), info),
         text("; " ++ cls_str ++ " is inexhaustive"),
       ]);
     };
@@ -208,10 +225,12 @@ let rec exp_view = (cls: Cls.t, status: Info.status_exp) =>
         ++ " arguments",
       ),
     ])
-  | InHole(Common(error)) => div_err(common_err_view(cls, error))
+  | InHole(Common(error)) =>
+    div_err(common_err_view(~lifted_ty=?info.lifted_ty, cls, error))
   | NotInHole(AnaDeferralConsistent(ana)) =>
     div_ok([text("Expecting type"), Type.view(ana)])
-  | NotInHole(Common(ok)) => div_ok(common_ok_view(cls, ok))
+  | NotInHole(Common(ok)) =>
+    div_ok(common_ok_view(~lifted_ty=?info.lifted_ty, cls, ok))
   };
 
 let rec pat_view = (cls: Cls.t, status: Info.status_pat) =>
@@ -266,7 +285,7 @@ let view_of_info = (~inject, ~settings, ci): list(Node.t) => {
   ];
   switch (ci) {
   | Secondary(_) => wrapper(div([]))
-  | InfoExp({cls, status, _}) => wrapper(exp_view(cls, status))
+  | InfoExp({cls, status, _} as ie) => wrapper(exp_view(cls, status, ie))
   | InfoPat({cls, status, _}) => wrapper(pat_view(cls, status))
   | InfoTyp({cls, status, _}) => wrapper(typ_view(cls, status))
   | InfoTPat({cls, status, _}) => wrapper(tpat_view(cls, status))