Indexed Inductive

Stream: lean4

[Arthur Adjedj]

Hi, I stumbled upon this error recently, that I wouldn't see happen on Coq and Agda :

def family := Type → Type

inductive good : Type → Type

inductive bad : family
--(kernel) error in 'noConfusion' generation, 'bad' inductive datatype declaration is corrupted

Is this an expected behaviour ? The error still arises when familyis marked as an abbrev or as `reducible.

[Mario Carneiro]

I believe that the design has gone back and forth on whether inductive types are allowed to not be syntactically a telescope ending in Sort u for some u, and I think you are seeing different parts of the system in disagreement about this. Last I heard these are disallowed completely, so you will have to define your type like good

[Arthur Adjedj]

If such a thing isn't allowed, maybe it would be best to have an accurate error for this, or at least a consistent result when doing this. When doing the same thing for something defequal to a Sort u, such an error does not arise:

def family := Type

inductive bad? : family
--no error

If I may ask, what would the drawbacks of allowing such a syntax be ?