Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Auto merge of #752 - Dirbaio:fix-recursive-hang, r=jackh726
recursive: fix hang on fulfill by slightly smarter check for progress. This fixes a hang using the recursive solver when trying to prove `exists<'a, T> { if(T: 'a) { WellFormed(&'a T) } }`. <details> <summary>Snippet of the log when looping</summary> 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 </details> 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).
- Loading branch information