No types or goals inside matches

[Kha]

Description

In the following definition, only the Nats outside the match seem to carry metadata

example : Nat → Nat
  | 0 => 0
  | n + 1 => by exact n

Expected behaviour

We should have type hover on 0/n/... and goals on by

Environment information

• Operating System: Linux
• Lean version: nightly-03-02
• LeanInk version: https://github.com/Kha/LeanInk/tree/main
• Alectryon version: https://github.com/insightmind/alectryon/tree/typeid

Additional Notes

Perhaps some unexpected order in the info tree?

[Elab.info] command @ ⟨3, 0⟩-⟨5, 23⟩ @ Lean.Elab.Command.elabDeclaration
  Nat → Nat : Type @ ⟨3, 10⟩-⟨3, 19⟩ @ Lean.Elab.Term.elabArrow
    Nat : Type @ ⟨3, 10⟩-⟨3, 13⟩ @ Lean.Elab.Term.elabIdent
      [.] `Nat : some Sort.{?_uniq.2} @ ⟨3, 10⟩-⟨3, 13⟩
      Nat : Type @ ⟨3, 10⟩-⟨3, 13⟩
    Nat : Type @ ⟨3, 16⟩-⟨3, 19⟩ @ Lean.Elab.Term.elabIdent
      [.] `Nat : some Sort.{?_uniq.3} @ ⟨3, 16⟩-⟨3, 19⟩
      Nat : Type @ ⟨3, 16⟩-⟨3, 19⟩
  fun x =>
    _example.match_1 (fun x => Nat) x (fun _ => 0) fun n =>
      n : <failed-to-infer-type> @ ⟨4, 2⟩†-⟨5, 23⟩ @ Lean.Elab.Term.elabExplicit
    fun x =>
      _example.match_1 (fun x => Nat) x (fun _ => 0) fun n =>
        n : <failed-to-infer-type> @ ⟨4, 2⟩†-⟨5, 23⟩ @ Lean.Elab.Term.elabFun
      Nat : Type @ ⟨4, 2⟩†-⟨5, 23⟩† @ Lean.Elab.Term.elabHole
      x (isBinder := true) : Nat @ ⟨4, 2⟩†-⟨5, 23⟩†
      _example.match_1 (fun x => Nat) x (fun _ => 0) fun n =>
        n : <failed-to-infer-type> @ ⟨4, 2⟩†-⟨5, 23⟩ @ Lean.Elab.Term.elabMatch
        x : Nat @ ⟨4, 2⟩†-⟨5, 23⟩†
        0 : Nat @ ⟨4, 4⟩-⟨4, 5⟩ @ Lean.Elab.Term.elabNumLit
        0 : Nat @ ⟨4, 9⟩-⟨4, 10⟩ @ Lean.Elab.Term.elabNumLit
        [.] `n : none @ ⟨5, 4⟩-⟨5, 5⟩
        n + 1 : Nat @ ⟨4, 2⟩†-⟨5, 9⟩ @ Lean.Elab.Term.BinOp.elabBinOp
          n : Nat @ ⟨5, 4⟩-⟨5, 5⟩ @ Lean.Elab.Term.elabIdent
            n : Nat @ ⟨5, 4⟩-⟨5, 5⟩
          1 : Nat @ ⟨5, 8⟩-⟨5, 9⟩ @ Lean.Elab.Term.elabNumLit
        Tactic @ ⟨5, 13⟩-⟨5, 23⟩
        (Term.byTactic "by" (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(group (Tactic.exact "exact" `n) [])])))
        before 
        n : Nat
        ⊢ Nat
        after no goals
          Tactic @ ⟨5, 16⟩-⟨5, 23⟩ @ Lean.Elab.Tactic.evalTacticSeq
          (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(group (Tactic.exact "exact" `n) [])]))
          before 
          n : Nat
          ⊢ Nat
          after no goals
            Tactic @ ⟨5, 16⟩-⟨5, 23⟩ @ Lean.Elab.Tactic.evalTacticSeq1Indented
            (Tactic.tacticSeq1Indented [(group (Tactic.exact "exact" `n) [])])
            before 
            n : Nat
            ⊢ Nat
            after no goals
              Tactic @ ⟨5, 16⟩-⟨5, 23⟩ @ Lean.Elab.Tactic.evalExact
              (Tactic.exact "exact" `n)
              before 
              n : Nat
              ⊢ Nat
              after no goals
                n : Nat @ ⟨5, 22⟩-⟨5, 23⟩ @ Lean.Elab.Term.elabIdent
                  n : Nat @ ⟨5, 22⟩-⟨5, 23⟩
  _example (isBinder := true) : Nat → Nat @ ⟨3, 0⟩-⟨3, 7⟩

[insightmind]

I have implemented a fix for this in commit 9f285ade1dd9f6913c7f228ce48bc85fd7228b03. In addition to that I added this example as a test case.

Can you check if the fix also works in your environment, and if any information is still missing?

[Kha]

Works great, thanks!