Decide on memory representation of opaque type definitions

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

Start with the opaque-type and FFI examples in the issue, then read the linked Zulip discussion and pull-request discussion. Determine the intended runtime representation and whether the NonemptyType default is safe for external objects; done means the representation policy is decided and any required instance change is specified.