ICE: to_sort_list called on bound variable list with non-refinements

[enjhnsn2]

This is a test case reduction of one of the Tock errors.

When I try to verify the code:

#[flux_rs::trusted]
pub fn get_filter_map(
) -> core::iter::FilterMap<core::slice::Iter<'static, Option<()>>, fn(&Option<()>) -> Option<()>> {
    unimplemented!()
}

fn use_filter_map() {
    let found = get_filter_map().find(|_| true);
}

It triggers the error:

error: internal compiler error: crates/flux-middle/src/rty/binder.rs:232:25: `to_sort_list` called on bound variable list with non-refinements
   --> src/main.rs:612:17
    |
612 |     let found = get_filter_map().find(|_| true);
    |                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

This error occurs 3 times in Tock, always with the FilterMap struct.

[nilehmann]

#812 fixes the issue with to_sort_list, but now we get

error: internal compiler error: crates/flux-middle/src/rty/projections.rs:342:21: cannot infer substitution for param GenericParamDef { name: "B", def_id: DefId(2:6179 ~ core[0688]::iter::adapters::filter_map::{impl#2}::B), index: 0, pure_wrt_drop: false, kind: Type { has_default: false, synthetic: false } }
  --> attic/playground.rs:14:17
   |
14 |     let found = get_filter_map().find(|_| true);
   |                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Ztrack-diagnostics: created at crates/flux-middle/src/rty/projections.rs:342:21

[ranjitjhala]

I'm seeing a lot of these cannot infere substitution for ... errors elsewhere too.

[nilehmann]

@ranjitjhala This is a bit tricky. When we normalize <MyType<...> as MyTrait<...>>::Assoc we get back an impl of the form

impl<T1, ..., Tn> MyTrait<...> for MyType<..> { 
    type Assoc = ...
}

Where T1,...,Tn are used as args for Trait and Type. To proceed with the normalization we need to find a substitution for the T1,...,Tn based on the refinements we have. For example, if we have

impl<T> MyTrait for MyType<T> {
    type Assoc = T;
}

And we are trying to normalize <MyType<Nat> as MyTrait>::Assoc we get the substitution T -> Nat by matching MyType<Nat> against MyType<T>. This step is important because with this substitution we can infer that <MyType<Nat> as MyTrait>::Assoc normalizes to Nat.

Now, the implementation of Iterator for FilterMap looks like:

impl<B, I: Iterator, F> Iterator for FilterMap<I, F>
where
    F: FnMut(I::Item) -> Option<B>,
{
    type Item = B;
    ...
}

The B is not used in Iterator or in FilterMap<I, F> so we can't find a substitution for it when doing the matching. The B appears to be unconstrained but it's actually constrained by the bound F: FnMut(I::Item) -> Option<B>. This bounds desugars to the bounds

F: FnMut<I::Item>,
F::Output == Option<B>   

The second equality bound is constraining B

[ranjitjhala]

interesting... what is the method name we're working with here? does the B not appear anywhere in it's signature?

[nilehmann]

This happens when normalizing this signature

pub fn get_filter_map(
) -> core::iter::FilterMap<core::slice::Iter<'static, Option<()>>, fn(&Option<()>) -> Option<()>>;

In this case B must be equal to (). I think the logic goes something like:

1. By matching FilterMap<I, F> against core::iter::FilterMap<core::slice::Iter<'static, Option<()>>, fn(&Option<()>) -> Option<()>> we can infer
   I = core::slice::Iter<'static, Option<()>>
F = fn(&Option<()>) -> Option<()>
2. Because fn(&Option<()>) -> Option<()> implements FnMut we can normalize <fn(&Option<()>) -> Option<()> as FnMut>::Output to Option<()>.
3. From the bound F::Output == Option<B> and the normalization in 2. we can infer B = ()

[nilehmann]

I think implementing the logic above is not too crazy. Another alternative is to try to improve our fallback when there are no refinements to be seen.

[nilehmann]

Anyhow, here's a minimal reproduction of the issue

trait Trait1 {
    type Assoc1;
}

impl Trait1 for i32 {
    type Assoc1 = i32;
}

trait Trait2 {
    type Assoc2;
}

struct S<T> {
    f: T,
}

impl<T1, T2> Trait2 for S<T2>
where
    T2: Trait1<Assoc1 = T1>,
{
    type Assoc2 = T1;
}

fn test(x: <S<i32> as Trait2>::Assoc2) {}

[ranjitjhala]

Closing the "original" issue as solved; have forked the second thing out in #829