WF of a type variable unconditionally evaluates to Yes #36
Description
In compute_well_formed_goal, when given a goal WF(?0), it adds the same input goal as a recursive goal, which is then evaluated to Yes because of WF goals being coinductive.
TODO: write a test (it seems hard to exploit).