Issue in `[elabAsElim]` generalization order

[digama0]

Lean 3:

@[elab_as_eliminator] theorem eq.subst' {α} {motive : α → Prop} {a b : α} :
  a = b → motive a → motive b := eq.subst

example {α} (P : α → Prop) {a b} (e : a = b) (h : P a) : P b :=
begin
  refine eq.subst' e _,
  -- goal is |- P a
  exact h
end

Lean 4:

@[elabAsElim] theorem Eq.subst' {α} {motive : α → Prop} {a b : α} :
  a = b → motive a → motive b := Eq.subst

example {α} (P : α → Prop) {a b} (e : a = b) (h : P a) : P b := by
  refine Eq.subst' e ?_
  -- goal is |- P b, should be |- P a
  exact h

In the elabAsElim implementation, we go over all the arguments and delay all elaboration goals except for the target(s) (that's b here) and the motive (not provided). In particular, that means we don't elaborate the e argument here, so when we get through all the arguments the b argument of Eq.subst' is still a metavariable, and the kabstract fails to generalize anything, which is why the goal is still P b after the refine.

In the lean 3 code we use more than just the targets to synthesize the motive. If I'm reading the code right, it considers arguments which are "first order" (meaning all applications in the type have a const at the head) and also have an fvar in the type which is also a target. In this case the check would pass for the e argument because it is first order (the only application head is Eq), and it references b which is an fvar and a target.

This should probably be implemented as a preprocessing step on the eliminator, stored in the ElimInfo.