recursive: fix hang on fulfill by slightly smarter check for progress.

[Dirbaio]

This fixes a hang using the recursive solver when trying to prove exists<'a, T> { if(T: 'a) { WellFormed(&'a T) } }.

Snippet of the log when looping

617ms DEBUG start of round, 2 obligations prove wc=InEnvironment { environment: Env([for<> ?0: '?1]), goal: ?2: '?3 } solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([for<> ^1.0: '^1.1]), goal: ^0.0: '^0.1 }, binders: [U0 with kind type, U0 with kind lifetime] }, universes: 1 } 0ms DEBUG Cache hit, goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([for<> ^1.0: '^1.1]), goal: ^0.0: '^0.1 }, binders: [U0 with kind type, U0 with kind lifetime] }, universes: 1 }, result=Ok(Ambig(Definite(Canonical { value: [?0 := ^0.0, ?1 := '^0.1], binders: [U0 with kind type, U0 with kind lifetime] }))) 0ms DEBUG solve_reduced_goal: cache hit, value=Ok(Ambig(Definite(Canonical { value: [?0 := ^0.0, ?1 := '^0.1], binders: [U0 with kind type, U0 with kind lifetime] }))) 618ms DEBUG fulfill::apply_solution: adding constraints [] 618ms DEBUG unify(?2, ?1140) succeeded 618ms DEBUG unify: goals=[] 618ms DEBUG unify('?3, '?1141) succeeded 618ms DEBUG unify: goals=[] 618ms DEBUG ambiguous result: Prove(InEnvironment { environment: Env([for<> ?0: '?1]), goal: ?2: '?3 }) prove wc=InEnvironment { environment: Env([for<> ?0: '?1]), goal: WellFormed(?2) } solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([for<> ^1.0: '^1.1]), goal: WellFormed(^0.0) }, binders: [U0 with kind type, U0 with kind lifetime] }, universes: 1 } 0ms DEBUG Cache hit, goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([for<> ^1.0: '^1.1]), goal: WellFormed(^0.0) }, binders: [U0 with kind type, U0 with kind lifetime] }, universes: 1 }, result=Ok(Ambig(Unknown)) 0ms DEBUG solve_reduced_goal: cache hit, value=Ok(Ambig(Unknown)) 618ms DEBUG ambiguous result: Prove(InEnvironment { environment: Env([for<> ?0: '?1]), goal: WellFormed(?2) }) 618ms DEBUG end of round, 2 obligations left 618ms DEBUG start of round, 2 obligations prove wc=InEnvironment { environment: Env([for<> ?0: '?1]), goal: WellFormed(?2) } solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([for<> ^1.0: '^1.1]), goal: WellFormed(^0.0) }, binders: [U0 with kind type, U0 with kind lifetime] }, universes: 1 } 0ms DEBUG Cache hit, goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([for<> ^1.0: '^1.1]), goal: WellFormed(^0.0) }, binders: [U0 with kind type, U0 with kind lifetime] }, universes: 1 }, result=Ok(Ambig(Unknown)) 0ms DEBUG solve_reduced_goal: cache hit, value=Ok(Ambig(Unknown)) 619ms DEBUG ambiguous result: Prove(InEnvironment { environment: Env([for<> ?0: '?1]), goal: WellFormed(?2) }) prove wc=InEnvironment { environment: Env([for<> ?0: '?1]), goal: ?2: '?3 } solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([for<> ^1.0: '^1.1]), goal: ^0.0: '^0.1 }, binders: [U0 with kind type, U0 with kind lifetime] }, universes: 1 } 0ms DEBUG Cache hit, goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([for<> ^1.0: '^1.1]), goal: ^0.0: '^0.1 }, binders: [U0 with kind type, U0 with kind lifetime] }, universes: 1 }, result=Ok(Ambig(Definite(Canonical { value: [?0 := ^0.0, ?1 := '^0.1], binders: [U0 with kind type, U0 with kind lifetime] }))) 0ms DEBUG solve_reduced_goal: cache hit, value=Ok(Ambig(Definite(Canonical { value: [?0 := ^0.0, ?1 := '^0.1], binders: [U0 with kind type, U0 with kind lifetime] }))) 619ms DEBUG fulfill::apply_solution: adding constraints [] 619ms DEBUG unify(?2, ?1142) succeeded 619ms DEBUG unify: goals=[] 619ms DEBUG unify('?3, '?1143) succeeded 619ms DEBUG unify: goals=[] 619ms DEBUG ambiguous result: Prove(InEnvironment { environment: Env([for<> ?0: '?1]), goal: ?2: '?3 }) 619ms DEBUG end of round, 2 obligations left 619ms DEBUG start of round, 2 obligations prove wc=InEnvironment { environment: Env([for<> ?0: '?1]), goal: ?2: '?3 } solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([for<> ^1.0: '^1.1]), goal: ^0.0: '^0.1 }, binders: [U0 with kind type, U0 with kind lifetime] }, universes: 1 } 0ms DEBUG Cache hit, goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([for<> ^1.0: '^1.1]), goal: ^0.0: '^0.1 }, binders: [U0 with kind type, U0 with kind lifetime] }, universes: 1 }, result=Ok(Ambig(Definite(Canonical { value: [?0 := ^0.0, ?1 := '^0.1], binders: [U0 with kind type, U0 with kind lifetime] }))) 0ms DEBUG solve_reduced_goal: cache hit, value=Ok(Ambig(Definite(Canonical { value: [?0 := ^0.0, ?1 := '^0.1], binders: [U0 with kind type, U0 with kind lifetime] }))) 620ms DEBUG fulfill::apply_solution: adding constraints [] 620ms DEBUG unify(?2, ?1144) succeeded 620ms DEBUG unify: goals=[] 620ms DEBUG unify('?3, '?1145) succeeded 620ms DEBUG unify: goals=[] 620ms DEBUG ambiguous result: Prove(InEnvironment { environment: Env([for<> ?0: '?1]), goal: ?2: '?3 }) prove wc=InEnvironment { environment: Env([for<> ?0: '?1]), goal: WellFormed(?2) } solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([for<> ^1.0: '^1.1]), goal: WellFormed(^0.0) }, binders: [U0 with kind type, U0 with kind lifetime] }, universes: 1 } 0ms DEBUG Cache hit, goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([for<> ^1.0: '^1.1]), goal: WellFormed(^0.0) }, binders: [U0 with kind type, U0 with kind lifetime] }, universes: 1 }, result=Ok(Ambig(Unknown)) 0ms DEBUG solve_reduced_goal: cache hit, value=Ok(Ambig(Unknown)) 620ms DEBUG ambiguous result: Prove(InEnvironment { environment: Env([for<> ?0: '?1]), goal: WellFormed(?2) }) 620ms DEBUG end of round, 2 obligations left

The issue is:

• it tries to prove InEnvironment { environment: Env([for<> ?0: '?1]), goal: ?2: '?3 }
• it gets "useless" substs [?0 := ^0.0, ?1 := '^0.1]
• it applies them, they cause nothing to change but it thinks they did
• so in next round it processes again the exact same obligation...

There was already an if treating empty substs as "useless", this extends it to treating trivial subs as "useless". (empty substs are also trivial).

[flodiebold]

The check makes sense to me, though also we probably shouldn't return a trivial substitution as guidance.

[jackh726]

The check makes sense to me, though also we probably shouldn't return a trivial substitution as guidance.

I dont know if I agree with this. The trivial substitution is guidance ("whatever T and 'a provided will satisfies the goal").

[flodiebold]

No, the guidance just means that all solutions will have this form -- which is trivial if the substitution is trivial. It doesn't mean that all such substitutions are valid answers. (If we knew that all T and 'a provided would satisfy the goal, the answer wouldn't be ambiguous -- that'd just be the solution.)

[jackh726]

I'm going to go ahead and merge this for now, since this fixes a hang. We can iterate on this later (whether that's changing this to be Definite or NoGuidance

@bors r+

[bors]

:pushpin: Commit 91f2ee77bb22dfd5bf2ca41248796e12b49fdee9 has been approved by jackh726

[bors]

:hourglass: Testing commit 91f2ee77bb22dfd5bf2ca41248796e12b49fdee9 with merge b32c563fe230d230266aab30050b209e62a9fff0...

[bors]

:sunny: Test successful - checks-actions Approved by: jackh726 Pushing b32c563fe230d230266aab30050b209e62a9fff0 to master...