Uninformative error message for a write without full permission about steel HOT 1 CLOSED

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!

from steel.