Re-implement unsafe coercions in terms of unsafe equality proofs

(Commit message written by Omer, most of the code is written by Simon
and Richard)

See Note [Implementing unsafeCoerce] for how unsafe equality proofs and
the new unsafeCoerce# are implemented.

New notes added:

- [Checking for levity polymorphism] in CoreLint.hs
- [Implementing unsafeCoerce] in base/Unsafe/Coerce.hs
- [Patching magic definitions] in Desugar.hs
- [Wiring in unsafeCoerce#] in Desugar.hs

Only breaking change in this patch is unsafeCoerce# is not exported from
GHC.Exts, instead of GHC.Prim.

Fixes #17443
Fixes #16893

NoFib
-----

--------------------------------------------------------------------------------
        Program           Size    Allocs    Instrs     Reads    Writes
--------------------------------------------------------------------------------
             CS          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
            CSD          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
             FS          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
              S          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
             VS          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
            VSD          -0.1%      0.0%     -0.0%     -0.0%     -0.1%
            VSM          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
           anna          -0.0%      0.0%     -0.0%     -0.0%     -0.0%
           ansi          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
           atom          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
         awards          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
         banner          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
     bernouilli          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
   binary-trees          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
          boyer          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
         boyer2          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
           bspt          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
      cacheprof          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
       calendar          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
       cichelli          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
        circsim          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
       clausify          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
  comp_lab_zift          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
       compress          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
      compress2          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
    constraints          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
   cryptarithm1          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
   cryptarithm2          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
            cse          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
   digits-of-e1          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
   digits-of-e2          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
         dom-lt          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
          eliza          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
          event          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
    exact-reals          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
         exp3_8          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
         expert          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
 fannkuch-redux          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
          fasta          -0.1%      0.0%     -0.5%     -0.3%     -0.4%
            fem          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
            fft          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
           fft2          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
       fibheaps          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
           fish          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
          fluid          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
         fulsom          -0.1%      0.0%     +0.0%     +0.0%     +0.0%
         gamteb          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
            gcd          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
    gen_regexps          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
         genfft          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
             gg          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
           grep          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
         hidden          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
            hpg          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
            ida          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
          infer          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
        integer          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
      integrate          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
   k-nucleotide          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
          kahan          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
        knights          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
         lambda          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
     last-piece          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
           lcss          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
           life          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
           lift          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
         linear          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
      listcompr          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
       listcopy          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
       maillist          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
         mandel          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
        mandel2          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
           mate          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
        minimax          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
        mkhprog          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
     multiplier          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
         n-body          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
       nucleic2          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
           para          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
      paraffins          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
         parser          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
        parstof          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
            pic          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
       pidigits          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
          power          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
         pretty          -0.1%      0.0%     -0.1%     -0.1%     -0.1%
         primes          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
      primetest          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
         prolog          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
         puzzle          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
         queens          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
        reptile          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
reverse-complem          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
        rewrite          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
           rfib          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
            rsa          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
            scc          -0.1%      0.0%     -0.1%     -0.1%     -0.1%
          sched          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
            scs          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
         simple          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
          solid          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
        sorting          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
  spectral-norm          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
         sphere          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
         symalg          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
            tak          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
      transform          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
       treejoin          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
      typecheck          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
        veritas          -0.0%      0.0%     -0.0%     -0.0%     -0.0%
           wang          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
      wave4main          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
   wheel-sieve1          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
   wheel-sieve2          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
           x2n1          -0.1%      0.0%     -0.0%     -0.0%     -0.0%
--------------------------------------------------------------------------------
            Min          -0.1%      0.0%     -0.5%     -0.3%     -0.4%
            Max          -0.0%      0.0%     +0.0%     +0.0%     +0.0%
 Geometric Mean          -0.1%     -0.0%     -0.0%     -0.0%     -0.0%

Test changes
------------

- break006 is marked as broken, see #17833
- The compiler allocates less when building T14683 (an unsafeCoerce#-
  heavy happy-generated code) on 64-platforms. Allocates more on 32-bit
  platforms.
- Rest of the increases are tiny amounts (still enough to pass the
  threshold) in micro-benchmarks. I briefly looked at each one in a
  profiling build: most of the increased allocations seem to be because
  of random changes in the generated code.

Metric Decrease:
    T14683

Metric Increase:
    T12150
    T12234
    T12425
    T13035
    T14683
    T5837
    T6048

Co-Authored-By: Richard Eisenberg <rae@cs.brynmawr.edu>
Co-Authored-By: Ömer Sinan Ağacan <omeragacan@gmail.com>

9 files changed, 324 insertions, 67 deletions

diff --git a/libraries/base/Data/Typeable/Internal.hs b/libraries/base/Data/Typeable/Internal.hs
index 6135487e6e..4ccbd5fd52 100644
--- a/libraries/base/Data/Typeable/Internal.hs
+++ b/libraries/base/Data/Typeable/Internal.hs
@@ -565,7 +565,7 @@ typeRepTyCon (TrFun {})               = typeRepTyCon $ typeRep @(->)
 eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2).
              TypeRep a -> TypeRep b -> Maybe (a :~~: b)
 eqTypeRep a b
-  | sameTypeRep a b = Just (unsafeCoerce# HRefl)
+  | sameTypeRep a b = Just (unsafeCoerce HRefl)
   | otherwise       = Nothing
 -- We want GHC to inline eqTypeRep to get rid of the Maybe
 -- in the usual case that it is scrutinized immediately. We
diff --git a/libraries/base/GHC/Base.hs b/libraries/base/GHC/Base.hs
index 9e64cf50d1..65ec3ea1b7 100644
--- a/libraries/base/GHC/Base.hs
+++ b/libraries/base/GHC/Base.hs
@@ -1300,6 +1300,7 @@ The rules for map work like this.
 --   http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/coercible.pdf
 
 {-# RULES "map/coerce" [1] map coerce = coerce #-}
+-- See Note [Getting the map/coerce RULE to work] in CoreOpt
 
 ----------------------------------------------
 --              append
diff --git a/libraries/base/GHC/Conc/Sync.hs b/libraries/base/GHC/Conc/Sync.hs
index de8ca8e5a0..d6ffbc2de9 100644
--- a/libraries/base/GHC/Conc/Sync.hs
+++ b/libraries/base/GHC/Conc/Sync.hs
@@ -117,6 +117,8 @@ import GHC.Show         ( Show(..), showParen, showString )
 import GHC.Stable       ( StablePtr(..) )
 import GHC.Weak
 
+import Unsafe.Coerce    ( unsafeCoerce# )
+
 infixr 0 `par`, `pseq`
 
 -----------------------------------------------------------------------------
@@ -621,6 +623,9 @@ data PrimMVar
 newStablePtrPrimMVar :: MVar () -> IO (StablePtr PrimMVar)
 newStablePtrPrimMVar (MVar m) = IO $ \s0 ->
   case makeStablePtr# (unsafeCoerce# m :: PrimMVar) s0 of
+    -- Coerce unlifted  m :: MVar# RealWorld ()
+    --     to lifted    PrimMVar
+    -- apparently because mkStablePtr is not levity-polymorphic
     (# s1, sp #) -> (# s1, StablePtr sp #)
 
 -----------------------------------------------------------------------------
diff --git a/libraries/base/GHC/Conc/Windows.hs b/libraries/base/GHC/Conc/Windows.hs
index ed5e0452a0..53f22d6d50 100644
--- a/libraries/base/GHC/Conc/Windows.hs
+++ b/libraries/base/GHC/Conc/Windows.hs
@@ -52,6 +52,7 @@ import GHC.Real (div, fromIntegral)
 import GHC.Show (Show)
 import GHC.Word (Word32, Word64)
 import GHC.Windows
+import Unsafe.Coerce ( unsafeCoerceUnlifted )
 
 #if defined(mingw32_HOST_OS)
 # if defined(i386_HOST_ARCH)
@@ -93,11 +94,11 @@ asyncDoProc (FunPtr proc) (Ptr param) =
 -- this better be a pinned byte array!
 asyncReadBA :: Int -> Int -> Int -> Int -> MutableByteArray# RealWorld -> IO (Int,Int)
 asyncReadBA fd isSock len off bufB =
-  asyncRead fd isSock len ((Ptr (byteArrayContents# (unsafeCoerce# bufB))) `plusPtr` off)
+  asyncRead fd isSock len ((Ptr (byteArrayContents# (unsafeCoerceUnlifted bufB))) `plusPtr` off)
 
 asyncWriteBA :: Int -> Int -> Int -> Int -> MutableByteArray# RealWorld -> IO (Int,Int)
 asyncWriteBA fd isSock len off bufB =
-  asyncWrite fd isSock len ((Ptr (byteArrayContents# (unsafeCoerce# bufB))) `plusPtr` off)
+  asyncWrite fd isSock len ((Ptr (byteArrayContents# (unsafeCoerceUnlifted bufB))) `plusPtr` off)
 
 -- ----------------------------------------------------------------------------
 -- Threaded RTS implementation of threadDelay
diff --git a/libraries/base/GHC/Exts.hs b/libraries/base/GHC/Exts.hs
index 9bce21cd27..b5c0361de8 100755
--- a/libraries/base/GHC/Exts.hs
+++ b/libraries/base/GHC/Exts.hs
@@ -68,6 +68,9 @@ module GHC.Exts
         -- @since 4.7.0.0
         Data.Coerce.coerce, Data.Coerce.Coercible,
 
+        -- * Very unsafe coercion
+        unsafeCoerce#,
+
         -- * Equality
         type (~~),
 
@@ -112,6 +115,7 @@ import Data.Data
 import Data.Ord
 import Data.Version ( Version(..), makeVersion )
 import qualified Debug.Trace
+import Unsafe.Coerce ( unsafeCoerce# ) -- just for re-export
 
 import Control.Applicative (ZipList(..))
 
diff --git a/libraries/base/GHC/ForeignPtr.hs b/libraries/base/GHC/ForeignPtr.hs
index 5eb5f14870..92aef540d1 100644
--- a/libraries/base/GHC/ForeignPtr.hs
+++ b/libraries/base/GHC/ForeignPtr.hs
@@ -55,6 +55,8 @@ import GHC.IORef
 import GHC.STRef        ( STRef(..) )
 import GHC.Ptr          ( Ptr(..), FunPtr(..) )
 
+import Unsafe.Coerce    ( unsafeCoerce, unsafeCoerceUnlifted )
+
 -- |The type 'ForeignPtr' represents references to objects that are
 -- maintained in a foreign language, i.e., that are not part of the
 -- data structures usually managed by the Haskell storage manager.
@@ -165,7 +167,7 @@ mallocForeignPtr = doMalloc undefined
           r <- newIORef NoFinalizers
           IO $ \s ->
             case newAlignedPinnedByteArray# size align s of { (# s', mbarr# #) ->
-             (# s', ForeignPtr (byteArrayContents# (unsafeCoerce# mbarr#))
+             (# s', ForeignPtr (byteArrayContents# (unsafeCoerceUnlifted mbarr#))
                                (MallocPtr mbarr# r) #)
             }
             where !(I# size)  = sizeOf a
@@ -180,7 +182,7 @@ mallocForeignPtrBytes (I# size) = do
   r <- newIORef NoFinalizers
   IO $ \s ->
      case newPinnedByteArray# size s      of { (# s', mbarr# #) ->
-       (# s', ForeignPtr (byteArrayContents# (unsafeCoerce# mbarr#))
+       (# s', ForeignPtr (byteArrayContents# (unsafeCoerceUnlifted mbarr#))
                          (MallocPtr mbarr# r) #)
      }
 
@@ -194,7 +196,7 @@ mallocForeignPtrAlignedBytes (I# size) (I# align) = do
   r <- newIORef NoFinalizers
   IO $ \s ->
      case newAlignedPinnedByteArray# size align s of { (# s', mbarr# #) ->
-       (# s', ForeignPtr (byteArrayContents# (unsafeCoerce# mbarr#))
+       (# s', ForeignPtr (byteArrayContents# (unsafeCoerceUnlifted mbarr#))
                          (MallocPtr mbarr# r) #)
      }
 
@@ -218,7 +220,7 @@ mallocPlainForeignPtr = doMalloc undefined
           | I# size < 0 = errorWithoutStackTrace "mallocForeignPtr: size must be >= 0"
           | otherwise = IO $ \s ->
             case newAlignedPinnedByteArray# size align s of { (# s', mbarr# #) ->
-             (# s', ForeignPtr (byteArrayContents# (unsafeCoerce# mbarr#))
+             (# s', ForeignPtr (byteArrayContents# (unsafeCoerceUnlifted mbarr#))
                                (PlainPtr mbarr#) #)
             }
             where !(I# size)  = sizeOf a
@@ -233,7 +235,7 @@ mallocPlainForeignPtrBytes size | size < 0 =
   errorWithoutStackTrace "mallocPlainForeignPtrBytes: size must be >= 0"
 mallocPlainForeignPtrBytes (I# size) = IO $ \s ->
     case newPinnedByteArray# size s      of { (# s', mbarr# #) ->
-       (# s', ForeignPtr (byteArrayContents# (unsafeCoerce# mbarr#))
+       (# s', ForeignPtr (byteArrayContents# (unsafeCoerceUnlifted mbarr#))
                          (PlainPtr mbarr#) #)
      }
 
@@ -246,7 +248,7 @@ mallocPlainForeignPtrAlignedBytes size _align | size < 0 =
   errorWithoutStackTrace "mallocPlainForeignPtrAlignedBytes: size must be >= 0"
 mallocPlainForeignPtrAlignedBytes (I# size) (I# align) = IO $ \s ->
     case newAlignedPinnedByteArray# size align s of { (# s', mbarr# #) ->
-       (# s', ForeignPtr (byteArrayContents# (unsafeCoerce# mbarr#))
+       (# s', ForeignPtr (byteArrayContents# (unsafeCoerceUnlifted mbarr#))
                          (PlainPtr mbarr#) #)
      }
 
@@ -350,7 +352,7 @@ ensureCFinalizerWeak ref@(IORef (STRef r#)) value = do
       CFinalizers weak -> return (MyWeak weak)
       HaskellFinalizers{} -> noMixingError
       NoFinalizers -> IO $ \s ->
-          case mkWeakNoFinalizer# r# (unsafeCoerce# value) s of { (# s1, w #) ->
+          case mkWeakNoFinalizer# r# (unsafeCoerce value) s of { (# s1, w #) ->
              -- See Note [MallocPtr finalizers] (#10904)
           case atomicModifyMutVar2# r# (update w) s1 of
               { (# s2, _, (_, (weak, needKill )) #) ->
@@ -463,4 +465,3 @@ finalizeForeignPtr (ForeignPtr _ foreignPtr) = foreignPtrFinalizer refFinalizers
                         (MallocPtr     _ ref) -> ref
                         PlainPtr _            ->
                             errorWithoutStackTrace "finalizeForeignPtr PlainPtr"
-
diff --git a/libraries/base/GHC/IO.hs b/libraries/base/GHC/IO.hs
index 55291cca4b..ee293112a6 100644
--- a/libraries/base/GHC/IO.hs
+++ b/libraries/base/GHC/IO.hs
@@ -47,6 +47,7 @@ import GHC.ST
 import GHC.Exception
 import GHC.Show
 import GHC.IO.Unsafe
+import Unsafe.Coerce ( unsafeCoerce )
 
 import {-# SOURCE #-} GHC.IO.Exception ( userError, IOError )
 
@@ -99,7 +100,7 @@ ioToST (IO m) = (ST m)
 -- This relies on 'IO' and 'ST' having the same representation modulo the
 -- constraint on the state thread type parameter.
 unsafeIOToST        :: IO a -> ST s a
-unsafeIOToST (IO io) = ST $ \ s -> (unsafeCoerce# io) s
+unsafeIOToST (IO io) = ST $ \ s -> (unsafeCoerce io) s
 
 -- | Convert an 'ST' action to an 'IO' action.
 -- This relies on 'IO' and 'ST' having the same representation modulo the
@@ -108,7 +109,7 @@ unsafeIOToST (IO io) = ST $ \ s -> (unsafeCoerce# io) s
 -- For an example demonstrating why this is unsafe, see
 -- https://mail.haskell.org/pipermail/haskell-cafe/2009-April/060719.html
 unsafeSTToIO :: ST s a -> IO a
-unsafeSTToIO (ST m) = IO (unsafeCoerce# m)
+unsafeSTToIO (ST m) = IO (unsafeCoerce m)
 
 -- -----------------------------------------------------------------------------
 -- | File and directory names are values of type 'String', whose precise
diff --git a/libraries/base/GHC/Stable.hs b/libraries/base/GHC/Stable.hs
index 1ea0d6d166..3cd26302f4 100644
--- a/libraries/base/GHC/Stable.hs
+++ b/libraries/base/GHC/Stable.hs
@@ -31,6 +31,8 @@ module GHC.Stable (
 import GHC.Ptr
 import GHC.Base
 
+import Unsafe.Coerce ( unsafeCoerceAddr )
+
 -----------------------------------------------------------------------------
 -- Stable Pointers
 
@@ -85,7 +87,7 @@ foreign import ccall unsafe "hs_free_stable_ptr" freeStablePtr :: StablePtr a ->
 -- undefined behaviour.
 --
 castStablePtrToPtr :: StablePtr a -> Ptr ()
-castStablePtrToPtr (StablePtr s) = Ptr (unsafeCoerce# s)
+castStablePtrToPtr (StablePtr s) = Ptr (unsafeCoerceAddr s)
 
 
 -- |
@@ -99,7 +101,7 @@ castStablePtrToPtr (StablePtr s) = Ptr (unsafeCoerce# s)
 -- 'castStablePtrToPtr'.
 --
 castPtrToStablePtr :: Ptr () -> StablePtr a
-castPtrToStablePtr (Ptr a) = StablePtr (unsafeCoerce# a)
+castPtrToStablePtr (Ptr a) = StablePtr (unsafeCoerceAddr a)
 
 -- | @since 2.01
 instance Eq (StablePtr a) where
diff --git a/libraries/base/Unsafe/Coerce.hs b/libraries/base/Unsafe/Coerce.hs
index 86e2d9fd65..bad2e5bea6 100644
--- a/libraries/base/Unsafe/Coerce.hs
+++ b/libraries/base/Unsafe/Coerce.hs
@@ -1,62 +1,304 @@
-{-# LANGUAGE Unsafe #-}
-{-# LANGUAGE NoImplicitPrelude, MagicHash #-}
+-- We don't to strictness analysis on this file to avoid turning loopy unsafe
+-- equality terms below to actual loops. Details in (U5) of
+-- Note [Implementing unsafeCoerce]
+{-# OPTIONS_GHC -fno-strictness #-}
 
------------------------------------------------------------------------------
--- |
--- Module      :  Unsafe.Coerce
--- Copyright   :  Malcolm Wallace 2006
--- License     :  BSD-style (see the LICENSE file in the distribution)
+{-# LANGUAGE Unsafe, NoImplicitPrelude, MagicHash, GADTs, TypeApplications,
+             ScopedTypeVariables, TypeOperators, KindSignatures, PolyKinds,
+             StandaloneKindSignatures, DataKinds #-}
+
+module Unsafe.Coerce
+  ( unsafeCoerce, unsafeCoerceUnlifted, unsafeCoerceAddr
+  , unsafeEqualityProof
+  , UnsafeEquality (..)
+  , unsafeCoerce#
+  ) where
+
+import GHC.Arr (amap) -- For amap/unsafeCoerce rule
+import GHC.Base
+import GHC.Integer () -- See Note [Depend on GHC.Integer] in GHC.Base
+import GHC.Natural () -- See Note [Depend on GHC.Natural] in GHC.Base
+
+import GHC.Types
+
+{- Note [Implementing unsafeCoerce]
+
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The implementation of unsafeCoerce is surprisingly subtle.
+This Note describes the moving parts.  You will find more
+background in MR !1869 and ticket #16893.
+
+The key challenge is this.  Suppose we have
+   case sameTypeRep t1 t2 of
+      False -> blah2
+      True  -> ...(case (x |> UnsafeCo @t1 @t2) of { K -> blah })...
+
+The programmer thinks that the unsafeCoerce from 't1' to 't2' is safe,
+because it is justified by a runtime test (sameTypeRep t1 t2).
+It used to compile to a cast, with a magical 'UnsafeCo' coercion.
+
+But alas, nothing then stops GHC floating that call to unsafeCoerce
+outwards so we get
+   case (x |> UnsafeCo @t1 @t2) of
+     K -> case sameTypeRep t1 t2 of
+             False -> blah2
+             True  -> ...blah...
+
+and this is utterly wrong, because the unsafeCoerce is being performed
+before the dynamic test. This is exactly the setup in #16893.
+
+The solution is this:
+
+* In the library Unsafe.Coerce we define:
+
+     unsafeEqualityProof :: forall k (a :: k) (b :: k).
+                            UnsafeEquality a b
+
+* It uses a GADT, Unsafe.Coerce.UnsafeEquality, that is exactly like :~:
+
+    data UnsafeEquality (a :: k) (b :: k) where
+      UnsafeRefl :: UnsafeEquality a a
+
+* We can now define Unsafe.Coerce.unsafeCoerce very simply:
+
+   unsafeCoerce :: forall (a :: Type) (b :: Type) . a -> b
+   unsafeCoerce x = case unsafeEqualityProof @a @b of
+                      UnsafeRefl -> x
+
+  There is nothing special about unsafeCoerce; it is an
+  ordinary library definition, and can be freely inlined.
+
+Now our bad case can't happen.  We'll have
+     case unsafeEqualityProof @t1 @t2 of
+        UnsafeRefl (co :: t1 ~ t2) -> ....(x |> co)....
+
+and the (x |> co) mentions the evidence 'co', which prevents it
+floating.
+
+But what stops the whole (case unsafeEqualityProof of ...) from
+floating?  Answer: we never float a case on a redex that can fail
+outside a conditional.  See Primop.hs,
+Note [Transformations affected by can_fail and has_side_effects].
+And unsafeEqualityProof (being opaque) is definitely treated as
+can-fail.
+
+While unsafeCoerce is a perfectly ordinary function that needs no
+special treatment, Unsafe.Coerce.unsafeEqualityProof is magical, in
+several ways
+
+(U1) unsafeEqualityProof is /never/ inlined.
+
+(U2) In CoreToStg.coreToStg, we transform
+       case unsafeEqualityProof of UnsafeRefl -> blah
+      ==>
+       blah
+
+     This eliminates the overhead of evaluating the unsafe
+     equality proof.
+
+     Any /other/ occurrence of unsafeEqualityProof is left alone.
+     For example you could write
+         f :: UnsafeEquality a b -> blah
+         f eq_proof = case eq_proof of UnsafeRefl -> ...
+    (Nothing special about that.)  In a call, you might write
+         f unsafeEqualityProof
+
+    and we'll generate code simply by passing the top-level
+    unsafeEqualityProof to f.  As (U5) says, it is implemented as
+    UnsafeRefl so all is good.
+
+(U3) In GHC.CoreToStg.Prep.cpeRhsE, if we see
+       let x = case unsafeEqualityProof ... of
+                 UnsafeRefl -> K e
+       in ...
+
+     there is a danger that we'll go to
+        let x = case unsafeEqualityProof ... of
+                  UnsafeRefl -> let a = e in K a
+        in ...
+
+     and produce a thunk even after discarding the unsafeEqualityProof.
+     So instead we float out the case to give
+        case unsafeEqualityProof ... of { UnsafeRefl ->
+        let a = K e
+            x = K a
+        in ...
+     Flaoting the case is OK here, even though it broardens the
+     scope, becuase we are done with simplification.
+
+(U4) GHC.CoreToStg.Prep.cpeExprIsTrivial anticipated the
+     upcoming discard of unsafeEqualityProof.
+
+(U5) The definition of unsafeEqualityProof in Unsafe.Coerce
+     looks very strange:
+        unsafeEqualityProof = case unsafeEqualityProof @a @b of
+                                 UnsafeRefl -> UnsafeRefl
+
+     It looks recursive!  But the above-mentioned CoreToStg
+     transform will change it to
+        unsafeEqualityProof = UnsafeRefl
+     And that is exactly the code we want!  For example, if we say
+        f unsafeEqualityProof
+     we want to pass an UnsafeRefl constructor to f.
+
+     We turn off strictness analysis in this module, otherwise
+     the strictness analyser will mark unsafeEqualityProof as
+     bottom, which is utterly wrong.
+
+(U6) The UnsafeEquality data type is also special in one way.
+     Consider this piece of Core
+        case unsafeEqualityProof @Int @Bool of
+           UnsafeRefl (g :: Int ~# Bool) -> ...g...
+
+     The simplifier normally eliminates case alternatives with
+     contradicatory GADT data constructors; here we bring into
+     scope evidence (g :: Int~Bool).  But we do not want to
+     eliminate this particular alternative!  So we put a special
+     case into DataCon.dataConCannotMatch to account for this.
+
+(U7) We add a built-in RULE
+       unsafeEqualityProof k t t  ==>  UnsafeRefl (Refl t)
+     to simplify the ase when the two tpyes are equal.
+
+(U8) The is a super-magic RULE in GHC.base
+         map cocerce = coerce
+     (see Note [Getting the map/coerce RULE to work] in CoreOpt)
+     But it's all about turning coerce into a cast, and unsafeCoerce
+     no longer does that.  So we need a separate map/unsafeCoerce
+     RULE, in this module.
+
+There are yet more wrinkles
+
+(U9) unsafeCoerce works only over types of kind `Type`.
+     But what about other types?  In Unsafe.Coerce we also define
+
+      unsafeCoerceUnlifted :: forall (a :: TYPE UnliftedRep)
+                                     (b :: TYPE UnliftedRep).
+                              a -> b
+      unsafeCoerceUnlifted x
+        = case unsafeEqualityProof @a @b of
+              UnsafeRefl -> x
+
+     and similarly for unsafeCoerceAddr, unsafeCoerceInt, etc.
+
+(U10) We also want a levity-polymorphic unsafeCoerce#:
+
+       unsafeCoerce# :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
+                        (a :: TYPE r1) (b :: TYPE r2).
+                        a -> b
+
+      This is even more dangerous, because it converts between two types
+      *with different runtime representations*!!  Our goal is to deprecate
+      it entirely.  But for now we want it.
+
+      But having it is hard!  It is defined by a kind of stub in Unsafe.Coerce,
+      and overwritten by the desugarer.  See Note [Wiring in unsafeCoerce#]
+      in Desugar.  Here's the code for it
+        unsafeCoerce# x = case unsafeEqualityProof @r1 @r2 of UnsafeRefl ->
+                          case unsafeEqualityProof @a  @b  of UnsafeRefl ->
+                          x
+      Notice that we can define this kind-/heterogeneous/ function by calling
+      the kind-/homogeneous/ unsafeEqualityProof twice.
+
+      See Note [Wiring in unsafeCoerce#] in Desugar.
+
+(U11) We must also be careful to discard unsafeEqualityProof in the
+      bytecode generator; see ByteCodeGen.bcView.  Here we don't really
+      care about fast execution, but (annoyingly) we /do/ care about the
+      GHCi debugger, and GHCi itself uses unsafeCoerce.
+
+      Moreover, in TcRnDriver.tcGhciStmts we use unsafeCoerce#, rather
+      than the more kosher unsafeCoerce, becuase (with -O0) the latter
+      may not be inlined.
+
+      Sigh
+-}
+
+-- | This type is treated magically within GHC. Any pattern match of the
+-- form @case unsafeEqualityProof of UnsafeRefl -> body@ gets transformed just into @body@.
+-- This is ill-typed, but the transformation takes place after type-checking is
+-- complete. It is used to implement 'unsafeCoerce'. You probably don't want to
+-- use 'UnsafeRefl' in an expression, but you might conceivably want to pattern-match
+-- on it. Use 'unsafeEqualityProof' to create one of these.
+data UnsafeEquality a b where
+  UnsafeRefl :: UnsafeEquality a a
+
+{-# NOINLINE unsafeEqualityProof #-}
+unsafeEqualityProof :: forall a b . UnsafeEquality a b
+-- See (U5) of Note [Implementing unsafeCoerce]
+unsafeEqualityProof = case unsafeEqualityProof @a @b of UnsafeRefl -> UnsafeRefl
+
+{-# INLINE [1] unsafeCoerce #-}
+-- The INLINE will almost certainly happen automatically, but it's almost
+-- certain to generate (slightly) better code, so let's do it.  For example
+--
+--   case (unsafeCoerce blah) of ...
+--
+-- will turn into
+--
+--   case unsafeEqualityProof of UnsafeRefl -> case blah of ...
+--
+-- which is definitely better.
+
+-- | Coerce a value from one type to another, bypassing the type-checker.
+--
+-- There are several legitimate ways to use 'unsafeCoerce':
 --
--- Maintainer  :  libraries@haskell.org
--- Stability   :  experimental
--- Portability :  portable
+--   1. To coerce e.g. @Int@ to @HValue@, put it in a list of @HValue@,
+--      and then later coerce it back to @Int@ before using it.
 --
--- The highly unsafe primitive 'unsafeCoerce' converts a value from any
--- type to any other type.  Needless to say, if you use this function,
--- it is your responsibility to ensure that the old and new types have
--- identical internal representations, in order to prevent runtime corruption.
+--   2. To produce e.g. @(a+b) :~: (b+a)@ from @unsafeCoerce Refl@.
+--      Here the two sides really are the same type -- so nothing unsafe is happening
+--      -- but GHC is not clever enough to see it.
 --
--- The types for which 'unsafeCoerce' is representation-safe may differ
--- from compiler to compiler (and version to version).
+--   3. In @Data.Typeable@ we have
 --
---   * Documentation for correct usage in GHC will be found under
---     'unsafeCoerce#' in "GHC.Base" (around which 'unsafeCoerce' is just a
---     trivial wrapper).
+--      @
+--        eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2).
+--                     TypeRep a -> TypeRep b -> Maybe (a :~~: b)
+--        eqTypeRep a b
+--          | sameTypeRep a b = Just (unsafeCoerce HRefl)
+--          | otherwise       = Nothing
+--      @
 --
---   * In nhc98, the only representation-safe coercions are between
---     'Prelude.Enum' types with the same range (e.g. 'Prelude.Int',
---     'Data.Int.Int32', 'Prelude.Char', 'Data.Word.Word32'), or between a
---     newtype and the type that it wraps.
+--      Here again, the @unsafeCoerce HRefl@ is safe, because the two types really
+--      are the same  -- but the proof of that relies on the complex, trusted
+--      implementation of @Typeable@.
 --
------------------------------------------------------------------------------
+--   4. The "reflection trick", which takes advantanage of the fact that in
+--      @class C a where { op :: ty }@, we can safely coerce between @C a@ and @ty@
+--      (which have different kinds!) because it's really just a newtype.
+--      Note: there is /no guarantee, at all/ that this behavior will be supported
+--      into perpetuity.
+unsafeCoerce :: forall (a :: Type) (b :: Type) . a -> b
+unsafeCoerce x = case unsafeEqualityProof @a @b of UnsafeRefl -> x
 
-module Unsafe.Coerce (unsafeCoerce) where
+unsafeCoerceUnlifted :: forall (a :: TYPE 'UnliftedRep) (b :: TYPE 'UnliftedRep) . a -> b
+-- Kind-homogeneous, but levity monomorphic (TYPE UnliftedRep)
+unsafeCoerceUnlifted x = case unsafeEqualityProof @a @b of UnsafeRefl -> x
 
-import GHC.Integer () -- See Note [Depend on GHC.Integer] in GHC.Base
-import GHC.Natural () -- See Note [Depend on GHC.Natural] in GHC.Base
-import GHC.Prim (unsafeCoerce#)
-
-local_id :: a -> a
-local_id x = x   -- See Note [Mega-hack for coerce]
-
-{- Note [Mega-hack for coerce]
-
-If we just say
-  unsafeCoerce x = unsafeCoerce# x
-then the simple-optimiser that the desugarer runs will eta-reduce to
-  unsafeCoerce :: forall (a:*) (b:*). a -> b
-  unsafeCoerce = unsafeCoerce#
-But we shouldn't be calling unsafeCoerce# in a higher
-order way; it has a compulsory unfolding
-   unsafeCoerce# a b x = x |> UnsafeCo a b
-and we really rely on it being inlined pronto. But the simple-optimiser doesn't.
-The identity function local_id delays the eta reduction just long enough
-for unsafeCoerce# to get inlined.
-
-Sigh. This is horrible, but then so is unsafeCoerce.
--}
+unsafeCoerceAddr :: forall (a :: TYPE 'AddrRep) (b :: TYPE 'AddrRep) . a -> b
+-- Kind-homogeneous, but levity monomorphic (TYPE AddrRep)
+unsafeCoerceAddr x = case unsafeEqualityProof @a @b of UnsafeRefl -> x
+
+-- | Highly, terribly dangerous coercion from one representation type
+-- to another. Misuse of this function can invite the garbage collector
+-- to trounce upon your data and then laugh in your face. You don't want
+-- this function. Really.
+unsafeCoerce# :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
+                        (a :: TYPE r1) (b :: TYPE r2).
+                 a -> b
+unsafeCoerce# = error "GHC internal error: unsafeCoerce# not unfolded"
+-- See (U10) of Note [Implementing unsafeCorece]
+-- The RHS is updated by Desugar.patchMagicDefns
+-- See Desugar Note [Wiring in unsafeCoerce#]
+
+{-# RULES
+-- See (U8) in Note [Implementing unsafeCoerce]
+
+-- unsafeCoerce version of the map/coerce rule defined in GHC.Base
+"map/unsafeCoerce" map unsafeCoerce = unsafeCoerce
 
-unsafeCoerce :: a -> b
-unsafeCoerce x = local_id (unsafeCoerce# x)
-  -- See Note [Unsafe coerce magic] in basicTypes/MkId
-  -- NB: Do not eta-reduce this definition (see above)
+-- unsafeCoerce version of the amap/coerce rule defined in GHC.Arr
+"amap/unsafeCoerce" amap unsafeCoerce = unsafeCoerce
+#-}