Unsafe inhabited constants

Stream: lean4

[Mac]

So I was modelling pointers and discovered a weird oddity with unsafe constants:

def Addr := USize
def Addr.zero : Addr := (0 : USize)
instance : Inhabited Addr := ⟨Addr.zero⟩

constant Ptr (α : Type) : Type := Addr

@[extern c inline "0"]
unsafe axiom Ptr.null {α : Type} : Ptr α
unsafe instance : Inhabited (Ptr α) := ⟨Ptr.null⟩

unsafe constant Ptr.ofAddr (addr : Addr) : Ptr α
-- error: (kernel) invalid declaration, it uses unsafe declaration 'instInhabitedPtr'

Why can't unsafe constants use unsafe Inhabited instances to believe the resulting type is inhabited?

[Wojciech Nawrocki]

There are other issues with unsafe instances. For example, it doesn't seem possible to use them in initialize blocks unless you modify the initialize macro to emit an unsafe def.

[Mac]

Wojciech Nawrocki said:

For example, it doesn't seem possible to use them in initialize blocks unless you modify the initialize macro to emit an unsafe def.

That makes more sense. A normal def (which initialize produces) can't use unsafe definitions/instances/constants. Only unsafe ones can. Though, admittedly, it would be desirable for initialize blocks to support declModifiers themselves.

[Wojciech Nawrocki]

My rough guess is there's a missing check for unsafety or something like it in add_opaque but I wouldn't wanna touch the kernel to add it :) You can also do unsafe def Ptr.ofAddr (addr : Addr) : Ptr a := arbitrary and maybe even figure out how to put opaque reducibility on that.