Using values returned by ghost fun

[mtzguido]

ghost
fn ghostpair ()
  requires emp
  returns r : int & int
  ensures emp
{
  admit();
}

fn use_ghost ()
  requires emp
  ensures emp
{
  let Mktuple2 x y = ghostpair();
  ()
}

Fails with

- Expected a term with a non-informative (e.g., erased) type.
- Got: int & int

It would be nice if instead of failing to reveal the tuple, we would bind x and y to erased values.