a-mir-formality icon indicating copy to clipboard operation
a-mir-formality copied to clipboard

Negative bounds (with feature gate)

Open yoshuawuyts opened this issue 2 years ago • 0 comments

A counterpart to https://github.com/rust-lang/a-mir-formality/issues/73 enabling negative bounds checking. Currently the impl in the compiler is being reworked to make use of the new trait solver (https://github.com/rust-lang/rust/pull/112875). Despite the feature being unstable it would be great if MIR formality could model these rules.

Example

Negative bounds should only match on types which have negative trait impls. This example implements FooTrait for CoreStruct because CoreStruct implements !CoreTrait:

crate core {
    trait CoreTrait<> where [] {}
    struct CoreStruct<> where [] {}
    impl<> !CoreTrait<> for CoreStruct<> where [] {}
}
crate foo {
    trait FooTrait<> where [] {}
    impl<ty T> FooTrait<> for T where [T: !CoreTrait<>] {}
}

note: When converting this into a test some assertion should be written to ensure that CoreStruct actually implements FooTrait.

yoshuawuyts avatar Jul 04 '23 10:07 yoshuawuyts