inductive type with dependent recursive substructure

Stream: lean4

[TheGreatCatAdorer]

Is there a way to create an inductive type with a dependent recursive substructure?
Lean says its kernel found a non-valid instance of the type being declared.

class Indexed (α : Type u → Type u) (β : Type u) where
  index : α β → Nat → Option β
  length : α β → Nat

instance : Indexed List α where
  index := λ (list : List α) (index : Nat) =>
    List.head? (List.drop index list)
  length := List.length

inductive Rose (m : Type u → Type u) (α : Type u) [Indexed m α] where
  | null : Rose m α
  | tree : α → m (Rose m α) → Rose m α```

[Mario Carneiro]

No, these kinds of inductive types cannot be accepted, because m A can be something like A -> False which you can use to deduce contradictions

[Mario Carneiro]

maybe a better example, if you take m A := A -> Bool in this definition, then Rose m Unit will violate cantor's theorem

[TheGreatCatAdorer]

The kernel has an issue with the below definition. Is there a way to do it in Lean?

inductive Rose (m : Type u → Type u) (α : Type u)  where
  | null : Rose m α
  | tree : α → m (Rose m α) → Rose m α

[Mario Carneiro]

@TheGreatCatAdorer See above

[Leonardo de Moura]

@TheGreatCatAdorer
You can use

unsafe inductive Rose (m : Type u → Type u) (α : Type u)  where
  | null : Rose m α
  | tree : α → m (Rose m α) → Rose m α

Any definition that uses Rose will also have to be marked as unsafe.
See @Mario Carneiro's explanation above to understand why it cannot be a regular Lean declaration.

[Leonardo de Moura]

Not sure exactly what you are trying to do, but you may also consider writing a macro that given a m, generates a new Rose type instantiated with the given m.

[Leonardo de Moura]

The macro expansion should work for many m we care in practice, and will fail for examples like the ones Mario mentioned above.

[TheGreatCatAdorer]

I do enjoy macros.

[Joseph O]

Mario Carneiro said:

maybe a better example, if you take m A := A -> Bool in this definition, then Rose m Unit will violate cantor's theorem

Why would it violate the theorem?

[Mario Carneiro]

You get a type with the shape

inductive Foo
| null : Foo
| tree : Unit -> (Foo -> Bool) -> Foo

or if we simplify things a bit:

inductive Foo
| tree : (Foo -> Bool) -> Foo

Constructors of inductive types are always injective, so Foo.tree : (Foo -> Bool) -> Foo is an injective function, so card (Foo -> Bool) <= card Foo. But cantor's theorem says card X < card (X -> Bool) for any X, contradiction.