Sealing an unsafe inductive

Stream: lean4

[Wojciech Nawrocki]

Is it possible to seal an unsafe inductive type? The trouble I am running into is that the safe, opaque version of the type is not defeq to the unsafe version and consequently implemented_by rejects definitions on the safe version. More specifically,

unsafe inductive RecMapUnsafe (α β : Type) : Type where
  | mk (m : α → Option (RecMapUnsafe α β → Option β)) : RecMapUnsafe α β

unsafe def RecMapUnsafe.get? (a : α) : RecMapUnsafe α β → Option β
  | mk m => m a |>.bind (· $ mk m)

@[implemented_by RecMapUnsafe]
opaque RecMap : Type → Type → Type

/- invalid 'implemented_by' argument 'Ii.RecMapUnsafe.get?', 'Ii.RecMapUnsafe.get?' has type
  {α β : Type} → α → RecMapUnsafe α β → Option β
but 'Ii.RecMap.get?' has type
  {α β : Type} → α → RecMap α β → Option β -/
@[implemented_by RecMapUnsafe.get?]
opaque RecMap.get? (a : α) : RecMap α β → Option β

[Wojciech Nawrocki]

I guess we can write

unsafe def RecMap.get?Unsafe (a : α) (m : RecMap α β) : Option β :=
  let m : RecMapUnsafe α β := unsafeCast m
  m.get? a

@[implemented_by RecMap.get?Unsafe]
opaque RecMap.get? (a : α) : RecMap α β → Option β

[Gabriel Ebner]

You might be interested in https://github.com/leanprover-community/mathlib4/blob/067dad6dcbd5e61738f205faaeb4a0a3e26d9efd/Mathlib/Data/ListM/Basic.lean

[Wojciech Nawrocki]

As in, the strategy of sealing a whole API at once? Or are you saying I should be interested in that data structure itself?

[Wojciech Nawrocki]

As a side note, there seems to be some kind of miselaboration when I change the type a bit:

/- application type mismatch
  Array.size vs
argument has type
  _nested.Array_4
but function has type
  Array (RecMapUnsafe' α β → Option β) → ℕ -/
unsafe inductive RecMapUnsafe' (α : Type u) [BEq α] [Hashable α] (β : Type v) : Type (max u v) where
  | mk (m : PersistentHashMap α (RecMapUnsafe' α β → Option β)) : RecMapUnsafe' α β

[Gabriel Ebner]

I was only suggesting the strategy.