Chalk hang in Ajour

[lnicola]

https://github.com/ajour/ajour/

Minimized code:

fn query_and_sort_catalog(addons: &[()]) {
    let mut catalog_rows_and_score = addons
        .iter()
        .filter_map(|a| Some((a, 0)))
        .filter(|(a, _)| true)
        .map(|(a, score)| (a, 0))
        .collect::<Vec<_>>();

    catalog_rows_and_score.sort_by(|(addon_a, score_a), (addon_b, score_b)| score_a.cmp(&score_b));
}

fn main() {}

[lnicola]

CC @detrumi you might want to take a look at this.

[detrumi]

Chalk hangs on this goal:

solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: AliasEq(<{closure:ClosureId(3)}<[?0 := () for<0> [?0 := (&'static 2<[?0 := ^1.0, ?1 := (&'static ^1.1)]>), ?1 := (&'static 2<[?0 := ^1.2, ?1 := ^1.1]>), ?2 := Ordering<[]>]]> as FnOnce<2<[?0 := (&'static 2<[?0 := ^0.3, ?1 := ^0.4]>), ?1 := (&'static 2<[?0 := ^0.3, ?1 := ^0.4]>)]>>>::Output = Ordering<[]>) }, binders: [U0 with kind type, U0 with kind type, U0 with kind type, U0 with kind type, U0 with kind type] }, universes: 1 }

It then keeps on expanding:

goal: Normalize(<{closure:ClosureId(3)}<[?0 := () for<0> [?0 := (&'static 2<[?0 := ^1.0, ?1 := (&'^1.1 (&'^1.2 (&'^1.3 (&'^1.4 (&'^1.5 (&'^1.6 (&'^1.7 (&'^1.8 (&'^1.9 (&'^1.10 (&'^1.11 (&'^1.12 (&'^1.13 (&'^1.14 (&'^1.15 (&'^1.16 (&'^1.17 (&'^1.18 (&'^1.19 (&'^1.20 (&'^1.21 (&'^1.22 (&'^1.23 (&'^1.24 (&'^1.25 (&'^1.26 (&'^1.27 (&'^1.28 (&'^1.29 (&'^1.30 (&'^1.31 (&'^1.32 (&'^1.33 (&'^1.34 ^1.35))))))))))))))))))))))))))))))))))]>), ?1 := (&'static 2<[?0 := ^1.36, ?1 := (&'^1.2 (&'^1.3 (&'^1.4 (&'^1.5 (&'^1.6 (&'^1.7 (&'^1.8 (&'^1.9 (&'^1.10 (&'^1.11 (&'^1.12 (&'^1.13 (&'^1.14 (&'^1.15 (&'^1.16 (&'^1.17 (&'^1.18 (&'^1.19 (&'^1.20 (&'^1.21 (&'^1.22 (&'^1.23 (&'^1.24 (&'^1.25 (&'^1.26 (&'^1.27 (&'^1.28 (&'^1.29 (&'^1.30 (&'^1.31 (&'^1.32 (&'^1.33 (&'^1.34 ^1.37)))))))))))))))))))))))))))))))))]>), ?2 := Ordering<[]>]]> as FnOnce<2<[?0 := (&'static 2<[?0 := ^0.38, ?1 := (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static ^0.39)))))))))))))))))))))))))))))))))]>), ?1 := (&'static 2<[?0 := ^0.38, ?1 := (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static (&'static ^0.39)))))))))))))))))))))))))))))))))]>)]>>>::Output -> Ordering<[]>)

[lnicola]

Marking as "broken window" because it's a bad issue that can make people think RA doesn't work at all. Marking "unactionable" because we need to wait for a chalk fix.

[matklad]

@flodiebold IIRC, we use fuel for chalk, right? Is there perhaps some quick fix here to make this run out of fuel, rather than completely hang?

[flodiebold]

The recursive solver doesn't support fuel, and IIRC it's kind of hard to implement there 🤔

[matklad]

Heh, this shows the depth of my knowledge about our current state of type inference. I had a vague feeling that something happened to chalk fuel...

[flodiebold]

There were also the plans with making the recursive solver cacheable through Salsa, which I think would make fuel even harder (unless we implement it in Salsa? 🤔 )

[Veykril]

The provided snippet no longer hangs, I assume fuel being re-added fixed this?

[lnicola]

I suspect a lot of these turned into type inference issues. But chalk is mostly abandoned so we can't do anything about it in the short/medium term.

[Veykril]

anythings better than hangs though, and as these are mainly chalk issues they are out of our hands anyways. I don't think we gain much from having a bunch of them open.