False positive when checking for type parameter constraints #2236
Description
In the code below, Verus reports an error:
error: the type parameter `A7_B` is not constrained by the impl trait, self type, or predicates
--> scratch/map.rs:15:6
|
15 | impl <B, I, F> T for core::iter::Map<I, F>
| ^^^^
even though B appears in the bound for F. I think we need to fix this if we want to provide a specification for the std::iter::Map iterator adaptor.
use vstd::prelude::*;
verus! {
#[verifier::external_body]
#[verifier::external_type_specification]
#[verifier::reject_recursive_types(I)]
#[verifier::reject_recursive_types(F)]
pub struct ExMap<I, F>(core::iter::Map<I, F>);
trait T: core::iter::Iterator {
spec fn test() -> bool;
}
impl <B, I, F> T for core::iter::Map<I, F>
where
I: Iterator,
F: FnMut(I::Item) -> B,
{
spec fn test() -> bool {
true
}
}
}