Warning for empty inductive types?

Stream: lean4

[François G. Dorais]

Should there be a warning (but not an error!) when a user defines an empty inductive type?

Empty inductive types happen when all constructors have the inductively defined type as an argument. For example:

inductive NotMuch (α : Type _) where
| ctor : α → NotMuch α → NotMuch α

While False and Empty are deliberately empty and useful, types like NotMuch are generally useless and probably not what the user intended.

My motivation for this is indirect. I have a project that transforms inductive types into related inductive types and proves some stuff about this transform. I would like to dismiss empty inductive types like NotMuch with an error since they don't work for the construction. This sounds a bit wrong since there are no prior warnings that this is just a "bad" inductive type.

Anyway, I'm okay with just sending an error in my use case, but I think an early warning about empty inductive types could be useful for users to avoid some paper cuts.

[Marcus Rossel]

I think you're going to have a hard time checking whether an inductive type is empty in general:

inductive AmIEmpty? where
  | intro (h : RiemannHypothesisIsTrue)

Or are you only interested in an incomplete procedure which checks certain known scenarios?

[Damiano Testa]

In Mathlib3 there was a has_nonempty_instance linter: every inductive either had a Nonempty instance recorded or a nolint on the inductive.

[Damiano Testa]

https://github.com/leanprover-community/mathlib/blob/65a1391a0106c9204fe45bc73a039f056558cb83/src/tactic/lint/default.lean#L38

[François G. Dorais]

@Marcus Rossel You got the wrong idea, it's not about the parameters, only the constructors!

This is totally fine:

inductive MaybeMore (α : Type _) where
| base : α → MaybeMore α
| ctor : α → MaybeMore α → MaybeMore α

The issue is when all constructors depend on the inductive type being defined.

[Marcus Rossel]

François G. Dorais said:

Marcus Rossel You got the wrong idea, it's not about the parameters, only the constructors!

This is totally fine:

inductive MaybeMore (α : Type _) where
| base : α → MaybeMore α
| ctor : α → MaybeMore α → MaybeMore α

The issue is when all constructors depend on the inductive type being defined.

But aren't the parameters part of the constructors? What I was trying to say is that you can have structurally innocent looking constructors which will never be applicable because they have parameters whose types may or may not be empty.
Thus, "when all constructors depend on the inductive type being defined" you have a sufficient condition for emptiness of the inductive type, but not a necessary one.

That's why I was wondering if you're only interested in an incomplete decision procedure (warning procedure) for the emptiness of an inductive type, because a complete one won't be possible.

[François G. Dorais]

This is a syntactic check not a semantic one. I think you're taking the title of the thread a bit too literally.