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>

4 files changed, 101 insertions, 43 deletions

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