ICE: cannot infer substitution during normalization

[ranjitjhala]

(Creating a separate issue from #808 FTR)

@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

Originally posted by @nilehmann in #808 (comment)

[ranjitjhala]

[ see other commentary in #808 ]

[ranjitjhala]

Good point! Can you make a small mock for the real thing with FnOnce ?

[nilehmann]

This is a minimal example that should trigger the original behavior in #808

trait Trait {
    type Assoc;
}

struct S<T> {
    fld: T,
}

impl<T1, T2> Trait for S<T1>
where
    T1: FnOnce() -> T2,
{
    type Assoc = T1;
}

fn test(x: <S<fn()> as Trait>::Assoc) {}

[nilehmann]

Even simpler. The following triggers the normalization for function pointers which is orthogonal to the ambiguous substitution part of this issue

fn test01<F: FnOnce() -> i32>(f: F) -> F::Output {
    f()
}

fn test02(f: fn() -> i32) -> i32 {
    test01(f)
}

It turns out it's "working" thanks to this (unsound) hack

flux/crates/flux-middle/src/rty/projections.rs

Line 129 in 9695996

let ty = self.normalize_projection_ty_with_rustc(obligation)?;

[ranjitjhala]

Reopening to make sure we actually fix the issue described in #808 re: FnOnce and FnPtr

[ranjitjhala]

btw the hack is only unsound once we allow refinements on fnptrs, yes?

[nilehmann]

btw the hack is only unsound once we allow refinements on fnptrs, yes?

The hack is unsound if:

1. The type being normalized has refinements
2. The normalization candidate has refinements (e.g., a projection predicate with refinements on a type parameter)

So yes, it's not unsound for fn ptrs unless we allow refinements on them because 2. doesn't apply here.

[ranjitjhala]

indeed the above don't trigger the ICE... probably should fix at the same time as #803

[enjhnsn2]

The original issue from #808 still appears to fail:

#[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);
}

This errs with:

error: internal compiler error: crates/flux-middle/src/rty/projections.rs:516: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 } }
   --> src/main.rs:786:17
    |
786 |     let found = get_filter_map().find(|_| true);
    |    

Do we have a solution for this?

@nilehmann @ranjitjhala

[nilehmann]

@enjhnsn2 I think we never fix #808. The fix we implemented didn't consider fn trait bounds. I'm preparing a fix.

[enjhnsn2]

@nilehmann
#892 fixes the issue above, however, I have a test case closer to the actual tock code that is still failing:

pub trait MyTrait {}

pub type Handle = &'static dyn MyTrait;

pub fn filter_handles(
    slice: &'static [Option<Handle>],
) -> core::iter::FilterMap<
     core::slice::Iter<'static, Option<Handle>>, 
     fn(&Option<Handle>) -> Option<Handle>> 
{
    slice.iter().filter_map(|&x| x)
}

which fails with the error:

error: internal compiler error: crates/flux-infer/src/infer.rs:674:17: assertion `left == right` failed
                                  left: for<'_> fn(&'_0 Option<λb0. &'?38 dyn MyTrait + '?39[b0]>[]) -> Option<λb1. &'?40 dyn MyTrait + '?41[b1]>[]
                                 right: for<'_> fn(&'_0 Option<λb0. &'_ dyn MyTrait + '_[b0]>[]) -> Option<λb1. &'_ dyn MyTrait + '_[b1]>[]
   --> src/main.rs:802:5
    |
802 |     slice.iter().filter_map(|&x| x)
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

It looks like there is just a lifetime parameter that needs to be erased to make them match, but idk.

[nilehmann]

I'll take a look. I think the assert is just being overly cautious.