Can't understand universes in inductives

Stream: new members

[Jakub Nowak]

If I write:

inductive Foo : Type → Type where
| nil : {α : Type} → Foo α

then Lean accepts this without errors.

But when I add constructor like this:

inductive Foo : Type → Type where
| nil : {α : Type} → Foo α
| cons : {α β : Type} → (α → Foo β) → Foo β

then now I get error about universes in constructor nil which worked fine before.

What's going on?

[Aaron Liu]

that's because the index is not being promoted to a parameter anymore

[Aaron Liu]

Since you can rewrite the first Foo as

inductive Foo (α : Type) : Type where
| nil : Foo α

But you can't do the same kind of thing for the other Foo

[Jakub Nowak]

I see. That's kinda confusing, is there a reason why Lean does that automatic promotion of indexes to parameters?

[Aaron Liu]

it's so you don't get the error on a perfectly reasonable inductive

[Jakub Nowak]

Is it reasonable though? It seems like it's impossible to write inductive with signature Type → Type unless the argument is a parameter.

[Aaron Liu]

so it's fine if the argument is a parameter

[Kenny Lau]

@Jakub Nowak Foo β must contain cons f for any function f : α → Foo β for any α : Type!! Surely that is too big for something in Type

[Jakub Nowak]

Actually, I think that

inductive Foo (α : Type) : Type where
| nil : Foo α

and

inductive Foo : Type → Type where
| nil : (α : Type) → Foo α

aren't the same.

In first case α is a parameter of Foo, while in second, it's a parameter of Foo.nil.

[Aaron Liu]

comparison:

inductive Foo (α : Type) : Type where
| nil : Foo α

/--
info: inductive Foo : Type → Type
number of parameters: 1
constructors:
Foo.nil : {α : Type} → Foo α
-/
#guard_msgs in
#print Foo

and the other one

inductive Foo : Type → Type where
| nil : (α : Type) → Foo α

/--
info: inductive Foo : Type → Type
number of parameters: 1
constructors:
Foo.nil : (α : Type) → Foo α
-/
#guard_msgs in
#print Foo

[Aaron Liu]

so I think they're basically the same

[Kenny Lau]

@Jakub Nowak in both cases, each Foo α just contains .nil and nothing else