rust-lang / chalk

An implementation and definition of the Rust trait system using a PROLOG-like logic solver
https://rust-lang.github.io/chalk/book/
Other
1.84k stars 182 forks source link

Solving closure goal keeps expanding lifetimes #688

Open detrumi opened 3 years ago

detrumi commented 3 years ago

Found in rust-analyzer#7796: When trying to solve this goal:

Implemented({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<[]>]
]> : FnMut<2<[
    ?0 := (&'static 2<[?0 := ^0.3, ?1 := ^0.4]>),
    ?1 := (&'static 2<[?0 := ^0.3, ?1 := ^0.4]>)
]>>)

Chalk keeps expanding the query when trying to normalize this:

Normalize(<{closure:ClosureId(3)}<[?0 := () for<0> [
    ?0 := (&'static 2<[?0 := ^1.0, ?1 := EXPAND_1]>),
    ?1 := (&'static 2<[?0 := ^1.36, ?1 := EXPAND_2]>),
    ?2 := Ordering<[]>]
]> as FnOnce<2<[
    ?0 := (&'static 2<[?0 := ^0.38, ?1 := EXPAND_3]>),
    ?1 := (&'static 2<[?0 := ^0.38, ?1 := EXPAND_3)]>)
]>>>::Output -> Ordering<[]>)

EXPAND_1 = (&'^1.1 (&'^1.2 (&'^1.3 ... (&'^1.34 ^1.35))))
EXPAND_2 = (&'^1.2 (&'^1.3 (&'^1.4 ... (&'^1.34 ^1.37))))
EXPAND_3 = (&'static (&'static ... (&'static ^0.39)))

It's tricky to translate the rust-analyzer example to a chalk test case because closures are involved, but hopefully this should be enough info to make the problem clear.

detrumi commented 3 years ago

rust-analyzer#7680 might also be related, as that keeps expanding nested queries with dyn/AliasEq, again inside a closure substitution.

jackh726 commented 3 years ago

I'm still having trouble creating a chalk test case that repros this. @detrumi do you think you could capture a CHALK_DEBUG log up to a couple rounds of expansion?

I have a feeling this might be caused by the difference in representation between the chalk-integration closure substs and rust-analyzer/rustc closure substs

detrumi commented 3 years ago

@jackh726 Sure! It's a lot of output, but I think this shows the first few repeats:

``` [INFO hir_ty::traits] trait_solve_query(Implements(|&(?0.0, &?0.1), &(?0.2, ?0.1)| -> Ordering: FnMut<(&(?0.3, ?0.4), &(?0.3, ?0.4))>)) solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: Implemented({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<[]>]]>: FnMut<2<[?0 := (&'static 2<[?0 := ^0.3, ?1 := ^0.4]>), ?1 := (&'static 2<[?0 := ^0.3, ?1 := ^0.4]>)]>>) }, binders: [U0 with kind type, U0 with kind type, U0 with kind type, U0 with kind type, U0 with kind type] }, universes: 1 } ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: FromEnv({closure:ClosureId(3)}<[?0 := () for<0> [?0 := (&'static 2<[?0 := ^1.0, ?1 := (&'^1.1 ^1.2)]>), ?1 := (&'static 2<[?0 := ^1.3, ?1 := ^1.4]>), ?2 := Ordering<[]>]]>: FnMut<2<[?0 := (&'static 2<[?0 := ^0.5, ?1 := ^0.6]>), ?1 := (&'static 2<[?0 := ^0.5, ?1 := ^0.6]>)]>>) }, binders: [U0 with kind type, U0 with kind lifetime, U0 with kind type, U0 with kind type, U0 with kind type, U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─0ms INFO solve_goal: solution = Err(NoSolution) prio High ├─┘ ├─0ms INFO solve_goal: solution = Err(NoSolution) prio High [INFO hir_ty::traits] trait_solve_query(Normalize(<|&(?0.0, &?0.1), &(?0.2, ?0.1)| -> Ordering as FnOnce<(&(?0.3, ?0.4), &(?0.3, ?0.4))>>::Output => Ordering)) 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 } ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: Normalize(<{closure:ClosureId(3)}<[?0 := () for<0> [?0 := (&'static 2<[?0 := ^1.0, ?1 := (&'^1.1 ^1.2)]>), ?1 := (&'static 2<[?0 := ^1.3, ?1 := ^1.4]>), ?2 := Ordering<[]>]]> as FnOnce<2<[?0 := (&'static 2<[?0 := ^0.5, ?1 := ^0.6]>), ?1 := (&'static 2<[?0 := ^0.5, ?1 := ^0.6]>)]>>>::Output -> Ordering<[]>) }, binders: [U0 with kind type, U0 with kind lifetime, U0 with kind type, U0 with kind type, U0 with kind type, U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'static ^0.0) <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ │ │ ├─0ms INFO solve_goal: solution = Ok(Ambig(Unknown)) prio High │ │ ├─┘ │ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: 'static: '^0.0 }, binders: [U0 with kind lifetime] }, universes: 1 } │ │ │ ├─0ms INFO solve_goal: solution = Ok(Unique(Canonical { value: ConstrainedSubst { subst: [?0 := '^0.0], constraints: [InEnvironment { environment: Env([]), goal: 'static: '^0.0 }] }, binders: [U0 with kind lifetime] })) prio High │ │ ├─┘ │ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ │ ├─┘ │ │ ├─0ms INFO solve_goal: solution = Ok(Ambig(Definite(Canonical { value: [?0 := ^0.0, ?1 := (&'^0.1 ^0.2)], binders: [U0 with kind type, U0 with kind lifetime, U0 with kind type] }))) prio High │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'^0.0 ^0.1) <: (&'static ^0.2)) }, binders: [U0 with kind lifetime, U0 with kind type, U0 with kind type] }, universes: 1 } │ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ │ ├─┘ │ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: '^0.0: 'static }, binders: [U0 with kind lifetime] }, universes: 1 } │ │ │ ├─0ms INFO solve_goal: solution = Ok(Unique(Canonical { value: ConstrainedSubst { subst: [?0 := '^0.0], constraints: [InEnvironment { environment: Env([]), goal: '^0.0: 'static }] }, binders: [U0 with kind lifetime] })) prio High │ │ ├─┘ │ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ │ ├─┘ │ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ │ ├─┘ │ │ ├─0ms INFO solve_goal: solution = Ok(Ambig(Unknown)) prio High │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'^0.0 ^0.1) <: (&'static ^0.2)) }, binders: [U0 with kind lifetime, U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'static ^0.0) <: (&'^0.1 ^0.2)) }, binders: [U0 with kind type, U0 with kind lifetime, U0 with kind type] }, universes: 1 } │ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ │ ├─┘ │ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: 'static: '^0.0 }, binders: [U0 with kind lifetime] }, universes: 1 } │ │ ├─┘ │ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ │ ├─┘ │ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ │ ├─┘ │ │ ├─0ms INFO solve_goal: solution = Ok(Ambig(Unknown)) prio High │ ├─┘ │ ├─0ms INFO solve_goal: solution = Ok(Ambig(Definite(Canonical { value: [?0 := ^0.0, ?1 := '^0.1, ?2 := ^0.2, ?3 := ^0.3, ?4 := (&'^0.4 ^0.5), ?5 := ^0.6, ?6 := (&'static ^0.7)], binders: [U0 with kind type, U0 with kind lifetime, U0 with kind type, U0 with kind type, U0 with kind lifetime, U0 with kind type, U0 with kind type, U0 with kind type] }))) prio High ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: (&'^0.1 ^0.2)) }, binders: [U0 with kind type, U0 with kind lifetime, U0 with kind type] }, universes: 1 } │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─0ms INFO solve_goal: solution = Ok(Ambig(Definite(Canonical { value: [?0 := (&'^0.0 ^0.1), ?1 := '^0.0, ?2 := ^0.2], binders: [U0 with kind lifetime, U0 with kind type, U0 with kind type] }))) prio High ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'^0.0 ^0.1) <: ^0.2) }, binders: [U0 with kind lifetime, U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─0ms INFO solve_goal: solution = Ok(Ambig(Definite(Canonical { value: [?0 := '^0.0, ?1 := ^0.1, ?2 := (&'^0.0 ^0.2)], binders: [U0 with kind lifetime, U0 with kind type, U0 with kind type] }))) prio High ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: 'static: '^0.0 }, binders: [U0 with kind lifetime] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'^0.0 ^0.1) <: (&'^0.0 ^0.2)) }, binders: [U0 with kind lifetime, U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─0ms INFO solve_goal: solution = Ok(Ambig(Unknown)) prio High ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'^0.0 ^0.1) <: (&'^0.0 ^0.2)) }, binders: [U0 with kind lifetime, U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: '^0.0: 'static }, binders: [U0 with kind lifetime] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'^0.0 ^0.1) <: (&'^0.0 ^0.2)) }, binders: [U0 with kind lifetime, U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'^0.0 ^0.1) <: (&'^0.0 ^0.2)) }, binders: [U0 with kind lifetime, U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'^0.0 ^0.1) <: (&'^0.0 ^0.2)) }, binders: [U0 with kind lifetime, U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'^0.0 ^0.1) <: (&'^0.0 ^0.2)) }, binders: [U0 with kind lifetime, U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: Normalize(<{closure:ClosureId(3)}<[?0 := () for<0> [?0 := (&'static 2<[?0 := ^1.0, ?1 := (&'^1.1 (&'^1.2 ^1.3))]>), ?1 := (&'static 2<[?0 := ^1.4, ?1 := (&'^1.2 ^1.5)]>), ?2 := Ordering<[]>]]> as FnOnce<2<[?0 := (&'static 2<[?0 := ^0.6, ?1 := (&'static ^0.7)]>), ?1 := (&'static 2<[?0 := ^0.6, ?1 := (&'static ^0.7)]>)]>>>::Output -> Ordering<[]>) }, binders: [U0 with kind type, U0 with kind lifetime, U0 with kind lifetime, U0 with kind type, U0 with kind type, U0 with kind type, U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'static ^0.0) <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'^0.0 ^0.1) <: (&'static ^0.2)) }, binders: [U0 with kind lifetime, U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'^0.0 ^0.1) <: (&'static ^0.2)) }, binders: [U0 with kind lifetime, U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'static ^0.0) <: (&'^0.1 ^0.2)) }, binders: [U0 with kind type, U0 with kind lifetime, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─0ms INFO solve_goal: solution = Ok(Ambig(Definite(Canonical { value: [?0 := ^0.0, ?1 := '^0.1, ?2 := '^0.2, ?3 := ^0.3, ?4 := ^0.4, ?5 := (&'^0.5 ^0.6), ?6 := ^0.7, ?7 := (&'static ^0.8)], binders: [U0 with kind type, U0 with kind lifetime, U0 with kind lifetime, U0 with kind type, U0 with kind type, U0 with kind lifetime, U0 with kind type, U0 with kind type, U0 with kind type] }))) prio High ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: Normalize(<{closure:ClosureId(3)}<[?0 := () for<0> [?0 := (&'static 2<[?0 := ^1.0, ?1 := (&'^1.1 (&'^1.2 ^1.3))]>), ?1 := (&'static 2<[?0 := ^1.4, ?1 := (&'^1.2 (&'^1.5 ^1.6))]>), ?2 := Ordering<[]>]]> as FnOnce<2<[?0 := (&'static 2<[?0 := ^0.7, ?1 := (&'static (&'static ^0.8))]>), ?1 := (&'static 2<[?0 := ^0.7, ?1 := (&'static (&'static ^0.8))]>)]>>>::Output -> Ordering<[]>) }, binders: [U0 with kind type, U0 with kind lifetime, U0 with kind lifetime, U0 with kind type, U0 with kind type, U0 with kind lifetime, U0 with kind type, U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─0ms INFO solve_goal: solution = Ok(Ambig(Unknown)) prio High ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'^0.0 ^0.1) <: (&'^0.0 (&'^0.2 ^0.3))) }, binders: [U0 with kind lifetime, U0 with kind type, U0 with kind lifetime, U0 with kind type] }, universes: 1 } │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─0ms INFO solve_goal: solution = Ok(Ambig(Definite(Canonical { value: [?0 := '^0.0, ?1 := (&'^0.1 ^0.2), ?2 := '^0.1, ?3 := ^0.3], binders: [U0 with kind lifetime, U0 with kind lifetime, U0 with kind type, U0 with kind type] }))) prio High ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'^0.0 (&'^0.1 ^0.2)) <: (&'^0.0 ^0.3)) }, binders: [U0 with kind lifetime, U0 with kind lifetime, U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─0ms INFO solve_goal: solution = Ok(Ambig(Definite(Canonical { value: [?0 := '^0.0, ?1 := '^0.1, ?2 := ^0.2, ?3 := (&'^0.1 ^0.3)], binders: [U0 with kind lifetime, U0 with kind lifetime, U0 with kind type, U0 with kind type] }))) prio High ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'^0.0 (&'^0.1 ^0.2)) <: (&'^0.0 (&'^0.1 ^0.3))) }, binders: [U0 with kind lifetime, U0 with kind lifetime, U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─0ms INFO solve_goal: solution = Ok(Ambig(Unknown)) prio High ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'^0.0 (&'^0.1 ^0.2)) <: (&'^0.0 (&'^0.1 ^0.3))) }, binders: [U0 with kind lifetime, U0 with kind lifetime, U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'^0.0 (&'^0.1 ^0.2)) <: (&'^0.0 (&'^0.1 ^0.3))) }, binders: [U0 with kind lifetime, U0 with kind lifetime, U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'^0.0 (&'^0.1 ^0.2)) <: (&'^0.0 (&'^0.1 ^0.3))) }, binders: [U0 with kind lifetime, U0 with kind lifetime, U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'^0.0 (&'^0.1 ^0.2)) <: (&'^0.0 (&'^0.1 ^0.3))) }, binders: [U0 with kind lifetime, U0 with kind lifetime, U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'^0.0 (&'^0.1 ^0.2)) <: (&'^0.0 (&'^0.1 ^0.3))) }, binders: [U0 with kind lifetime, U0 with kind lifetime, U0 with kind type, U0 with kind type] }, universes: 1 } ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: Normalize(<{closure:ClosureId(3)}<[?0 := () for<0> [?0 := (&'static 2<[?0 := ^1.0, ?1 := (&'^1.1 (&'^1.2 (&'^1.3 ^1.4)))]>), ?1 := (&'static 2<[?0 := ^1.5, ?1 := (&'^1.2 (&'^1.3 ^1.6))]>), ?2 := Ordering<[]>]]> as FnOnce<2<[?0 := (&'static 2<[?0 := ^0.7, ?1 := (&'static (&'static ^0.8))]>), ?1 := (&'static 2<[?0 := ^0.7, ?1 := (&'static (&'static ^0.8))]>)]>>>::Output -> Ordering<[]>) }, binders: [U0 with kind type, U0 with kind lifetime, U0 with kind lifetime, U0 with kind lifetime, U0 with kind type, U0 with kind type, U0 with kind type, U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'static ^0.0) <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'^0.0 ^0.1) <: (&'static ^0.2)) }, binders: [U0 with kind lifetime, U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'^0.0 ^0.1) <: (&'static ^0.2)) }, binders: [U0 with kind lifetime, U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: (^0.0 <: ^0.1) }, binders: [U0 with kind type, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: ((&'static ^0.0) <: (&'^0.1 ^0.2)) }, binders: [U0 with kind type, U0 with kind lifetime, U0 with kind type] }, universes: 1 } │ ├─┘ │ ├─0ms INFO solve_goal: solution = Ok(Ambig(Definite(Canonical { value: [?0 := ^0.0, ?1 := '^0.1, ?2 := '^0.2, ?3 := '^0.3, ?4 := ^0.4, ?5 := ^0.5, ?6 := (&'^0.6 ^0.7), ?7 := ^0.8, ?8 := (&'static ^0.9)], binders: [U0 with kind type, U0 with kind lifetime, U0 with kind lifetime, U0 with kind lifetime, U0 with kind type, U0 with kind type, U0 with kind lifetime, U0 with kind type, U0 with kind type, U0 with kind type] }))) prio High ├─┘ ├─┐solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: Normalize(<{closure:ClosureId(3)}<[?0 := () for<0> [?0 := (&'static 2<[?0 := ^1.0, ?1 := (&'^1.1 (&'^1.2 (&'^1.3 ^1.4)))]>), ?1 := (&'static 2<[?0 := ^1.5, ?1 := (&'^1.2 (&'^1.3 (&'^1.6 ^1.7)))]>), ?2 := Ordering<[]>]]> as FnOnce<2<[?0 := (&'static 2<[?0 := ^0.8, ?1 := (&'static (&'static (&'static ^0.9)))]>), ?1 := (&'static 2<[?0 := ^0.8, ?1 := (&'static (&'static (&'static ^0.9)))]>)]>>>::Output -> Ordering<[]>) }, binders: [U0 with kind type, U0 with kind lifetime, U0 with kind lifetime, U0 with kind lifetime, U0 with kind type, U0 with kind type, U0 with kind lifetime, U0 with kind type, U0 with kind type, U0 with kind type] }, universes: 1 } ```

The full ist of solve queries that happened before might also be useful:

``` [INFO hir_ty::traits] trait_solve_query(Implements(Iter<()>: Deref)) [INFO hir_ty::traits] trait_solve_query(Implements(Iter<()>: Iterator)) [INFO hir_ty::traits] trait_solve_query(Implements(Iter<()>: Sized)) [INFO hir_ty::traits] trait_solve_query(Implements(?0.0: FnMut<( as Iterator>::Item,)>)) [INFO hir_ty::traits] trait_solve_query(Normalize( as Iterator>::Item,)>>::Output => Option)) [INFO hir_ty::traits] trait_solve_query(Implements(|?0.0| -> ?0.1: FnMut<( as Iterator>::Item,)>)) [INFO hir_ty::traits] trait_solve_query(Normalize(<|&()| -> ?0.0 as FnOnce<( as Iterator>::Item,)>>::Output => Option)) [INFO hir_ty::traits] trait_solve_query(Implements(|&()| -> ?0.0: FnMut<( as Iterator>::Item,)>)) [INFO hir_ty::traits] trait_solve_query(Implements(|&()| -> Option: FnMut<( as Iterator>::Item,)>)) [INFO hir_ty::traits] trait_solve_query(Implements(Some(?0.0) -> Option: Deref)) [INFO hir_ty::traits] trait_solve_query(Implements(Option<(&(), ?0.0)>: CoerceUnsized>)) [INFO hir_ty::traits] trait_solve_query(Implements(|&()| -> Option<(&(), ?0.0)>: CoerceUnsized<|&()| -> Option<(&(), ?0.0)>>)) [INFO hir_ty::traits] trait_solve_query(Implements(FilterMap, |&()| -> Option<(&(), ?0.0)>>: Deref)) [INFO hir_ty::traits] trait_solve_query(Implements(FilterMap, |&()| -> Option<(&(), ?0.0)>>: Iterator)) [INFO hir_ty::traits] trait_solve_query(Implements(FilterMap, |&()| -> Option<(&(), ?0.0)>>: Sized)) [INFO hir_ty::traits] trait_solve_query(Implements(?0.0: FnMut<(&, |&()| -> Option<(&(), ?0.1)>> as Iterator>::Item,)>)) [INFO hir_ty::traits] trait_solve_query(Normalize(, |&()| -> Option<(&(), ?0.1)>> as Iterator>::Item,)>>::Output => bool)) [INFO hir_ty::traits] trait_solve_query(Implements(|?0.0| -> ?0.1: FnMut<(&, |&()| -> Option<(&(), ?0.2)>> as Iterator>::Item,)>)) [INFO hir_ty::traits] trait_solve_query(Normalize(<|&(&(), ?0.0)| -> ?0.1 as FnOnce<(&, |&()| -> Option<(&(), ?0.0)>> as Iterator>::Item,)>>::Output => bool)) [INFO hir_ty::traits] trait_solve_query(Implements(|&(&(), ?0.0)| -> ?0.1: FnMut<(&, |&()| -> Option<(&(), ?0.0)>> as Iterator>::Item,)>)) [INFO hir_ty::traits] trait_solve_query(Implements(|&(&(), ?0.0)| -> bool: FnMut<(&, |&()| -> Option<(&(), ?0.0)>> as Iterator>::Item,)>)) [INFO hir_ty::traits] trait_solve_query(Implements(bool: CoerceUnsized)) [INFO hir_ty::traits] trait_solve_query(Implements(|&(&(), ?0.0)| -> bool: CoerceUnsized<|&(&(), ?0.0)| -> bool>)) [INFO hir_ty::traits] trait_solve_query(Implements(Filter, |&()| -> Option<(&(), ?0.0)>>, |&(&(), ?0.0)| -> bool>: Deref)) [INFO hir_ty::traits] trait_solve_query(Implements(Filter, |&()| -> Option<(&(), ?0.0)>>, |&(&(), ?0.0)| -> bool>: Iterator)) [INFO hir_ty::traits] trait_solve_query(Implements(Filter, |&()| -> Option<(&(), ?0.0)>>, |&(&(), ?0.0)| -> bool>: Sized)) [INFO hir_ty::traits] trait_solve_query(Implements(?0.0: FnMut<(, |&()| -> Option<(&(), ?0.1)>>, |&(&(), ?0.1)| -> bool> as Iterator>::Item,)>)) [INFO hir_ty::traits] trait_solve_query(Normalize(, |&()| -> Option<(&(), ?0.1)>>, |&(&(), ?0.1)| -> bool> as Iterator>::Item,)>>::Output => ?0.2)) [INFO hir_ty::traits] trait_solve_query(Implements(|?0.0| -> ?0.1: FnMut<(, |&()| -> Option<(&(), ?0.2)>>, |&(&(), ?0.2)| -> bool> as Iterator>::Item,)>)) [INFO hir_ty::traits] trait_solve_query(Normalize(<|(&(), ?0.0)| -> ?0.1 as FnOnce<(, |&()| -> Option<(&(), ?0.0)>>, |&(&(), ?0.0)| -> bool> as Iterator>::Item,)>>::Output => ?0.2)) [INFO hir_ty::traits] trait_solve_query(Implements(|(&(), ?0.0)| -> ?0.1: FnMut<(, |&()| -> Option<(&(), ?0.0)>>, |&(&(), ?0.0)| -> bool> as Iterator>::Item,)>)) [INFO hir_ty::traits] trait_solve_query(Implements(|(&(), ?0.0)| -> (&(), ?0.1): FnMut<(, |&()| -> Option<(&(), ?0.0)>>, |&(&(), ?0.0)| -> bool> as Iterator>::Item,)>)) [INFO hir_ty::traits] trait_solve_query(Normalize(<|(&(), ?0.0)| -> (&(), ?0.1) as FnOnce<(, |&()| -> Option<(&(), ?0.0)>>, |&(&(), ?0.0)| -> bool> as Iterator>::Item,)>>::Output => ?0.2)) [INFO hir_ty::traits] trait_solve_query(Implements(|(&(), ?0.0)| -> (&(), ?0.1): CoerceUnsized<|(&(), ?0.0)| -> (&(), ?0.1)>)) [INFO hir_ty::traits] trait_solve_query(Implements(Map, |&()| -> Option<(&(), ?0.0)>>, |&(&(), ?0.0)| -> bool>, |(&(), ?0.0)| -> (&(), ?0.1)>: Deref)) [INFO hir_ty::traits] trait_solve_query(Normalize(, |&()| -> Option<(&(), ?0.0)>>, |&(&(), ?0.0)| -> bool>, |(&(), ?0.0)| -> (&(), ?0.1)> as Deref>::Target => ?0.2)) [INFO hir_ty::autoderef] Ambiguous solution for derefing Canonical { value: Adt(StructId(StructId(66)), Substs([Adt(StructId(StructId(57)), Substs([Adt(StructId(StructId(58)), Substs([Adt(StructId(StructId(128)), Substs([Tuple(0, Substs([]))])), Closure(FunctionId(FunctionId(961)), Idx::(7), Substs([Function(FnPointer { num_args: 1, sig: FnSig { variadic: false }, substs: Substs([Ref(Not, Substs([Tuple(0, Substs([]))])), Adt(EnumId(EnumId(18)), Substs([Tuple(2, Substs([Ref(Not, Substs([Tuple(0, Substs([]))])), BoundVar(^0.0)]))]))]) })]))])), Closure(FunctionId(FunctionId(961)), Idx::(10), Substs([Function(FnPointer { num_args: 1, sig: FnSig { variadic: false }, substs: Substs([Ref(Not, Substs([Tuple(2, Substs([Ref(Not, Substs([Tuple(0, Substs([]))])), BoundVar(^0.0)]))])), Scalar(Bool)]) })]))])), Closure(FunctionId(FunctionId(961)), Idx::(15), Substs([Function(FnPointer { num_args: 1, sig: FnSig { variadic: false }, substs: Substs([Tuple(2, Substs([Ref(Not, Substs([Tuple(0, Substs([]))])), BoundVar(^0.0)])), Tuple(2, Substs([Ref(Not, Substs([Tuple(0, Substs([]))])), BoundVar(^0.1)]))]) })]))])), kinds: [Integer, Integer] }: Ambig(Unknown) [INFO hir_ty::traits] trait_solve_query(Implements(Map, |&()| -> Option<(&(), ?0.0)>>, |&(&(), ?0.0)| -> bool>, |(&(), ?0.0)| -> (&(), ?0.1)>: Iterator)) [INFO hir_ty::traits] trait_solve_query(Implements(Vec: FromIterator<, |&()| -> Option<(&(), ?0.1)>>, |&(&(), ?0.1)| -> bool>, |(&(), ?0.1)| -> (&(), ?0.2)> as Iterator>::Item>)) [INFO hir_ty::traits] trait_solve_query(Implements(Map, |&()| -> Option<(&(), ?0.0)>>, |&(&(), ?0.0)| -> bool>, |(&(), ?0.0)| -> (&(), ?0.1)>: Sized)) [INFO hir_ty::traits] trait_solve_query(Implements(Vec: Deref)) [INFO hir_ty::traits] trait_solve_query(Normalize( as Deref>::Target => ?0.1)) [INFO hir_ty::traits] trait_solve_query(Implements([?0.0]: Deref)) [INFO hir_ty::traits] trait_solve_query(Implements(?0.0: FnMut<(&?0.1, &?0.1)>)) [INFO hir_ty::traits] trait_solve_query(Normalize(>::Output => Ordering)) [INFO hir_ty::traits] trait_solve_query(Implements(|?0.0, ?0.1| -> ?0.2: FnMut<(&?0.3, &?0.3)>)) [INFO hir_ty::traits] trait_solve_query(Normalize(<|&?0.0, &?0.1| -> ?0.2 as FnOnce<(&?0.3, &?0.3)>>::Output => Ordering)) [INFO hir_ty::traits] trait_solve_query(Implements(|&?0.0, &?0.1| -> ?0.2: FnMut<(&?0.3, &?0.3)>)) [INFO hir_ty::traits] trait_solve_query(Implements(|&?0.0, &?0.1| -> Ordering: FnMut<(&?0.2, &?0.2)>)) [INFO hir_ty::traits] trait_solve_query(Normalize(<|&?0.0, &?0.1| -> Ordering as FnOnce<(&?0.2, &?0.2)>>::Output => Ordering)) [INFO hir_ty::traits] trait_solve_query(Implements(|&(?0.0, ?0.1), &?0.2| -> Ordering: FnMut<(&?0.3, &?0.3)>)) [INFO hir_ty::traits] trait_solve_query(Normalize(<|&(?0.0, ?0.1), &(?0.2, ?0.3)| -> Ordering as FnOnce<(&(?0.4, ?0.5), &(?0.4, ?0.5))>>::Output => Ordering)) [INFO hir_ty::traits] trait_solve_query(Implements(Vec<(?0.0, ?0.1), Global>: FromIterator<, |&()| -> Option<(&(), ?0.2)>>, |&(&(), ?0.2)| -> bool>, |(&(), ?0.2)| -> (&(), ?0.3)> as Iterator>::Item>)) [INFO hir_ty::traits] trait_solve_query(Implements(|&(?0.0, ?0.1), &(?0.2, ?0.3)| -> Ordering: FnMut<(&(?0.4, ?0.5), &(?0.4, ?0.5))>)) [INFO hir_ty::traits] trait_solve_query(Implements(?0.0: Deref)) [INFO hir_ty::traits] trait_solve_query(Normalize(::Target => ?0.1)) [INFO hir_ty::autoderef] Ambiguous solution for derefing Canonical { value: BoundVar(^0.0), kinds: [General] }: Ambig(Unknown) [INFO hir_ty::traits] trait_solve_query(Implements(&?0.0: Iterator)) [INFO hir_ty::traits] trait_solve_query(Implements(?0.0: Ord)) [INFO hir_ty::traits] trait_solve_query(Implements(?0.0: Eq)) [INFO hir_ty::traits] trait_solve_query(Implements(?0.0: PartialOrd)) [INFO hir_ty::traits] trait_solve_query(Implements(&&?0.0: CoerceUnsized<&?0.1>)) [INFO hir_ty::traits] trait_solve_query(Implements(|&(?0.0, &?0.1), &(?0.2, ?0.1)| -> Ordering: FnMut<(&(?0.3, ?0.4), &(?0.3, ?0.4))>)) [INFO hir_ty::traits] trait_solve_query(Normalize(<|&(?0.0, &?0.1), &(?0.2, ?0.1)| -> Ordering as FnOnce<(&(?0.3, ?0.4), &(?0.3, ?0.4))>>::Output => Ordering)) ```

Full output for completeness, which also shows chalk programs: https://gist.github.com/detrumi/a7112751e901bbbd864a83e011f93cae

For reference, this was output from the following:

RA_LOG=hir_ty=info CHALK_DEBUG=3 CHALK_PRINT=1 cargo run --release -p rust-analyzer -- analysis-stats ../tryout
flodiebold commented 3 years ago

I think the difference that's likely the source of problems is that rust-analyzer (and I think I got this from rustc) puts the closure signature in a function pointer type in the substs. (rustc puts some more stuff in there, we currently only have the signature.)

Especially the fact that it's in a function pointer may be relevant, since that's caused problems because of variance already.

flodiebold commented 3 years ago

It's also worth noting that rust-analyzer never passes any lifetimes except 'static to Chalk.

jackh726 commented 3 years ago

@detrumi so the output there only shows chalk_recursive tracing output, which isn't super helpful. Haven't looked into how rust-analyzer enables the logging, but I would expect to also see chalk_solve output.

@flodiebold yeah, I'm wondering if we're relating all the substs somewhere that we should only be relating the "function substitution"

jackh726 commented 3 years ago

Yeah, actually, I bet this is happening because we call generalize_substitution on the whole closure substitution

JakobDegen commented 2 years ago

After #733 this reproduces as

#[test]
fn chalk_688() {
    test! {
        program {
            #[lang(fn_once)]
            trait FnOnce<Args> {
                type Output;
            }

            struct Ordering {}

            closure foo<F>(self,) {}

            impl<A, B, U> FnOnce<(A, B)> for foo<fn(A, B) -> U> {
                type Output = U;
            }
        }
        goal {
            exists <R, S, T, U> {
                <
                    foo<fn(&'static (R, &'static S), &'static (T, S)) -> Ordering>
                    as
                    FnOnce<(&'static (T, U), &'static (T, U))>
                >::Output
                = Ordering
            }
        } yields {
            "Ambiguous; no inference guidance"
        }
    }
}

on the recursive solver only

jackh726 commented 2 years ago

@JakobDegen just now finding some time to look at this and #733. Sorry for the delay. Shouldn't the repro for this end up with a hang, instead of an answer?

JakobDegen commented 2 years ago

@JakobDegen just now finding some time to look at this and #733. Sorry for the delay. Shouldn't the repro for this end up with a hang, instead of an answer?

Yeah should have clarified, that test does hang on the recursive solver on my branch; the answer in the test is needed so that this passes the SLG solver, as otherwise the recursive solver doesn't even run.

jackh726 commented 2 years ago

Ah okay. For future reference, you can use } yields[SolverChoice::recursive_default()] { to restrict to only the recursive solver!

Are you up for trying to fix this? (The work done in #733 is great, but I need to go through it more thoroughly; can definitely work on fixing the actual problem concurrently though). If so, feel free to reach out on Zulip if you have questions or run into problems :)

JakobDegen commented 2 years ago

Ah okay. For future reference, you can use } yields[SolverChoice::recursive_default()] { to restrict to only the recursive solver!

That's good to know, thanks!

Are you up for trying to fix this?

I am definitely interested in it, but time is currently a bit of an issue for me. I'm hoping to get around to looking at chalk more within the next two weeks; I'll claim the issue at that point if no one else has gotten started before then.