Ascriptions in local lets seemingly dropped

[mtzguido]

fn foo (xy : int & int)
  requires
    pure (xy._1 > 0 /\ xy._2 > 0)
{
  admit();
}

fn test0 (r : ref pos) // works
  preserves live r
{
  let vx = !r;
  let vy = !r;
  foo ((vx <: int), (vy <: int));
  ()
}

fn test (r : ref pos) // fails
  preserves live r
{
  let vx = !r <: int;
  let vy = !r <: int;
  foo (vx, vy);
  ()
}

- Ill-typed term
- Assertion failed
- The SMT solver could not prove the query.
- Env =
    (r : Pulse.Lib.Reference.ref Prims.pos) (y : FStar.Ghost.erased Prims.pos)
    (vx : Prims.pos) (__ : Prims.squash (Pulse.Lib.Core.rewrites_to_p vx y))
    (vy : Prims.pos) (__ : Prims.squash (Pulse.Lib.Core.rewrites_to_p vy y))
- VC = forall (i: Prims.int). Prims.l_True == (i > 0 == true)
- Also see: Prims.fst:165.28-165.39

The last tuple is pos & pos, so it does not match the call

Related to #2452, #3772?

[mtzguido]

This passes

fn test (r : ref int)
  preserves live r
{
  let vx = !r <: pos;
  ()
}

They are just completely ignored by the hoisting phase, due to calling collect_app_ln which unascribes terms.