Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Solving closure goal keeps expanding lifetimes #688

Open
detrumi opened this issue Feb 27, 2021 · 12 comments
Open

Solving closure goal keeps expanding lifetimes #688

detrumi opened this issue Feb 27, 2021 · 12 comments
Labels
bug A bug C-chalk-recursive Issues related to the chalk-recursive crate C-chalk-solve Issues related to the chalk-solve crate

Comments

@detrumi
Copy link
Member

detrumi commented Feb 27, 2021

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
Copy link
Member Author

detrumi commented Feb 27, 2021

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

@detrumi detrumi added bug A bug C-chalk-solve Issues related to the chalk-solve crate C-chalk-engine Issues related to the chalk-engine crate and removed C-chalk-solve Issues related to the chalk-solve crate C-chalk-engine Issues related to the chalk-engine crate labels Feb 27, 2021
casperstorm added a commit to ajour/ajour that referenced this issue Mar 4, 2021
@flodiebold flodiebold added C-chalk-recursive Issues related to the chalk-recursive crate C-chalk-solve Issues related to the chalk-solve crate and removed C-chalk-solve Issues related to the chalk-solve crate labels Mar 13, 2021
@jackh726
Copy link
Member

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
Copy link
Member Author

detrumi commented Mar 14, 2021

@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<(<Iter<()> as Iterator>::Item,)>))
[INFO hir_ty::traits] trait_solve_query(Normalize(<?0.0 as FnOnce<(<Iter<()> as Iterator>::Item,)>>::Output => Option<?0.1>))
[INFO hir_ty::traits] trait_solve_query(Implements(|?0.0| -> ?0.1: FnMut<(<Iter<()> as Iterator>::Item,)>))
[INFO hir_ty::traits] trait_solve_query(Normalize(<|&()| -> ?0.0 as FnOnce<(<Iter<()> as Iterator>::Item,)>>::Output => Option<?0.1>))
[INFO hir_ty::traits] trait_solve_query(Implements(|&()| -> ?0.0: FnMut<(<Iter<()> as Iterator>::Item,)>))
[INFO hir_ty::traits] trait_solve_query(Implements(|&()| -> Option<?0.0>: FnMut<(<Iter<()> as Iterator>::Item,)>))
[INFO hir_ty::traits] trait_solve_query(Implements(Some<?0.0>(?0.0) -> Option<?0.0>: Deref))
[INFO hir_ty::traits] trait_solve_query(Implements(Option<(&(), ?0.0)>: CoerceUnsized<Option<?0.1>>))
[INFO hir_ty::traits] trait_solve_query(Implements(|&()| -> Option<(&(), ?0.0)>: CoerceUnsized<|&()| -> Option<(&(), ?0.0)>>))
[INFO hir_ty::traits] trait_solve_query(Implements(FilterMap<Iter<()>, |&()| -> Option<(&(), ?0.0)>>: Deref))
[INFO hir_ty::traits] trait_solve_query(Implements(FilterMap<Iter<()>, |&()| -> Option<(&(), ?0.0)>>: Iterator))
[INFO hir_ty::traits] trait_solve_query(Implements(FilterMap<Iter<()>, |&()| -> Option<(&(), ?0.0)>>: Sized))
[INFO hir_ty::traits] trait_solve_query(Implements(?0.0: FnMut<(&<FilterMap<Iter<()>, |&()| -> Option<(&(), ?0.1)>> as Iterator>::Item,)>))
[INFO hir_ty::traits] trait_solve_query(Normalize(<?0.0 as FnOnce<(&<FilterMap<Iter<()>, |&()| -> Option<(&(), ?0.1)>> as Iterator>::Item,)>>::Output => bool))
[INFO hir_ty::traits] trait_solve_query(Implements(|?0.0| -> ?0.1: FnMut<(&<FilterMap<Iter<()>, |&()| -> Option<(&(), ?0.2)>> as Iterator>::Item,)>))
[INFO hir_ty::traits] trait_solve_query(Normalize(<|&(&(), ?0.0)| -> ?0.1 as FnOnce<(&<FilterMap<Iter<()>, |&()| -> Option<(&(), ?0.0)>> as Iterator>::Item,)>>::Output => bool))
[INFO hir_ty::traits] trait_solve_query(Implements(|&(&(), ?0.0)| -> ?0.1: FnMut<(&<FilterMap<Iter<()>, |&()| -> Option<(&(), ?0.0)>> as Iterator>::Item,)>))
[INFO hir_ty::traits] trait_solve_query(Implements(|&(&(), ?0.0)| -> bool: FnMut<(&<FilterMap<Iter<()>, |&()| -> Option<(&(), ?0.0)>> as Iterator>::Item,)>))
[INFO hir_ty::traits] trait_solve_query(Implements(bool: CoerceUnsized<bool>))
[INFO hir_ty::traits] trait_solve_query(Implements(|&(&(), ?0.0)| -> bool: CoerceUnsized<|&(&(), ?0.0)| -> bool>))
[INFO hir_ty::traits] trait_solve_query(Implements(Filter<FilterMap<Iter<()>, |&()| -> Option<(&(), ?0.0)>>, |&(&(), ?0.0)| -> bool>: Deref))
[INFO hir_ty::traits] trait_solve_query(Implements(Filter<FilterMap<Iter<()>, |&()| -> Option<(&(), ?0.0)>>, |&(&(), ?0.0)| -> bool>: Iterator))
[INFO hir_ty::traits] trait_solve_query(Implements(Filter<FilterMap<Iter<()>, |&()| -> Option<(&(), ?0.0)>>, |&(&(), ?0.0)| -> bool>: Sized))
[INFO hir_ty::traits] trait_solve_query(Implements(?0.0: FnMut<(<Filter<FilterMap<Iter<()>, |&()| -> Option<(&(), ?0.1)>>, |&(&(), ?0.1)| -> bool> as Iterator>::Item,)>))
[INFO hir_ty::traits] trait_solve_query(Normalize(<?0.0 as FnOnce<(<Filter<FilterMap<Iter<()>, |&()| -> 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<(<Filter<FilterMap<Iter<()>, |&()| -> Option<(&(), ?0.2)>>, |&(&(), ?0.2)| -> bool> as Iterator>::Item,)>))
[INFO hir_ty::traits] trait_solve_query(Normalize(<|(&(), ?0.0)| -> ?0.1 as FnOnce<(<Filter<FilterMap<Iter<()>, |&()| -> 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<(<Filter<FilterMap<Iter<()>, |&()| -> Option<(&(), ?0.0)>>, |&(&(), ?0.0)| -> bool> as Iterator>::Item,)>))
[INFO hir_ty::traits] trait_solve_query(Implements(|(&(), ?0.0)| -> (&(), ?0.1): FnMut<(<Filter<FilterMap<Iter<()>, |&()| -> Option<(&(), ?0.0)>>, |&(&(), ?0.0)| -> bool> as Iterator>::Item,)>))
[INFO hir_ty::traits] trait_solve_query(Normalize(<|(&(), ?0.0)| -> (&(), ?0.1) as FnOnce<(<Filter<FilterMap<Iter<()>, |&()| -> 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<Filter<FilterMap<Iter<()>, |&()| -> Option<(&(), ?0.0)>>, |&(&(), ?0.0)| -> bool>, |(&(), ?0.0)| -> (&(), ?0.1)>: Deref))
[INFO hir_ty::traits] trait_solve_query(Normalize(<Map<Filter<FilterMap<Iter<()>, |&()| -> 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::<Expr>(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::<Expr>(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::<Expr>(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<Filter<FilterMap<Iter<()>, |&()| -> Option<(&(), ?0.0)>>, |&(&(), ?0.0)| -> bool>, |(&(), ?0.0)| -> (&(), ?0.1)>: Iterator))
[INFO hir_ty::traits] trait_solve_query(Implements(Vec<?0.0, Global>: FromIterator<<Map<Filter<FilterMap<Iter<()>, |&()| -> Option<(&(), ?0.1)>>, |&(&(), ?0.1)| -> bool>, |(&(), ?0.1)| -> (&(), ?0.2)> as Iterator>::Item>))
[INFO hir_ty::traits] trait_solve_query(Implements(Map<Filter<FilterMap<Iter<()>, |&()| -> Option<(&(), ?0.0)>>, |&(&(), ?0.0)| -> bool>, |(&(), ?0.0)| -> (&(), ?0.1)>: Sized))
[INFO hir_ty::traits] trait_solve_query(Implements(Vec<?0.0, Global>: Deref))
[INFO hir_ty::traits] trait_solve_query(Normalize(<Vec<?0.0, Global> 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(<?0.0 as FnOnce<(&?0.1, &?0.1)>>::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<<Map<Filter<FilterMap<Iter<()>, |&()| -> 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(<?0.0 as Deref>::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<?0.0>))
[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
Copy link
Member

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
Copy link
Member

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

@jackh726
Copy link
Member

@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
Copy link
Member

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

@JakobDegen
Copy link
Contributor

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
Copy link
Member

@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
Copy link
Contributor

@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
Copy link
Member

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
Copy link
Contributor

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug A bug C-chalk-recursive Issues related to the chalk-recursive crate C-chalk-solve Issues related to the chalk-solve crate
Projects
None yet
Development

No branches or pull requests

4 participants