Opaque type issue

[cynecx]

This chalk test fails:

#[test]
fn warp() {
    test! {
        program {
            struct Product<H, T>
            where
              T: HList
            {}

            trait HList {
              type Tuple: Tuple<HList=Self>;
            }

            trait Tuple {
              type HList: HList<Tuple=Self>;
            }

            trait Combine<T>
            where
              T: HList
            {
              type Output: HList;
            }

            impl<T> Combine<T> for ()
            where
                T: HList
            {
                type Output = T;
            }

            impl<H, T, U> Combine<U> for Product<H, T>
            where
                T: HList,
                T: Combine<U>,
                U: HList,
                Product<H, <T as Combine<U>>::Output>: HList,
            {
                type Output = Product<H, <T as Combine<U>>::Output>;
            }

            impl HList for () {
                type Tuple = ();
            }

            impl Tuple for () {
                type HList = ();
            }

            impl<T16> HList for Product<T16, ()> {
                type Tuple = (T16,);
            }
            impl<T16> Tuple for (T16,) {
                type HList = Product<T16, ()>;
            }

            trait FilterBase {
              type Extract: Tuple;
            }

            trait Filter
            where Self: FilterBase {
            }

            impl<T> Filter for T
            where T: FilterBase {}

            trait Mumbo {
              type Extract;
            }

            impl<T, U> Mumbo for (T, U)
            where
              T: Filter,
              U: Filter,
              <<T as FilterBase>::Extract as Tuple>::HList: Combine<<<U as FilterBase>::Extract as Tuple>::HList>
            {
              type Extract = <<<<T as FilterBase>::Extract as Tuple>::HList as Combine<<<U as FilterBase>::Extract as Tuple>::HList>>::Output as HList>::Tuple;
            }

            struct Exact<T> {}
            impl<T> FilterBase for Exact<T> {
              type Extract = ();
            }

            struct Param {}
            impl FilterBase for Param {
              type Extract = (usize,);
            }

            opaque type AnonParam: FilterBase<Extract = (usize,)> = Param;
        }

        goal {
            (Exact<usize>, Param): Mumbo
        } yields {
            "Unique; substitution [], lifetime constraints []"
        }

        goal {
            (Exact<usize>, AnonParam): Mumbo
        } yields {
            "Unique; substitution [], lifetime constraints []"
        }
    }
}

The second goal should succeed, however it fails with "No possible solution".

Ref: rust-lang/rust-analyzer#4774

[shamatar]

I've tried to solve it. One aspect that I've found that for any tuple facts about it's members were missing, like the fact of aliasing AnonParam and Param. Unfortunately it was not enough to guide the solver. I think the problem is in trying to prove for<type, type> Implemented(<<Exact<Uint(Usize)> as FilterBase>::Extract as Tuple>::HList: Combine<<<^0.0 as FilterBase>::Extract as Tuple>::HList>) :- Implemented(^0.1: Combine<<<^0.0 as FilterBase>::Extract as Tuple>::HList>), AliasEq(<<Exact<Uint(Usize)> as FilterBase>::Extract as Tuple>::HList = ^0.1) roughly reading that for some ^0.1 that is ^0.0...HList for some ^0.0 such ^0.1 is itself a HList for Exact<Uint(Usize)>. Logically we should normalize <Exact<Uint(Usize)> as FilterBase>::Extract as Tuple>::HList immediately and check for all available implementations for concrete substitution of ^0.1. But solver goes some other way for<type, type> AliasEq(<<Exact<Uint(Usize)> as FilterBase>::Extract as Tuple>::HList = ^0.0) :- AliasEq(<^0.1 as Tuple>::HList = ^0.0), AliasEq(<Exact<Uint(Usize)> as FilterBase>::Extract = ^0.1) that makes more substitutions and while it's formally correct it's kind of road to nowhere.

May be someone can provide extra guideness