creusot icon indicating copy to clipboard operation
creusot copied to clipboard

Broken interaction betwene `extern_spec!` and trait method generics

Open xldenis opened this issue 2 years ago • 0 comments

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

xldenis avatar Oct 17 '22 19:10 xldenis