Some bad error messages

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 (1,0-1,0)
Ambig.fst(1, 1): related location
```

Reproduce the two Pulse examples and inspect the reported paths through Tactics.refl_core_check_term_at_type, refl_core_check_term, and top-level subtyping. Compare the diagnostics with the intended refinement and type errors; done means both examples report clear, relevant failure locations and explanations.

Written by the indexing model from the issue text.