Elaborator doesn't produce InfoTree for incomplete match and incomplete terms in apply

[mhuisi]

Description

In incomplete match statements and in incomplete terms in apply, the elaborator often does not produce InfoTrees.

Context

This issue is derived from #5172. #5299 resolves the fact that completion doesn't trigger in these contexts, but it doesn't resolve the underlying problem that the elaborator does not produce InfoTrees in this example, which are also needed for all kinds of other language server features.

Steps to Reproduce

Consider the following example from #5172:

set_option trace.Elab.info true

inductive Direction where
  | up
  | right
  | down
  | left
deriving Repr

def angle (d: Direction) :=
  match d with
  | Direction. => 90 
  | Direction.right => 0
  | Direction.down => 270
  | Direction.left => 180

example : p ∨ (q ∧ r) → (p ∨ q) ∧ (p ∨ r) := by
  intro h
  cases h with
  | inl hp => apply And. (Or.intro_left q hp) (Or.intro_left r hp)
  | inr hqr => apply And.intro (Or.intro_right p hqr.left) (Or.intro_right p hqr.right)

In angle, all InfoTree information for the incomplete match statement is missing. In the example, all InfoTree information for the incomplete term in the first apply is missing.

Versions

Current master (ec98c92).

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[Kha]

Related: #3831. I thought we also had one for match

[kmill]

#5862 added info for apply, but match is still remaining.