Add a safe wrapper around `ptrEq`

We want to use pointer equality as a performance optimization. For example, as a first check in DecidableEq instances: if the two arguments are pointer-equal, then we can immediately return isTrue. However ptrEq is unsafe, and every time it is used via implementedBy we potentially introduce bugs. Therefore we want a safe wrapper around ptrEq. There are several issues to consider:

1. ptrEq is not compatible with equality. ptrEq a a will always return true, but ptrEq a b may return false even if a = b. This is easy to address by either using a CPS-style definition or wrapping the result in a quotient like safePtrEq (a b : α) : Squash Bool.
2. We need some information about the result of ptrEq beyond the fact that it is a Boolean, so that we can conclude a = b if ptrEq a b returns true. This is also straightforward to encode, e.g. with safePtrEq (a b : α) : Squash { b : Bool // b → a = b }.
3. In general, ptrEq a b does not imply a = b.

Number (3) causes the withPtrEq function in core to be unsafe:

withPtrEq {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool

The problem is that it is very easy to construct provably different Lean terms that evaluate to identical VM objects. In hindsight, this is an obvious effect of erasure and common subexpression elimination. The following are some concrete examples:

@[simp] theorem Bool_ne_Empty : Bool ≠ Empty :=
  (Empty.rec <| · ▸ true)

-- 1) Types are erased, so ptrEq will always claim that they are equal:
def problem1 := withPtrEq Bool Empty (fun _ => false) (by simp)
#reduce problem1 -- false
#eval problem1 -- true

-- 2) This works even if we're not directly comparing types, but also when
-- they're nested in a heap value (due to CSE).
def problem2 := withPtrEq (Bool, 1) (Empty, 1) (fun _ => false) (by simp)
#reduce problem2 -- false
#eval problem2 -- true

Potential fixes:

1. Cripple the compiler to never do CSE after erasure, and have withPtrEq return false if one of the arguments is box(0). (Only mentioned for completeness, I don't think this is a good idea.)
2. Add a type class class InjectiveVMRepr (α : Sort u) : Prop where private mk ::, auto-generate instances for inductives and structures that are safe to compare with ptrEq, and add an additional [InjectiveVMRepr α] argument to withPtrEq. Unfortunately it is not possible to use unsafe for such Rust-style "marker traits", because we need to prove Nonempty (InjectiveVMRepr α) to define the safe instances.
3. Add a type class SafePtrEq with a safePtrEq (a b : α) : Squash { b : Bool // b → a = b } operation. This has the downside of increasing the compiled code size (due to monomorphization), and we can't define instances like [SafePtrEq α] → SafePtrEq (Array α).