Should we also hoist/ANF ghost calls?

[mtzguido]

See this snippet, the last definition fails since we are not hosting the reveal b in the condition of the if.

ghost
fn test1 (b : erased bool)
{
  let vb = reveal b;
  if (vb) {
    ();
  } else {
    ();
  }
}

ghost
fn st_reveal (#a:Type0) (x : erased a)
  returns r : a
  ensures pure (r == reveal x)
{
  reveal x;
}

ghost
fn test2 (b : erased bool)
{
  if (st_reveal b) {
    ();
  } else {
    ();
  }
}

// - Ill-typed term: b
// - Expected a term of type bool
// - refl_core_check_term failed:  Top ()
//   > top-level subtyping ()
//     - Expected a Total computation, but got Ghost
ghost
fn test3 (b : erased bool)
{
  if (reveal b) {
    ();
  } else {
    ();
  }
}

I suppose another fix is to allow if conditions to be ghost when we are in a ghost context.