Tactics: return proper errors when guards fail for typing reflection

src/extraction/FStarC.Extraction.ML.Modul.fst

@@ -750,7 +750,7 @@ let karamel_fixup_qual (se:sigelt) : sigelt =
 
 let mark_sigelt_erased (se:sigelt) (g:uenv) : uenv =
   debug g (fun u -> BU.print1 ">>>> NOT extracting %s \n" (Print.sigelt_to_string_short se));
-  // Cheating with delta levels and qualifiers below, but we don't ever use them.
+  // Cheating with fv qualifiers below, but we don't ever use them.
   List.fold_right (fun lid g -> extend_erased_fv g (S.lid_as_fv lid None))
                   (U.lids_of_sigelt se) g
 

src/extraction/FStarC.Extraction.ML.UEnv.fst

@@ -150,44 +150,56 @@ let print_mlpath_map (g:uenv) =
   Takes a range for error reporting.
   *)
 
+type lookup_res =
+  | Found of exp_binding
+  | WasErased of Range.range (* position of the definition that was erased *)
+  | NotFound
+
+instance showable_lookup_res : showable lookup_res = {
+  show = (function Found t -> "Found .."
+                 | WasErased r -> "WasErased " ^ show r
+                 | NotFound -> "NotFound");
+}
+
 // Inr b: success
 // Inl true: was erased
 // Inl false: not found
-let lookup_fv_generic (g:uenv) (fv:fv) : either bool exp_binding =
+let lookup_fv_generic (g:uenv) (fv:fv) : lookup_res =
   let v =
     BU.find_map g.env_bindings
       (function
-       | Fv (fv', t) when fv_eq fv fv' -> Some (Inr t)
-       | ErasedFv fv' when fv_eq fv fv' -> Some (Inl true)
+       | Fv (fv', t) when fv_eq fv fv' -> Some (Found t)
+       | ErasedFv fv' when fv_eq fv fv' -> Some (WasErased (pos fv'))
        | _ -> None)
   in
   match v with
   | Some r -> r
-  | None -> Inl false
+  | None -> NotFound
 
 let try_lookup_fv (r:Range.range) (g:uenv) (fv:fv) : option exp_binding =
   match lookup_fv_generic g fv with
-  | Inr r -> Some r
-  | Inl true ->
+  | Found r -> Some r
+  | WasErased pos ->
     (* Log an error/warning and return None *)
     let open FStarC.Errors.Msg in
     Errors.log_issue r Errors.Error_CallToErased [
-       text <| BU.format1 "Will not extract reference to variable `%s` since it has the `noextract` qualifier." (show fv);
-       text <| "Either remove its qualifier or add it to this definition.";
+       text <| BU.format1 "Will not extract reference to variable `%s` since it has the `noextract` qualifier." (string_of_lid fv.fv_name.v);
+       text <| BU.format2 "Either remove the noextract qualifier from %s (defined in %s) or add it to this definition."
+                 (string_of_lid fv.fv_name.v) (show pos);
        text <| BU.format1 "This error can be ignored with `--warn_error -%s`." (string_of_int Errors.call_to_erased_errno)];
     None
-  | Inl false ->
+  | NotFound ->
     None
 
 (** Fatal failure version of try_lookup_fv *)
 let lookup_fv (r:Range.range) (g:uenv) (fv:fv) : exp_binding =
   match lookup_fv_generic g fv with
-  | Inr t -> t
-  | Inl b ->
-    failwith (BU.format3 "Internal error: (%s) free variable %s not found during extraction (erased=%s)\n"
+  | Found t -> t
+  | res ->
+    failwith (BU.format3 "Internal error: (%s) free variable %s not found during extraction (res=%s)\n"
               (Range.string_of_range fv.fv_name.p)
               (show fv.fv_name.v)
-              (string_of_bool b))
+              (show res))
 
 (** An F* local variable (bv) can be mapped either to
     a ML type variable or a term variable *)

src/tactics/FStarC.Tactics.Monad.fst

@@ -205,6 +205,13 @@ let rec iter_tac f l =
   | [] -> ret ()
   | hd::tl -> f hd ;! iter_tac f tl
 
+let rec fold_right f l x =
+  match l with
+  | [] -> return x
+  | hd::tl ->
+    let! r = fold_right f tl x in
+    f hd r
+
 exception Bad of string
 
 (* private *)

src/tactics/FStarC.Tactics.Monad.fsti

@@ -66,6 +66,8 @@ val trytac_exn : tac 'a -> tac (option 'a)
 (* iter combinator *)
 val iter_tac (f: 'a -> tac unit) (l:list 'a) : tac unit
 
+val fold_right (f: 'a -> 'b -> tac 'b) (l:list 'a) (x:'b) : tac 'b
+
 (* Defensive checks. Will only do anything if --defensive is on. If so,
 and some goal is ill-scoped, they will log a warning. *)
 val check_valid_goal (g:goal) : unit

src/tactics/FStarC.Tactics.Types.fst

@@ -26,6 +26,15 @@ module O       = FStarC.Options
 module Range   = FStarC.Range
 module U       = FStarC.Syntax.Util
 
+instance showable_guard_policy : showable guard_policy = {
+  show = (function | Goal -> "Goal"
+                   | SMT -> "SMT"
+                   | SMTSync -> "SMTSync"
+                   | Force -> "Force"
+                   | ForceSMT -> "ForceSMT"
+                   | Drop -> "Drop");
+}
+
 let goal_env g = g.goal_main_env
 let goal_range g = g.goal_main_env.range
 let goal_witness g =

src/tactics/FStarC.Tactics.Types.fsti

@@ -20,6 +20,7 @@ open FStarC.Effect
 open FStarC.Syntax.Syntax
 open FStarC.TypeChecker.Env
 open FStarC.Tactics.Common
+open FStarC.Class.Show
 
 module PO      = FStarC.TypeChecker.Primops
 module Range   = FStarC.Range
@@ -50,6 +51,8 @@ type guard_policy =
     | ForceSMT
     | Drop // unsound
 
+instance val showable_guard_policy : showable guard_policy
+
 type proofstate = {
     main_context : env;          //the shared top-level context for all goals
     all_implicits: implicits ;   //all the implicits currently open, partially resolved

src/tactics/FStarC.Tactics.V2.Basic.fst

@@ -234,6 +234,9 @@ let proc_guard_formula
   (rng:Range.range)
 : tac unit
 = let! ps = get in
+  if !dbg_Tac then
+    BU.print2 "Guard policy is %s, trying to discharge %s\n"
+      (show ps.guard_policy) (show f);
   match ps.guard_policy with
   | Drop ->
     // should somehow taint the state instead of just printing a warning
@@ -2241,6 +2244,10 @@ let write (r:tref 'a) (x:'a) : tac unit =
 
 (***** Builtins used in the meta DSL framework *****)
 
+(* reflection typing calls generate guards in this format, and are mostly discharged
+   internally. *)
+type refl_guard_t = env & typ
+
 let dbg_refl (g:env) (msg:unit -> string) =
   if !dbg_ReflTc
   then BU.print_string (msg ())
@@ -2253,7 +2260,16 @@ let refl_typing_guard (e:env) (g:typ) : tac unit =
 
 let uncurry f (x, y) = f x y
 
-let __refl_typing_builtin_wrapper (f:unit -> 'a & list (env & typ)) : tac (option 'a & issues) =
+let exn_to_issue (e:exn) : Errors.issue =
+  FStarC.Errors.({
+    issue_msg = Errors.mkmsg (BU.print_exn e);
+    issue_level = EError;
+    issue_range = None;
+    issue_number = (Some 17);
+    issue_ctx = get_ctx ()
+  })
+
+let __refl_typing_builtin_wrapper (f:unit -> 'a & list refl_guard_t) : tac (option 'a & issues) =
   (* We ALWAYS rollback the state. This wrapper is meant to ensure that
   the UF graph is not affected by whatever we are wrapping. This means
   any returned term must be deeply-compressed. The guards are compressed by
@@ -2263,13 +2279,7 @@ let __refl_typing_builtin_wrapper (f:unit -> 'a & list (env & typ)) : tac (optio
   let errs, r =
     try Errors.catch_errors_and_ignore_rest f
     with exn -> //catch everything
-      let issue = FStarC.Errors.({
-        issue_msg = Errors.mkmsg (BU.print_exn exn);
-        issue_level = EError;
-        issue_range = None;
-        issue_number = (Some 17);
-        issue_ctx = get_ctx ()
-      }) in
+      let issue = exn_to_issue exn in
       [issue], None
   in
 
@@ -2297,8 +2307,32 @@ let __refl_typing_builtin_wrapper (f:unit -> 'a & list (env & typ)) : tac (optio
   if List.length errs > 0
   then return (None, errs)
   else (
-    iter_tac (uncurry refl_typing_guard) gs;!
-    return (r, errs)
+    (* Try to discharge the guards, but if any of them fails, return a decent error. *)
+    let! ok, guard_errs =
+      fold_right (fun (e,g) (ok, errs) ->
+        match! catch (refl_typing_guard e g) with
+        | Inr () -> return (ok, errs)
+        | Inl e ->
+          (* the exception is not really useful. *)
+          let iss =
+            FStarC.Errors.({
+              issue_msg = [
+                Pprint.doc_of_string "Discharging guard failed.";
+                Pprint.doc_of_string "g = " ^^ pp g;
+              ];
+              issue_level = EError;
+              issue_range = None;
+              issue_number = (Some 17);
+              issue_ctx = get_ctx ()
+            })
+          in
+          return (false, iss :: errs)
+      ) gs (true, [])
+    in
+    if ok then
+      return (r, errs @ guard_errs)
+    else
+      return (None, errs @ guard_errs)
   )
 
 (* This runs the tactic `f` in the current proofstate, and returns an
@@ -2317,7 +2351,7 @@ errors in the tactic execution, e.g. those related to discharging the
 guards if a synchronous mode (SMTSync/Force) was used.
 
 This also adds the label to the messages (when debugging) to identify the primitive. *)
-let refl_typing_builtin_wrapper (label:string) (f:unit -> 'a & list (env & typ)) : tac (option 'a & issues) =
+let refl_typing_builtin_wrapper (label:string) (f:unit -> 'a & list refl_guard_t) : tac (option 'a & issues) =
   let open FStarC.Errors in
   let! o, errs =
     match! catch_all (__refl_typing_builtin_wrapper f) with
@@ -2432,7 +2466,7 @@ let refl_core_compute_term_type (g:env) (e:term) : tac (option (Core.tot_or_ghos
          let g = Env.set_range g e.pos in
          dbg_refl g (fun _ ->
            BU.format1 "refl_core_compute_term_type: %s\n" (show e));
-         let guards : ref (list (env & typ)) = mk_ref [] in
+         let guards : ref (list refl_guard_t) = mk_ref [] in
          let gh = fun g guard ->
            (* FIXME: this is kinda ugly, we store all the guards
            in a local ref and fetch them at the end. *)
@@ -2552,7 +2586,7 @@ let refl_tc_term (g:env) (e:term) : tac (option (term & (Core.tot_or_ghost & typ
       dbg_refl g (fun _ ->
         BU.format1 "} finished tc with e = %s\n"
           (show e));
-      let guards : ref (list (env & typ)) = mk_ref [] in
+      let guards : ref (list refl_guard_t) = mk_ref [] in
       let gh = fun g guard ->
         (* collect guards and return them *)
         dbg_refl g (fun _ ->