Fstar core modelling of IntoIterator trait fails on some generated code using it

[maximebuyse]

/* fn test(items: impl IntoIterator<Item = i32>) -> bool {
    let mut has_negative = false;
    for i in items.into_iter() {
        if i < 0{
            has_negative = true
        }
    }
    has_negative
} */

fn test(items: impl IntoIterator<Item = bool>) -> bool {
    items.into_iter().next().unwrap_or(false)
}
fn main (v: Vec<bool>) -> bool {
    test(v)
}

Open this code snippet in the playground

The generated code has the following lax-checking error:

* Error 228 at Playground.fst(19,7-19,38):
  - Could not solve typeclass constraint
      `Core.Iter.Traits.Iterator.iterator i1.f_IntoIter`
  - See also FStar.Tactics.Typeclasses.fst(297,6-300,7)

[franziskuskiefer]

Needs a fix in F* core iter library.

[franziskuskiefer]

Let's PR the changes @maximebuyse

[maximebuyse]

Let's PR the changes @maximebuyse

Actually the IntoIter problem that I fixed in #1192 is different. So as far as I know, the issue here still needs a fix.