## Stream: general

### Topic: Bad instance name lint

#### Mario Carneiro (Aug 12 2020 at 18:15):

This has caught me out many times, so I'm wondering if we can get a lint to watch for it (or maybe even fix lean so it doesn't happen).

inductive widget : Type

instance : has_to_string widget := ⟨λ x, by cases x⟩ -- widget.has_to_string
instance : has_to_string doodad := ⟨λ x, by cases x⟩ -- doodad.has_to_string

namespace foo

inductive widget : Type

instance : has_to_string widget := ⟨λ x, by cases x⟩ -- foo.has_to_string
instance : has_to_string doodad := ⟨λ x, by cases x⟩ -- foo.has_to_string, error

end foo


Usually I won't even notice that foo.widget's instance has a name that doesn't mention widget until I write foo.doodad and hit the name conflict, so I'm quite sure that there are many uncaught instances of this problem in mathlib.

#### Kevin Buzzard (Aug 12 2020 at 18:23):

ha ha I'm not sure I want to know the number of instances with bad names in mathlib :-) Wouldn't it be more fun to change Lean so that it names the instances in a cleverer way and then see if mathlib still compiles? So what is the algorithm for naming instances? It's well-known that the current method is laughed at but is there a cleverer proposal which is less bad? In namespace foo I decide to prove foo A -> baz B -> bar (prod A B) and also bar A -> foo B -> baz (prod A B) (with foo, bar, baz all classes). Are these now both named something like foo.prod? What is your proposal for the example you post? What do you want has_to_string foo to be called in namespace foo? I think there was a discussion here a long time ago about naming lemmas and how it wasn't at all automatic because you have a tree of constants which you want to turn into a list of constants.

#### Mario Carneiro (Aug 12 2020 at 18:57):

I think that for the most part the instance names that are automatically generated are okay, not great but usable

#### Mario Carneiro (Aug 12 2020 at 18:58):

not to mention that they more or less by necessity have to define our style guide for naming instances

#### Mario Carneiro (Aug 12 2020 at 19:01):

I think that the right answer in this instance is that namespaces should always just append, never replace bits of the name. So this one should be called foo.widget.has_to_string

#### Mario Carneiro (Aug 12 2020 at 19:02):

Although, I think that this would name your instances foo.prod.bar and foo.prod.baz respectively which is a bit odd to say the least

#### Mario Carneiro (Aug 12 2020 at 19:05):

Another thing that would help is if the instance naming algorithm was more comfortable saying "I don't know what to call this, you do it"

#### Mario Carneiro (Aug 12 2020 at 19:07):

For example

instance : has_to_string (Sort -> Sort) := sorry


gives failed to synthesize instance name, name should be provided explicitly but

namespace foo
instance : has_to_string (Sort -> Sort) := sorry
end foo


gives foo.has_to_string like the others. I think that when this situation occurs (lean wants to call it foo.has_to_string) we are in the case that we should at least lint and maybe also give the failed to synthesize instance name error

#### Kevin Buzzard (Aug 12 2020 at 19:13):

I think I'd rather be asked for an instance name than accidentally name an instance badly

#### Mario Carneiro (Aug 12 2020 at 19:17):

Here is the relevant code:

        /* Try to synthesize name */
expr it = type;
while (is_pi(it)) it = binding_body(it);
expr const & C = get_app_fn(it);
name ns = get_namespace(p.env());
if (is_constant(C) && !ns.is_anonymous()) {
c_name = const_name(C);
scope.set_name(c_name);
} else if (is_constant(C) && is_app(it) && is_constant(get_app_fn(app_arg(it)))) {
c_name = const_name(get_app_fn(app_arg(it))) + const_name(C);
scope.set_name(c_name);
} else {
p.maybe_throw_error({"failed to synthesize instance name, name should be provided explicitly", c_pos});
c_name = mk_unused_name(p.env(), "_inst");
}


In english, it says to get the conclusion of the theorem, and call it it, with the head constant of it (the instance like has_to_string) being C. If we are not at the top level, then name it current_namespace.C (this is the bad case), else if the last argument of it is itself a constant D applied to things then name it current_namespace.D.C, else complain to the user

#### Mario Carneiro (Aug 12 2020 at 19:19):

We could just swap the two if statements, so that the present case gets the name current_namespace.D.C, and the scheme current_namespace.C is only used for things like the has_to_string (Sort -> Sort) example

#### Mario Carneiro (Aug 12 2020 at 19:19):

or we could just delete that case entirely so that this case gives the failed to synthesize instance name error

#### Reid Barton (Aug 29 2020 at 16:48):

I think the first case probably exists to handle situations like

structure foo : Type
namespace foo
instance : has_add foo := ⟨λ _ _, ⟨⟩⟩
end foo
#check foo.has_add   -- not foo.foo.has_add


because it's pretty common to create a structure and then add a lot of things in a namespace, and some of those things are likely to be instances for the structure you just made.

#### Reid Barton (Aug 29 2020 at 16:50):

Of course it can also choose the wrong name in other situations, for example if the namespace is something like category_theory

#### Reid Barton (Aug 29 2020 at 16:55):

How about this heuristic: drop the first case and, in the second case, don't include the D part of the name if it equals the last component of the current namespace.

#### Reid Barton (Aug 29 2020 at 17:56):

A better version of this is: drop the current namespace from either the C or the D component if it happens to be a prefix of them

#### Reid Barton (Aug 29 2020 at 20:50):

lean#458 is my proposal

#### Reid Barton (Aug 30 2020 at 00:39):

wait, no. I was supposed to say "My proposal is lean#458"

Last updated: May 10 2021 at 00:31 UTC