Recursive solver fails on some WF checks

[nathanwhit]

While debugging a separate issue, I noticed that in our tests all WF checks are done by the SLG solver. Out of curiosity I tried using the recursive solver for the WF checks and noticed a handful of failures (i.e. the solver incorrectly determines the program to be not WF) and cases which run forever.

Failures:

• test::cycle::overflow
• test::misc::subgoal_abstraction
• test::misc::subgoal_cycle_inhabited
• test::misc::subgoal_cycle_uninhabited

Infinite execution:

• test::misc::lifetime_outlives_constraints
• test::misc::type_outlives_constraints

[nathanwhit]

With #569 applied, the two outlives_constraints tests fail instead of running forever.

[jackh726]

This has gotten worse, I think. Current state:

Stack overflow:

• test::wf_lowering::ill_formed_type_in_header

Failures:

• test::cycle::overflow
• test::lifetimes::empty_outlives
• test::lifetimes::erased_outlives
• test::lifetimes::static_outlives
• test::misc::lifetime_outlives_constraints
• test::misc::subgoal_abstraction
• test::misc::subgoal_cycle_inhabited
• test::misc::subgoal_cycle_uninhabited
• test::misc::type_outlives_constraints
• test::wf_lowering::higher_ranked_cyclic_requirements