[Merged by Bors] - refactor(tactic/lint/type_classes): change inhabited linter to nonempty linter

[kmill]

The inhabited typeclass is intended to be a default value (and computable, if one is writing programs) but many times it is filled in with a junk (and perhaps noncomputable) value to satisfy the has_inhabited_instance linter. This commit switches to a has_nonempty_instance linter to push contributors toward supplying a nonempty instance instead. The linter still accepts inhabited and unique instances, which should be preferred over nonempty when appropriate.

---

[kmill]

#1898 is where the has_inhabited_instance linter was added, which had some discussion.

@gebner I think I still don't fully understand the inhabited instance linter, and it might be because the corners of mathlib I'm familiar with don't tend to need inhabited over nonempty. Maybe these are the goals:

• if a definition needs a default value, you'd prefer to have a computable inhabited instance.
• if that definition is noncomputable, it's ok to use nonempty and choice.
• if a theorem needs a default value in a proof, nonempty is enough.

There are a number of places in mathlib where there are arbitrary values (like 37), or inhabited instances that require hard-to-meet additional typeclasses, or they're noncomputable. These all seem to subvert the goals of the linter, which is why I was thinking about changing it to a nonempty linter. But this might subvert the goals further since now people will write nonempty instances when inhabited instances might be preferred.

Maybe it would be better to have the linter itself suggest adding a nolint if there are no good default values? Or extend it to be satisfied with a nonempty instance (while keeping the has_inhabited_instance name) and document this somewhere?

[gebner]

My original intention with the inhabited linter was to flag issues like inhabited (array α) is missing (and there were a lot of such more-or-less clear-cut missing instances back in the day). I wanted to push people to add general instances like inhabited α → inhabited (additive α). The concrete motivation was an encoding to simply-typed higher-order logic, were types are required to be nonempty (and the encoding can be made simpler if we know that the Lean type is nonempty).

For many types in mathlib, requiring inhabited doesn't make much sense though (like morphism types, etc.) because there is no canonical or general instance. This is also reflected in the sheer number of @[nolint has_inhabited] attributes. For that reason, I proposed retiring the inhabited linter, since I thought it was just annoying people.

But to my surprise, some people actually took the linter's advice in an unexpected and different direction. Instead of adding general instances, they added particular examples of the type in the question (such as the 37 you refer to). This is certainly valuable information (and a sneaky way to get around mathlib's "no examples" policy), but not really what the inhabited type class is for. (I guess I should have just made the linter smarter.)

In general, making these noncanonical inhabitants nonempty rather than inhabited seems like a good change to me. Maybe we also need a more explicit and officially sanctioned way to include examples (I have no data on how common this abuse of inhabited is). There is one notable use of inhabited though, namely in the unique type class, so we can't just change everything to nonempty.

[fpvandoorn]

I am personally more in favor of retiring this linter (and removing a bunch of inhabited instances that are never used), but I don't mind this change either.

[eric-wieser]

I think pushing for nonempty instances is a good idea still; it forces users contributing new structures to avoid defining something that aliases false for every parametrization by accident.

[Vierkantor]

I'm enough of an intuitionist to think that we should push inhabited as much as possible, but I guess the consensus in this thread overrules me.

I'd still like the documentation to push the user a bit further towards inhabited or unique if appropriate, otherwise this looks good to me.

Could you merge master before handing the PR over to bors?

bors d+

[bors]

✌️ kmill can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[kmill]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests

[digama0]

Why are there junk inhabited instances being made? I did see a 37 in one of them, but I think we should try to avoid that kind of thing. There should be an inhabited instance where applicable, and it should be canonical where possible.