flux-rs / flux

Refinement Types for Rust
MIT License
663 stars 21 forks source link

Fail to equate BaseTypes for `dyn Trait` #790

Closed enjhnsn2 closed 2 months ago

enjhnsn2 commented 2 months ago

This is a test case reduction for one of the failing test cases in Tock.

When I attempt to verify the code:

pub trait MyTrait<'a> {}
pub struct MyStruct {
    t: &'static dyn MyTrait<'static>,
}

pub fn new(t: &'static dyn MyTrait) -> MyStruct {
    MyStruct {
        t
    }
}

It fails with:

thread 'rustc' panicked at crates/flux-infer/src/infer.rs:551:17:
assertion `left == right` failed
  left: [MyTrait<'?11>]
 right: [MyTrait<'static>]

which points to the code: https://github.com/flux-rs/flux/blob/46965ea0ecdeb7747d0a70aa4aae6290e247a20b/crates/flux-infer/src/infer.rs#L550-L553 that seems to be equating two basetypes for dyn Traits.

My guess is that the lifetimes are not getting normalized which leads to the assertion failure. Not an urgent issue, but fixing this will let me untrust about ~100 lines of code in Tock and it doesn't look too hard (although I don't really know).