Draft: Add utilities to use unsafe equality proofs

Add utilities to use unsafe equality proofs

It's generally best practice to limit unsafe equalities as much as possible, to avoid mistakes. A good way to do that is to use unsafeEqualityProof to produce fake evidence of the smallest equality needed. For example, if you know that A and P are sufficiently similar and you need to coerce [A] -> B -> C to [P] -> B -> C, it's much nicer to explicitly introduce fake evidence that A ~ P than to use unsafeCoerce and hope you aren't accidentally coercing some unrelated things elsewhere in the type.

Unfortunately, actually using the limited fake evidence can be tricky. You might think you could write something like

cabc :: ([A] -> B -> C) -> [P] -> B -> C
cabc f = case unsafeEqualityProof @A @P of
  UnsafeRefl -> f

But this won't work! When type checking the case branch, GHC rejects A ~ P without even noticing that there's evidence for it available. This means that more explicit utilities are needed to manipulate unsafe equalities. One simple option would be to offer just a single function

unsafeEqualityProofToEquality :: UnsafeEquality a b -> a :~: b
unsafeEqualityProofToEquality UnsafeRefl = Refl

Then people could use the utilities in Data.Type.Equality to manipulate the resulting equality. But it seems to me that it's much nicer to help users keep equality proofs obviously unsafe right up to the point of use, to avoid a sort of "equality blindness". This commit adds versions of the various equality proof functions in Data.Type.Equality for UnsafeEquality, along with a few more for convenience inspired by the Agda standard library.