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]

📌 Commit 91f2ee7 has been approved by jackh726

[bors]

⌛ Testing commit 91f2ee7 with merge b32c563...

[bors]

☀️ Test successful - checks-actions
Approved by: jackh726
Pushing b32c563 to master...