instance name auto-generating does not respect `protected`?

Stream: general

[SnO2WMaN]

A simple question: when instantiating some class for a protected definition, why doesn’t the auto-generated instance name respect the protected qualifier? I know there’s some history here—like the problem of instance names getting too long, which was improved in the past—but personally I’d prefer if it did respect protected.

My personal context is that I have a large number of definitions spread across multiple files, and I rely on auto-generated instance names. When importing those files, the names inevitably clash. Manually naming each instance isn’t very appealing in terms of code size.

import Mathlib.Data.Set.Basic

namespace Foo.Bar

protected abbrev Variable := Set ℕ

end Foo.Bar

-- Auto generated name is `instInhabitedVariable`
-- But it should be `instInhabitedBarVariable` if it respected the protected name?
instance : Inhabited Foo.Bar.Variable := ⟨∅⟩

[Robin Arnez]

Instance names simply never include namespaces; that's just how it works. But you should probably not rely on auto-generated names in your case, just

instance instInhabitedBarVariable : Inhabited Foo.Bar.Variable := ⟨∅⟩

[Robert Maxton]

That's kinda gross, honestly; I'd certainly prefer automatic names to respect protected to having to name instances that I don't intend to refer to

[Robin Arnez]

Oh wait maybe I misunderstood; normally it should automatically use instInhabitedVariable_1 if instInhabitedVariable already exists; the import structure may make this a bit difficult though. I guess if you have clashing instance names you can have one module import the other?

[Robin Arnez]

Or, you know, put the instance within a namespace

[SnO2WMaN]

Robert Maxton said:

That's kinda gross, honestly; I'd certainly prefer automatic names to respect protected to having to name instances that I don't intend to refer to

I agree this opinion. My adhoc fix for this problem with adding namespace to protect, but we have 20 more defs, tbh, it's cumbersome.

[Kyle Miller]

The intended way to do this is

namespace Foo.Bar

protected abbrev Variable := Set ℕ

namespace Variable
instance : Inhabited Foo.Bar.Variable := ⟨∅⟩
end Variable

end Foo.Bar

The automatic instance name system is not designed to put the instance into a different namespace. It always puts the instances into the current namespace.

SnO2WMaN said:

I’d prefer if it did respect protected

How do you imagine this would work? What does "respect" mean to you? Would you want the automatic instance name system to use an ad hoc rule to decide what the typeclass is "about" and copy the protected modifier? How would this work in the root namespace?