nested inductive datatypes parameters cannot contain local v

Stream: lean4

[Adrien Champion]

Here is a tiny example of a problem I ran into recently

inductive Ty
  | bool
  | nat
def Ty.type : Ty → Type
  | .bool => Bool
  | .nat => Nat

inductive E₁ : Ty → Type
| cst {ty : Ty} : ty.type → E₁ ty
| eq {ty : Ty} : E₁ ty → E₁ ty → E₁ Ty.bool
-- no problem

inductive E₂ : Ty → Type
| cst {ty : Ty} : ty.type → E₂ ty
| app {ty : Ty} : (op : String) → (args : Array (E₂ ty)) → E₂ ty
-- no problem

inductive E₃ : Ty → Type
| cst {ty : Ty} : ty.type → E₃ ty
| eq {ty : Ty} : E₃ ty → E₃ ty → E₃ Ty.bool
| app {ty : Ty} : (op : String) → (args : Array (E₃ ty)) → E₃ ty
-- (kernel) invalid nested inductive datatype 'Array',
-- nested inductive datatypes parameters cannot contain local variables.

[Adrien Champion]

I found a handful of discussions that are somewhat related:

• https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Tree.20with.20fixed.20branching
• https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20requiring.20proofs.20on.20inductive.20constructors

But even after reading them, I'm not sure what precisely the problem is in my example and how to solve it assuming it's possible.

[Adrien Champion]

Admittedly it's probably because I'm still too much of a Lean noob to actually understand these discussions fully, so any direct help or pointers to related discussions elsewhere would be greatly appreciated :smile:

[Mario Carneiro]

What is happening is that the presence of the eq constructor is making ty have to be treated as an index of the inductive type instead of a parameter. (In lean 3, the parameters all came before the colon in the inductive type declaration and the indices after, but lean 4 tries to be clever and promote indices to parameters when it can.)

[Mario Carneiro]

That's only half of the error though, the other half is that the nested inductive checker does not accept inductives which depend on local variables like ty here. I think this is not an essential constraint, and the checker could accept nested inductive families, but this is a very thorny part of the theory and I would prefer to be conservative without an explicit proof that it's sound to do this

[Siddharth Bhat]

Is this the MWE, or can it be made smaller?

inductive Const : Type _ | mk

inductive Const1 (t: Type _) : Type _ | mk : Const1 t

inductive E₃ : Const → Type
| mk : {c : Const} → (args : Const1 (E₃ c)) → E₃ Const.mk

[Adrien Champion]

Mario Carneiro said:

What is happening is that the presence of the eq constructor is making ty have to be treated as an index of the inductive type instead of a parameter. (In lean 3, the parameters all came before the colon in the inductive type declaration and the indices after, but lean 4 tries to be clever and promote indices to parameters when it can.)

That's quite helpful thanks. I did not know about this distinction between parameters and indices

[Mario Carneiro]

Indeed the following mutual inductive is accepted

mutual
inductive E₃ : Ty → Type
| cst {ty : Ty} : ty.type → E₃ ty
| eq {ty : Ty} : E₃ ty → E₃ ty → E₃ Ty.bool
| app {ty : Ty} : (op : String) → (args : List_E₃ ty) → E₃ ty

inductive List_E₃ : Ty → Type
| nil : List_E₃ ty
| cons : E₃ ty → List_E₃ ty → List_E₃ ty
end

so I think it is an issue in the checker (which is trying to verify that the reduction to this mutual inductive is legal)

[Adrien Champion]

For readers that want to learn more about indices/parameters, I found the answer for this SO post helpful:

• https://stackoverflow.com/questions/24600256/difference-between-type-parameters-and-indices

[Adrien Champion]

Mario Carneiro said:

so I think it is an issue in the checker (which is trying to verify that the reduction to this mutual inductive is legal)

Are you saying that the error I get is not expected in the sense that the checker could/should see there's such a reduction, and accept the original code with the standard List/Array types?

[Mario Carneiro]

yes, at least from my cursory reading of it

[Mario Carneiro]

My knowledge of the nested inductive checker is only indirect, I haven't read the code and there isn't really any spec for it besides what I've said so far (Sebastian's thesis extends #leantt to include lean 4 features but I don't think it covers the nested inductive checker in full detail - things get pretty hairy when you write it all down)