Some bad error messages

[mtzguido]

First:

```pulse
fn foo ()
  requires emp
  ensures  emp
{
  let x : nat = -1;
  ()
}
```

Highlights the whole body and says:

- Expected a term with a non-informative (e.g., erased) type; got
  squash (x == - 1)

Very puzzling since we expect to see that we failed to prove the refinement, and on top of that squash is actually non-informative?

Second:

```pulse
fn foo (y:string)
  requires emp
  ensures  emp
{
  let x : nat = y;
  ()
}
```

Highlights the whole definition (from backticks to backticks) and says:

- refl_core_check_term failed:  Top ()
  > top-level subtyping ()
  Prims.string is not a subtype of i: Prims.int{i >= 0}
- Raised within Tactics.refl_core_check_term_at_type
- See also <input>(1,0-1,0)
Ambig.fst(1, 1): related location

[JonasAlaif]

Another bad error message issue that I ran into is with partially applied functions with "preconditions", the error doesn't point to the actual use which violates the precondition. For example:

open Pulse.Lib.Pervasives

let divide (a: erased int) (b: erased int { reveal b <> 0 }) : GTot (erased int) = a / b

```pulse
fn test()
  requires emp
  ensures emp
{
    let hundred = divide 100;
    let unknown = hundred 0;
    ()
}
\```

results in an error pointing to divide in let hundred = divide 100; with a secondary span pointing to the b argument of divide. This makes the error very difficult to debug if I used hundred in multiple places in the fn and I'm not sure which one may have been called with 0