Invalid occurrence of datatype being declared

Stream: general

[nrs]

structure Signature where
  symbols : Type
  arity : symbols -> Nat

inductive Vect (α : Type u) : Nat → Type u where
   | nil : Vect α 0
   | cons : α → Vect α n → Vect α (n + 1)

def semF (σ : Signature) (α : Type) : Type := Sigma (fun x => Vect α (σ.arity x))

inductive μ : (σ : Signature) -> Type _
| mk : semF σ (μ σ) -> μ σ

how come the above produces (kernel) arg #2 of 'μ.mk' contains a non valid occurrence of the datatypes being declared?

[nrs]

It works if we use unsafe inductive μ (σ : Signature)

[nrs]

I've also tried replacing occurrence of Type in semF by Type _

[Mario Carneiro]

because nested inductive types only work through other inductives

[nrs]

Mario Carneiro said:

because nested inductive types only work through other inductives

i.e. semF should be inductive for this to work?

[Mario Carneiro]

If you inline the definition of semF it appears to work

[nrs]

Mario Carneiro said:

If you inline the definition of semF it appears to work

ah thank you very much! I'm adding that to my heuristics. First: check whether you need to change parameters ordering. Second, check whether universe level is right. Now adding third: try inlining.

[nrs]

in this case this happened because semF was not inductive right?

[Mario Carneiro]

yes

[nrs]

noted, tyvm for help!!

[Mario Carneiro]

specifically, try inlining any functions which use the type being defined, here μ σ