fix: make elab_as_elim eagerly elaborate arguments for parameters appearing in the types of targets

[kmill]

The elab_as_elim elaborator eagerly elaborates arguments that can help with elaborating the motive, however it does not include the transitive closure of parameters appearing in types of parameters appearing in ... types of targets.

This leads to counter-intuitive behavior where arguments supplied to the eliminator may unexpectedly have postponed elaboration, causing motives to be type incorrect for under-applied eliminators such as the following:

class IsEmpty (α : Sort u) : Prop where
  protected false : α → False

@[elab_as_elim]
def isEmptyElim [IsEmpty α] {p : α → Sort _} (a : α) : p a :=
  (IsEmpty.false a).elim

example {α : Type _} [IsEmpty α] :
  id (α → False) := isEmptyElim (α := α)

The issue is that when isEmptyElim (α := α) is computing its motive, the value of the postponed argument α is still an unassignable metavariable. With this PR, this argument is now among those that are eagerly elaborated since it appears as the type of the target a.

This PR also contains some other fixes:

• When underapplied, does unification when instantiating foralls in the expected type.
• When overapplied, type checks the generalized-and-reverted expected type.
• When collecting targets, collects them in the correct order.

Adds trace class trace.Elab.app.elab_as_elim.

This is a followup to #4722, which added motive type checking but exposed the eagerness issue.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-4800 build failed against this PR. (2024-07-20 23:35:14) View Log
• 💥 Mathlib branch lean-pr-testing-4800 build failed against this PR. (2024-07-21 00:32:03) View Log
• 💥 Mathlib branch lean-pr-testing-4800 build failed against this PR. (2024-07-21 06:45:19) View Log
• ✅ Mathlib branch lean-pr-testing-4800 has successfully built against this PR. (2024-07-21 17:06:23) View Log
• ✅ Mathlib branch lean-pr-testing-4800 has successfully built against this PR. (2024-07-22 19:20:30) View Log
• ✅ Mathlib branch lean-pr-testing-4800 has successfully built against this PR. (2024-07-23 00:34:27) View Log