inductive datatype error

Stream: new members

[Michael Hahn]

Hello,
I'm currently getting an error about inductive types that I don't quite understand:

structure simple_graph :=
(E: V → V → Prop)
(loopless: irreflexive E)
(undirected: symmetric E)


inductive path [G : simple_graph V]: V → V → Type*
| nil  : Π (h : V), path h h
| cons : Π {h s t : V} (e : G.E h s) (l : path s t), path h t

Error:

universe level of type_of(arg #3) of 'path.nil' is too big for the corresponding inductive datatype

[Bryan Gin-ge Chen]

This works:

universes u
variable (V : Type u)

structure simple_graph :=
(E: V → V → Prop)
(loopless: irreflexive E)
(undirected: symmetric E)


inductive path [G : simple_graph V]: V → V → Type u
| nil  : Π (h : V), path h h
| cons : Π {h s t : V} (e : G.E h s) (l : path s t), path h t

I think the universe assigned to the Type* in path has to be greater than or equal to the universe level that V lives in?

[Michael Hahn]

Thank you!