Uninformative error message for a write without full permission

[tdardinier]

The following Pulse program fails to verify, which is expected since we only have p0 permission to r0, but need 1 to be able to write:

module PM = Pulse.Main
open Steel.ST.Reference
open Steel.FractionalPermission
open Pulse.Steel.Wrapper

```pulse
fn simple_write (r0: ref nat)
               (#p0:perm)
    requires pts_to r0 p0 0
    ensures pts_to r0 p0 1
{
    r0 := 1;
}

However, the error message we get is

"(Error 228) user tactic failed: Pulse checker failed (see also FStar.Tactics.V2.Derived.fst(447,4-449,16))
(Error) inference failed in building head, no solution for ?n_0"

which is not really helpful

[nikswamy]

I have a fix for this in my branch, which I'll soon push to main. The error message now looks like this:

ExistsWitness.fst(12,8-12,8): (Error 228) user tactic failed: `Pulse checker failed` (see also FStar.Tactics.V2.Derived.fst(447,4-449,16))
ExistsWitness.fst(18,4-18,11): (Error) Could not infer some implicit arguments: ?.n;
Failed to prove the following goals:
  1. Steel.ST.Reference.pts_to r0 Steel.FractionalPermission.full_perm (FStar.Ghost.reveal ?.n)
The remaining conjuncts in the separation logic context available for use are:
  1. Steel.ST.Reference.pts_to r0 p0 0
The typing context is:
  p0 : Steel.FractionalPermission.perm
  r0 : Steel.ST.Reference.ref Prims.nat

2 errors were reported (see above)

The first error is always reported when a Pulse term fails to check: It's the top-level failure raised by the Pulse tactic.
The second error is the relevant one here:

• It points to the source location of the r0 := 1
• It says that it could not infer some of the implict arguments, in this case ?.n. That n refers to the name of the bound variable in the primitive Pulse.Steel.Wrapper.write ... so, it's not very meaningful in this case, but for a user-defined Pulse function, the name of the uninferred implicit should help.
• It prints the part of the precondition that couldn't be proven, showing the unresolved occurrence of the ?.n
• It shows what was available in the context for matching and all the other typing hypotheses in the environment

I guess it could be nicer if we could somehow highlight the difference why the goal couldn't be matched in the context, e.g., highlighting the full_perm vs p0. But that's for another day ...

Thanks for the report!