Decide on memory representation of opaque type definitions

[gebner]

In short, the question is whether the following cast is safe:

opaque Foo : Type := Bool
unsafe def foo : Foo := unsafeCast "123"

This pattern is used extensively with FFI types:

opaque Foo : NonemptyType.{0} -- := ⟨Unit, inferInstance⟩
@[extern "lean_func"] opaque func : Nat → Foo.1

The function lean_func then returns an external object, so the type Foo.1 will have an external object as a runtime value. This is only safe if Foo.1 has a different runtime representation than Unit. If the code generator reduces the opaque definition Foo.1 to Unit, then this could be unsafe.

If we decide that this usage of (default : NonemptyType) is unsafe for FFI types, then we should change the Inhabited NonemptyType instance to remove the footgun.

There are also cases where we might want to unfold opaque type definitions, for example when using opaque to hide implementation details:

structure BarApi where
  α : Type
  frob : α → α → α
  zero : α
  frob_comm : frob a b = frob b a

opaque barApi : BarApi := {
  α := UInt8
  zero := 0
  frob := (· &&& ·)
  frob_comm := by simp
}

def someBar : barApi.α := barApi.zero -- should compile to someBar : u8

See https://leanprover.zulipchat.com/#narrow/stream/147302-lean4-dev/topic/NonScalar.20and.20PNonScalar/near/295689656 and https://github.com/leanprover/lean4/pull/1528#discussion_r956714722

[gebner]

We could define PNonScalar using choice. This 1) makes it explicitly an unspecified type, 2) works with both the old and new compiler (being erased to the any type as Classical.choice is not a type former):

private opaque PNonScalarSpec : NonemptyType.{u} :=
  -- This is essentially an eta-expansion of `Classical.choice ⟨⟨PUnit, inferInstance⟩⟩`
  ⟨id (Classical.epsilon Nonempty), Classical.epsilon_spec ⟨PUnit, by infer_instance⟩⟩

def PNonScalar : Type u := PNonScalarSpec.1
instance : Nonempty PNonScalar.{u} := PNonScalarSpec.2

instance : Inhabited NonemptyType.{u} where
  default := ⟨PNonScalar, inferInstance⟩