kernel err: non valid occurrence of the datatypes being decl

Stream: lean4

[Yuri]

Consider:

inductive Sig where
  | sum (l r : Sig)
  | empty
  | var
  | prod (l r : Sig)
  | fix

def decode : Sig → (Type × Type → Type)
  | .sum l r  => fun (αβ : Type × Type) => Sum ((decode l) αβ) ((decode r) αβ)
  | .empty    => fun (_  : Type × Type) => Empty
  | .var      => fun (αβ : Type × Type) => αβ.1
  | .prod l r => fun (αβ : Type × Type) => Prod ((decode l) αβ) ((decode r) αβ)
  | .fix      => fun (αβ : Type × Type) => αβ.2

inductive Mu (S : Sig) (A : Type) where -- <== ERROR HERE
  | fold : decode S (A, Mu S A) → Mu S A

I get the following error:

(kernel) arg #3 of 'Mu.fold' contains a non valid occurrence of the datatypes being declared

What is the problem here?

[Shreyas Srinivas]

you have a negative occurrence of S in fold

[Shreyas Srinivas]

The error message could be better though if the issue was caught before sending the code to the kernel.