flux::alias does not propagate across crates

[enjhnsn2]

The following code declares a type FluxPtr indexed by ptr: int and an alias FluxPtrU8 that is also indexed by the same variable. The struct CortexMLocation is then indexed by this same variable. This code passes verification.

#[flux::opaque]
#[flux::refined_by(ptr: int)]
pub struct FluxPtr {
    _inner: *mut u8,
}

#[flux::alias(type FluxPtrU8[ptr: int] = FluxPtr[ptr])]
pub type FluxPtrU8 = FluxPtr;

#[flux::refined_by(ptr: int)]
struct CortexMLocation {
    #[flux::field(FluxPtrU8[addr])]
    pub addr: FluxPtrU8,
}

However, if you split up the code: other/lib.rs (another crate)

#[flux::opaque]
#[flux::refined_by(ptr: int)]
pub struct FluxPtr {
    _inner: *mut u8,
}

#[flux::alias(type FluxPtrU8[ptr: int] = FluxPtr[ptr])]
pub type FluxPtrU8 = FluxPtr;

main.rs

use other::*;
#[flux::refined_by(ptr: int)]
struct CortexMLocation {
    #[flux::field(FluxPtrU8[addr])]
    pub addr: FluxPtrU8,
}

It fails with

  --> src/main.rs:88:29
   |
88 |     #[flux::field(FluxPtrU8[addr])]
   |                             ^^^^ expected `FluxPtrU8`, found `int`

because the information from the flux::alias (that FluxPtrU8 has an int index) got lost at some point.