Kernel error: '.. non valid occurrence of the datatypes ..'

Stream: lean4

[Yuri]

I am a bit confused by the error message in :

inductive Desc (I J : Type) : Type 1
  | σ : (A : Type) → (A → Desc I J) → Desc I J
  | X : J → Desc I J → Desc I J
  | stop : I → Desc I J

def denote {I J : Type} : (Desc I J) →  (J → Type) → (I → Type)
  | .σ A d, X, i => Σ (a : A), denote (d a) X i
  | .X j d, X, i => X j × denote d X i
  | .stop j, _, i => PLift (i = j)

inductive μ (d : Desc I I) : I → Type   -- error here!
  | con : denote d (μ d) i → μ d i

The error: (kernel) arg #4 of 'μ.con' contains a non valid occurrence of the datatypes being declared.

Any ideas? This was translated from Agda.

[Jovan Gerbscheid]

Lean cannot figure out that the inductive type is valid, because μ doesn't appear in a position where it is obvious that the inductive is valid. To figure out that it is valid, you need to look closely at the definition of denote, which Lean doesn't know how to do.

An even simpler case that Lean can't yet do is with Std.HashMap, see also #lean4 > Tree/Map/HashMap in Inductive Data Type