Go-to-def on typeclass fields and type-dependent notation

Stream: lean4

[Thomas Murrills]

Often I want to go-to-definition to see what's going on in the code I'm looking at. However, if I try to go-to-def on type-dependent notation or a typeclass field, I get the generic template instead of the specific implementation. For example:

example : 1 + 1 = 2 := rfl
--          ^command+click

goes to

macro_rules | `($x + $y)   => `(binop% HAdd.hAdd $x $y)

Likewise,

example : HAdd.hAdd 1 1 = 2 := rfl
--             ^^^^command+click

goes to the hAdd field of

/--
The notation typeclass for heterogeneous addition.
This enables the notation `a + b : γ` where `a : α`, `b : β`.
-/
class HAdd (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  /-- `a + b` computes the sum of `a` and `b`.
  The meaning of this notation is type-dependent. -/
  hAdd : α → β → γ

Ideally, in this case, I'd like to command+click and get to instAddNat.add in both cases instead. It would be an improvement in my eyes if command-clicking brought me to the field of the instance being used. (Note that we could then command-click the field itself or the type to get to the typeclass itself, so the typeclass wouldn't be totally inaccessible.)

But, there's a small problem with that (which shows that "fixing" this would be a little complicated): even if command-clicking took me to the hAdd field of the instance of HAdd being used here, I'd actually get to

@[default_instance]
instance [Add α] : HAdd α α α where
  hAdd a b := Add.add a b

and now have to write #synth Add Nat anyway, then command+click again to get to instAddNat.add. Which is better than doing it twice, but still not ideal. I would guess that this is the situation for a few commonly used H-typeclasses.

However, if it did jump straight to instAddNat.add, that might be confusing too, as we would be jumping past the typeclass that actually appears there, which might leave the user disoriented or misinformed.

So there are three questions here:

1. do other people also feel that command-clicking should, generally, lead to the specific implementation at hand rather than the "template"?
2. is this already easy through a different shortcut somehow, and I just don't know how to do it?
3. if (1), then what's the right approach to the "chained instances" issue above?

[Alex J. Best]

I would normally use the infoview for this, clicking on the plus to pop out the full term and then cmd+click on instAddNat to jump to it.
I'm not sure what's better but I'm used to the way it works right now so don't really see the benefit of changing it (I probably want to look at the instance and at the typeclass roughly equally often)

[Jovan Gerbscheid]

I'm not able to reproduce it now, but I remember a couple of times when I ctrl+clicked on a definition from a type class, it didn't directly send me to the definition, but instead showed multiple definitions that I could then click on. One being the type class and one or more being the instance. I quite like this. So in the example of addition, it would show 3 definitions: HAdd, instHAdd and instAddNat.

[Jovan Gerbscheid]

I finally managed to reproduce the behaviour I mentioned: crtl + click gives a list of all definitions used in constructing the instance field, allowing you to choose which definition to go to, and showing a preview of the definitions. See the screenshot. But only if the function is not applied to any arguments. It seems to work on 4.8.0-rc2, but not on 4.7.0. I am quite surprised by this, and I wonder what the intent is, given that it only works when there are no explicit arguments.

image.png

[Jovan Gerbscheid]

Note that this only works in the editor. ctrl + click in the infoview still just goes to the definition of HAdd.hAdd.

[Jovan Gerbscheid]

When there are a lot of instances involved, it goes a bit crazy, and it duplicates instances that appear multiple times:

image.png

[Jovan Gerbscheid]

In this example it's surprising that the Monad MetaM instance shows up among the used instances, because it isn't necessary for the MonadStateOf instance. But it turns out that docs#StateRefT'.instMonadStateOfOfMonadLiftTSTOfMonad unnecessarily takes the monad instance as an argument.

So it turns out that this view is already helpful for debugging :laughing:

[Jovan Gerbscheid]

I'm surprised there is no unused variable linter ever being run on Lean core

[Sebastian Ullrich]

There is no variable name here so there is no unused variable lint

[Jovan Gerbscheid]

Oh, so there is no linter that checks for unused instance arguments?

[Eric Wieser]

I think that one only exists in mathlib

[Jovan Gerbscheid]

How can we run mathlib's linters on Lean core?

[Eric Wieser]

I think it would be easy enough to modify the script to work, but quite hard to integrate it into cores CI without making dependency spaghetti

[Kim Morrison]

Just running once would be nice.

[Jovan Gerbscheid]

I found out how to run the linters on all imported files. It turns out that there is a lot to fix in core Lean.

import Std.Tactic.Lint

#lint only unusedArguments in all -- Found 113 errors
#lint only checkUnivs in all -- Found 1 error
#lint only defLemma in all -- Found 40 errors
#lint only explicitVarsOfIff in all -- Found 56 errors
#lint only dupNamespace in all -- Found 8 errors
#lint only impossibleInstance  in all -- Found 1 error
#lint only simpNF in all -- Found 27 errors
#lint only simpVarHead in all -- Found 1 error
#lint only unusedHavesSuffices in all  -- Found 3 errors

About half of the unused variable errors I believe are intended. But most other errors are genuine errors.

[Kim Morrison]

@Jovan Gerbscheid has now fixed some of these in lean#4502.

I'm surprised there are only 27 simpNF linter errors, I was expecting way more. I will work on these soon.

[Kim Morrison]

I've now fixed most of the fixable linter reports. See batteries#871 for details.

[Kim Morrison]

I still haven't touched explicitVarsOfIff. I'd welcome a PR making progress on that.

[Thomas Murrills]

Jovan Gerbscheid said:

ctrl + click

Hmm, on a mac, control + click gives me the context menu ("right click"), and command + click is the usual go-to-def; I can get a panel with "Definitions" rendered like that if click "Peek Definitions..."—but I only ever see one definition in that panel, even when reproducing the example in the image exactly. (Other modifier keys don't seem to get any closer either.) I wonder what the difference is...