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>

65 files changed, 1118 insertions, 493 deletions

diff --git a/compiler/GHC/CoreToByteCode.hs b/compiler/GHC/CoreToByteCode.hs
index f6ceadf1be..73a54fb3e2 100644
--- a/compiler/GHC/CoreToByteCode.hs
+++ b/compiler/GHC/CoreToByteCode.hs
@@ -56,6 +56,7 @@ import GHC.Data.Bitmap
 import OrdList
 import Maybes
 import VarEnv
+import PrelNames ( unsafeEqualityProofName )
 
 import Data.List
 import Foreign
@@ -634,11 +635,12 @@ schemeE d s p exp@(AnnTick (Breakpoint _id _fvs) _rhs)
 -- ignore other kinds of tick
 schemeE d s p (AnnTick _ (_, rhs)) = schemeE d s p rhs
 
+-- no alts: scrut is guaranteed to diverge
 schemeE d s p (AnnCase (_,scrut) _ _ []) = schemeE d s p scrut
-        -- no alts: scrut is guaranteed to diverge
 
+-- handle pairs with one void argument (e.g. state token)
 schemeE d s p (AnnCase scrut bndr _ [(DataAlt dc, [bind1, bind2], rhs)])
-   | isUnboxedTupleCon dc -- handles pairs with one void argument (e.g. state token)
+   | isUnboxedTupleCon dc
         -- Convert
         --      case .... of x { (# V'd-thing, a #) -> ... }
         -- to
@@ -655,11 +657,13 @@ schemeE d s p (AnnCase scrut bndr _ [(DataAlt dc, [bind1, bind2], rhs)])
                    _ -> Nothing
    = res
 
+-- handle unit tuples
 schemeE d s p (AnnCase scrut bndr _ [(DataAlt dc, [bind1], rhs)])
    | isUnboxedTupleCon dc
-   , typePrimRep (idType bndr) `lengthAtMost` 1 -- handles unit tuples
+   , typePrimRep (idType bndr) `lengthAtMost` 1
    = doCase d s p scrut bind1 [(DEFAULT, [], rhs)] (Just bndr)
 
+-- handle nullary tuples
 schemeE d s p (AnnCase scrut bndr _ alt@[(DEFAULT, [], _)])
    | isUnboxedTupleType (idType bndr)
    , Just ty <- case typePrimRep (idType bndr) of
@@ -983,6 +987,7 @@ doCase
 doCase d s p (_,scrut) bndr alts is_unboxed_tuple
   | typePrimRep (idType bndr) `lengthExceeds` 1
   = multiValException
+
   | otherwise
   = do
      dflags <- getDynFlags
@@ -1883,6 +1888,7 @@ bcView :: AnnExpr' Var ann -> Maybe (AnnExpr' Var ann)
 --  b) type applications
 --  c) casts
 --  d) ticks (but not breakpoints)
+--  e) case unsafeEqualityProof of UnsafeRefl -> e  ==> e
 -- Type lambdas *can* occur in random expressions,
 -- whereas value lambdas cannot; that is why they are nuked here
 bcView (AnnCast (_,e) _)             = Just e
@@ -1890,8 +1896,19 @@ bcView (AnnLam v (_,e)) | isTyVar v  = Just e
 bcView (AnnApp (_,e) (_, AnnType _)) = Just e
 bcView (AnnTick Breakpoint{} _)      = Nothing
 bcView (AnnTick _other_tick (_,e))   = Just e
+bcView (AnnCase (_,e) _ _ alts)  -- Handle unsafe equality proof
+  | AnnVar id <- bcViewLoop e
+  , idName id == unsafeEqualityProofName
+  , [(_, _, (_, rhs))] <- alts
+  = Just rhs
 bcView _                             = Nothing
 
+bcViewLoop :: AnnExpr' Var ann -> AnnExpr' Var ann
+bcViewLoop e =
+    case bcView e of
+      Nothing -> e
+      Just e' -> bcViewLoop e'
+
 isVAtom :: AnnExpr' Var ann -> Bool
 isVAtom e | Just e' <- bcView e = isVAtom e'
 isVAtom (AnnVar v)              = isVoidArg (bcIdArgRep v)
diff --git a/compiler/GHC/CoreToIface.hs b/compiler/GHC/CoreToIface.hs
index d52c664783..277656d134 100644
--- a/compiler/GHC/CoreToIface.hs
+++ b/compiler/GHC/CoreToIface.hs
@@ -301,7 +301,6 @@ toIfaceCoercionX fr co
                             fr' = fr `delVarSet` tv
 
     go_prov :: UnivCoProvenance -> IfaceUnivCoProv
-    go_prov UnsafeCoerceProv    = IfaceUnsafeCoerceProv
     go_prov (PhantomProv co)    = IfacePhantomProv (go co)
     go_prov (ProofIrrelProv co) = IfaceProofIrrelProv (go co)
     go_prov (PluginProv str)    = IfacePluginProv str
diff --git a/compiler/GHC/CoreToStg.hs b/compiler/GHC/CoreToStg.hs
index b0738fdb82..2e922b6de6 100644
--- a/compiler/GHC/CoreToStg.hs
+++ b/compiler/GHC/CoreToStg.hs
@@ -46,6 +46,7 @@ import ForeignCall
 import Demand           ( isUsedOnce )
 import PrimOp           ( PrimCall(..), primOpWrapperId )
 import SrcLoc           ( mkGeneralSrcSpan )
+import PrelNames        ( unsafeEqualityProofName )
 
 import Data.List.NonEmpty (nonEmpty, toList)
 import Data.Maybe    (fromMaybe)
@@ -404,11 +405,23 @@ coreToStgExpr (Case scrut _ _ [])
     -- runtime system error function.
 
 
-coreToStgExpr (Case scrut bndr _ alts) = do
+coreToStgExpr e0@(Case scrut bndr _ alts) = do
     alts2 <- extendVarEnvCts [(bndr, LambdaBound)] (mapM vars_alt alts)
     scrut2 <- coreToStgExpr scrut
-    return (StgCase scrut2 bndr (mkStgAltType bndr alts) alts2)
+    let stg = StgCase scrut2 bndr (mkStgAltType bndr alts) alts2
+    -- See (U2) in Note [Implementing unsafeCoerce] in base:Unsafe.Coerce
+    case scrut2 of
+      StgApp id [] | idName id == unsafeEqualityProofName ->
+        case alts2 of
+          [(_, [_co], rhs)] ->
+            return rhs
+          _ ->
+            pprPanic "coreToStgExpr" $
+              text "Unexpected unsafe equality case expression:" $$ ppr e0 $$
+              text "STG:" $$ ppr stg
+      _ -> return stg
   where
+    vars_alt :: (AltCon, [Var], CoreExpr) -> CtsM (AltCon, [Var], StgExpr)
     vars_alt (con, binders, rhs)
       | DataAlt c <- con, c == unboxedUnitDataCon
       = -- This case is a bit smelly.
diff --git a/compiler/GHC/CoreToStg/Prep.hs b/compiler/GHC/CoreToStg/Prep.hs
index fdd182b48b..edfe9cc363 100644
--- a/compiler/GHC/CoreToStg/Prep.hs
+++ b/compiler/GHC/CoreToStg/Prep.hs
@@ -54,7 +54,7 @@ import DynFlags
 import Util
 import Outputable
 import FastString
-import Name             ( NamedThing(..), nameSrcSpan )
+import Name             ( NamedThing(..), nameSrcSpan, isInternalName )
 import SrcLoc           ( SrcSpan(..), realSrcLocSpan, mkRealSrcLoc )
 import Data.Bits
 import MonadUtils       ( mapAccumLM )
@@ -381,22 +381,24 @@ cpeBind :: TopLevelFlag -> CorePrepEnv -> CoreBind
                                    -- Nothing <=> added bind' to floats instead
 cpeBind top_lvl env (NonRec bndr rhs)
   | not (isJoinId bndr)
-  = do { (_, bndr1) <- cpCloneBndr env bndr
+  = do { (env1, bndr1) <- cpCloneBndr env bndr
        ; let dmd         = idDemandInfo bndr
              is_unlifted = isUnliftedType (idType bndr)
        ; (floats, rhs1) <- cpePair top_lvl NonRecursive
                                    dmd is_unlifted
                                    env bndr1 rhs
        -- See Note [Inlining in CorePrep]
-       ; if exprIsTrivial rhs1 && isNotTopLevel top_lvl
-            then return (extendCorePrepEnvExpr env bndr rhs1, floats, Nothing)
-            else do {
+       ; let triv_rhs = cpExprIsTrivial rhs1
+             env2    | triv_rhs  = extendCorePrepEnvExpr env1 bndr rhs1
+                     | otherwise = env1
+             floats1 | triv_rhs, isInternalName (idName bndr)
+                     = floats
+                     | otherwise
+                     = addFloat floats new_float
 
-       ; let new_float = mkFloat dmd is_unlifted bndr1 rhs1
+             new_float = mkFloat dmd is_unlifted bndr1 rhs1
 
-       ; return (extendCorePrepEnv env bndr bndr1,
-                 addFloat floats new_float,
-                 Nothing) }}
+       ; return (env2, floats1, Nothing) }
 
   | otherwise -- A join point; see Note [Join points and floating]
   = ASSERT(not (isTopLevel top_lvl)) -- can't have top-level join point
@@ -613,6 +615,18 @@ cpeRhsE env expr@(Lam {})
         ; return (emptyFloats, mkLams bndrs' body') }
 
 cpeRhsE env (Case scrut bndr ty alts)
+  | isUnsafeEqualityProof scrut
+  , [(con, bs, rhs)] <- alts
+  = do { (floats1, scrut') <- cpeBody env scrut
+       ; (env1, bndr')     <- cpCloneBndr env bndr
+       ; (env2, bs')       <- cpCloneBndrs env1 bs
+       ; (floats2, rhs')   <- cpeBody env2 rhs
+       ; let case_float = FloatCase scrut' bndr' con bs' True
+             floats'    = (floats1 `addFloat` case_float)
+                          `appendFloats` floats2
+       ; return (floats', rhs') }
+
+  | otherwise
   = do { (floats, scrut') <- cpeBody env scrut
        ; (env', bndr2) <- cpCloneBndr env bndr
        ; let alts'
@@ -629,6 +643,7 @@ cpeRhsE env (Case scrut bndr ty alts)
                where err = mkRuntimeErrorApp rUNTIME_ERROR_ID ty
                                              "Bottoming expression returned"
        ; alts'' <- mapM (sat_alt env') alts'
+
        ; return (floats, Case scrut' bndr2 ty alts'') }
   where
     sat_alt env (con, bs, rhs)
@@ -983,7 +998,28 @@ okCpeArg :: CoreExpr -> Bool
 -- Don't float literals. See Note [ANF-ising literal string arguments].
 okCpeArg (Lit _) = False
 -- Do not eta expand a trivial argument
-okCpeArg expr    = not (exprIsTrivial expr)
+okCpeArg expr    = not (cpExprIsTrivial expr)
+
+cpExprIsTrivial :: CoreExpr -> Bool
+cpExprIsTrivial e
+  | Tick t e <- e
+  , not (tickishIsCode t)
+  = cpExprIsTrivial e
+  | Case scrut _ _ alts <- e
+  , isUnsafeEqualityProof scrut
+  , [(_,_,rhs)] <- alts
+  = cpExprIsTrivial rhs
+  | otherwise
+  = exprIsTrivial e
+
+isUnsafeEqualityProof :: CoreExpr -> Bool
+-- See (U3) and (U4) in
+-- Note [Implementing unsafeCoerce] in base:Unsafe.Coerce
+isUnsafeEqualityProof e
+  | Var v `App` Type _ `App` Type _ `App` Type _ <- e
+  = idName v == unsafeEqualityProofName
+  | otherwise
+  = False
 
 -- This is where we arrange that a non-trivial argument is let-bound
 cpeArg :: CorePrepEnv -> Demand
@@ -1174,8 +1210,11 @@ data FloatingBind
                          -- unlifted ones are done with FloatCase
 
  | FloatCase
-      Id CpeBody
-      Bool              -- The bool indicates "ok-for-speculation"
+      CpeBody         -- Always ok-for-speculation
+      Id              -- Case binder
+      AltCon [Var]    -- Single alternative
+      Bool            -- Ok-for-speculation; False of a strict,
+                      -- but lifted binding
 
  -- | See Note [Floating Ticks in CorePrep]
  | FloatTick (Tickish Id)
@@ -1184,7 +1223,11 @@ data Floats = Floats OkToSpec (OrdList FloatingBind)
 
 instance Outputable FloatingBind where
   ppr (FloatLet b) = ppr b
-  ppr (FloatCase b r ok) = brackets (ppr ok) <+> ppr b <+> equals <+> ppr r
+  ppr (FloatCase r b k bs ok) = text "case" <> braces (ppr ok) <+> ppr r
+                                <+> text "of"<+> ppr b <> text "@"
+                                <> case bs of
+                                   [] -> ppr k
+                                   _  -> parens (ppr k <+> ppr bs)
   ppr (FloatTick t) = ppr t
 
 instance Outputable Floats where
@@ -1207,17 +1250,19 @@ data OkToSpec
 
 mkFloat :: Demand -> Bool -> Id -> CpeRhs -> FloatingBind
 mkFloat dmd is_unlifted bndr rhs
-  | use_case  = FloatCase bndr rhs (exprOkForSpeculation rhs)
+  | is_strict
+  , not is_hnf  = FloatCase rhs bndr DEFAULT [] (exprOkForSpeculation rhs)
+    -- Don't make a case for a HNF binding, even if it's strict
+    -- Otherwise we get  case (\x -> e) of ...!
+
+  | is_unlifted = ASSERT2( exprOkForSpeculation rhs, ppr rhs )
+                  FloatCase rhs bndr DEFAULT [] True
   | is_hnf    = FloatLet (NonRec bndr                       rhs)
   | otherwise = FloatLet (NonRec (setIdDemandInfo bndr dmd) rhs)
                    -- See Note [Pin demand info on floats]
   where
     is_hnf    = exprIsHNF rhs
     is_strict = isStrictDmd dmd
-    use_case  = is_unlifted || is_strict && not is_hnf
-                -- Don't make a case for a value binding,
-                -- even if it's strict.  Otherwise we get
-                --      case (\x -> e) of ...!
 
 emptyFloats :: Floats
 emptyFloats = Floats OkToSpec nilOL
@@ -1229,19 +1274,19 @@ wrapBinds :: Floats -> CpeBody -> CpeBody
 wrapBinds (Floats _ binds) body
   = foldrOL mk_bind body binds
   where
-    mk_bind (FloatCase bndr rhs _) body = mkDefaultCase rhs bndr body
-    mk_bind (FloatLet bind)        body = Let bind body
-    mk_bind (FloatTick tickish)    body = mkTick tickish body
+    mk_bind (FloatCase rhs bndr con bs _) body = Case rhs bndr (exprType body) [(con,bs,body)]
+    mk_bind (FloatLet bind)               body = Let bind body
+    mk_bind (FloatTick tickish)           body = mkTick tickish body
 
 addFloat :: Floats -> FloatingBind -> Floats
 addFloat (Floats ok_to_spec floats) new_float
   = Floats (combine ok_to_spec (check new_float)) (floats `snocOL` new_float)
   where
-    check (FloatLet _) = OkToSpec
-    check (FloatCase _ _ ok_for_spec)
-        | ok_for_spec  =  IfUnboxedOk
-        | otherwise    =  NotOkToSpec
-    check FloatTick{}  = OkToSpec
+    check (FloatLet {})  = OkToSpec
+    check (FloatCase _ _ _ _ ok_for_spec)
+      | ok_for_spec = IfUnboxedOk
+      | otherwise   = NotOkToSpec
+    check FloatTick{}    = OkToSpec
         -- The ok-for-speculation flag says that it's safe to
         -- float this Case out of a let, and thereby do it more eagerly
         -- We need the top-level flag because it's never ok to float
@@ -1270,8 +1315,8 @@ deFloatTop (Floats _ floats)
   = foldrOL get [] floats
   where
     get (FloatLet b) bs = occurAnalyseRHSs b : bs
-    get (FloatCase var body _) bs  =
-      occurAnalyseRHSs (NonRec var body) : bs
+    get (FloatCase body var _ _ _) bs
+      = occurAnalyseRHSs (NonRec var body) : bs
     get b _ = pprPanic "corePrepPgm" (ppr b)
 
     -- See Note [Dead code in CorePrep]
@@ -1334,65 +1379,67 @@ allLazyNested is_rec (Floats IfUnboxedOk _) = isNonRec is_rec
 --                      The environment
 -- ---------------------------------------------------------------------------
 
--- Note [Inlining in CorePrep]
--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~
--- There is a subtle but important invariant that must be upheld in the output
--- of CorePrep: there are no "trivial" updatable thunks.  Thus, this Core
--- is impermissible:
---
---      let x :: ()
---          x = y
---
--- (where y is a reference to a GLOBAL variable).  Thunks like this are silly:
--- they can always be profitably replaced by inlining x with y. Consequently,
--- the code generator/runtime does not bother implementing this properly
--- (specifically, there is no implementation of stg_ap_0_upd_info, which is the
--- stack frame that would be used to update this thunk.  The "0" means it has
--- zero free variables.)
---
--- In general, the inliner is good at eliminating these let-bindings.  However,
--- there is one case where these trivial updatable thunks can arise: when
--- we are optimizing away 'lazy' (see Note [lazyId magic], and also
--- 'cpeRhsE'.)  Then, we could have started with:
---
---      let x :: ()
---          x = lazy @ () y
---
--- which is a perfectly fine, non-trivial thunk, but then CorePrep will
--- drop 'lazy', giving us 'x = y' which is trivial and impermissible.
--- The solution is CorePrep to have a miniature inlining pass which deals
--- with cases like this.  We can then drop the let-binding altogether.
---
--- Why does the removal of 'lazy' have to occur in CorePrep?
--- The gory details are in Note [lazyId magic] in MkId, but the
--- main reason is that lazy must appear in unfoldings (optimizer
--- output) and it must prevent call-by-value for catch# (which
--- is implemented by CorePrep.)
---
--- An alternate strategy for solving this problem is to have the
--- inliner treat 'lazy e' as a trivial expression if 'e' is trivial.
--- We decided not to adopt this solution to keep the definition
--- of 'exprIsTrivial' simple.
---
--- There is ONE caveat however: for top-level bindings we have
--- to preserve the binding so that we float the (hacky) non-recursive
--- binding for data constructors; see Note [Data constructor workers].
---
--- Note [CorePrep inlines trivial CoreExpr not Id]
--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--- Why does cpe_env need to be an IdEnv CoreExpr, as opposed to an
--- IdEnv Id?  Naively, we might conjecture that trivial updatable thunks
--- as per Note [Inlining in CorePrep] always have the form
--- 'lazy @ SomeType gbl_id'.  But this is not true: the following is
--- perfectly reasonable Core:
---
---      let x :: ()
---          x = lazy @ (forall a. a) y @ Bool
---
--- When we inline 'x' after eliminating 'lazy', we need to replace
--- occurrences of 'x' with 'y @ bool', not just 'y'.  Situations like
--- this can easily arise with higher-rank types; thus, cpe_env must
--- map to CoreExprs, not Ids.
+{- Note [Inlining in CorePrep]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+There is a subtle but important invariant that must be upheld in the output
+of CorePrep: there are no "trivial" updatable thunks.  Thus, this Core
+is impermissible:
+
+     let x :: ()
+         x = y
+
+(where y is a reference to a GLOBAL variable).  Thunks like this are silly:
+they can always be profitably replaced by inlining x with y. Consequently,
+the code generator/runtime does not bother implementing this properly
+(specifically, there is no implementation of stg_ap_0_upd_info, which is the
+stack frame that would be used to update this thunk.  The "0" means it has
+zero free variables.)
+
+In general, the inliner is good at eliminating these let-bindings.  However,
+there is one case where these trivial updatable thunks can arise: when
+we are optimizing away 'lazy' (see Note [lazyId magic], and also
+'cpeRhsE'.)  Then, we could have started with:
+
+     let x :: ()
+         x = lazy @ () y
+
+which is a perfectly fine, non-trivial thunk, but then CorePrep will
+drop 'lazy', giving us 'x = y' which is trivial and impermissible.
+The solution is CorePrep to have a miniature inlining pass which deals
+with cases like this.  We can then drop the let-binding altogether.
+
+Why does the removal of 'lazy' have to occur in CorePrep?
+The gory details are in Note [lazyId magic] in MkId, but the
+main reason is that lazy must appear in unfoldings (optimizer
+output) and it must prevent call-by-value for catch# (which
+is implemented by CorePrep.)
+
+An alternate strategy for solving this problem is to have the
+inliner treat 'lazy e' as a trivial expression if 'e' is trivial.
+We decided not to adopt this solution to keep the definition
+of 'exprIsTrivial' simple.
+
+There is ONE caveat however: for top-level bindings we have
+to preserve the binding so that we float the (hacky) non-recursive
+binding for data constructors; see Note [Data constructor workers].
+
+Note [CorePrep inlines trivial CoreExpr not Id]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Why does cpe_env need to be an IdEnv CoreExpr, as opposed to an
+IdEnv Id?  Naively, we might conjecture that trivial updatable thunks
+as per Note [Inlining in CorePrep] always have the form
+'lazy @ SomeType gbl_id'.  But this is not true: the following is
+perfectly reasonable Core:
+
+     let x :: ()
+         x = lazy @ (forall a. a) y @ Bool
+
+When we inline 'x' after eliminating 'lazy', we need to replace
+occurrences of 'x' with 'y @ bool', not just 'y'.  Situations like
+this can easily arise with higher-rank types; thus, cpe_env must
+map to CoreExprs, not Ids.
+
+-}
 
 data CorePrepEnv
   = CPE { cpe_dynFlags        :: DynFlags
@@ -1622,9 +1669,9 @@ wrapTicks (Floats flag floats0) expr =
         go (floats, ticks) f
           = (foldr wrap f (reverse ticks):floats, ticks)
 
-        wrap t (FloatLet bind)    = FloatLet (wrapBind t bind)
-        wrap t (FloatCase b r ok) = FloatCase b (mkTick t r) ok
-        wrap _ other              = pprPanic "wrapTicks: unexpected float!"
+        wrap t (FloatLet bind)           = FloatLet (wrapBind t bind)
+        wrap t (FloatCase r b con bs ok) = FloatCase (mkTick t r) b con bs ok
+        wrap _ other                     = pprPanic "wrapTicks: unexpected float!"
                                              (ppr other)
         wrapBind t (NonRec binder rhs) = NonRec binder (mkTick t rhs)
         wrapBind t (Rec pairs)         = Rec (mapSnd (mkTick t) pairs)
diff --git a/compiler/GHC/HsToCore.hs b/compiler/GHC/HsToCore.hs
index 6802319be2..fc290737ca 100644
--- a/compiler/GHC/HsToCore.hs
+++ b/compiler/GHC/HsToCore.hs
@@ -9,6 +9,7 @@ The Desugarer: turning HsSyn into Core.
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
 
 module GHC.HsToCore (
     -- * Desugaring operations
@@ -27,29 +28,32 @@ import TcRnTypes
 import TcRnMonad  ( finalSafeMode, fixSafeInstances )
 import TcRnDriver ( runTcInteractive )
 import Id
+import IdInfo
 import Name
 import Type
+import TyCon       ( tyConDataCons )
 import Avail
 import CoreSyn
 import CoreFVs     ( exprsSomeFreeVarsList )
 import CoreOpt     ( simpleOptPgm, simpleOptExpr )
+import CoreUtils
+import CoreUnfold
 import PprCore
 import GHC.HsToCore.Monad
 import GHC.HsToCore.Expr
 import GHC.HsToCore.Binds
 import GHC.HsToCore.Foreign.Decl
-import PrelNames   ( coercibleTyConKey )
-import TysPrim     ( eqReprPrimTyCon )
-import Unique      ( hasKey )
-import Coercion    ( mkCoVarCo )
-import TysWiredIn  ( coercibleDataCon )
+import PrelNames
+import TysPrim
+import Coercion
+import TysWiredIn
 import DataCon     ( dataConWrapId )
-import MkCore      ( mkCoreLet )
+import MkCore
 import Module
 import NameSet
 import NameEnv
 import Rules
-import BasicTypes       ( Activation(.. ), competesWith, pprRuleName )
+import BasicTypes
 import CoreMonad        ( CoreToDo(..) )
 import CoreLint         ( endPassIO )
 import VarSet
@@ -130,6 +134,7 @@ deSugar hsc_env
         ; (msgs, mb_res) <- initDs hsc_env tcg_env $
                        do { ds_ev_binds <- dsEvBinds ev_binds
                           ; core_prs <- dsTopLHsBinds binds_cvr
+                          ; core_prs <- patchMagicDefns core_prs
                           ; (spec_prs, spec_rules) <- dsImpSpecs imp_specs
                           ; (ds_fords, foreign_prs) <- dsForeigns fords
                           ; ds_rules <- mapMaybeM dsRule rules
@@ -506,7 +511,7 @@ For that we replace any forall'ed `c :: Coercible a b` value in a RULE by
 corresponding `co :: a ~#R b` and wrap the LHS and the RHS in
 `let c = MkCoercible co in ...`. This is later simplified to the desired form
 by simpleOptExpr (for the LHS) resp. the simplifiers (for the RHS).
-See also Note [Getting the map/coerce RULE to work] in CoreSubst.
+See also Note [Getting the map/coerce RULE to work] in CoreOpt.
 
 Note [Rules and inlining/other rules]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -543,3 +548,209 @@ firing.  But it's not clear what to do instead.  We could make the
 class method rules inactive in phase 2, but that would delay when
 subsequent transformations could fire.
 -}
+
+{-
+************************************************************************
+*                                                                      *
+*              Magic definitions
+*                                                                      *
+************************************************************************
+
+Note [Patching magic definitions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We sometimes need to have access to defined Ids in pure contexts. Usually, we
+simply "wire in" these entities, as we do for types in TysWiredIn and for Ids
+in MkId. See Note [Wired-in Ids] in MkId.
+
+However, it is sometimes *much* easier to define entities in Haskell,
+even if we need pure access; note that wiring-in an Id requires all
+entities used in its definition *also* to be wired in, transitively
+and recursively.  This can be a huge pain.  The little trick
+documented here allows us to have the best of both worlds.
+
+Motivating example: unsafeCoerce#. See [Wiring in unsafeCoerce#] for the
+details.
+
+The trick is to
+
+* Define the known-key Id in a library module, with a stub definition,
+     unsafeCoerce# :: ..a suitable type signature..
+     unsafeCoerce# = error "urk"
+
+* Magically over-write its RHS here in the desugarer, in
+  patchMagicDefns.  This update can be done with full access to the
+  DsM monad, and hence, dsLookupGlobal. We thus do not have to wire in
+  all the entities used internally, a potentially big win.
+
+  This step should not change the Name or type of the Id.
+
+Because an Id stores its unfolding directly (as opposed to in the second
+component of a (Id, CoreExpr) pair), the patchMagicDefns function returns
+a new Id to use.
+
+Here are the moving parts:
+
+- patchMagicDefns checks whether we're in a module with magic definitions;
+  if so, patch the magic definitions. If not, skip.
+
+- patchMagicDefn just looks up in an environment to find a magic defn and
+  patches it in.
+
+- magicDefns holds the magic definitions.
+
+- magicDefnsEnv allows for quick access to magicDefns.
+
+- magicDefnModules, built also from magicDefns, contains the modules that
+  need careful attention.
+
+Note [Wiring in unsafeCoerce#]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We want (Haskell)
+
+  unsafeCoerce# :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
+                          (a :: TYPE r1) (b :: TYPE r2).
+                   a -> b
+  unsafeCoerce# x = case unsafeEqualityProof @r1 @r2 of
+    UnsafeRefl -> case unsafeEqualityProof @a @b of
+      UnsafeRefl -> x
+
+or (Core)
+
+  unsafeCoerce# :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
+                          (a :: TYPE r1) (b :: TYPE r2).
+                   a -> b
+  unsafeCoerce# = \ @r1 @r2 @a @b (x :: a).
+    case unsafeEqualityProof @RuntimeRep @r1 @r2 of
+      UnsafeRefl (co1 :: r1 ~# r2) ->
+        case unsafeEqualityProof @(TYPE r2) @(a |> TYPE co1) @b of
+          UnsafeRefl (co2 :: (a |> TYPE co1) ~# b) ->
+            (x |> (GRefl :: a ~# (a |> TYPE co1)) ; co2)
+
+It looks like we can write this in Haskell directly, but we can't:
+the levity polymorphism checks defeat us. Note that `x` is a levity-
+polymorphic variable. So we must wire it in with a compulsory
+unfolding, like other levity-polymorphic primops.
+
+The challenge is that UnsafeEquality is a GADT, and wiring in a GADT
+is *hard*: it has a worker separate from its wrapper, with all manner
+of complications. (Simon and Richard tried to do this. We nearly wept.)
+
+The solution is documented in Note [Patching magic definitions]. We now
+simply look up the UnsafeEquality GADT in the environment, leaving us
+only to wire in unsafeCoerce# directly.
+
+Wrinkle:
+--------
+We must make absolutely sure that unsafeCoerce# is inlined. You might
+think that giving it a compulsory unfolding is enough. However,
+unsafeCoerce# is put in an interface file like any other definition.
+At optimization level 0, we enable -fignore-interface-pragmas, which
+ignores pragmas in interface files. We thus must check to see whether
+there is a compulsory unfolding, even with -fignore-interface-pragmas.
+This is done in TcIface.tcIdInfo.
+
+Test case: ghci/linker/dyn/T3372
+
+-}
+
+
+-- Postcondition: the returned Ids are in one-to-one correspondence as the
+-- input Ids; each returned Id has the same type as the passed-in Id.
+-- See Note [Patching magic definitions]
+patchMagicDefns :: OrdList (Id,CoreExpr)
+                -> DsM (OrdList (Id,CoreExpr))
+patchMagicDefns pairs
+  -- optimization: check whether we're in a magic module before looking
+  -- at all the ids
+  = do { this_mod <- getModule
+       ; if this_mod `elemModuleSet` magicDefnModules
+         then traverse patchMagicDefn pairs
+         else return pairs }
+
+patchMagicDefn :: (Id, CoreExpr) -> DsM (Id, CoreExpr)
+patchMagicDefn orig_pair@(orig_id, orig_rhs)
+  | Just mk_magic_pair <- lookupNameEnv magicDefnsEnv (getName orig_id)
+  = do { magic_pair@(magic_id, _) <- mk_magic_pair orig_id orig_rhs
+
+       -- Patching should not change the Name or the type of the Id
+       ; MASSERT( getUnique magic_id == getUnique orig_id )
+       ; MASSERT( varType magic_id `eqType` varType orig_id )
+
+       ; return magic_pair }
+  | otherwise
+  = return orig_pair
+
+magicDefns :: [(Name,    Id -> CoreExpr     -- old Id and RHS
+                      -> DsM (Id, CoreExpr) -- new Id and RHS
+               )]
+magicDefns = [ (unsafeCoercePrimName, mkUnsafeCoercePrimPair) ]
+
+magicDefnsEnv :: NameEnv (Id -> CoreExpr -> DsM (Id, CoreExpr))
+magicDefnsEnv = mkNameEnv magicDefns
+
+magicDefnModules :: ModuleSet
+magicDefnModules = mkModuleSet $ map (nameModule . getName . fst) magicDefns
+
+mkUnsafeCoercePrimPair :: Id -> CoreExpr -> DsM (Id, CoreExpr)
+-- See Note [Wiring in unsafeCoerce#] for the defn we are creating here
+mkUnsafeCoercePrimPair _old_id old_expr
+  = do { unsafe_equality_proof_id <- dsLookupGlobalId unsafeEqualityProofName
+       ; unsafe_equality_tc       <- dsLookupTyCon unsafeEqualityTyConName
+
+       ; let [unsafe_refl_data_con] = tyConDataCons unsafe_equality_tc
+
+             rhs = mkLams [ runtimeRep1TyVar, runtimeRep2TyVar
+                          , openAlphaTyVar, openBetaTyVar
+                          , x ] $
+                   mkSingleAltCase scrut1
+                                   (mkWildValBinder scrut1_ty)
+                                   (DataAlt unsafe_refl_data_con)
+                                   [rr_cv] $
+                   mkSingleAltCase scrut2
+                                   (mkWildValBinder scrut2_ty)
+                                   (DataAlt unsafe_refl_data_con)
+                                   [ab_cv] $
+                   Var x `mkCast` x_co
+
+             [x, rr_cv, ab_cv] = mkTemplateLocals
+               [ openAlphaTy -- x :: a
+               , rr_cv_ty    -- rr_cv :: r1 ~# r2
+               , ab_cv_ty    -- ab_cv :: (alpha |> alpha_co ~# beta)
+               ]
+
+             -- Returns (scrutinee, scrutinee type, type of covar in AltCon)
+             unsafe_equality k a b
+               = ( mkTyApps (Var unsafe_equality_proof_id) [k,b,a]
+                 , mkTyConApp unsafe_equality_tc [k,b,a]
+                 , mkHeteroPrimEqPred k k a b
+                 )
+             -- NB: UnsafeRefl :: (b ~# a) -> UnsafeEquality a b, so we have to
+             -- carefully swap the arguments above
+
+             (scrut1, scrut1_ty, rr_cv_ty) = unsafe_equality runtimeRepTy
+                                                             runtimeRep1Ty
+                                                             runtimeRep2Ty
+             (scrut2, scrut2_ty, ab_cv_ty) = unsafe_equality (tYPE runtimeRep2Ty)
+                                                             (openAlphaTy `mkCastTy` alpha_co)
+                                                             openBetaTy
+
+             -- alpha_co :: TYPE r1 ~# TYPE r2
+             -- alpha_co = TYPE rr_cv
+             alpha_co = mkTyConAppCo Nominal tYPETyCon [mkCoVarCo rr_cv]
+
+             -- x_co :: alpha ~R# beta
+             x_co = mkGReflCo Representational openAlphaTy (MCo alpha_co) `mkTransCo`
+                    mkSubCo (mkCoVarCo ab_cv)
+
+
+             info = noCafIdInfo `setInlinePragInfo` alwaysInlinePragma
+                                `setUnfoldingInfo` mkCompulsoryUnfolding rhs
+
+             ty = mkSpecForAllTys [ runtimeRep1TyVar, runtimeRep2TyVar
+                                  , openAlphaTyVar, openBetaTyVar ] $
+                  mkVisFunTy openAlphaTy openBetaTy
+
+             id   = mkExportedVanillaId unsafeCoercePrimName ty `setIdInfo` info
+       ; return (id, old_expr) }
+
+  where
diff --git a/compiler/GHC/Iface/Syntax.hs b/compiler/GHC/Iface/Syntax.hs
index 45751424d6..668ce1ec7b 100644
--- a/compiler/GHC/Iface/Syntax.hs
+++ b/compiler/GHC/Iface/Syntax.hs
@@ -360,7 +360,9 @@ data IfaceUnfolding
                                 -- Possibly could eliminate the Bool here, the information
                                 -- is also in the InlinePragma.
 
-  | IfCompulsory IfaceExpr      -- Only used for default methods, in fact
+  | IfCompulsory IfaceExpr      -- default methods and unsafeCoerce#
+                                -- for more about unsafeCoerce#, see
+                                -- Note [Wiring in unsafeCoerce#] in Desugar
 
   | IfInlineRule Arity          -- INLINE pragmas
                  Bool           -- OK to inline even if *un*-saturated
@@ -1618,7 +1620,6 @@ freeNamesIfCoercion (IfaceAxiomRuleCo _ax cos)
   = fnList freeNamesIfCoercion cos
 
 freeNamesIfProv :: IfaceUnivCoProv -> NameSet
-freeNamesIfProv IfaceUnsafeCoerceProv    = emptyNameSet
 freeNamesIfProv (IfacePhantomProv co)    = freeNamesIfCoercion co
 freeNamesIfProv (IfaceProofIrrelProv co) = freeNamesIfCoercion co
 freeNamesIfProv (IfacePluginProv _)      = emptyNameSet
diff --git a/compiler/GHC/Iface/Tidy.hs b/compiler/GHC/Iface/Tidy.hs
index 2b1a4b7108..3d08b139b5 100644
--- a/compiler/GHC/Iface/Tidy.hs
+++ b/compiler/GHC/Iface/Tidy.hs
@@ -454,8 +454,15 @@ trimId :: Id -> Id
 trimId id
   | not (isImplicitId id)
   = id `setIdInfo` vanillaIdInfo
+       `setIdUnfolding` unfolding
   | otherwise
   = id
+  where
+    unfolding
+      | isCompulsoryUnfolding (idUnfolding id)
+      = idUnfolding id
+      | otherwise
+      = noUnfolding
 
 {- Note [Drop wired-in things]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1195,8 +1202,11 @@ tidyTopIdInfo dflags rhs_tidy_env name orig_rhs tidy_rhs idinfo show_unfold
 
     --------- Unfolding ------------
     unf_info = unfoldingInfo idinfo
-    unfold_info | show_unfold = tidyUnfolding rhs_tidy_env unf_info unf_from_rhs
-                | otherwise   = minimal_unfold_info
+    unfold_info
+      | isCompulsoryUnfolding unf_info || show_unfold
+      = tidyUnfolding rhs_tidy_env unf_info unf_from_rhs
+      | otherwise
+      = minimal_unfold_info
     minimal_unfold_info = zapUnfolding unf_info
     unf_from_rhs = mkTopUnfolding dflags is_bot tidy_rhs
     is_bot = isBottomingSig final_sig
diff --git a/compiler/GHC/Iface/Type.hs b/compiler/GHC/Iface/Type.hs
index f879013283..3ff25ba20e 100644
--- a/compiler/GHC/Iface/Type.hs
+++ b/compiler/GHC/Iface/Type.hs
@@ -237,6 +237,12 @@ data IfaceTyConSort = IfaceNormalTyCon          -- ^ a regular tycon
                       -- only: see Note [Equality predicates in IfaceType]
                     deriving (Eq)
 
+instance Outputable IfaceTyConSort where
+  ppr IfaceNormalTyCon         = text "normal"
+  ppr (IfaceTupleTyCon n sort) = ppr sort <> colon <> ppr n
+  ppr (IfaceSumTyCon n)        = text "sum:" <> ppr n
+  ppr IfaceEqualityTyCon       = text "equality"
+
 {- Note [Free tyvars in IfaceType]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Nowadays (since Nov 16, 2016) we pretty-print a Type by converting to
@@ -350,8 +356,7 @@ data IfaceCoercion
   | IfaceHoleCo       CoVar    -- ^ See Note [Holes in IfaceCoercion]
 
 data IfaceUnivCoProv
-  = IfaceUnsafeCoerceProv
-  | IfacePhantomProv IfaceCoercion
+  = IfacePhantomProv IfaceCoercion
   | IfaceProofIrrelProv IfaceCoercion
   | IfacePluginProv String
 
@@ -525,7 +530,6 @@ substIfaceType env ty
 
     go_cos = map go_co
 
-    go_prov IfaceUnsafeCoerceProv    = IfaceUnsafeCoerceProv
     go_prov (IfacePhantomProv co)    = IfacePhantomProv (go_co co)
     go_prov (IfaceProofIrrelProv co) = IfaceProofIrrelProv (go_co co)
     go_prov (IfacePluginProv str)    = IfacePluginProv str
@@ -1559,11 +1563,6 @@ ppr_co _ (IfaceFreeCoVar covar) = ppr covar
 ppr_co _ (IfaceCoVarCo covar)   = ppr covar
 ppr_co _ (IfaceHoleCo covar)    = braces (ppr covar)
 
-ppr_co ctxt_prec (IfaceUnivCo IfaceUnsafeCoerceProv r ty1 ty2)
-  = maybeParen ctxt_prec appPrec $
-    text "UnsafeCo" <+> ppr r <+>
-    pprParendIfaceType ty1 <+> pprParendIfaceType ty2
-
 ppr_co _ (IfaceUnivCo prov role ty1 ty2)
   = text "Univ" <> (parens $
       sep [ ppr role <+> pprIfaceUnivCoProv prov
@@ -1607,8 +1606,6 @@ ppr_role r = underscore <> pp_role
 
 ------------------
 pprIfaceUnivCoProv :: IfaceUnivCoProv -> SDoc
-pprIfaceUnivCoProv IfaceUnsafeCoerceProv
-  = text "unsafe"
 pprIfaceUnivCoProv (IfacePhantomProv co)
   = text "phantom" <+> pprParendIfaceCoercion co
 pprIfaceUnivCoProv (IfaceProofIrrelProv co)
@@ -1620,6 +1617,11 @@ pprIfaceUnivCoProv (IfacePluginProv s)
 instance Outputable IfaceTyCon where
   ppr tc = pprPromotionQuote tc <> ppr (ifaceTyConName tc)
 
+instance Outputable IfaceTyConInfo where
+  ppr (IfaceTyConInfo { ifaceTyConIsPromoted = prom
+                      , ifaceTyConSort       = sort })
+    = angleBrackets $ ppr prom <> comma <+> ppr sort
+
 pprPromotionQuote :: IfaceTyCon -> SDoc
 pprPromotionQuote tc =
     pprPromotionQuoteI $ ifaceTyConIsPromoted $ ifaceTyConInfo tc
@@ -1951,26 +1953,24 @@ instance Binary IfaceCoercion where
            _ -> panic ("get IfaceCoercion " ++ show tag)
 
 instance Binary IfaceUnivCoProv where
-  put_ bh IfaceUnsafeCoerceProv = putByte bh 1
   put_ bh (IfacePhantomProv a) = do
-          putByte bh 2
+          putByte bh 1
           put_ bh a
   put_ bh (IfaceProofIrrelProv a) = do
-          putByte bh 3
+          putByte bh 2
           put_ bh a
   put_ bh (IfacePluginProv a) = do
-          putByte bh 4
+          putByte bh 3
           put_ bh a
 
   get bh = do
       tag <- getByte bh
       case tag of
-           1 -> return $ IfaceUnsafeCoerceProv
-           2 -> do a <- get bh
+           1 -> do a <- get bh
                    return $ IfacePhantomProv a
-           3 -> do a <- get bh
+           2 -> do a <- get bh
                    return $ IfaceProofIrrelProv a
-           4 -> do a <- get bh
+           3 -> do a <- get bh
                    return $ IfacePluginProv a
            _ -> panic ("get IfaceUnivCoProv " ++ show tag)
 
diff --git a/compiler/GHC/IfaceToCore.hs b/compiler/GHC/IfaceToCore.hs
index 5cd4806e62..aa74a16284 100644
--- a/compiler/GHC/IfaceToCore.hs
+++ b/compiler/GHC/IfaceToCore.hs
@@ -1249,7 +1249,6 @@ tcIfaceCo = go
     go_var = tcIfaceLclId
 
 tcIfaceUnivCoProv :: IfaceUnivCoProv -> IfL UnivCoProvenance
-tcIfaceUnivCoProv IfaceUnsafeCoerceProv     = return UnsafeCoerceProv
 tcIfaceUnivCoProv (IfacePhantomProv kco)    = PhantomProv <$> tcIfaceCo kco
 tcIfaceUnivCoProv (IfaceProofIrrelProv kco) = ProofIrrelProv <$> tcIfaceCo kco
 tcIfaceUnivCoProv (IfacePluginProv str)     = return $ PluginProv str
@@ -1465,12 +1464,23 @@ tcIdInfo ignore_prags toplvl name ty info = do
     -- we start; default assumption is that it has CAFs
     let init_info | if_boot lcl_env = vanillaIdInfo `setUnfoldingInfo` BootUnfolding
                   | otherwise       = vanillaIdInfo
-    if ignore_prags
-        then return init_info
-        else case info of
-                NoInfo -> return init_info
-                HasInfo info -> foldlM tcPrag init_info info
+
+    case info of
+      NoInfo       -> return init_info
+      HasInfo info -> let needed = needed_prags info in
+                      foldlM tcPrag init_info needed
   where
+    needed_prags :: [IfaceInfoItem] -> [IfaceInfoItem]
+    needed_prags items
+      | not ignore_prags = items
+      | otherwise        = filter need_prag items
+
+    need_prag :: IfaceInfoItem -> Bool
+      -- compulsory unfoldings are really compulsory.
+      -- See wrinkle in Note [Wiring in unsafeCoerce#] in Desugar
+    need_prag (HsUnfold _ (IfCompulsory {})) = True
+    need_prag _                              = False
+
     tcPrag :: IdInfo -> IfaceInfoItem -> IfL IdInfo
     tcPrag info HsNoCafRefs        = return (info `setCafInfo`   NoCafRefs)
     tcPrag info (HsArity arity)    = return (info `setArityInfo` arity)
@@ -1493,7 +1503,7 @@ tcJoinInfo IfaceNotJoinPoint   = Nothing
 tcUnfolding :: TopLevelFlag -> Name -> Type -> IdInfo -> IfaceUnfolding -> IfL Unfolding
 tcUnfolding toplvl name _ info (IfCoreUnfold stable if_expr)
   = do  { dflags <- getDynFlags
-        ; mb_expr <- tcPragExpr toplvl name if_expr
+        ; mb_expr <- tcPragExpr False toplvl name if_expr
         ; let unf_src | stable    = InlineStable
                       | otherwise = InlineRhs
         ; return $ case mb_expr of
@@ -1507,13 +1517,13 @@ tcUnfolding toplvl name _ info (IfCoreUnfold stable if_expr)
      -- Strictness should occur before unfolding!
     strict_sig = strictnessInfo info
 tcUnfolding toplvl name _ _ (IfCompulsory if_expr)
-  = do  { mb_expr <- tcPragExpr toplvl name if_expr
+  = do  { mb_expr <- tcPragExpr True toplvl name if_expr
         ; return (case mb_expr of
                     Nothing   -> NoUnfolding
                     Just expr -> mkCompulsoryUnfolding expr) }
 
 tcUnfolding toplvl name _ _ (IfInlineRule arity unsat_ok boring_ok if_expr)
-  = do  { mb_expr <- tcPragExpr toplvl name if_expr
+  = do  { mb_expr <- tcPragExpr False toplvl name if_expr
         ; return (case mb_expr of
                     Nothing   -> NoUnfolding
                     Just expr -> mkCoreUnfolding InlineStable True expr guidance )}
@@ -1535,17 +1545,20 @@ For unfoldings we try to do the job lazily, so that we never type check
 an unfolding that isn't going to be looked at.
 -}
 
-tcPragExpr :: TopLevelFlag -> Name -> IfaceExpr -> IfL (Maybe CoreExpr)
-tcPragExpr toplvl name expr
+tcPragExpr :: Bool  -- Is this unfolding compulsory?
+                    -- See Note [Checking for levity polymorphism] in CoreLint
+           -> TopLevelFlag -> Name -> IfaceExpr -> IfL (Maybe CoreExpr)
+tcPragExpr is_compulsory toplvl name expr
   = forkM_maybe doc $ do
     core_expr' <- tcIfaceExpr expr
 
     -- Check for type consistency in the unfolding
     -- See Note [Linting Unfoldings from Interfaces]
-    when (isTopLevel toplvl) $ whenGOptM Opt_DoCoreLinting $ do
+    when (isTopLevel toplvl) $
+      whenGOptM Opt_DoCoreLinting $ do
         in_scope <- get_in_scope
         dflags   <- getDynFlags
-        case lintUnfolding dflags noSrcLoc in_scope core_expr' of
+        case lintUnfolding is_compulsory dflags noSrcLoc in_scope core_expr' of
           Nothing       -> return ()
           Just fail_msg -> do { mod <- getIfModule
                               ; pprPanic "Iface Lint failure"
@@ -1555,7 +1568,8 @@ tcPragExpr toplvl name expr
                                         , text "Iface expr =" <+> ppr expr ]) }
     return core_expr'
   where
-    doc = text "Unfolding of" <+> ppr name
+    doc = ppWhen is_compulsory (text "Compulsory") <+>
+          text "Unfolding of" <+> ppr name
 
     get_in_scope :: IfL VarSet -- Totally disgusting; but just for linting
     get_in_scope
@@ -1686,7 +1700,7 @@ tcIfaceTyCon (IfaceTyCon name info)
   = do { thing <- tcIfaceGlobal name
        ; return $ case ifaceTyConIsPromoted info of
            NotPromoted -> tyThingTyCon thing
-           IsPromoted    -> promoteDataCon $ tyThingDataCon thing }
+           IsPromoted  -> promoteDataCon $ tyThingDataCon thing }
 
 tcIfaceCoAxiom :: Name -> IfL (CoAxiom Branched)
 tcIfaceCoAxiom name = do { thing <- tcIfaceImplicit name
diff --git a/compiler/GHC/Runtime/Eval.hs b/compiler/GHC/Runtime/Eval.hs
index d43c5be7b8..9686c7105c 100644
--- a/compiler/GHC/Runtime/Eval.hs
+++ b/compiler/GHC/Runtime/Eval.hs
@@ -105,9 +105,9 @@ import Data.Map (Map)
 import qualified Data.Map as Map
 import StringBuffer (stringToStringBuffer)
 import Control.Monad
-import GHC.Exts
 import Data.Array
 import Exception
+import Unsafe.Coerce ( unsafeCoerce )
 
 import TcRnDriver ( runTcInteractive, tcRnType, loadUnqualIfaces )
 import TcHsSyn          ( ZonkFlexi (SkolemiseFlexi) )
@@ -1225,7 +1225,7 @@ dynCompileExpr expr = do
       to_dyn_expr = mkHsApp (L loc . HsVar noExtField . L loc $ getRdrName toDynName)
                             parsed_expr
   hval <- compileParsedExpr to_dyn_expr
-  return (unsafeCoerce# hval :: Dynamic)
+  return (unsafeCoerce hval :: Dynamic)
 
 -----------------------------------------------------------------------------
 -- show a module and it's source/object filenames
@@ -1254,7 +1254,7 @@ obtainTermFromVal hsc_env bound force ty x
   = throwIO (InstallationError
       "this operation requires -fno-external-interpreter")
   | otherwise
-  = cvObtainTerm hsc_env bound force ty (unsafeCoerce# x)
+  = cvObtainTerm hsc_env bound force ty (unsafeCoerce x)
 
 obtainTermFromId :: HscEnv -> Int -> Bool -> Id -> IO Term
 obtainTermFromId hsc_env bound force id =  do
diff --git a/compiler/GHC/Runtime/Loader.hs b/compiler/GHC/Runtime/Loader.hs
index a1c7c2a0fa..0156b16044 100644
--- a/compiler/GHC/Runtime/Loader.hs
+++ b/compiler/GHC/Runtime/Loader.hs
@@ -54,7 +54,7 @@ import Hooks
 
 import Control.Monad     ( when, unless )
 import Data.Maybe        ( mapMaybe )
-import GHC.Exts          ( unsafeCoerce# )
+import Unsafe.Coerce     ( unsafeCoerce )
 
 -- | Loads the plugins specified in the pluginModNames field of the dynamic
 -- flags. Should be called after command line arguments are parsed, but before
@@ -222,7 +222,7 @@ lessUnsafeCoerce :: DynFlags -> String -> a -> IO b
 lessUnsafeCoerce dflags context what = do
     debugTraceMsg dflags 3 $ (text "Coercing a value in") <+> (text context) <>
                              (text "...")
-    output <- evaluate (unsafeCoerce# what)
+    output <- evaluate (unsafeCoerce what)
     debugTraceMsg dflags 3 (text "Successfully evaluated coercion")
     return output
 
diff --git a/compiler/basicTypes/BasicTypes.hs b/compiler/basicTypes/BasicTypes.hs
index bff97a1887..83ebb67c5c 100644
--- a/compiler/basicTypes/BasicTypes.hs
+++ b/compiler/basicTypes/BasicTypes.hs
@@ -325,6 +325,9 @@ isPromoted :: PromotionFlag -> Bool
 isPromoted IsPromoted  = True
 isPromoted NotPromoted = False
 
+instance Outputable PromotionFlag where
+  ppr NotPromoted = text "NotPromoted"
+  ppr IsPromoted  = text "IsPromoted"
 
 {-
 ************************************************************************
diff --git a/compiler/basicTypes/DataCon.hs b/compiler/basicTypes/DataCon.hs
index 4c429ea61d..c89dab3349 100644
--- a/compiler/basicTypes/DataCon.hs
+++ b/compiler/basicTypes/DataCon.hs
@@ -24,7 +24,7 @@ module DataCon (
         FieldLbl(..), FieldLabel, FieldLabelString,
 
         -- ** Type construction
-        mkDataCon, buildAlgTyCon, buildSynTyCon, fIRST_TAG,
+        mkDataCon, fIRST_TAG,
 
         -- ** Type deconstruction
         dataConRepType, dataConInstSig, dataConFullSig,
@@ -65,7 +65,6 @@ import GhcPrelude
 
 import {-# SOURCE #-} MkId( DataConBoxer )
 import Type
-import ForeignCall ( CType )
 import Coercion
 import Unify
 import TyCon
@@ -75,7 +74,6 @@ import Name
 import PrelNames
 import Predicate
 import Var
-import VarSet( emptyVarSet )
 import Outputable
 import Util
 import BasicTypes
@@ -1381,6 +1379,10 @@ dataConCannotMatch :: [Type] -> DataCon -> Bool
 --                  scrutinee of type (T tys)
 --                  where T is the dcRepTyCon for the data con
 dataConCannotMatch tys con
+  -- See (U6) in Note [Implementing unsafeCoerce]
+  -- in base:Unsafe.Coerce
+  | dataConName con == unsafeReflDataConName
+                      = False
   | null inst_theta   = False   -- Common
   | all isTyVarTy tys = False   -- Also common
   | otherwise         = typesCantMatch (concatMap predEqs inst_theta)
@@ -1464,38 +1466,3 @@ splitDataProductType_maybe ty
   | otherwise
   = Nothing
 
-{-
-************************************************************************
-*                                                                      *
-              Building an algebraic data type
-*                                                                      *
-************************************************************************
-
-buildAlgTyCon is here because it is called from TysWiredIn, which can
-depend on this module, but not on BuildTyCl.
--}
-
-buildAlgTyCon :: Name
-              -> [TyVar]               -- ^ Kind variables and type variables
-              -> [Role]
-              -> Maybe CType
-              -> ThetaType             -- ^ Stupid theta
-              -> AlgTyConRhs
-              -> Bool                  -- ^ True <=> was declared in GADT syntax
-              -> AlgTyConFlav
-              -> TyCon
-
-buildAlgTyCon tc_name ktvs roles cType stupid_theta rhs
-              gadt_syn parent
-  = mkAlgTyCon tc_name binders liftedTypeKind roles cType stupid_theta
-               rhs parent gadt_syn
-  where
-    binders = mkTyConBindersPreferAnon ktvs emptyVarSet
-
-buildSynTyCon :: Name -> [KnotTied TyConBinder] -> Kind   -- ^ /result/ kind
-              -> [Role] -> KnotTied Type -> TyCon
-buildSynTyCon name binders res_kind roles rhs
-  = mkSynonymTyCon name binders res_kind roles rhs is_tau is_fam_free
-  where
-    is_tau      = isTauTy rhs
-    is_fam_free = isFamFreeTy rhs
diff --git a/compiler/basicTypes/MkId.hs b/compiler/basicTypes/MkId.hs
index a0b84a6aa5..5c268d37ef 100644
--- a/compiler/basicTypes/MkId.hs
+++ b/compiler/basicTypes/MkId.hs
@@ -22,11 +22,12 @@ module MkId (
         mkPrimOpId, mkFCallId,
 
         unwrapNewTypeBody, wrapFamInstBody,
-        DataConBoxer(..), mkDataConRep, mkDataConWorkId,
+        DataConBoxer(..), vanillaDataConBoxer,
+        mkDataConRep, mkDataConWorkId,
 
         -- And some particular Ids; see below for why they are wired in
         wiredInIds, ghcPrimIds,
-        unsafeCoerceName, unsafeCoerceId, realWorldPrimId,
+        realWorldPrimId,
         voidPrimId, voidArgId,
         nullAddrId, seqId, lazyId, lazyIdKey,
         coercionTokenId, magicDictId, coerceId,
@@ -46,6 +47,7 @@ import TysPrim
 import TysWiredIn
 import PrelRules
 import Type
+import TyCoRep
 import FamInstEnv
 import Coercion
 import TcType
@@ -151,7 +153,6 @@ ghcPrimIds :: [Id]  -- See Note [ghcPrimIds (aka pseudoops)]
 ghcPrimIds
   = [ realWorldPrimId
     , voidPrimId
-    , unsafeCoerceId
     , nullAddrId
     , seqId
     , magicDictId
@@ -601,6 +602,10 @@ newtype DataConBoxer = DCB ([Type] -> [Var] -> UniqSM ([Var], [CoreBind]))
                        -- Bind these src-level vars, returning the
                        -- rep-level vars to bind in the pattern
 
+vanillaDataConBoxer :: DataConBoxer
+-- No transformation on arguments needed
+vanillaDataConBoxer = DCB (\_tys args -> return (args, []))
+
 {-
 Note [Inline partially-applied constructor wrappers]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -666,7 +671,7 @@ mkDataConRep dflags fam_envs wrap_name mb_bangs data_con
                -- the strictness signature (#14290).
 
              mk_dmd str | isBanged str = evalDmd
-                        | otherwise           = topDmd
+                        | otherwise    = topDmd
 
              wrap_prag = alwaysInlinePragma `setInlinePragmaActivation`
                          activeDuringFinal
@@ -1322,19 +1327,14 @@ no curried identifier for them.  That's what mkCompulsoryUnfolding
 does.  If we had a way to get a compulsory unfolding from an interface
 file, we could do that, but we don't right now.
 
-unsafeCoerce# isn't so much a PrimOp as a phantom identifier, that
-just gets expanded into a type coercion wherever it occurs.  Hence we
-add it as a built-in Id with an unfolding here.
-
 The type variables we use here are "open" type variables: this means
 they can unify with both unlifted and lifted types.  Hence we provide
 another gun with which to shoot yourself in the foot.
 -}
 
-unsafeCoerceName, nullAddrName, seqName,
+nullAddrName, seqName,
    realWorldName, voidPrimIdName, coercionTokenName,
    magicDictName, coerceName, proxyName :: Name
-unsafeCoerceName  = mkWiredInIdName gHC_PRIM  (fsLit "unsafeCoerce#")  unsafeCoerceIdKey  unsafeCoerceId
 nullAddrName      = mkWiredInIdName gHC_PRIM  (fsLit "nullAddr#")      nullAddrIdKey      nullAddrId
 seqName           = mkWiredInIdName gHC_PRIM  (fsLit "seq")            seqIdKey           seqId
 realWorldName     = mkWiredInIdName gHC_PRIM  (fsLit "realWorld#")     realWorldPrimIdKey realWorldPrimId
@@ -1366,28 +1366,6 @@ proxyHashId
     ty      = mkInvForAllTy kv $ mkSpecForAllTy tv $ mkProxyPrimTy kv_ty tv_ty
 
 ------------------------------------------------
-unsafeCoerceId :: Id
-unsafeCoerceId
-  = pcMiscPrelId unsafeCoerceName ty info
-  where
-    info = noCafIdInfo `setInlinePragInfo` alwaysInlinePragma
-                       `setUnfoldingInfo`  mkCompulsoryUnfolding rhs
-
-    -- unsafeCoerce# :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
-    --                         (a :: TYPE r1) (b :: TYPE r2).
-    --                         a -> b
-    bndrs = mkTemplateKiTyVars [runtimeRepTy, runtimeRepTy]
-                               (\ks -> map tYPE ks)
-
-    [_, _, a, b] = mkTyVarTys bndrs
-
-    ty  = mkSpecForAllTys bndrs (mkVisFunTy a b)
-
-    [x] = mkTemplateLocals [a]
-    rhs = mkLams (bndrs ++ [x]) $
-          Cast (Var x) (mkUnsafeCo Representational a b)
-
-------------------------------------------------
 nullAddrId :: Id
 -- nullAddr# :: Addr#
 -- The reason it is here is because we don't provide
@@ -1487,22 +1465,6 @@ coerceId = pcMiscPrelId coerceName ty info
           [(DataAlt coercibleDataCon, [eq], Cast (Var x) (mkCoVarCo eq))]
 
 {-
-Note [Unsafe coerce magic]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-We define a *primitive*
-   GHC.Prim.unsafeCoerce#
-and then in the base library we define the ordinary function
-   Unsafe.Coerce.unsafeCoerce :: forall (a:*) (b:*). a -> b
-   unsafeCoerce x = unsafeCoerce# x
-
-Notice that unsafeCoerce has a civilized (albeit still dangerous)
-polymorphic type, whose type args have kind *.  So you can't use it on
-unboxed values (unsafeCoerce 3#).
-
-In contrast unsafeCoerce# is even more dangerous because you *can* use
-it on unboxed things, (unsafeCoerce# 3#) :: Int. Its type is
-   forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (a: TYPE r1) (b: TYPE r2). a -> b
-
 Note [seqId magic]
 ~~~~~~~~~~~~~~~~~~
 'GHC.Prim.seq' is special in several ways.
diff --git a/compiler/basicTypes/Unique.hs b/compiler/basicTypes/Unique.hs
index f14f22d625..f6f46914f0 100644
--- a/compiler/basicTypes/Unique.hs
+++ b/compiler/basicTypes/Unique.hs
@@ -394,12 +394,6 @@ mkPreludeTyConUnique i                = mkUnique '3' (2*i)
 tyConRepNameUnique :: Unique -> Unique
 tyConRepNameUnique  u = incrUnique u
 
--- Data constructor keys occupy *two* slots.  The first is used for the
--- data constructor itself and its wrapper function (the function that
--- evaluates arguments as necessary and calls the worker). The second is
--- used for the worker function (the function that builds the constructor
--- representation).
-
 --------------------------------------------------
 -- Wired-in data constructor keys occupy *three* slots:
 --    * u: the DataCon itself
diff --git a/compiler/coreSyn/CoreFVs.hs b/compiler/coreSyn/CoreFVs.hs
index 82b6805af5..b249f50c29 100644
--- a/compiler/coreSyn/CoreFVs.hs
+++ b/compiler/coreSyn/CoreFVs.hs
@@ -393,7 +393,6 @@ orphNamesOfCo (AxiomRuleCo _ cs)    = orphNamesOfCos cs
 orphNamesOfCo (HoleCo _)            = emptyNameSet
 
 orphNamesOfProv :: UnivCoProvenance -> NameSet
-orphNamesOfProv UnsafeCoerceProv    = emptyNameSet
 orphNamesOfProv (PhantomProv co)    = orphNamesOfCo co
 orphNamesOfProv (ProofIrrelProv co) = orphNamesOfCo co
 orphNamesOfProv (PluginProv _)      = emptyNameSet
diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index c81d754131..aa31aed0b5 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -84,7 +84,7 @@ Core Lint is the type-checker for Core. Using it, we get the following guarantee
 
 If all of:
 1. Core Lint passes,
-2. there are no unsafe coercions (i.e. UnsafeCoerceProv),
+2. there are no unsafe coercions (i.e. unsafeEqualityProof),
 3. all plugin-supplied coercions (i.e. PluginProv) are valid, and
 4. all case-matches are complete
 then running the compiled program will not seg-fault, assuming no bugs downstream
@@ -494,18 +494,23 @@ hence the `TopLevelFlag` on `tcPragExpr` in GHC.IfaceToCore.
 
 -}
 
-lintUnfolding :: DynFlags
+lintUnfolding :: Bool           -- True <=> is a compulsory unfolding
+              -> DynFlags
               -> SrcLoc
               -> VarSet         -- Treat these as in scope
               -> CoreExpr
               -> Maybe MsgDoc   -- Nothing => OK
 
-lintUnfolding dflags locn vars expr
+lintUnfolding is_compulsory dflags locn vars expr
   | isEmptyBag errs = Nothing
   | otherwise       = Just (pprMessageBag errs)
   where
     in_scope = mkInScopeSet vars
-    (_warns, errs) = initL dflags defaultLintFlags in_scope linter
+    (_warns, errs) = initL dflags defaultLintFlags in_scope $
+                     if is_compulsory
+                       -- See Note [Checking for levity polymorphism]
+                     then noLPChecks linter
+                     else linter
     linter = addLoc (ImportedUnfolding locn) $
              lintCoreExpr expr
 
@@ -683,7 +688,10 @@ lintIdUnfolding :: Id -> Type -> Unfolding -> LintM ()
 lintIdUnfolding bndr bndr_ty uf
   | isStableUnfolding uf
   , Just rhs <- maybeUnfoldingTemplate uf
-  = do { ty <- lintRhs bndr rhs
+  = do { ty <- if isCompulsoryUnfolding uf
+               then noLPChecks $ lintRhs bndr rhs
+                     -- See Note [Checking for levity polymorphism]
+               else lintRhs bndr rhs
        ; ensureEqTys bndr_ty ty (mkRhsMsg bndr (text "unfolding") ty) }
 lintIdUnfolding  _ _ _
   = return ()       -- Do not Lint unstable unfoldings, because that leads
@@ -699,6 +707,23 @@ that form a mutually recursive group.  Only after a round of
 simplification are they unravelled.  So we suppress the test for
 the desugarer.
 
+Note [Checking for levity polymorphism]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We ordinarily want to check for bad levity polymorphism. See
+Note [Levity polymorphism invariants] in CoreSyn. However, we do *not*
+want to do this in a compulsory unfolding. Compulsory unfoldings arise
+only internally, for things like newtype wrappers, dictionaries, and
+(notably) unsafeCoerce#. These might legitimately be levity-polymorphic;
+indeed levity-polyorphic unfoldings are a primary reason for the
+very existence of compulsory unfoldings (we can't compile code for
+the original, levity-poly, binding).
+
+It is vitally important that we do levity-polymorphism checks *after*
+performing the unfolding, but not beforehand. This is all safe because
+we will check any unfolding after it has been unfolded; checking the
+unfolding beforehand is merely an optimization, and one that actively
+hurts us here.
+
 ************************************************************************
 *                                                                      *
 \subsection[lintCoreExpr]{lintCoreExpr}
@@ -997,7 +1022,8 @@ lintCoreArg fun_ty (Type arg_ty)
 lintCoreArg fun_ty arg
   = do { arg_ty <- markAllJoinsBad $ lintCoreExpr arg
            -- See Note [Levity polymorphism invariants] in CoreSyn
-       ; lintL (not (isTypeLevPoly arg_ty))
+       ; flags <- getLintFlags
+       ; lintL (not (lf_check_levity_poly flags) || not (isTypeLevPoly arg_ty))
            (text "Levity-polymorphic argument:" <+>
              (ppr arg <+> dcolon <+> parens (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))))
           -- check for levity polymorphism first, because otherwise isUnliftedType panics
@@ -1055,10 +1081,6 @@ lintTyKind :: OutTyVar -> OutType -> LintM ()
 -- If you edit this function, you may need to update the GHC formalism
 -- See Note [GHC Formalism]
 lintTyKind tyvar arg_ty
-        -- Arg type might be boxed for a function with an uncommitted
-        -- tyvar; notably this is used so that we can give
-        --      error :: forall a:*. String -> a
-        -- and then apply it to both boxed and unboxed types.
   = do { arg_kind <- lintType arg_ty
        ; unless (arg_kind `eqType` tyvar_kind)
                 (addErrL (mkKindErrMsg tyvar arg_ty $$ (text "Linted Arg kind:" <+> ppr arg_kind))) }
@@ -1286,7 +1308,7 @@ lintIdBndr top_lvl bind_site id linterF
                     lintInTy (idType id)
 
           -- See Note [Levity polymorphism invariants] in CoreSyn
-       ; lintL (isJoinId id || not (isKindLevPoly k))
+       ; lintL (isJoinId id || not (lf_check_levity_poly flags) || not (isKindLevPoly k))
            (text "Levity-polymorphic binder:" <+>
                  (ppr id <+> dcolon <+> parens (ppr ty <+> dcolon <+> ppr k)))
 
@@ -1819,8 +1841,6 @@ lintCoercion co@(UnivCo prov r ty1 ty2)
   = do { k1 <- lintType ty1
        ; k2 <- lintType ty2
        ; case prov of
-           UnsafeCoerceProv -> return ()  -- no extra checks
-
            PhantomProv kco    -> do { lintRole co Phantom r
                                     ; check_kinds kco k1 k2 }
 
@@ -2095,6 +2115,7 @@ data LintFlags
        , lf_check_inline_loop_breakers :: Bool -- See Note [Checking for INLINE loop breakers]
        , lf_check_static_ptrs :: StaticPtrCheck -- ^ See Note [Checking StaticPtrs]
        , lf_report_unsat_syns :: Bool -- ^ See Note [Linting type synonym applications]
+       , lf_check_levity_poly :: Bool -- See Note [Checking for levity polymorphism]
     }
 
 -- See Note [Checking StaticPtrs]
@@ -2112,6 +2133,7 @@ defaultLintFlags = LF { lf_check_global_ids = False
                       , lf_check_inline_loop_breakers = True
                       , lf_check_static_ptrs = AllowAnywhere
                       , lf_report_unsat_syns = True
+                      , lf_check_levity_poly = True
                       }
 
 newtype LintM a =
@@ -2248,6 +2270,13 @@ setReportUnsat ru thing_inside
     let env' = env { le_flags = (le_flags env) { lf_report_unsat_syns = ru } }
     in unLintM thing_inside env' errs
 
+-- See Note [Checking for levity polymorphism]
+noLPChecks :: LintM a -> LintM a
+noLPChecks thing_inside
+  = LintM $ \env errs ->
+    let env' = env { le_flags = (le_flags env) { lf_check_levity_poly = False } }
+    in unLintM thing_inside env' errs
+
 getLintFlags :: LintM LintFlags
 getLintFlags = LintM $ \ env errs -> (Just (le_flags env), errs)
 
diff --git a/compiler/coreSyn/CoreOpt.hs b/compiler/coreSyn/CoreOpt.hs
index 2c775353be..1f94e5b9dc 100644
--- a/compiler/coreSyn/CoreOpt.hs
+++ b/compiler/coreSyn/CoreOpt.hs
@@ -28,7 +28,7 @@ import CoreSyn
 import CoreSubst
 import CoreUtils
 import CoreFVs
-import {-#SOURCE #-} CoreUnfold ( mkUnfolding )
+import {-# SOURCE #-} CoreUnfold ( mkUnfolding )
 import MkCore ( FloatBind(..) )
 import PprCore  ( pprCoreBindings, pprRules )
 import OccurAnal( occurAnalyseExpr, occurAnalysePgm )
diff --git a/compiler/coreSyn/CoreSyn.hs b/compiler/coreSyn/CoreSyn.hs
index 72c7e5211a..6758cebbee 100644
--- a/compiler/coreSyn/CoreSyn.hs
+++ b/compiler/coreSyn/CoreSyn.hs
@@ -593,11 +593,7 @@ this exhaustive list can be empty!
   because x might raise an exception, and *that*'s what we want to see!
   (#6067 is an example.) To preserve semantics we'd have to say
      x `seq` error Bool "Inaccessible case"
-  but the 'seq' is just a case, so we are back to square 1.  Or I suppose
-  we could say
-     x |> UnsafeCoerce T Bool
-  but that loses all trace of the fact that this originated with an empty
-  set of alternatives.
+  but the 'seq' is just such a case, so we are back to square 1.
 
 * We can use the empty-alternative construct to coerce error values from
   one type to another.  For example
diff --git a/compiler/coreSyn/CoreUnfold.hs-boot b/compiler/coreSyn/CoreUnfold.hs-boot
index da50fbf75c..9f298f7d9d 100644
--- a/compiler/coreSyn/CoreUnfold.hs-boot
+++ b/compiler/coreSyn/CoreUnfold.hs-boot
@@ -1,11 +1,13 @@
 module CoreUnfold (
-        mkUnfolding
+        mkUnfolding, mkInlineUnfolding
     ) where
 
 import GhcPrelude
 import CoreSyn
 import DynFlags
 
+mkInlineUnfolding :: CoreExpr -> Unfolding
+
 mkUnfolding :: DynFlags
             -> UnfoldingSource
             -> Bool
diff --git a/compiler/coreSyn/PprCore.hs b/compiler/coreSyn/PprCore.hs
index 44d7fac878..6a08b4a442 100644
--- a/compiler/coreSyn/PprCore.hs
+++ b/compiler/coreSyn/PprCore.hs
@@ -462,6 +462,50 @@ pprIdBndrInfo info
           , (has_lbv , text "OS=" <> ppr lbv_info)
           ]
 
+instance Outputable IdInfo where
+  ppr info = showAttributes
+    [ (has_prag,         text "InlPrag=" <> pprInlineDebug prag_info)
+    , (has_occ,          text "Occ=" <> ppr occ_info)
+    , (has_dmd,          text "Dmd=" <> ppr dmd_info)
+    , (has_lbv ,         text "OS=" <> ppr lbv_info)
+    , (has_arity,        text "Arity=" <> int arity)
+    , (has_called_arity, text "CallArity=" <> int called_arity)
+    , (has_caf_info,     text "Caf=" <> ppr caf_info)
+    , (has_str_info,     text "Str=" <> pprStrictness str_info)
+    , (has_unf,          text "Unf=" <> ppr unf_info)
+    , (has_rules,        text "RULES:" <+> vcat (map pprRule rules))
+    ]
+    where
+      prag_info = inlinePragInfo info
+      has_prag  = not (isDefaultInlinePragma prag_info)
+
+      occ_info  = occInfo info
+      has_occ   = not (isManyOccs occ_info)
+
+      dmd_info  = demandInfo info
+      has_dmd   = not $ isTopDmd dmd_info
+
+      lbv_info  = oneShotInfo info
+      has_lbv   = not (hasNoOneShotInfo lbv_info)
+
+      arity = arityInfo info
+      has_arity = arity /= 0
+
+      called_arity = callArityInfo info
+      has_called_arity = called_arity /= 0
+
+      caf_info = cafInfo info
+      has_caf_info = not (mayHaveCafRefs caf_info)
+
+      str_info = strictnessInfo info
+      has_str_info = not (isTopSig str_info)
+
+      unf_info = unfoldingInfo info
+      has_unf = hasSomeUnfolding unf_info
+
+      rules = ruleInfoRules (ruleInfo info)
+      has_rules = not (null rules)
+
 {-
 -----------------------------------------------------
 --      IdDetails and IdInfo
diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index 6b066e3208..f5e2fd93aa 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -4755,6 +4755,7 @@ impliedXFlags
 -- Make sure to note whether a flag is implied by -O0, -O or -O2.
 
 optLevelFlags :: [([Int], GeneralFlag)]
+-- Default settings of flags, before any command-line overrides
 optLevelFlags -- see Note [Documenting optimisation flags]
   = [ ([0,1,2], Opt_DoLambdaEtaExpansion)
     , ([0,1,2], Opt_DoEtaReduction)       -- See Note [Eta-reduction in -O0]
@@ -4774,8 +4775,13 @@ optLevelFlags -- see Note [Documenting optimisation flags]
     , ([1,2],   Opt_CSE)
     , ([1,2],   Opt_StgCSE)
     , ([2],     Opt_StgLiftLams)
-    , ([1,2],   Opt_EnableRewriteRules)  -- Off for -O0; see Note [Scoping for Builtin rules]
-                                         --              in PrelRules
+
+    , ([1,2],   Opt_EnableRewriteRules)
+          -- Off for -O0.   Otherwise we desugar list literals
+          -- to 'build' but don't run the simplifier passes that
+          -- would rewrite them back to cons cells!  This seems
+          -- silly, and matters for the GHCi debugger.
+
     , ([1,2],   Opt_FloatIn)
     , ([1,2],   Opt_FullLaziness)
     , ([1,2],   Opt_IgnoreAsserts)
diff --git a/compiler/main/HscMain.hs b/compiler/main/HscMain.hs
index aa4a6a4875..709999e06a 100644
--- a/compiler/main/HscMain.hs
+++ b/compiler/main/HscMain.hs
@@ -1895,7 +1895,7 @@ hscCompileCoreExpr' hsc_env srcspan ds_expr
     = do { let dflags = hsc_dflags hsc_env
 
            {- Simplify it -}
-         ; simpl_expr <- simplifyExpr dflags ds_expr
+         ; simpl_expr <- simplifyExpr hsc_env ds_expr
 
            {- Tidy it (temporary, until coreSat does cloning) -}
          ; let tidy_expr = tidyExpr emptyTidyEnv simpl_expr
diff --git a/compiler/main/HscTypes.hs b/compiler/main/HscTypes.hs
index 223b566031..25b2f3e172 100644
--- a/compiler/main/HscTypes.hs
+++ b/compiler/main/HscTypes.hs
@@ -2276,28 +2276,28 @@ lookupTypeHscEnv hsc_env name = do
     hpt = hsc_HPT hsc_env
 
 -- | Get the 'TyCon' from a 'TyThing' if it is a type constructor thing. Panics otherwise
-tyThingTyCon :: TyThing -> TyCon
+tyThingTyCon :: HasDebugCallStack => TyThing -> TyCon
 tyThingTyCon (ATyCon tc) = tc
 tyThingTyCon other       = pprPanic "tyThingTyCon" (ppr other)
 
 -- | Get the 'CoAxiom' from a 'TyThing' if it is a coercion axiom thing. Panics otherwise
-tyThingCoAxiom :: TyThing -> CoAxiom Branched
+tyThingCoAxiom :: HasDebugCallStack => TyThing -> CoAxiom Branched
 tyThingCoAxiom (ACoAxiom ax) = ax
 tyThingCoAxiom other         = pprPanic "tyThingCoAxiom" (ppr other)
 
 -- | Get the 'DataCon' from a 'TyThing' if it is a data constructor thing. Panics otherwise
-tyThingDataCon :: TyThing -> DataCon
+tyThingDataCon :: HasDebugCallStack => TyThing -> DataCon
 tyThingDataCon (AConLike (RealDataCon dc)) = dc
 tyThingDataCon other                       = pprPanic "tyThingDataCon" (ppr other)
 
 -- | Get the 'ConLike' from a 'TyThing' if it is a data constructor thing.
 -- Panics otherwise
-tyThingConLike :: TyThing -> ConLike
+tyThingConLike :: HasDebugCallStack => TyThing -> ConLike
 tyThingConLike (AConLike dc) = dc
 tyThingConLike other         = pprPanic "tyThingConLike" (ppr other)
 
 -- | Get the 'Id' from a 'TyThing' if it is a id *or* data constructor thing. Panics otherwise
-tyThingId :: TyThing -> Id
+tyThingId :: HasDebugCallStack => TyThing -> Id
 tyThingId (AnId id)                   = id
 tyThingId (AConLike (RealDataCon dc)) = dataConWrapId dc
 tyThingId other                       = pprPanic "tyThingId" (ppr other)
diff --git a/compiler/prelude/PrelNames.hs b/compiler/prelude/PrelNames.hs
index 095b853927..3873dbceeb 100644
--- a/compiler/prelude/PrelNames.hs
+++ b/compiler/prelude/PrelNames.hs
@@ -463,6 +463,12 @@ basicKnownKeyNames
         , typeErrorVAppendDataConName
         , typeErrorShowTypeDataConName
 
+        -- Unsafe coercion proofs
+        , unsafeEqualityProofName
+        , unsafeEqualityTyConName
+        , unsafeReflDataConName
+        , unsafeCoercePrimName
+        , unsafeCoerceName
     ]
 
 genericTyConNames :: [Name]
@@ -511,7 +517,7 @@ gHC_PRIM, gHC_TYPES, gHC_GENERICS, gHC_MAGIC,
     rEAD_PREC, lEX, gHC_INT, gHC_WORD, mONAD, mONAD_FIX, mONAD_ZIP, mONAD_FAIL,
     aRROW, cONTROL_APPLICATIVE, gHC_DESUGAR, rANDOM, gHC_EXTS,
     cONTROL_EXCEPTION_BASE, gHC_TYPELITS, gHC_TYPENATS, dATA_TYPE_EQUALITY,
-    dATA_COERCE, dEBUG_TRACE :: Module
+    dATA_COERCE, dEBUG_TRACE, uNSAFE_COERCE :: Module
 
 gHC_PRIM        = mkPrimModule (fsLit "GHC.Prim")   -- Primitive types and values
 gHC_TYPES       = mkPrimModule (fsLit "GHC.Types")
@@ -574,6 +580,7 @@ gHC_TYPENATS    = mkBaseModule (fsLit "GHC.TypeNats")
 dATA_TYPE_EQUALITY = mkBaseModule (fsLit "Data.Type.Equality")
 dATA_COERCE     = mkBaseModule (fsLit "Data.Coerce")
 dEBUG_TRACE     = mkBaseModule (fsLit "Debug.Trace")
+uNSAFE_COERCE   = mkBaseModule (fsLit "Unsafe.Coerce")
 
 gHC_SRCLOC :: Module
 gHC_SRCLOC = mkBaseModule (fsLit "GHC.SrcLoc")
@@ -1319,7 +1326,14 @@ typeErrorVAppendDataConName =
 typeErrorShowTypeDataConName =
   dcQual gHC_TYPELITS (fsLit "ShowType") typeErrorShowTypeDataConKey
 
-
+-- Unsafe coercion proofs
+unsafeEqualityProofName, unsafeEqualityTyConName, unsafeCoercePrimName,
+  unsafeCoerceName, unsafeReflDataConName :: Name
+unsafeEqualityProofName = varQual uNSAFE_COERCE (fsLit "unsafeEqualityProof") unsafeEqualityProofIdKey
+unsafeEqualityTyConName = tcQual uNSAFE_COERCE (fsLit "UnsafeEquality") unsafeEqualityTyConKey
+unsafeReflDataConName   = dcQual uNSAFE_COERCE (fsLit "UnsafeRefl")     unsafeReflDataConKey
+unsafeCoercePrimName    = varQual uNSAFE_COERCE (fsLit "unsafeCoerce#") unsafeCoercePrimIdKey
+unsafeCoerceName        = varQual uNSAFE_COERCE (fsLit "unsafeCoerce")  unsafeCoerceIdKey
 
 -- Dynamic
 toDynName :: Name
@@ -1891,6 +1905,11 @@ someTypeRepDataConKey = mkPreludeTyConUnique 189
 typeSymbolAppendFamNameKey :: Unique
 typeSymbolAppendFamNameKey = mkPreludeTyConUnique 190
 
+-- Unsafe equality
+unsafeEqualityTyConKey :: Unique
+unsafeEqualityTyConKey = mkPreludeTyConUnique 191
+
+
 ---------------- Template Haskell -------------------
 --      THNames.hs: USES TyConUniques 200-299
 -----------------------------------------------------
@@ -2060,6 +2079,9 @@ typeLitSymbolDataConKey, typeLitNatDataConKey :: Unique
 typeLitSymbolDataConKey   = mkPreludeDataConUnique 112
 typeLitNatDataConKey      = mkPreludeDataConUnique 113
 
+-- Unsafe equality
+unsafeReflDataConKey :: Unique
+unsafeReflDataConKey      = mkPreludeDataConUnique 114
 
 ---------------- Template Haskell -------------------
 --      THNames.hs: USES DataUniques 200-250
@@ -2111,11 +2133,10 @@ typeErrorIdKey                = mkPreludeMiscIdUnique 22
 divIntIdKey                   = mkPreludeMiscIdUnique 23
 modIntIdKey                   = mkPreludeMiscIdUnique 24
 
-unsafeCoerceIdKey, concatIdKey, filterIdKey, zipIdKey, bindIOIdKey,
-    returnIOIdKey, newStablePtrIdKey,
+concatIdKey, filterIdKey, zipIdKey,
+    bindIOIdKey, returnIOIdKey, newStablePtrIdKey,
     printIdKey, failIOIdKey, nullAddrIdKey, voidArgIdKey,
     fstIdKey, sndIdKey, otherwiseIdKey, assertIdKey :: Unique
-unsafeCoerceIdKey             = mkPreludeMiscIdUnique 30
 concatIdKey                   = mkPreludeMiscIdUnique 31
 filterIdKey                   = mkPreludeMiscIdUnique 32
 zipIdKey                      = mkPreludeMiscIdUnique 33
@@ -2409,6 +2430,12 @@ mkNaturalIdKey          = mkPreludeMiscIdUnique 567
 naturalSDataConKey      = mkPreludeMiscIdUnique 568
 wordToNaturalIdKey      = mkPreludeMiscIdUnique 569
 
+-- Unsafe coercion proofs
+unsafeEqualityProofIdKey, unsafeCoercePrimIdKey, unsafeCoerceIdKey :: Unique
+unsafeEqualityProofIdKey = mkPreludeMiscIdUnique 570
+unsafeCoercePrimIdKey    = mkPreludeMiscIdUnique 571
+unsafeCoerceIdKey        = mkPreludeMiscIdUnique 572
+
 {-
 ************************************************************************
 *                                                                      *
diff --git a/compiler/prelude/PrelRules.hs b/compiler/prelude/PrelRules.hs
index 0f8836e3ef..72d77b07e0 100644
--- a/compiler/prelude/PrelRules.hs
+++ b/compiler/prelude/PrelRules.hs
@@ -14,7 +14,7 @@ ToDo:
 
 {-# LANGUAGE CPP, RankNTypes, PatternSynonyms, ViewPatterns, RecordWildCards,
     DeriveFunctor #-}
-{-# OPTIONS_GHC -optc-DNON_POSIX_SOURCE #-}
+{-# OPTIONS_GHC -optc-DNON_POSIX_SOURCE -Wno-incomplete-uni-patterns #-}
 
 module PrelRules
    ( primOpRules
@@ -40,7 +40,7 @@ import TysPrim
 import TyCon       ( tyConDataCons_maybe, isAlgTyCon, isEnumerationTyCon
                    , isNewTyCon, unwrapNewTyCon_maybe, tyConDataCons
                    , tyConFamilySize )
-import DataCon     ( dataConTagZ, dataConTyCon, dataConWorkId )
+import DataCon     ( dataConTagZ, dataConTyCon, dataConWrapId, dataConWorkId )
 import CoreUtils   ( cheapEqExpr, cheapEqExpr', exprIsHNF, exprType, stripTicksTop, stripTicksTopT, mkTicks )
 import CoreUnfold  ( exprIsConApp_maybe )
 import Type
@@ -777,23 +777,26 @@ but that is only a historical accident.
 mkBasicRule :: Name -> Int -> RuleM CoreExpr -> CoreRule
 -- Gives the Rule the same name as the primop itself
 mkBasicRule op_name n_args rm
-  = BuiltinRule { ru_name = occNameFS (nameOccName op_name),
-                  ru_fn = op_name,
+  = BuiltinRule { ru_name  = occNameFS (nameOccName op_name),
+                  ru_fn    = op_name,
                   ru_nargs = n_args,
-                  ru_try = \ dflags in_scope _ -> runRuleM rm dflags in_scope }
+                  ru_try   = runRuleM rm }
 
 newtype RuleM r = RuleM
-  { runRuleM :: DynFlags -> InScopeEnv -> [CoreExpr] -> Maybe r }
+  { runRuleM :: DynFlags -> InScopeEnv -> Id -> [CoreExpr] -> Maybe r }
   deriving (Functor)
 
 instance Applicative RuleM where
-    pure x = RuleM $ \_ _ _ -> Just x
+    pure x = RuleM $ \_ _ _ _ -> Just x
     (<*>) = ap
 
 instance Monad RuleM where
-  RuleM f >>= g = RuleM $ \dflags iu e -> case f dflags iu e of
-    Nothing -> Nothing
-    Just r -> runRuleM (g r) dflags iu e
+  RuleM f >>= g
+    = RuleM $ \dflags iu fn args ->
+              case f dflags iu fn args of
+                Nothing -> Nothing
+                Just r  -> runRuleM (g r) dflags iu fn args
+
 #if !MIN_VERSION_base(4,13,0)
   fail = MonadFail.fail
 #endif
@@ -802,14 +805,14 @@ instance MonadFail.MonadFail RuleM where
     fail _ = mzero
 
 instance Alternative RuleM where
-  empty = RuleM $ \_ _ _ -> Nothing
-  RuleM f1 <|> RuleM f2 = RuleM $ \dflags iu args ->
-    f1 dflags iu args <|> f2 dflags iu args
+  empty = RuleM $ \_ _ _ _ -> Nothing
+  RuleM f1 <|> RuleM f2 = RuleM $ \dflags iu fn args ->
+    f1 dflags iu fn args <|> f2 dflags iu fn args
 
 instance MonadPlus RuleM
 
 instance HasDynFlags RuleM where
-    getDynFlags = RuleM $ \dflags _ _ -> Just dflags
+    getDynFlags = RuleM $ \dflags _ _ _ -> Just dflags
 
 liftMaybe :: Maybe a -> RuleM a
 liftMaybe Nothing = mzero
@@ -835,15 +838,18 @@ removeOp32 = do
       mzero
 
 getArgs :: RuleM [CoreExpr]
-getArgs = RuleM $ \_ _ args -> Just args
+getArgs = RuleM $ \_ _ _ args -> Just args
 
 getInScopeEnv :: RuleM InScopeEnv
-getInScopeEnv = RuleM $ \_ iu _ -> Just iu
+getInScopeEnv = RuleM $ \_ iu _ _ -> Just iu
+
+getFunction :: RuleM Id
+getFunction = RuleM $ \_ _ fn _ -> Just fn
 
 -- return the n-th argument of this rule, if it is a literal
 -- argument indices start from 0
 getLiteral :: Int -> RuleM Literal
-getLiteral n = RuleM $ \_ _ exprs -> case drop n exprs of
+getLiteral n = RuleM $ \_ _ _ exprs -> case drop n exprs of
   (Lit l:_) -> Just l
   _ -> Nothing
 
@@ -1118,14 +1124,35 @@ is:
   by PrelRules.caseRules; see Note [caseRules for dataToTag]
 
 See #15696 for a long saga.
+-}
+
+{- *********************************************************************
+*                                                                      *
+             unsafeEqualityProof
+*                                                                      *
+********************************************************************* -}
 
+-- unsafeEqualityProof k t t  ==>  UnsafeRefl (Refl t)
+-- That is, if the two types are equal, it's not unsafe!
 
-************************************************************************
+unsafeEqualityProofRule :: RuleM CoreExpr
+unsafeEqualityProofRule
+  = do { [Type rep, Type t1, Type t2] <- getArgs
+       ; guard (t1 `eqType` t2)
+       ; fn <- getFunction
+       ; let (_, ue) = splitForAllTys (idType fn)
+             tc      = tyConAppTyCon ue  -- tycon:    UnsafeEquality
+             (dc:_)  = tyConDataCons tc  -- data con: UnsafeRefl
+             -- UnsafeRefl :: forall (r :: RuntimeRep) (a :: TYPE r).
+             --               UnsafeEquality r a a
+       ; return (mkTyApps (Var (dataConWrapId dc)) [rep, t1]) }
+
+
+{- *********************************************************************
 *                                                                      *
-\subsection{Rules for seq# and spark#}
+             Rules for seq# and spark#
 *                                                                      *
-************************************************************************
--}
+********************************************************************* -}
 
 {- Note [seq# magic]
 ~~~~~~~~~~~~~~~~~~~~
@@ -1218,13 +1245,11 @@ Then a rewrite would give
         ....and lower down...
         eqString = ...
 
-and lo, eqString is not in scope.  This only really matters when we get to code
-generation.  With -O we do a GlomBinds step that does a new SCC analysis on the whole
-set of bindings, which sorts out the dependency.  Without -O we don't do any rule
-rewriting so again we are fine.
-
-(This whole thing doesn't show up for non-built-in rules because their dependencies
-are explicit.)
+and lo, eqString is not in scope.  This only really matters when we
+get to code generation.  But the occurrence analyser does a GlomBinds
+step when necessary, that does a new SCC analysis on the whole set of
+bindings (see occurAnalysePgm), which sorts out the dependency, so all
+is fine.
 -}
 
 builtinRules :: [CoreRule]
@@ -1239,6 +1264,9 @@ builtinRules
                    ru_nargs = 2, ru_try = \_ _ _ -> match_inline },
      BuiltinRule { ru_name = fsLit "MagicDict", ru_fn = idName magicDictId,
                    ru_nargs = 4, ru_try = \_ _ _ -> match_magicDict },
+
+     mkBasicRule unsafeEqualityProofName 3 unsafeEqualityProofRule,
+
      mkBasicRule divIntName 2 $ msum
         [ nonZeroLit 1 >> binaryLit (intOp2 div)
         , leftZero zeroi
@@ -1248,6 +1276,7 @@ builtinRules
           dflags <- getDynFlags
           return $ Var (mkPrimOpId ISraOp) `App` arg `App` mkIntVal dflags n
         ],
+
      mkBasicRule modIntName 2 $ msum
         [ nonZeroLit 1 >> binaryLit (intOp2 mod)
         , leftZero zeroi
diff --git a/compiler/prelude/TysPrim.hs b/compiler/prelude/TysPrim.hs
index acf71c999a..e50030b0f6 100644
--- a/compiler/prelude/TysPrim.hs
+++ b/compiler/prelude/TysPrim.hs
@@ -376,6 +376,8 @@ runtimeRep1Ty = mkTyVarTy runtimeRep1TyVar
 runtimeRep2Ty = mkTyVarTy runtimeRep2TyVar
 
 openAlphaTyVar, openBetaTyVar :: TyVar
+-- alpha :: TYPE r1
+-- beta  :: TYPE r2
 [openAlphaTyVar,openBetaTyVar]
   = mkTemplateTyVars [tYPE runtimeRep1Ty, tYPE runtimeRep2Ty]
 
@@ -459,7 +461,7 @@ generator never has to manipulate a value of type 'a :: TYPE rr'.
 * error :: forall (rr:RuntimeRep) (a:TYPE rr). String -> a
   Code generator never has to manipulate the return value.
 
-* unsafeCoerce#, defined in MkId.unsafeCoerceId:
+* unsafeCoerce#, defined in Desugar.mkUnsafeCoercePair:
   Always inlined to be a no-op
      unsafeCoerce# :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
                              (a :: TYPE r1) (b :: TYPE r2).
diff --git a/compiler/prelude/TysWiredIn.hs b/compiler/prelude/TysWiredIn.hs
index a14fcc0732..0ea3ec2dd7 100644
--- a/compiler/prelude/TysWiredIn.hs
+++ b/compiler/prelude/TysWiredIn.hs
@@ -126,7 +126,6 @@ module TysWiredIn (
         int64ElemRepDataConTy, word8ElemRepDataConTy, word16ElemRepDataConTy,
         word32ElemRepDataConTy, word64ElemRepDataConTy, floatElemRepDataConTy,
         doubleElemRepDataConTy
-
     ) where
 
 #include "HsVersions.h"
@@ -155,8 +154,7 @@ import RdrName
 import Name
 import NameEnv          ( NameEnv, mkNameEnv, lookupNameEnv, lookupNameEnv_NF )
 import NameSet          ( NameSet, mkNameSet, elemNameSet )
-import BasicTypes       ( Arity, Boxity(..), TupleSort(..), ConTagZ,
-                          SourceText(..) )
+import BasicTypes
 import ForeignCall
 import SrcLoc           ( noSrcSpan )
 import Unique
@@ -565,6 +563,13 @@ pcDataConWithFixity' :: Bool -> Name -> Unique -> RuntimeRepInfo
                      -> [Type] -> TyCon -> DataCon
 -- The Name should be in the DataName name space; it's the name
 -- of the DataCon itself.
+--
+-- IMPORTANT NOTE:
+--    if you try to wire-in a /GADT/ data constructor you will
+--    find it hard (we did).  You will need wrapper and worker
+--    Names, a DataConBoxer, DataConRep, EqSpec, etc.
+--    Try hard not to wire-in GADT data types. You will live
+--    to regret doing so (we do).
 
 pcDataConWithFixity' declared_infix dc_name wrk_key rri
                      tyvars ex_tyvars user_tyvars arg_tys tycon
@@ -1513,12 +1518,7 @@ mkListTy :: Type -> Type
 mkListTy ty = mkTyConApp listTyCon [ty]
 
 listTyCon :: TyCon
-listTyCon =
-  buildAlgTyCon listTyConName alpha_tyvar [Representational]
-                Nothing []
-                (mkDataTyConRhs [nilDataCon, consDataCon])
-                False
-                (VanillaAlgTyCon $ mkPrelTyConRepName listTyConName)
+listTyCon = pcTyCon listTyConName Nothing [alphaTyVar] [nilDataCon, consDataCon]
 
 -- See also Note [Empty lists] in GHC.Hs.Expr.
 nilDataCon :: DataCon
diff --git a/compiler/simplCore/SimplCore.hs b/compiler/simplCore/SimplCore.hs
index 4c7e509f4c..35fd744b84 100644
--- a/compiler/simplCore/SimplCore.hs
+++ b/compiler/simplCore/SimplCore.hs
@@ -169,7 +169,7 @@ getCoreToDo dflags
     simpl_gently = CoreDoSimplify max_iter
                        (base_mode { sm_phase = InitialPhase
                                   , sm_names = ["Gentle"]
-                                  , sm_rules = rules_on   -- Note [RULEs enabled in SimplGently]
+                                  , sm_rules = rules_on   -- Note [RULEs enabled in InitialPhase]
                                   , sm_inline = True
                                               -- See Note [Inline in InitialPhase]
                                   , sm_case_case = False })
@@ -381,9 +381,10 @@ when I made this change:
    perf/compiler/T9872b.run           T9872b [stat too good] (normal)
    perf/compiler/T9872d.run           T9872d [stat too good] (normal)
 
-Note [RULEs enabled in SimplGently]
+Note [RULEs enabled in InitialPhase]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-RULES are enabled when doing "gentle" simplification.  Two reasons:
+RULES are enabled when doing "gentle" simplification in InitialPhase,
+or with -O0.  Two reasons:
 
   * We really want the class-op cancellation to happen:
         op (df d1 d2) --> $cop3 d1 d2
@@ -557,23 +558,25 @@ observe do_pass = doPassM $ \binds -> do
 ************************************************************************
 -}
 
-simplifyExpr :: DynFlags -- includes spec of what core-to-core passes to do
+simplifyExpr :: HscEnv -- includes spec of what core-to-core passes to do
              -> CoreExpr
              -> IO CoreExpr
 -- simplifyExpr is called by the driver to simplify an
 -- expression typed in at the interactive prompt
---
--- Also used by Template Haskell
-simplifyExpr dflags expr
+simplifyExpr hsc_env expr
   = withTiming dflags (text "Simplify [expr]") (const ()) $
-    do  {
-        ; us <-  mkSplitUniqSupply 's'
+    do  { eps <- hscEPS hsc_env ;
+        ; let rule_env  = mkRuleEnv (eps_rule_base eps) []
+              fi_env    = ( eps_fam_inst_env eps
+                          , extendFamInstEnvList emptyFamInstEnv $
+                            snd $ ic_instances $ hsc_IC hsc_env )
+              simpl_env = simplEnvForGHCi dflags
 
+        ; us <-  mkSplitUniqSupply 's'
         ; let sz = exprSize expr
 
-        ; (expr', counts) <- initSmpl dflags emptyRuleEnv
-                               emptyFamInstEnvs us sz
-                               (simplExprGently (simplEnvForGHCi dflags) expr)
+        ; (expr', counts) <- initSmpl dflags rule_env fi_env us sz $
+                             simplExprGently simpl_env expr
 
         ; Err.dumpIfSet dflags (dopt Opt_D_dump_simpl_stats dflags)
                   "Simplifier statistics" (pprSimplCount counts)
@@ -584,6 +587,8 @@ simplifyExpr dflags expr
 
         ; return expr'
         }
+  where
+    dflags = hsc_dflags hsc_env
 
 simplExprGently :: SimplEnv -> CoreExpr -> SimplM CoreExpr
 -- Simplifies an expression
@@ -594,7 +599,7 @@ simplExprGently :: SimplEnv -> CoreExpr -> SimplM CoreExpr
 --      (b) the LHS and RHS of a RULE
 --      (c) Template Haskell splices
 --
--- The name 'Gently' suggests that the SimplMode is SimplGently,
+-- The name 'Gently' suggests that the SimplMode is InitialPhase,
 -- and in fact that is so.... but the 'Gently' in simplExprGently doesn't
 -- enforce that; it just simplifies the expression twice
 
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index 21e1ba81ba..193d6b70bb 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -163,7 +163,7 @@ Note [Instances and loop breakers]
   loop-breaker because df_i isn't), op1_i will ironically never be
   inlined.  But this is OK: the recursion breaking happens by way of
   a RULE (the magic ClassOp rule above), and RULES work inside InlineRule
-  unfoldings. See Note [RULEs enabled in SimplGently] in SimplUtils
+  unfoldings. See Note [RULEs enabled in InitialPhase] in SimplUtils
 
 Note [ClassOp/DFun selection]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 85a59b697a..45863e4046 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -1394,7 +1394,6 @@ collect_cand_qtvs_co orig_ty bound = go_co
     go_mco dv MRefl    = return dv
     go_mco dv (MCo co) = go_co dv co
 
-    go_prov dv UnsafeCoerceProv    = return dv
     go_prov dv (PhantomProv co)    = go_co dv co
     go_prov dv (ProofIrrelProv co) = go_co dv co
     go_prov dv (PluginProv _)      = return dv
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index 99cbcf1578..2caee7df9f 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -62,7 +62,6 @@ import GHC.Rename.Types
 import GHC.Rename.Expr
 import GHC.Rename.Utils  ( HsDocContext(..) )
 import GHC.Rename.Fixity ( lookupFixityRn )
-import MkId
 import TysWiredIn ( unitTy, mkListTy )
 import Plugins
 import DynFlags
@@ -2270,51 +2269,57 @@ leaking memory as it is repeatedly queried.
 -- statement in the form 'IO [()]'.
 tcGhciStmts :: [GhciLStmt GhcRn] -> TcM PlanResult
 tcGhciStmts stmts
- = do { ioTyCon <- tcLookupTyCon ioTyConName ;
-        ret_id  <- tcLookupId returnIOName ;            -- return @ IO
-        let {
-            ret_ty      = mkListTy unitTy ;
-            io_ret_ty   = mkTyConApp ioTyCon [ret_ty] ;
+ = do { ioTyCon <- tcLookupTyCon ioTyConName
+      ; ret_id  <- tcLookupId returnIOName             -- return @ IO
+      ; let ret_ty      = mkListTy unitTy
+            io_ret_ty   = mkTyConApp ioTyCon [ret_ty]
             tc_io_stmts = tcStmtsAndThen GhciStmtCtxt tcDoStmt stmts
-                                         (mkCheckExpType io_ret_ty) ;
-            names = collectLStmtsBinders stmts ;
-         } ;
+                                         (mkCheckExpType io_ret_ty)
+            names = collectLStmtsBinders stmts
 
         -- OK, we're ready to typecheck the stmts
-        traceTc "TcRnDriver.tcGhciStmts: tc stmts" empty ;
-        ((tc_stmts, ids), lie) <- captureTopConstraints $
+      ; traceTc "TcRnDriver.tcGhciStmts: tc stmts" empty
+      ; ((tc_stmts, ids), lie) <- captureTopConstraints $
                                   tc_io_stmts $ \ _ ->
-                                  mapM tcLookupId names  ;
+                                  mapM tcLookupId names
                         -- Look up the names right in the middle,
                         -- where they will all be in scope
 
         -- Simplify the context
-        traceTc "TcRnDriver.tcGhciStmts: simplify ctxt" empty ;
-        const_binds <- checkNoErrs (simplifyInteractive lie) ;
+      ; traceTc "TcRnDriver.tcGhciStmts: simplify ctxt" empty
+      ; const_binds <- checkNoErrs (simplifyInteractive lie)
                 -- checkNoErrs ensures that the plan fails if context redn fails
 
-        traceTc "TcRnDriver.tcGhciStmts: done" empty ;
-        let {   -- mk_return builds the expression
-                --      returnIO @ [()] [coerce () x, ..,  coerce () z]
-                --
-                -- Despite the inconvenience of building the type applications etc,
-                -- this *has* to be done in type-annotated post-typecheck form
-                -- because we are going to return a list of *polymorphic* values
-                -- coerced to type (). If we built a *source* stmt
-                --      return [coerce x, ..., coerce z]
-                -- then the type checker would instantiate x..z, and we wouldn't
-                -- get their *polymorphic* values.  (And we'd get ambiguity errs
-                -- if they were overloaded, since they aren't applied to anything.)
-            ret_expr = nlHsApp (nlHsTyApp ret_id [ret_ty])
-                       (noLoc $ ExplicitList unitTy Nothing
-                                                            (map mk_item ids)) ;
-            mk_item id = let ty_args = [idType id, unitTy] in
-                         nlHsApp (nlHsTyApp unsafeCoerceId
-                                   (map getRuntimeRep ty_args ++ ty_args))
-                                 (nlHsVar id) ;
+
+      ; traceTc "TcRnDriver.tcGhciStmts: done" empty
+
+      -- rec_expr is the expression
+      --      returnIO @ [()] [unsafeCoerce# () x, ..,  unsafeCorece# () z]
+      --
+      -- Despite the inconvenience of building the type applications etc,
+      -- this *has* to be done in type-annotated post-typecheck form
+      -- because we are going to return a list of *polymorphic* values
+      -- coerced to type (). If we built a *source* stmt
+      --      return [coerce x, ..., coerce z]
+      -- then the type checker would instantiate x..z, and we wouldn't
+      -- get their *polymorphic* values.  (And we'd get ambiguity errs
+      -- if they were overloaded, since they aren't applied to anything.)
+
+      ; AnId unsafe_coerce_id <- tcLookupGlobal unsafeCoercePrimName
+           -- We use unsafeCoerce# here because of (U11) in
+           -- Note [Implementing unsafeCoerce] in base:Unsafe.Coerce
+
+      ; let ret_expr = nlHsApp (nlHsTyApp ret_id [ret_ty]) $
+                       noLoc $ ExplicitList unitTy Nothing $
+                       map mk_item ids
+
+            mk_item id = unsafe_coerce_id `nlHsTyApp` [ getRuntimeRep (idType id)
+                                                      , getRuntimeRep unitTy
+                                                      , idType id, unitTy]
+                                          `nlHsApp` nlHsVar id
             stmts = tc_stmts ++ [noLoc (mkLastStmt ret_expr)]
-        } ;
-        return (ids, mkHsDictLet (EvBinds const_binds) $
+
+      ; return (ids, mkHsDictLet (EvBinds const_binds) $
                      noLoc (HsDo io_ret_ty GhciStmtCtxt (noLoc stmts)))
     }
 
diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs
index ea848d391f..ed9895074b 100644
--- a/compiler/typecheck/TcSplice.hs
+++ b/compiler/typecheck/TcSplice.hs
@@ -135,7 +135,7 @@ import qualified Data.Map as Map
 import Data.Typeable ( typeOf, Typeable, TypeRep, typeRep )
 import Data.Data (Data)
 import Data.Proxy    ( Proxy (..) )
-import GHC.Exts         ( unsafeCoerce# )
+import Unsafe.Coerce        ( unsafeCoerce )
 
 {-
 ************************************************************************
@@ -777,7 +777,7 @@ convertAnnotationWrapper fhv = do
     else do
       annotation_wrapper <- liftIO $ wormhole dflags fhv
       return $ Right $
-        case unsafeCoerce# annotation_wrapper of
+        case unsafeCoerce annotation_wrapper of
            AnnotationWrapper value | let serialized = toSerialized serializeWithData value ->
                -- Got the value and dictionaries: build the serialized value and
                -- call it a day. We ensure that we seq the entire serialized value
@@ -1231,7 +1231,7 @@ runTH ty fhv = do
     then do
        -- Run it in the local TcM
       hv <- liftIO $ wormhole dflags fhv
-      r <- runQuasi (unsafeCoerce# hv :: TH.Q a)
+      r <- runQuasi (unsafeCoerce hv :: TH.Q a)
       return r
     else
       -- Run it on the server.  For an overview of how TH works with
diff --git a/compiler/typecheck/TcTyDecls.hs b/compiler/typecheck/TcTyDecls.hs
index 9aee045c7e..78104576ab 100644
--- a/compiler/typecheck/TcTyDecls.hs
+++ b/compiler/typecheck/TcTyDecls.hs
@@ -138,7 +138,6 @@ synonymTyConsOfType ty
      go_co (SubCo co)             = go_co co
      go_co (AxiomRuleCo _ cs)     = go_co_s cs
 
-     go_prov UnsafeCoerceProv     = emptyNameEnv
      go_prov (PhantomProv co)     = go_co co
      go_prov (ProofIrrelProv co)  = go_co co
      go_prov (PluginProv _)       = emptyNameEnv
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index 8a8fc3d838..eba05f8386 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -35,7 +35,7 @@ module Coercion (
         mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo, mkFunCo,
         mkForAllCo, mkForAllCos, mkHomoForAllCos,
         mkPhantomCo,
-        mkUnsafeCo, mkHoleCo, mkUnivCo, mkSubCo,
+        mkHoleCo, mkUnivCo, mkSubCo,
         mkAxiomInstCo, mkProofIrrelCo,
         downgradeRole, mkAxiomRuleCo,
         mkGReflRightCo, mkGReflLeftCo, mkCoherenceLeftCo, mkCoherenceRightCo,
@@ -637,8 +637,7 @@ it is not absolutely critical that setNominalRole_maybe be complete.
 
 Note that setNominalRole_maybe will never upgrade a phantom UnivCo. Phantom
 UnivCos are perfectly type-safe, whereas representational and nominal ones are
-not. Indeed, `unsafeCoerce` is implemented via a representational UnivCo.
-(Nominal ones are no worse than representational ones, so this function *will*
+not. (Nominal ones are no worse than representational ones, so this function *will*
 change a UnivCo Representational to a UnivCo Nominal.)
 
 Conal Elliott also came across a need for this function while working with the
@@ -936,14 +935,6 @@ mkAxInstLHS ax index tys cos
 mkUnbranchedAxInstLHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
 mkUnbranchedAxInstLHS ax = mkAxInstLHS ax 0
 
--- | Manufacture an unsafe coercion from thin air.
---   Currently (May 14) this is used only to implement the
---   @unsafeCoerce#@ primitive.  Optimise by pushing
---   down through type constructors.
-mkUnsafeCo :: Role -> Type -> Type -> Coercion
-mkUnsafeCo role ty1 ty2
-  = mkUnivCo UnsafeCoerceProv role ty1 ty2
-
 -- | Make a coercion from a coercion hole
 mkHoleCo :: CoercionHole -> Coercion
 mkHoleCo h = HoleCo h
@@ -1281,8 +1272,7 @@ setNominalRole_maybe r co
     setNominalRole_maybe_helper (InstCo co arg)
       = InstCo <$> setNominalRole_maybe_helper co <*> pure arg
     setNominalRole_maybe_helper (UnivCo prov _ co1 co2)
-      | case prov of UnsafeCoerceProv -> True   -- it's always unsafe
-                     PhantomProv _    -> False  -- should always be phantom
+      | case prov of PhantomProv _    -> False  -- should always be phantom
                      ProofIrrelProv _ -> True   -- it's always safe
                      PluginProv _     -> False  -- who knows? This choice is conservative.
       = Just $ UnivCo prov Nominal co1 co2
@@ -1388,7 +1378,6 @@ promoteCoercion co = case co of
     AxiomInstCo {} -> mkKindCo co
     AxiomRuleCo {} -> mkKindCo co
 
-    UnivCo UnsafeCoerceProv _ t1 t2   -> mkUnsafeCo Nominal (typeKind t1) (typeKind t2)
     UnivCo (PhantomProv kco) _ _ _    -> kco
     UnivCo (ProofIrrelProv kco) _ _ _ -> kco
     UnivCo (PluginProv _) _ _ _       -> mkKindCo co
@@ -2145,7 +2134,6 @@ seqCo (SubCo co)                = seqCo co
 seqCo (AxiomRuleCo _ cs)        = seqCos cs
 
 seqProv :: UnivCoProvenance -> ()
-seqProv UnsafeCoerceProv    = ()
 seqProv (PhantomProv co)    = seqCo co
 seqProv (ProofIrrelProv co) = seqCo co
 seqProv (PluginProv _)      = ()
diff --git a/compiler/types/Coercion.hs-boot b/compiler/types/Coercion.hs-boot
index eb5e81b819..6c7cfb5e68 100644
--- a/compiler/types/Coercion.hs-boot
+++ b/compiler/types/Coercion.hs-boot
@@ -21,7 +21,6 @@ mkFunCo :: Role -> Coercion -> Coercion -> Coercion
 mkCoVarCo :: CoVar -> Coercion
 mkAxiomInstCo :: CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
 mkPhantomCo :: Coercion -> Type -> Type -> Coercion
-mkUnsafeCo :: Role -> Type -> Type -> Coercion
 mkUnivCo :: UnivCoProvenance -> Role -> Type -> Type -> Coercion
 mkSymCo :: Coercion -> Coercion
 mkTransCo :: Coercion -> Coercion -> Coercion
diff --git a/compiler/types/OptCoercion.hs b/compiler/types/OptCoercion.hs
index b8f9f6ce8f..40c189c0a0 100644
--- a/compiler/types/OptCoercion.hs
+++ b/compiler/types/OptCoercion.hs
@@ -554,7 +554,6 @@ opt_univ env sym prov role oty1 oty2
 
   where
     prov' = case prov of
-      UnsafeCoerceProv   -> prov
       PhantomProv kco    -> PhantomProv $ opt_co4_wrap env sym False Nominal kco
       ProofIrrelProv kco -> ProofIrrelProv $ opt_co4_wrap env sym False Nominal kco
       PluginProv _       -> prov
@@ -634,7 +633,6 @@ opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1)
     mkUnivCo prov' r1 tyl1 tyr2
   where
     -- if the provenances are different, opt'ing will be very confusing
-    opt_trans_prov UnsafeCoerceProv      UnsafeCoerceProv      = Just UnsafeCoerceProv
     opt_trans_prov (PhantomProv kco1)    (PhantomProv kco2)
       = Just $ PhantomProv $ opt_trans is kco1 kco2
     opt_trans_prov (ProofIrrelProv kco1) (ProofIrrelProv kco2)
diff --git a/compiler/types/TyCoFVs.hs b/compiler/types/TyCoFVs.hs
index 2c425d59a2..e275d60e6b 100644
--- a/compiler/types/TyCoFVs.hs
+++ b/compiler/types/TyCoFVs.hs
@@ -642,7 +642,6 @@ tyCoFVsOfCoVar v fv_cand in_scope acc
   = (unitFV v `unionFV` tyCoFVsOfType (varType v)) fv_cand in_scope acc
 
 tyCoFVsOfProv :: UnivCoProvenance -> FV
-tyCoFVsOfProv UnsafeCoerceProv    fv_cand in_scope acc = emptyFV fv_cand in_scope acc
 tyCoFVsOfProv (PhantomProv co)    fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
 tyCoFVsOfProv (ProofIrrelProv co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
 tyCoFVsOfProv (PluginProv _)      fv_cand in_scope acc = emptyFV fv_cand in_scope acc
@@ -714,7 +713,6 @@ almost_devoid_co_var_of_prov (PhantomProv co) cv
   = almost_devoid_co_var_of_co co cv
 almost_devoid_co_var_of_prov (ProofIrrelProv co) cv
   = almost_devoid_co_var_of_co co cv
-almost_devoid_co_var_of_prov UnsafeCoerceProv _ = True
 almost_devoid_co_var_of_prov (PluginProv _) _ = True
 
 almost_devoid_co_var_of_type :: Type -> CoVar -> Bool
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 1d81788f0b..36744cbc19 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -1451,8 +1451,7 @@ in nominal ways. If not, having w be representational is OK.
 %************************************************************************
 
 A UnivCo is a coercion whose proof does not directly express its role
-and kind (indeed for some UnivCos, like UnsafeCoerceProv, there /is/
-no proof).
+and kind (indeed for some UnivCos, like PluginProv, there /is/ no proof).
 
 The different kinds of UnivCo are described by UnivCoProvenance.  Really
 each is entirely separate, but they all share the need to represent their
@@ -1469,9 +1468,7 @@ role and kind, which is done in the UnivCo constructor.
 -- that they don't tell you what types they coercion between. (That info
 -- is in the 'UnivCo' constructor of 'Coercion'.
 data UnivCoProvenance
-  = UnsafeCoerceProv   -- ^ From @unsafeCoerce#@. These are unsound.
-
-  | PhantomProv KindCoercion -- ^ See Note [Phantom coercions]. Only in Phantom
+  = PhantomProv KindCoercion -- ^ See Note [Phantom coercions]. Only in Phantom
                              -- roled coercions
 
   | ProofIrrelProv KindCoercion  -- ^ From the fact that any two coercions are
@@ -1484,7 +1481,6 @@ data UnivCoProvenance
   deriving Data.Data
 
 instance Outputable UnivCoProvenance where
-  ppr UnsafeCoerceProv   = text "(unsafeCoerce#)"
   ppr (PhantomProv _)    = text "(phantom)"
   ppr (ProofIrrelProv _) = text "(proof irrel.)"
   ppr (PluginProv str)   = parens (text "plugin" <+> brackets (text str))
@@ -1794,7 +1790,6 @@ foldTyCo (TyCoFolder { tcf_view       = view
 
     go_prov env (PhantomProv co)    = go_co env co
     go_prov env (ProofIrrelProv co) = go_co env co
-    go_prov _   UnsafeCoerceProv    = mempty
     go_prov _   (PluginProv _)      = mempty
 
 {- *********************************************************************
@@ -1848,7 +1843,6 @@ coercionSize (SubCo co)          = 1 + coercionSize co
 coercionSize (AxiomRuleCo _ cs)  = 1 + sum (map coercionSize cs)
 
 provSize :: UnivCoProvenance -> Int
-provSize UnsafeCoerceProv    = 1
 provSize (PhantomProv co)    = 1 + coercionSize co
 provSize (ProofIrrelProv co) = 1 + coercionSize co
 provSize (PluginProv _)      = 1
diff --git a/compiler/types/TyCoSubst.hs b/compiler/types/TyCoSubst.hs
index e15d2d69d7..8a471eb40d 100644
--- a/compiler/types/TyCoSubst.hs
+++ b/compiler/types/TyCoSubst.hs
@@ -819,7 +819,6 @@ subst_co subst co
                                 in cs1 `seqList` AxiomRuleCo c cs1
     go (HoleCo h)            = HoleCo $! go_hole h
 
-    go_prov UnsafeCoerceProv     = UnsafeCoerceProv
     go_prov (PhantomProv kco)    = PhantomProv (go kco)
     go_prov (ProofIrrelProv kco) = ProofIrrelProv (go kco)
     go_prov p@(PluginProv _)     = p
@@ -1029,4 +1028,3 @@ cloneTyVarBndrs subst (t:ts)  usupply = (subst'', tv:tvs)
     (uniq, usupply') = takeUniqFromSupply usupply
     (subst' , tv )   = cloneTyVarBndr subst t uniq
     (subst'', tvs)   = cloneTyVarBndrs subst' ts usupply'
-
diff --git a/compiler/types/TyCoTidy.hs b/compiler/types/TyCoTidy.hs
index 77dc32c39b..4142075f26 100644
--- a/compiler/types/TyCoTidy.hs
+++ b/compiler/types/TyCoTidy.hs
@@ -227,7 +227,6 @@ tidyCo env@(_, subst) co
     go (AxiomRuleCo ax cos)  = let cos1 = tidyCos env cos
                                in cos1 `seqList` AxiomRuleCo ax cos1
 
-    go_prov UnsafeCoerceProv    = UnsafeCoerceProv
     go_prov (PhantomProv co)    = PhantomProv (go co)
     go_prov (ProofIrrelProv co) = ProofIrrelProv (go co)
     go_prov p@(PluginProv _)    = p
diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs
index 0e658d7365..7e4cc35f3b 100644
--- a/compiler/types/TyCon.hs
+++ b/compiler/types/TyCon.hs
@@ -1061,7 +1061,7 @@ visibleDataCons (SumTyCon{ data_cons = cs })  = cs
 data AlgTyConFlav
   = -- | An ordinary type constructor has no parent.
     VanillaAlgTyCon
-       TyConRepName
+       TyConRepName   -- For Typeable
 
     -- | An unboxed type constructor. The TyConRepName is a Maybe since we
     -- currently don't allow unboxed sums to be Typeable since there are too
@@ -1300,9 +1300,10 @@ This eta-reduction is implemented in BuildTyCl.mkNewTyConRhs.
 *                                                                      *
 ********************************************************************* -}
 
-type TyConRepName = Name -- The Name of the top-level declaration
-                         --    $tcMaybe :: Data.Typeable.Internal.TyCon
-                         --    $tcMaybe = TyCon { tyConName = "Maybe", ... }
+type TyConRepName = Name
+   -- The Name of the top-level declaration for the Typeable world
+   --    $tcMaybe :: Data.Typeable.Internal.TyCon
+   --    $tcMaybe = TyCon { tyConName = "Maybe", ... }
 
 tyConRepName_maybe :: TyCon -> Maybe TyConRepName
 tyConRepName_maybe (FunTyCon   { tcRepName = rep_nm })
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 7e469c988b..9cb3016a3d 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -54,6 +54,7 @@ module Type (
         piResultTy, piResultTys,
         applyTysX, dropForAlls,
         mkFamilyTyConApp,
+        buildSynTyCon,
 
         mkNumLitTy, isNumLitTy,
         mkStrLitTy, isStrLitTy,
@@ -243,6 +244,7 @@ import TysPrim
 import {-# SOURCE #-} TysWiredIn ( listTyCon, typeNatKind
                                  , typeSymbolKind, liftedTypeKind
                                  , constraintKind )
+import Name( Name )
 import PrelNames
 import CoAxiom
 import {-# SOURCE #-} Coercion( mkNomReflCo, mkGReflCo, mkReflCo
@@ -467,7 +469,6 @@ expandTypeSynonyms ty
     go_co _ (HoleCo h)
       = pprPanic "expandTypeSynonyms hit a hole" (ppr h)
 
-    go_prov _     UnsafeCoerceProv    = UnsafeCoerceProv
     go_prov subst (PhantomProv co)    = PhantomProv (go_co subst co)
     go_prov subst (ProofIrrelProv co) = ProofIrrelProv (go_co subst co)
     go_prov _     p@(PluginProv _)    = p
@@ -691,7 +692,6 @@ mapCoercion mapper@(TyCoMapper { tcm_covar = covar
     go (KindCo co)         = mkKindCo <$> go co
     go (SubCo co)          = mkSubCo <$> go co
 
-    go_prov UnsafeCoerceProv    = return UnsafeCoerceProv
     go_prov (PhantomProv co)    = PhantomProv <$> go co
     go_prov (ProofIrrelProv co) = ProofIrrelProv <$> go co
     go_prov p@(PluginProv _)    = return p
@@ -1916,6 +1916,15 @@ isCoVarType ty
   | otherwise
   = False
 
+buildSynTyCon :: Name -> [KnotTied TyConBinder] -> Kind   -- ^ /result/ kind
+              -> [Role] -> KnotTied Type -> TyCon
+-- This function is here beucase here is where we have
+--   isFamFree and isTauTy
+buildSynTyCon name binders res_kind roles rhs
+  = mkSynonymTyCon name binders res_kind roles rhs is_tau is_fam_free
+  where
+    is_tau      = isTauTy rhs
+    is_fam_free = isFamFreeTy rhs
 
 {-
 ************************************************************************
@@ -2714,7 +2723,6 @@ occCheckExpand vs_to_avoid ty
                                              ; return (mkAxiomRuleCo ax cs') }
 
     ------------------
-    go_prov _   UnsafeCoerceProv    = return UnsafeCoerceProv
     go_prov cxt (PhantomProv co)    = PhantomProv <$> go_co cxt co
     go_prov cxt (ProofIrrelProv co) = ProofIrrelProv <$> go_co cxt co
     go_prov _   p@(PluginProv _)    = return p
@@ -2768,7 +2776,6 @@ tyConsOfType ty
      go_mco MRefl    = emptyUniqSet
      go_mco (MCo co) = go_co co
 
-     go_prov UnsafeCoerceProv    = emptyUniqSet
      go_prov (PhantomProv co)    = go_co co
      go_prov (ProofIrrelProv co) = go_co co
      go_prov (PluginProv _)      = emptyUniqSet
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
+#-}
diff --git a/testsuite/tests/codeGen/should_compile/Makefile b/testsuite/tests/codeGen/should_compile/Makefile
index 3c4339bd8c..203111f55e 100644
--- a/testsuite/tests/codeGen/should_compile/Makefile
+++ b/testsuite/tests/codeGen/should_compile/Makefile
@@ -44,20 +44,16 @@ T15723:
 	'$(TEST_HC)' $(TEST_HC_OPTS) -prof -fPIC -fexternal-dynamic-refs -fforce-recomp -O2 -c T15723B.hs -o T15723B.o
 	'$(TEST_HC)' $(TEST_HC_OPTS) -dynamic -shared T15723B.o -o T15723B.so
 
-## check that there are two assembly equates
-# mentioning T15155.a_closure (def and use)
+# Check that the static indirection b is compiled to an equiv directive
 T15155:
-	'$(TEST_HC)' $(TEST_HC_OPTS) -c -O0 -ddump-asm T15155l.hs | grep -F ".equiv " \
-	| grep -F "T15155.a_closure" | wc -l | sed -e 's/ *//g' | grep "2" ; echo $$?
+	'$(TEST_HC)' $(TEST_HC_OPTS) -c -O0 -ddump-asm T15155l.hs | \
+		grep -F ".equiv T15155.b_closure,T15155.a_closure"
 
-## check that there are two "$def" aliases:
-#  - one that bitcasts to %T15155_a_closure_struct*
-#  - and the other which bitcasts from %T15155_a_closure_struct*
-##
+# Same as above, but in LLVM. Check that the static indirection b is compiled to
+# an alias.
 T15155l:
-	'$(TEST_HC)' $(TEST_HC_OPTS) -c -O0 -ddump-llvm T15155l.hs 2>/dev/null \
-	| grep -F "= alias %T15155_" | grep -E "@T15155_[ab]_closure.def = " | grep -F "%T15155_a_closure_struct*" \
-	| wc -l | sed -e 's/ *//g' | grep "2"; echo $$?
+	'$(TEST_HC)' $(TEST_HC_OPTS) -c -O0 -ddump-llvm T15155l.hs 2>/dev/null | \
+		grep -F "@T15155_b_closure = alias i8, i8* @T15155_a_closure"
 
 # Without -fcatch-bottoms `f` is non-CAFFY. With -fcatch-bottoms it becomes
 # CAFFY. Before CafInfo rework (c846618a) this used to cause incorrect CafInfo
diff --git a/testsuite/tests/codeGen/should_compile/T15155.stdout b/testsuite/tests/codeGen/should_compile/T15155.stdout
index 389e262145..14935fc201 100644
--- a/testsuite/tests/codeGen/should_compile/T15155.stdout
+++ b/testsuite/tests/codeGen/should_compile/T15155.stdout
@@ -1,2 +1 @@
-2
-0
+.equiv T15155.b_closure,T15155.a_closure
diff --git a/testsuite/tests/codeGen/should_compile/T15155l.hs b/testsuite/tests/codeGen/should_compile/T15155l.hs
index 643610bc06..6f39648630 100644
--- a/testsuite/tests/codeGen/should_compile/T15155l.hs
+++ b/testsuite/tests/codeGen/should_compile/T15155l.hs
@@ -1,8 +1,11 @@
 module T15155 (a, B(..), b) where
 
+import Debug.Trace
+
 newtype A = A Int
 newtype B = B A
 
 {-# NOINLINE a #-}
-a = A 42
+a = trace "evaluating a" A 42
+
 b = B a
diff --git a/testsuite/tests/codeGen/should_compile/T15155l.stdout b/testsuite/tests/codeGen/should_compile/T15155l.stdout
index 389e262145..ea81e38ef8 100644
--- a/testsuite/tests/codeGen/should_compile/T15155l.stdout
+++ b/testsuite/tests/codeGen/should_compile/T15155l.stdout
@@ -1,2 +1 @@
-2
-0
+@T15155_b_closure = alias i8, i8* @T15155_a_closure
diff --git a/testsuite/tests/concurrent/should_run/hs_try_putmvar003.hs b/testsuite/tests/concurrent/should_run/hs_try_putmvar003.hs
index d0c973935c..caaadc1aae 100644
--- a/testsuite/tests/concurrent/should_run/hs_try_putmvar003.hs
+++ b/testsuite/tests/concurrent/should_run/hs_try_putmvar003.hs
@@ -11,6 +11,7 @@ import GHC.MVar (MVar(..))
 import GHC.Prim
 import System.Environment
 import System.Exit
+import Unsafe.Coerce
 
 -- Measure C to Haskell callback throughput under a workload with
 -- several dimensions:
diff --git a/testsuite/tests/ghci.debugger/scripts/all.T b/testsuite/tests/ghci.debugger/scripts/all.T
index 01662361c4..d38b3681ad 100644
--- a/testsuite/tests/ghci.debugger/scripts/all.T
+++ b/testsuite/tests/ghci.debugger/scripts/all.T
@@ -54,7 +54,11 @@ test('break001', extra_files(['../Test2.hs']), ghci_script, ['break001.script'])
 test('break002', extra_files(['../Test2.hs']), ghci_script, ['break002.script'])
 test('break003', extra_files(['../Test3.hs']), ghci_script, ['break003.script'])
 test('break005', extra_files(['../QSort.hs']), ghci_script, ['break005.script'])
-test('break006', extra_files(['../Test3.hs']), ghci_script, ['break006.script'])
+test('break006',
+     [ when(compiler_debugged(), expect_broken(17833)),
+       extra_files(['../Test3.hs'])],
+     ghci_script,
+     ['break006.script'])
 test('break007', extra_files(['Break007.hs']), ghci_script, ['break007.script'])
 test('break008', extra_files(['../Test3.hs']), ghci_script, ['break008.script'])
 test('break009', [extra_files(['../Test6.hs']),
diff --git a/testsuite/tests/ghci/should_run/T16096.stdout b/testsuite/tests/ghci/should_run/T16096.stdout
index 6b34692d54..5826057d42 100644
--- a/testsuite/tests/ghci/should_run/T16096.stdout
+++ b/testsuite/tests/ghci/should_run/T16096.stdout
@@ -16,7 +16,7 @@ GHC.Base.returnIO
   @[()]
   (GHC.Types.:
      @()
-     (GHC.Prim.unsafeCoerce#
+     (Unsafe.Coerce.unsafeCoerce#
         @'GHC.Types.LiftedRep @'GHC.Types.LiftedRep @[GHC.Types.Int] @() x)
      (GHC.Types.[] @()))
 
@@ -39,7 +39,7 @@ GHC.Base.returnIO
   @[()]
   (GHC.Types.:
      @()
-     (GHC.Prim.unsafeCoerce#
+     (Unsafe.Coerce.unsafeCoerce#
         @'GHC.Types.LiftedRep @'GHC.Types.LiftedRep @[GHC.Types.Int] @() x)
      (GHC.Types.[] @()))
 
diff --git a/testsuite/tests/lib/integer/integerImportExport.hs b/testsuite/tests/lib/integer/integerImportExport.hs
index bcd0531680..276167b6b6 100644
--- a/testsuite/tests/lib/integer/integerImportExport.hs
+++ b/testsuite/tests/lib/integer/integerImportExport.hs
@@ -6,6 +6,7 @@ import Data.List (group)
 import Data.Bits
 import Data.Word
 import Control.Monad
+import Unsafe.Coerce (unsafeCoerce#)
 
 import GHC.Word
 import GHC.Base
diff --git a/testsuite/tests/pmcheck/should_compile/T11195.hs b/testsuite/tests/pmcheck/should_compile/T11195.hs
index 80d31ab8a7..b5c5452361 100644
--- a/testsuite/tests/pmcheck/should_compile/T11195.hs
+++ b/testsuite/tests/pmcheck/should_compile/T11195.hs
@@ -79,8 +79,6 @@ opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1)
   | Just prov' <- opt_trans_prov p1 p2 = undefined
   where
     -- if the provenances are different, opt'ing will be very confusing
-    opt_trans_prov UnsafeCoerceProv UnsafeCoerceProv
-      = Just UnsafeCoerceProv
     opt_trans_prov (PhantomProv kco1) (PhantomProv kco2)
       = Just $ PhantomProv $ opt_trans is kco1 kco2
     opt_trans_prov (ProofIrrelProv kco1) (ProofIrrelProv kco2)
diff --git a/testsuite/tests/polykinds/T14561.hs b/testsuite/tests/polykinds/T14561.hs
index 8c74ab4740..4be0812c68 100644
--- a/testsuite/tests/polykinds/T14561.hs
+++ b/testsuite/tests/polykinds/T14561.hs
@@ -6,7 +6,7 @@
 module T14561 where
 
 import GHC.Types
-import GHC.Prim
+import Unsafe.Coerce
 
 badId :: forall r (a :: TYPE r). a -> a
 badId = unsafeCoerce#
diff --git a/testsuite/tests/simplCore/should_compile/T5359a.hs b/testsuite/tests/simplCore/should_compile/T5359a.hs
index 7b9c317567..ebe85ba4a0 100644
--- a/testsuite/tests/simplCore/should_compile/T5359a.hs
+++ b/testsuite/tests/simplCore/should_compile/T5359a.hs
@@ -5,6 +5,7 @@ module T5359a (linesT) where
 import GHC.Base hiding (empty)
 import GHC.Word
 import GHC.ST (ST(..), runST)
+import Unsafe.Coerce( unsafeCoerce# )
 
 nullT :: Text -> Bool
 nullT (Text _ _ len) = len <= 0
diff --git a/testsuite/tests/simplCore/should_run/T16893/T16893.stderr b/testsuite/tests/simplCore/should_run/T16893/T16893.stderr
new file mode 100644
index 0000000000..5dfa1d642f
--- /dev/null
+++ b/testsuite/tests/simplCore/should_run/T16893/T16893.stderr
@@ -0,0 +1,4 @@
+T16893: Prelude.undefined
+CallStack (from HasCallStack):
+  error, called at libraries/base/GHC/Err.hs:79:14 in base:GHC.Err
+  undefined, called at ./Complex.hs:47:28 in main:Complex
diff --git a/testsuite/tests/simplCore/should_run/T16893/all.T b/testsuite/tests/simplCore/should_run/T16893/all.T
index 0ef2f5219e..1848ef79b5 100644
--- a/testsuite/tests/simplCore/should_run/T16893/all.T
+++ b/testsuite/tests/simplCore/should_run/T16893/all.T
@@ -1,4 +1,4 @@
 test('T16893',
-     [expect_broken(16893), extra_files(['Complex.hs'])],
+     [extra_files(['Complex.hs']), exit_code(1)],
      compile_and_run,
      ['-O1'])