Improve inference of Ghost when erased

[xldenis]

See: verus-lang/verus#875

This improves the type inference of gh! when dealing with erased code.
Previously, it was required to always annotate gh bindings if you wanted the erased code to work. This was because when the gh code is erased, type inference is missing information to determine a concrete type and rustc will reject the code as ambiguous.

For example, the following failed to compile with rustc previously:

let x = gh! { 5 };

This PR fixes it by exploiting the coercion from ! to any type in Rust, so that when erased, we will 'default' to Ghost<!> while remaining capable to unify with any possible type annotation that was provided in a binding.

this was found in collaboration with @utaal