Improve error when implicit is solved to ghost value

[mtzguido]

#lang-pulse
open Pulse

fn foo (r : ref int) (#x : int)
  requires pts_to r x
  ensures  pts_to r x
{ () }

fn test (r : ref int) (#x : erased int)
  requires pts_to r x
  ensures  pts_to r x
{
  foo r;
}

The previous snippet should fail indeed, since we can't reveal x, but the error is not very informative:

- prover error
- For term (<stapp>foo r #x) implicit solution x has ghost effect