Help understanding universe error

Stream: general

[Ayhon]

The following type definition gives me a universe error (see in editor)

inductive Foo: List Type -> Type where
| A: Foo []
| B(S: List Type): Foo S

Why is this a problem? Is it that the constructor B has type (s:List Type) -> Foo S and List Type is a Type, same with Foo S, so B has type Type 1 and this prevents it from being defined in Foo?

More generally, I have trouble reasoning about universes. Any recommendations on resources on the topic, beyond the Functional Programming in Lean chapter, which I've already read and will read again

[Eric Wieser]

inductive Foo: List Type -> Type 1 where
| A: Foo []
| B(S: List Type): Foo S

is fine

[Ayhon]

Huh... Ok, let me try to incorporate it into my actualy code and see if that fixes it. I swear I tried that before

[Ayhon]

For now, this is closer to what I'm actually trying to model. It still doesn't work.

class Eff where
  inM:  Type -> Type
  outM: Type -> Type

-- EDITED: inductive P(A: Type): List ArrowEffect -> (Type 1) where
inductive P(A: Type): List Eff -> (Type 1) where
| Foo(a: A): P A []
| Bar{E: Eff}{S: List Eff}{B: Type}
  (input: E.inM A)
  (cont: E.outM A -> P B S)
  : P A S

[Eric Wieser]

What is ArrowEffect there?

[Ayhon]

Sorry, that's supposed to be Eff. Let me see if that fixes it

[Ayhon]

Different error, so progress, but still have an error
(kernel) arg #6 of 'P.Bar' contains a non valid occurrence of the datatypes being declared
See code

[Edward van de Meent]

the issue is that you're not allowed to change A in this inductive, since it's to the left of the colon. you do change it, however, when you write P B S in the type of the cont argument

[Edward van de Meent]

this is an example fix:

inductive P : Type → List Eff -> (Type 1) where
| Foo {A : Type} (a : A) : P A []
| Bar {A : Type} {E : Eff} {S : List Eff} {B: Type} (input: E.inM A) (cont: E.outM A -> P B S)
  : P A S

[Ayhon]

I see thanks! I never would have thought that the P B S was the issue. Why does this restriction exist? What property does it compromise?