fix type-inference issues in ghost code

[utaal]

by using a quirk of type inference with (inline) functions and unreachable_unchecked returning never.

In a nutshell, we're going to exploit this behavior:

pub struct Ghost<A> {
    p: std::marker::PhantomData<A>,
}

impl<A> Ghost<A> {
    fn from_fn(_: fn()->A) -> Ghost<A> {
        Ghost { p: std::marker::PhantomData }
    }
}

pub fn foo() {
    let l = Ghost::from_fn(|| unreachable!());
}

This type-checks successfully, despite l appearing underconstrained.

This is exactly the situation we encounter in a program like:

fn main() {
    let b = Ghost(4nat);
}

where b remained unconstrained after erasure.

This example program used to fail during compilation with:

error[E0282]: type annotations needed for `builtin::Ghost<A>`
  |
6 |     let b = Ghost(4nat);
  |         ^
  |
help: consider giving `b` an explicit type, where the type for type parameter `A` is specified
  |
6 |     let b: builtin::Ghost<A> = Ghost(4nat);
  |          +++++++++++++++++++

error: aborting due to previous error

and it now compiles successfully with this patch.

The technique was discovered in collaboration with @xldenis.

[utaal]

See also creusot-rs/creusot#905.

[Chris-Hawblitzel]

Cool! Do we need unsafe, or can we write it like:

pub struct Ghost<A> {
    p: std::marker::PhantomData<A>,
}
impl<A> Ghost<A> {
    #[inline(always)]
    fn from_fn(_: fn() -> A) -> Ghost<A> {
        Ghost { p: std::marker::PhantomData }
    }
}
pub fn ghost_erased() -> ! {
    panic!()
}
pub fn foo() {
    let l = Ghost::from_fn(|| { ghost_erased() });
}

[utaal]

That works too. I think it's essentially equivalent, as we should never call those lambdas, but I can see we may prefer to avoid unsafe anyway. The only difference may be that panic!() and the call to ghost_erased() may still produce some amount of code in the resulting library/binary, while unreachable_unchecked() may result in a little bit less code, but I haven't measured it.

I replaced the unsafe blocks with unreachable!() directly. Does that work or do you specifically prefer a separate ghost_erased function?

[jaybosamiya]

To reduce the amount of code generated, the best approaches to get the ! are the unsafe unreachable_unchecked() or the infinite loop loop {}. Notice that in this Compiler Explorer test, those two are the only ones that were entirely optimized out.

Fwiw, I don't think we should worry about the amount of code generated for this, since it should be dead-code-eliminated anyways in practice. We should go with whatever is clearest, and imho unreachable!() is the most clear with its intention there.