Potential unsoundness involving Any/downcasting

[dewert99]

I noticed that while flux's assumption about parametricity mostly holds, it has potential issues with downcasting. flux does seem to notice that type parameters with an explicit T: 'static bound don't have paramatricity, but misses implicit bounds caused by having &'static T in scope. For example flux verifies:

fn not_id<T>(mut t: T, _: PhantomData<&'static T>) -> T {
    let m: &mut dyn Any = &mut t;
    if let Some(n) =  m.downcast_mut(){
        *n = 42
    }
    t
}


#[sig(fn (b:bool[true]))]
pub fn assert(b:bool) {
    if !b { panic!("assertion failed") }
}

fn main() {
    assert(not_id(0u32, PhantomData) == 0u32)
}

While this issue could be addressed by not considering paramatricity for type parameters rustc can infer outlive 'static, there could still be potential unsound interactions with other crates that allow downcasting without 'static bounds.

For example, while the following example produces and error in flux

use castaway::cast;
use flux_rs::*;

fn not_id2<T>(mut t: T) -> T {
    if let Ok(n) = cast!(&mut t, &mut u32) {
        *n = 42;
    }
    t
}

#[sig(fn (b:bool[true]))]
pub fn assert(b:bool) {
    if !b { panic!("assertion failed") }
}

fn main() {
    assert(not_id2(0u32) == 0u32)
}

error[E0999]: internal flux error: crates/flux-infer/src/infer.rs:579:22
 --> src/main.rs:6:20
  |
6 |     if let Ok(n) = cast!(&mut t, &mut u32) {
  |                    ^^^^^^^^^^^^^^^^^^^^^^^
  |
  = note: incompatible types: `ptr(mut['?32], _1)` - `&'_ mut ∃b0. { T[b0] | * }`
  = note: this error originates in the macro `cast` (in Nightly builds, run with -Z macro-backtrace for more info)

error: could not compile `flux-test` (bin "flux-test") due to 1 previous error

If not_id2 came from a different crate flux would also verify it.