Bad error when forgetting to let-bind

[mtzguido]

This:

fn kswap
  (#t:Type0)
  (r1 : ref t)
  (#v1 : erased t)
  requires pts_to r1 v1
  ensures  pts_to r1 v1
{
  r1 := !r1;
}

Gives:

* Error 19 at src/examples/GPU.Polymorphism.fst(13,12-18,9):
  - Assertion failed
  - The SMT solver could not prove the query. Use --query_stats for more
    details.
  - Raised within Tactics.refl_tc_term

* Error 228 at src/examples/GPU.Polymorphism.fst(18,2-18,2):
  - Ill-typed term:r1 := !r1

which is not very clear.

If we use a concrete type, like int, instead of a type variable, things are slightly better. There is no SMT query so the failure is fast and we get:

* Error 228 at src/examples/GPU.Polymorphism.fst(11,0-18,1):
  - Could not check term: r1 := !r1

* Error 12 at src/examples/GPU.Polymorphism.fst(17,8-17,11):
  - Expected type Prims.int
    but !r1
    has type
        Pulse.Lib.Core.stt Prims.int
          (Pulse.Lib.Reference.pts_to r1 (FStar.Ghost.reveal (*?u107*) _))
          (fun x ->
              Pulse.Lib.Reference.pts_to r1 (FStar.Ghost.reveal (*?u107*) _) **
              Pulse.Lib.Core.pure (FStar.Ghost.reveal (*?u107*) _ == x))
  - Raised within Tactics.refl_instantiate_implicits

Which is a mouthful but a better clue.