Should we also hoist/ANF ghost calls?

See this snippet, the last definition fails since we are not hosting the `reveal b` in the condition of the if.
```fstar
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.

Start with the three F* examples in the issue, comparing test1, test2, and test3 and the reported type-checking failure. Determine which behavior is intended—hoisting/ANF of ghost calls or allowing ghost conditions in a ghost context—and define completion against these examples.

Written by the indexing model from the issue text.