Checker: set error bound to the term being checked

src/checker/Pulse.Checker.fst

@@ -175,7 +175,8 @@ let rec check
   (res_ppname:ppname)
   (t:st_term)
 : T.Tac (checker_result_t g0 pre0 post_hint)
-= if Pulse.Checker.AssertWithBinders.handle_head_immediately t
+= RU.with_error_bound #(checker_result_t g0 pre0 post_hint) t.range <| fun () ->
+  if Pulse.Checker.AssertWithBinders.handle_head_immediately t
   then Pulse.Checker.AssertWithBinders.check g0 pre0 pre0_typing post_hint res_ppname t check
   else (
     let (| g, pre, pre_typing, k_elim_pure |) = 

src/checker/Pulse.RuntimeUtils.fsti

@@ -20,6 +20,7 @@ module T = FStar.Tactics
 type context = FStar.Sealed.Inhabited.sealed #(list (string & option range)) []
 val extend_context (tag:string) (r:option range) (ctx:context) : context
 val with_context (c:context) (f:unit -> T.Tac 'a) : T.Tac 'a
+val with_error_bound (r:Range.range) (f:unit -> T.Tac 'a) : T.Tac 'a
 val with_extv (k v : string) (f:unit -> T.Tac 'a) : T.Tac 'a
 val disable_admit_smt_queries (f:unit -> T.Tac 'a) : T.Tac 'a
 val print_context (c:context) : T.Tac string

src/ocaml/plugin/Pulse_RuntimeUtils.ml

@@ -21,6 +21,9 @@ let rec with_context (c:context) (f: unit -> 'a utac) : 'a utac =
     | sr::tl ->
       with_context tl (fun _ ps ->
       FStar_Errors.with_ctx (ctxt_elt_as_string sr) (fun _ -> f () ps)) ps
+let with_error_bound (r:FStar_Range.range) (f: unit -> 'a utac) : 'a utac =
+  fun ps ->
+    FStar_Errors.with_error_bound r (fun _ -> f () ps)
 let disable_admit_smt_queries (f: unit -> 'a utac) : 'a utac =
   fun ps ->
     FStar_Options.with_saved_options (fun _ ->