creusot
creusot copied to clipboard
Broken interaction betwene `extern_spec!` and trait method generics
We like to use ExternSpec
to strengthen the predicates associated to trait methods. This works pretty well for methods of traits which do not have additional generic parameters, but completely breaks when they do. Not only do the extern_specs!
start to have issues properly typing, it becomes impossible to even write a valid instance of the methods in question!
Consider the following example, we have a trait T
from std
:
trait T {
fn m<B>(...);
}
and we give an extern_spec!
trait T {
#[contract...]
fn m<B>(...) where B : AdditionalConstraint;
}
How do you actually write a valid impl of T
now? Your impl cannot add B : AdditionalConstraint
as this will cause rust to yell at you saying impl has stricter requirements than trait