Bad instance name lint

Stream: general

[Mario Carneiro]

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
inductive doodad : 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
inductive doodad : 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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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]

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

[Mario Carneiro]

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]

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]

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

[Reid Barton]

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]

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

[Reid Barton]

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]

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]

lean#458 is my proposal

[Reid Barton]

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