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>

11 files changed, 458 insertions, 146 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