valid occurrence of the datatypes ...

Stream: lean4

[Yuri de Wit]

Consider the following inductive type:

inductive T
| node (children: Array T)
| ref (val: IO.Promise T)

I get the following error:

(kernel) arg #1 of 'T.ref' contains a non valid occurrence of the datatypes being declared

The same error happens if I use IO.Ref, but it works if I use something like a simpler wrapper:

structure Wrapper (a: Type) where
  val: a

inductive T
| node (children: Array T)
| ref (val: Wrapper T)

I did see earlier discussions on this same error message, but I still have no idea of what it means.

[Yuri de Wit]

Humm, one discussion did shed some light into the problem: https://github.com/leanprover/lean4/blob/a91b8619196b6d5d94a5bc39457b67314fd78953/src/Lean/Data/Json/Basic.lean#L137-L140 :

-- uses RBNode instead of RBMap because RBMap is a def
-- and thus currently cannot be used to define a type that
-- is recursive in one of its parameters

And Promise is indeed a def:

def Promise (α : Type) : Type := (PromiseImpl α).1

Does this mean that a Promise cannot be used in an inductive?

[Mario Carneiro]

yes, unless you use unsafe

[Mario Carneiro]

it's not def specifically which is the problem but rather if you unfold the def you need to get an inductive type (and I'm guessing PromiseImpl is an opaque)

[Yuri de Wit]

Yes, PromiseImpl is an opaque. Using unsafe gets me past the immediate issue, but it seems that it locks me out of most (all?) deriving instances (e.g. invalid declaration, it uses unsafe declaration 'Term'), which, I think, means I would have to create the instances by hand.

What is the proper solution to this even if it is not here in the short term?

[Jannis Limperg]

The deriving methods could probably be updated to generate unsafe definitions if the type itself is unsafe.

The more general issues is that an unsafe type forces every function mentioning it to be unsafe. If you don't want this, you can try to create a safe version of your type which is then implemented_by the unsafe version. See here for an example. You'll definitely pay a price in convenience though, e.g. deriving likely becomes impossible.