Inductive type constructed by a list of that type in Lean
<p>I would like to define an inductive type that can be constructed from a list of itself in lean.  However</p>

<pre><code>inductive a : Type :=
| aFromAs : list a → a
</code></pre>

<p>gives the error:</p>

<pre><code>failed to infer inductive datatype resultant universe, provide the universe levels explicitly
</code></pre>

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

<pre><code>inductive a : Type₁ :=
| aFromAs : list a → a
</code></pre>

<p>gives the error </p>

<pre><code>arg #1 of aFromAs contains an non valid occurrence of the datatype being declared
</code></pre>

<p>It looks valid to me. This seams like it should work.</p>