Improve error message for missing witness.

Author: gebner

src/checker/Pulse.Checker.Prover.fst

@@ -303,8 +303,8 @@ let intro_exists (g: env) (frame: slprop) (u: universe) (b: binder) (body: slpro
   let frame_typ : tot_typing g frame tm_slprop = RU.magic () in // implied by t2_typing
   let binder_ty_typ : tot_typing g b.binder_ty (tm_type u) = RU.magic() in // implied by t2_typing
   let tm_ex_typ : tot_typing g (tm_exists_sl u b body) tm_slprop = RU.magic() in // implied by t2_typing
-  // TODO: improve error message below. this will e.g. fail if we cannot solve e using unification
-  let e_typ = core_check_term g e T.E_Ghost b.binder_ty in
+  let e_typ = core_check_term' g e T.E_Ghost b.binder_ty (fun _ -> let open Pulse.PP in
+    [text "Cannot find witness for" ^/^ pp (tm_exists_sl u b body)]) in
   let h1: tot_typing g (tm_star frame (comp_pre (comp_intro_exists u b body e))) tm_slprop = RU.magic () in
   let h2: slprop_equiv g (tm_star frame (comp_pre (comp_intro_exists u b body e))) (tm_star frame (open_term' body e 0)) = RU.magic () in
   let h3: slprop_equiv g (tm_star (comp_post (comp_intro_exists u b body e)) frame) (tm_star frame (tm_exists_sl u b body)) = RU.magic () in

src/checker/Pulse.Checker.Pure.fst

@@ -466,7 +466,7 @@ let core_compute_term_type (g:env) (t:term)
   in
   RU.record_stats "Pulse.core_compute_term_type" aux
 
-let core_check_term g e eff t
+let core_check_term' g e eff t extra_msg
 = let aux () : T.Tac (typing g e eff t) 
   = let fg = elab_env g in
     let topt, issues =
@@ -476,11 +476,15 @@ let core_check_term g e eff t
         fg e eff t) in
     match topt with   
     | None ->
-      fail_doc_with_subissues g (Some <| RU.range_of_term e) issues (ill_typed_term e (Some t) None)
+      fail_doc_with_subissues g (Some <| RU.range_of_term e) issues (extra_msg () @ ill_typed_term e (Some t) None)
     | Some tok -> E (RT.T_Token _ _ _ (FStar.Squash.return_squash tok))
   in
   RU.record_stats "Pulse.core_check_term" aux
 
+
+let core_check_term g e eff t
+= core_check_term' g e eff t fun _ -> []
+
 let core_check_term_at_type g e t
 = let aux () : T.Tac (eff:T.tot_or_ghost & typing g e eff t) 
   = let fg = elab_env g in

src/checker/Pulse.Checker.Pure.fsti

@@ -65,6 +65,10 @@ val core_compute_term_type (g:env) (t:term)
            ty:term &
            typing g t eff ty)
 
+val core_check_term' (g:env) (e:term) (eff:T.tot_or_ghost) (t:term)
+    (extra_msg: unit -> T.Tac (list Pprint.document))
+  : T.Tac (typing g e eff t)
+
 val core_check_term (g:env) (e:term) (eff:T.tot_or_ghost) (t:term)
   : T.Tac (typing g e eff t)
 

test/nolib/ErrCantFindWitness.fst

@@ -0,0 +1,8 @@
+module ErrCantFindWitness
+#lang-pulse
+open Pulse.Nolib
+
+[@@expect_failure]
+fn foo ()
+  ensures exists* (x: nat). emp
+{}

test/nolib/ErrCantFindWitness.fst.output.expected

@@ -0,0 +1,8 @@
+* Info at ErrCantFindWitness.fst(8,1-8,1):
+  - Expected failure:
+  - Cannot find witness for exists*:
+  - (exists* (x:Prims.nat). emp)
+  - Ill-typed term: (*?u56*)_
+  - Expected a term of type Prims.nat
+  - Fstarcompiler.FStarC_Tactics_Common.TacticFailure(_)
+