Instance subgoal order has changed from R->L to L->R

[dselsam]

In Lean3, the coe_trans instance (https://github.com/leanprover-community/lean/blob/master/library/init/coe.lean#L95) starts stepping from the source, so e.g. the following instance is acceptable:

@[to_additive] instance : has_coe (units α) α := ⟨val⟩

In contrast, the coeTrans instance in Lean4 (https://github.com/leanprover/lean4/blob/master/src/Init/Coe.lean#L70) starts stepping from the target, so the same instance loops. This means that currently, many coercion-related synthesis queries will loop in Lean4.

EDIT: this explanation does not make sense. I am still diagnosing the reason for the loop.

[dselsam]

It turns out the loop is due to the TC subgoal order changing from Lean3 (R->L) to Lean4 (L->R). For now, I will add the [inferTCGoalsRL] annotation to all instances during mathport. However, this may not be an adequate long-term solution in light of the potential nested-TC-loops (which is why Lean4 uses L->R).

[gebner]

It turns out the loop is due to the TC subgoal order changing from Lean3 (R->L) to Lean4 (L->R).

Did the Lean4 order change, again? We switched from L->R to R->L in Lean 3 to simplify porting: https://github.com/leanprover-community/lean/pull/139