Zulip Chat Archive

Stream: lean4

Topic: valid occurrence of the datatypes ...


Yuri de Wit (Jan 30 2023 at 02:56):

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 (Jan 30 2023 at 03:07):

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 (Jan 30 2023 at 03:12):

yes, unless you use unsafe

Mario Carneiro (Jan 30 2023 at 03:13):

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 (Jan 30 2023 at 12:32):

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 (Jan 30 2023 at 12:43):

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.


Last updated: Dec 20 2023 at 11:08 UTC