top-level ghost effect accepted

[mtzguido]

let foo () : GTot int = 123

let bar : int = foo () + 1

This code warns like so:

* Warning 272 at G.fst(7,0-7,28):
  - Top-level let-bindings must be total; this term may have effects

but does extract into an empty module, having erased the ghost terms. This is somewhat expected for foo (it's a ghost function) but I did not expect it for bar. I would expect a hard error if we have a ghost top-level call. Maybe the user is indeed working with top-level effects (to do initialization) and has this warning disabled; if so, a ghost sub-term can invalidate the full initialization step in bar, silently.

Should we just error out on a ghost top-level effect?