Goto definition + have with pattern

Stream: lean4

[Julian Berman]

Is it a known issue that if you use goto definition on Nat in:

example : 2 = 2 := by
  have x : ∃ n : Nat, 1 = 1 := by sorry
  rfl

you get to Nat, but if you use it in the presence of a pattern:

example : 2 = 2 := by
  have ⟨x, y⟩ : ∃ n : Nat, 1 = 1 := by sorry
  rfl

you go to haveDecl?

[Kyle Miller]

This is an issue with the let tactic too, and it seems to be rooted in an issue with the let term. If you hover over any part of the type after the : it highlights the whole letDecl

example : 2 = 2 :=
  let ⟨x, y⟩ : ∃ n : Nat, 1 = 1 := (by sorry)
  rfl

[Kyle Miller]

That issue seems to be rooted in turn in how match handles type ascriptions. Hovering over the type highlights the whole type ascription.

example : 2 = 2 :=
  match ((by sorry) : ∃ n : Nat, 1 = 1) with
  | ⟨x, y⟩ => rfl

[Kyle Miller]

And it looks like it comes down to how type ascriptions themselves elaborate when the value is a tactic. Hovering over Nat gives information about the type ascription.

#check (by sorry : Nat)

[Kyle Miller]

Going back up to the original have notation, avoiding a tactic makes hovering over Nat highlight just Nat.

example : 2 = 2 := by
  have ⟨x, y⟩ : ∃ n : Nat, 1 = 1 := sorry
  rfl

[Julian Berman]

Thanks for the digging! You'd agree these are bugs I assume?

[Julian Berman]

It seems strange to me to even ever jump to / hover a tactic definition unless you specifically hover on the tactic name, but I'm not sure whether that's relevant / a good mental model in general for any possible tactic.

[Kyle Miller]

Somehow the type in (by sorry : ∃ n : Nat, 1 = 1) is losing some TermInfo, and as a fallback it's looking outward to anything that annotates how the term was elaborated. Here, it's the type ascription, and in your have tactic, it's the haveDecl syntax, which itself looks out to the have when doing "go to definition".

[Kyle Miller]

There's a whole tree of nested info, and it walks up the tree as a fallback. The whole tactic range itself is annotated with the tactic itself. (For example, if you "go to definition" on the => in a tactic, it's associated to the tactic itself. That's a counterexample to "only the tactic name itself refers to the tactic.")

[Julian Berman]

Yeah I figured something like that was going on (and I realize I'm just randomly talking) but to me it's odd even if pieces of syntax within a tactic end up jumping to the tactic

[Kyle Miller]

At least it unifies things, because there are also tactics like <;> that have no head keyword

[Julian Berman]

True.

[Kyle Miller]

Weird, I don't see anything about the ascription in the info tree when there's a tactic. When it's just (1 : Nat), there's elabTypeAscription.

set_option trace.Elab.info true
example := ((by exact 1) : Nat)
/-
• command @ ⟨55, 0⟩-⟨55, 31⟩ @ Lean.Elab.Command.elabDeclaration
      • ℕ : Type @ ⟨55, 8⟩†-⟨55, 31⟩† @ Lean.Elab.Term.elabHole
      • _example (isBinder := true) : ℕ @ ⟨55, 0⟩†-⟨55, 31⟩†
      • Tactic @ ⟨55, 13⟩-⟨55, 23⟩
        (Term.byTactic "by" (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact "exact" (num "1"))])))
        before
        ⊢ ℕ
        after no goals
        • Tactic @ ⟨55, 13⟩-⟨55, 15⟩
          "by"
          before
          ⊢ ℕ
          after no goals
          • Tactic @ ⟨55, 16⟩-⟨55, 23⟩ @ Lean.Elab.Tactic.evalTacticSeq
            (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact "exact" (num "1"))]))
            before
            ⊢ ℕ
            after no goals
            • Tactic @ ⟨55, 16⟩-⟨55, 23⟩ @ Lean.Elab.Tactic.evalTacticSeq1Indented
              (Tactic.tacticSeq1Indented [(Tactic.exact "exact" (num "1"))])
              before
              ⊢ ℕ
              after no goals
              • Tactic @ ⟨55, 16⟩-⟨55, 23⟩ @ Lean.Elab.Tactic.evalExact
                (Tactic.exact "exact" (num "1"))
                before
                ⊢ ℕ
                after no goals
                • 1 : ℕ @ ⟨55, 22⟩-⟨55, 23⟩ @ Lean.Elab.Term.elabNumLit
      • _example (isBinder := true) : ℕ @ ⟨55, 0⟩-⟨55, 7⟩
-/
example := (1            : Nat)
/-
• command @ ⟨88, 0⟩-⟨88, 31⟩ @ Lean.Elab.Command.elabDeclaration
      • ℕ : Type @ ⟨88, 8⟩†-⟨88, 31⟩† @ Lean.Elab.Term.elabHole
      • _example (isBinder := true) : ℕ @ ⟨88, 0⟩†-⟨88, 31⟩†
      • 1 : ℕ @ ⟨88, 11⟩-⟨88, 31⟩ @ Lean.Elab.Term.elabTypeAscription
        • ℕ : Type @ ⟨88, 27⟩-⟨88, 30⟩ @ Lean.Elab.Term.elabIdent
          • [.] Nat : some Sort.{?_uniq.17909} @ ⟨88, 27⟩-⟨88, 30⟩
          • ℕ : Type @ ⟨88, 27⟩-⟨88, 30⟩
        • 1 : ℕ @ ⟨88, 12⟩-⟨88, 13⟩ @ Lean.Elab.Term.elabNumLit
      • _example (isBinder := true) : ℕ @ ⟨88, 0⟩-⟨88, 7⟩
-/

[Julian Berman]

(I am modifying my dreamed up rule to be "hover and go to definition should work only on the first contiguous set of characters part of a tactic" :P) -- or even better, use textDocument/implementation for jumping to tactic definitions themselves, though probably it bears checking how other language servers use textDocument/definition vs textDocument/implementation vs textDocument/declaration.

[Julian Berman]

Less idly I'm trying to understand what those mean. I assume you basically knew that that output somehow corresponds to how Lean is calculating what range to return for the hover?

[Julian Berman]

Oh OK I see, that's literally embedding those ranges in the text there, got it.