Inductive type constructed by a list of that type in Lean

Question

I would like to define an inductive type that can be constructed from a list of itself in lean. However

inductive a : Type :=
| aFromAs : list a → a

gives the error:

failed to infer inductive datatype resultant universe, provide the universe levels explicitly

Fine, so I set_option pp.universes true and list belongs to the type universe of its parameter (unless the parameter is Prop). So if a is Type₁ everything should be fine. But

inductive a : Type₁ :=
| aFromAs : list a → a

gives the error

arg #1 of aFromAs contains an non valid occurrence of the datatype being declared

It looks valid to me. This seams like it should work.

Answer 1

Lean 3 now supports nested inductive declarations:

inductive a : Type
| aFromAs : list a → a