[Lean] Equality constraints on associated types of parent trait

[abentkamp]

Equality constraints on associated types of parent trait don't work well with Lean's type class search:

trait T1 {
    type A1;
    fn mkA1() -> Self::A1;
}

trait T2: T1 {}

fn m<T: T2<A1 = u8>>() -> u8 {
    T::mkA1()
}

impl T1 for bool {
    type A1 = u8;
    fn mkA1() -> u8 {
        0
    }
}

impl T2 for bool {}

fn test() -> u8 {
    m::<bool>()
}

https://hax-playground.cryspen.com/#fstar/latest-main/gist=bd6e8f2de5ed1832941dae51e093f1a5

[abentkamp]

The issue here is that when calling T::mkA1(), Lean's type class search looks for an instance of T1. To find an instance of T1, it finds that an instance of T2 would also be okay. Then, unfortunately, it commits to the associated types being arbitrary instead of allowing for A1 = u8. Perhaps this could be solved by declaring associated types using ( ... ) instead of [ ... ] to avoid immediate instantiation.