Implement the -XUnliftedNewtypes extension.

GHC Proposal: 0013-unlifted-newtypes.rst
Discussion: https://github.com/ghc-proposals/ghc-proposals/pull/98
Issues: #15219, #1311, #13595, #15883
Implementation Details:
  Note [Implementation of UnliftedNewtypes]
  Note [Unifying data family kinds]
  Note [Compulsory newtype unfolding]

This patch introduces the -XUnliftedNewtypes extension. When this
extension is enabled, GHC drops the restriction that the field in
a newtype must be of kind (TYPE 'LiftedRep). This allows types
like Int# and ByteArray# to be used in a newtype. Additionally,
coerce is made levity-polymorphic so that it can be used with
newtypes over unlifted types.

The bulk of the changes are in TcTyClsDecls.hs. With -XUnliftedNewtypes,
getInitialKind is more liberal, introducing a unification variable to
return the kind (TYPE r0) rather than just returning (TYPE 'LiftedRep).
When kind-checking a data constructor with kcConDecl, we attempt to
unify the kind of a newtype with the kind of its field's type. When
typechecking a data declaration with tcTyClDecl, we again perform a
unification. See the implementation note for more on this.

Co-authored-by: Richard Eisenberg <rae@richarde.dev>

20 files changed, 608 insertions, 150 deletions

diff --git a/compiler/basicTypes/Id.hs b/compiler/basicTypes/Id.hs
index 621be76570..e2dfe925b1 100644
--- a/compiler/basicTypes/Id.hs
+++ b/compiler/basicTypes/Id.hs
@@ -567,7 +567,7 @@ lambdas if it is not applied to enough arguments; e.g. (#14561)
 The desugar has special magic to detect such cases: DsExpr.badUseOfLevPolyPrimop.
 And we want that magic to apply to levity-polymorphic compulsory-inline things.
 The easiest way to do this is for hasNoBinding to return True of all things
-that have compulsory unfolding.  A very Ids with a compulsory unfolding also
+that have compulsory unfolding.  Some Ids with a compulsory unfolding also
 have a binding, but it does not harm to say they don't here, and its a very
 simple way to fix #14561.
 
diff --git a/compiler/basicTypes/MkId.hs b/compiler/basicTypes/MkId.hs
index f96b579ba9..741b48e58b 100644
--- a/compiler/basicTypes/MkId.hs
+++ b/compiler/basicTypes/MkId.hs
@@ -29,6 +29,7 @@ module MkId (
         nullAddrId, seqId, lazyId, lazyIdKey,
         coercionTokenId, magicDictId, coerceId,
         proxyHashId, noinlineId, noinlineIdName,
+        coerceName,
 
         -- Re-export error Ids
         module PrelRules
@@ -71,6 +72,7 @@ import DynFlags
 import Outputable
 import FastString
 import ListSetOps
+import Var (VarBndr(Bndr))
 import qualified GHC.LanguageExtensions as LangExt
 
 import Data.Maybe       ( maybeToList )
@@ -338,6 +340,32 @@ effect whether a wrapper is present or not:
     We'd like 'map Age' to match the LHS. For this to happen, Age
     must be unfolded, otherwise we'll be stuck. This is tested in T16208.
 
+It also allows for the posssibility of levity polymorphic newtypes
+with wrappers (with -XUnliftedNewtypes):
+
+  newtype N (a :: TYPE r) = MkN a
+
+With -XUnliftedNewtypes, this is allowed -- even though MkN is levity-
+polymorphic. It's OK because MkN evaporates in the compiled code, becoming
+just a cast. That is, it has a compulsory unfolding. As long as its
+argument is not levity-polymorphic (which it can't be, according to
+Note [Levity polymorphism invariants] in CoreSyn), and it's saturated,
+no levity-polymorphic code ends up in the code generator. The saturation
+condition is effectively checked by Note [Detecting forced eta expansion]
+in DsExpr.
+
+However, if we make a *wrapper* for a newtype, we get into trouble.
+The saturation condition is no longer checked (because hasNoBinding
+returns False) and indeed we generate a forbidden levity-polymorphic
+binding.
+
+The solution is simple, though: just make the newtype wrappers
+as ephemeral as the newtype workers. In other words, give the wrappers
+compulsory unfoldings and no bindings. The compulsory unfolding is given
+in wrap_unf in mkDataConRep, and the lack of a binding happens in
+TidyPgm.getTyConImplicitBinds, where we say that a newtype has no implicit
+bindings.
+
 ************************************************************************
 *                                                                      *
 \subsection{Dictionary selectors}
@@ -595,6 +623,7 @@ But if we inline the wrapper, we get
    map (\a. case i of I# i# a -> Foo i# a) (f a)
 
 and now case-of-known-constructor eliminates the redundant allocation.
+
 -}
 
 mkDataConRep :: DynFlags
@@ -624,7 +653,7 @@ mkDataConRep dflags fam_envs wrap_name mb_bangs data_con
                              -- We need to get the CAF info right here because TidyPgm
                              -- does not tidy the IdInfo of implicit bindings (like the wrapper)
                              -- so it not make sure that the CAF info is sane
-                         `setNeverLevPoly`      wrap_ty
+                         `setLevityInfoWithType` wrap_ty
 
              wrap_sig = mkClosedStrictSig wrap_arg_dmds (dataConCPR data_con)
 
@@ -1423,19 +1452,23 @@ coerceId = pcMiscPrelId coerceName ty info
   where
     info = noCafIdInfo `setInlinePragInfo` alwaysInlinePragma
                        `setUnfoldingInfo`  mkCompulsoryUnfolding rhs
-                       `setNeverLevPoly`   ty
-    eqRTy     = mkTyConApp coercibleTyCon [ liftedTypeKind
-                                          , alphaTy, betaTy ]
-    eqRPrimTy = mkTyConApp eqReprPrimTyCon [ liftedTypeKind
-                                           , liftedTypeKind
-                                           , alphaTy, betaTy ]
-    ty        = mkSpecForAllTys [alphaTyVar, betaTyVar] $
-                mkInvisFunTy eqRTy                      $
-                mkVisFunTy alphaTy betaTy
-
-    [eqR,x,eq] = mkTemplateLocals [eqRTy, alphaTy, eqRPrimTy]
-    rhs = mkLams [alphaTyVar, betaTyVar, eqR, x] $
-          mkWildCase (Var eqR) eqRTy betaTy $
+    eqRTy     = mkTyConApp coercibleTyCon [ tYPE r , a, b ]
+    eqRPrimTy = mkTyConApp eqReprPrimTyCon [ tYPE r, tYPE r, a, b ]
+    ty        = mkForAllTys [ Bndr rv Inferred
+                            , Bndr av Specified
+                            , Bndr bv Specified
+                            ] $
+                mkInvisFunTy eqRTy $
+                mkVisFunTy a b
+
+    bndrs@[rv,av,bv] = mkTemplateKiTyVar runtimeRepTy
+                        (\r -> [tYPE r, tYPE r])
+
+    [r, a, b] = mkTyVarTys bndrs
+
+    [eqR,x,eq] = mkTemplateLocals [eqRTy, a, eqRPrimTy]
+    rhs = mkLams (bndrs ++ [eqR, x]) $
+          mkWildCase (Var eqR) eqRTy b $
           [(DataAlt coercibleDataCon, [eq], Cast (Var x) (mkCoVarCo eq))]
 
 {-
diff --git a/compiler/codeGen/StgCmmForeign.hs b/compiler/codeGen/StgCmmForeign.hs
index 7e26e7e118..172dcba219 100644
--- a/compiler/codeGen/StgCmmForeign.hs
+++ b/compiler/codeGen/StgCmmForeign.hs
@@ -619,6 +619,9 @@ typeToStgFArgType typ
   | tycon == mutableByteArrayPrimTyCon = StgByteArrayType
   | otherwise = StgPlainType
   where
-  -- should be a tycon app, since this is a foreign call
+  -- Should be a tycon app, since this is a foreign call. We look
+  -- through newtypes so the offset does not change if a user replaces
+  -- a type in a foreign function signature with a representationally
+  -- equivalent newtype.
   tycon = tyConAppTyCon (unwrapType typ)
 
diff --git a/compiler/deSugar/DsExpr.hs b/compiler/deSugar/DsExpr.hs
index 12b0c838a6..9516fbbe82 100644
--- a/compiler/deSugar/DsExpr.hs
+++ b/compiler/deSugar/DsExpr.hs
@@ -1091,7 +1091,7 @@ Note [Detecting forced eta expansion]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We cannot have levity polymorphic function arguments. See
 Note [Levity polymorphism invariants] in CoreSyn. But we *can* have
-functions that take levity polymorphism arguments, as long as these
+functions that take levity polymorphic arguments, as long as these
 functions are eta-reduced. (See #12708 for an example.)
 
 However, we absolutely cannot do this for functions that have no
@@ -1162,7 +1162,11 @@ badUseOfLevPolyPrimop id ty
 
 levPolyPrimopErr :: Id -> Type -> [Type] -> DsM ()
 levPolyPrimopErr primop ty bad_tys
-  = errDs $ vcat [ hang (text "Cannot use primitive with levity-polymorphic arguments:")
-                      2 (ppr primop <+> dcolon <+> pprWithTYPE ty)
-                 , hang (text "Levity-polymorphic arguments:")
-                      2 (vcat (map (\t -> pprWithTYPE t <+> dcolon <+> pprWithTYPE (typeKind t)) bad_tys)) ]
+  = errDs $ vcat
+    [ hang (text "Cannot use function with levity-polymorphic arguments:")
+         2 (ppr primop <+> dcolon <+> pprWithTYPE ty)
+    , hang (text "Levity-polymorphic arguments:")
+         2 $ vcat $ map
+           (\t -> pprWithTYPE t <+> dcolon <+> pprWithTYPE (typeKind t))
+           bad_tys
+    ]
diff --git a/compiler/hsSyn/HsTypes.hs b/compiler/hsSyn/HsTypes.hs
index b186b36abb..130e39efab 100644
--- a/compiler/hsSyn/HsTypes.hs
+++ b/compiler/hsSyn/HsTypes.hs
@@ -62,6 +62,7 @@ module HsTypes (
         mkHsOpTy, mkHsAppTy, mkHsAppTys, mkHsAppKindTy,
         ignoreParens, hsSigType, hsSigWcType,
         hsLTyVarBndrToType, hsLTyVarBndrsToTypes,
+        hsConDetailsArgs,
 
         -- Printing
         pprHsType, pprHsForAll, pprHsForAllExtra, pprHsExplicitForAll,
@@ -912,6 +913,14 @@ instance (Outputable arg, Outputable rec)
   ppr (RecCon rec)     = text "RecCon:" <+> ppr rec
   ppr (InfixCon l r)   = text "InfixCon:" <+> ppr [l, r]
 
+hsConDetailsArgs ::
+     HsConDetails (LHsType a) (Located [LConDeclField a])
+  -> [LHsType a]
+hsConDetailsArgs details = case details of
+  InfixCon a b -> [a,b]
+  PrefixCon xs -> xs
+  RecCon r -> map (cd_fld_type . unLoc) (unLoc r)
+
 {-
 Note [ConDeclField passs]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index 1d026f6c99..805cdcef07 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -4527,6 +4527,7 @@ xFlagsDeps = [
   flagSpec "UndecidableSuperClasses"          LangExt.UndecidableSuperClasses,
   flagSpec "UnicodeSyntax"                    LangExt.UnicodeSyntax,
   flagSpec "UnliftedFFITypes"                 LangExt.UnliftedFFITypes,
+  flagSpec "UnliftedNewtypes"                 LangExt.UnliftedNewtypes,
   flagSpec "ViewPatterns"                     LangExt.ViewPatterns
   ]
 
diff --git a/compiler/main/TidyPgm.hs b/compiler/main/TidyPgm.hs
index 4f9c8c856f..66cef76861 100644
--- a/compiler/main/TidyPgm.hs
+++ b/compiler/main/TidyPgm.hs
@@ -566,7 +566,9 @@ See Note [Data constructor workers] in CorePrep.
 -}
 
 getTyConImplicitBinds :: TyCon -> [CoreBind]
-getTyConImplicitBinds tc = map get_defn (mapMaybe dataConWrapId_maybe (tyConDataCons tc))
+getTyConImplicitBinds tc
+  | isNewTyCon tc = []  -- See Note [Compulsory newtype unfolding] in MkId
+  | otherwise     = map get_defn (mapMaybe dataConWrapId_maybe (tyConDataCons tc))
 
 getClassImplicitBinds :: Class -> [CoreBind]
 getClassImplicitBinds cls
diff --git a/compiler/prelude/TysPrim.hs b/compiler/prelude/TysPrim.hs
index 3e0d87fd35..01c496a310 100644
--- a/compiler/prelude/TysPrim.hs
+++ b/compiler/prelude/TysPrim.hs
@@ -13,7 +13,7 @@ module TysPrim(
         mkPrimTyConName, -- For implicit parameters in TysWiredIn only
 
         mkTemplateKindVars, mkTemplateTyVars, mkTemplateTyVarsFrom,
-        mkTemplateKiTyVars,
+        mkTemplateKiTyVars, mkTemplateKiTyVar,
 
         mkTemplateTyConBinders, mkTemplateKindTyConBinders,
         mkTemplateAnonTyConBinders,
@@ -251,14 +251,15 @@ alphaTyVars is a list of type variables for use in templates:
         ["a", "b", ..., "z", "t1", "t2", ... ]
 -}
 
+mkTemplateKindVar :: Kind -> TyVar
+mkTemplateKindVar = mkTyVar (mk_tv_name 0 "k")
+
 mkTemplateKindVars :: [Kind] -> [TyVar]
 -- k0  with unique (mkAlphaTyVarUnique 0)
 -- k1  with unique (mkAlphaTyVarUnique 1)
 -- ... etc
-mkTemplateKindVars [kind]
-  = [mkTyVar (mk_tv_name 0 "k") kind]
-    -- Special case for one kind: just "k"
-
+mkTemplateKindVars [kind] = [mkTemplateKindVar kind]
+  -- Special case for one kind: just "k"
 mkTemplateKindVars kinds
   = [ mkTyVar (mk_tv_name u ('k' : show u)) kind
     | (kind, u) <- kinds `zip` [0..] ]
@@ -307,7 +308,7 @@ mkTemplateKiTyVars
     -> [TyVar]   -- [kv1:k1, ..., kvn:kn, av1:ak1, ..., avm:akm]
 -- Example: if you want the tyvars for
 --   forall (r:RuntimeRep) (a:TYPE r) (b:*). blah
--- call mkTemplateKiTyVars [RuntimeRep] (\[r]. [TYPE r, *)
+-- call mkTemplateKiTyVars [RuntimeRep] (\[r] -> [TYPE r, *])
 mkTemplateKiTyVars kind_var_kinds mk_arg_kinds
   = kv_bndrs ++ tv_bndrs
   where
@@ -315,6 +316,21 @@ mkTemplateKiTyVars kind_var_kinds mk_arg_kinds
     anon_kinds = mk_arg_kinds (mkTyVarTys kv_bndrs)
     tv_bndrs   = mkTemplateTyVarsFrom (length kv_bndrs) anon_kinds
 
+mkTemplateKiTyVar
+    :: Kind                  -- [k1, .., kn]   Kind of kind-forall'd var
+    -> (Kind -> [Kind])      -- Arg is kv1:k1
+                             -- Result is anon arg kinds [ak1, .., akm]
+    -> [TyVar]   -- [kv1:k1, ..., kvn:kn, av1:ak1, ..., avm:akm]
+-- Example: if you want the tyvars for
+--   forall (r:RuntimeRep) (a:TYPE r) (b:*). blah
+-- call mkTemplateKiTyVar RuntimeRep (\r -> [TYPE r, *])
+mkTemplateKiTyVar kind mk_arg_kinds
+  = kv_bndr : tv_bndrs
+  where
+    kv_bndr    = mkTemplateKindVar kind
+    anon_kinds = mk_arg_kinds (mkTyVarTy kv_bndr)
+    tv_bndrs   = mkTemplateTyVarsFrom 1 anon_kinds
+
 mkTemplateKindTyConBinders :: [Kind] -> [TyConBinder]
 -- Makes named, Specified binders
 mkTemplateKindTyConBinders kinds = [mkNamedTyConBinder Specified tv | tv <- mkTemplateKindVars kinds]
diff --git a/compiler/prelude/primops.txt.pp b/compiler/prelude/primops.txt.pp
index ef8a459100..3bf0180c45 100644
--- a/compiler/prelude/primops.txt.pp
+++ b/compiler/prelude/primops.txt.pp
@@ -3439,6 +3439,11 @@ pseudoop   "coerce"
      the newtype's concrete type to the abstract type. But it also works in
      more complicated settings, e.g. converting a list of newtypes to a list of
      concrete types.
+
+     This function is runtime-representation polymorphic, but the
+     {\tt RuntimeRep} type argument is marked as {\tt Inferred}, meaning
+     that it is not available for visible type application. This means
+     the typechecker will accept {\tt coerce @Int @Age 42}.
    }
 
 ------------------------------------------------------------------------
diff --git a/compiler/rename/RnSource.hs b/compiler/rename/RnSource.hs
index 9e0d616ace..e3c9576e94 100644
--- a/compiler/rename/RnSource.hs
+++ b/compiler/rename/RnSource.hs
@@ -69,7 +69,7 @@ import Control.Arrow ( first )
 import Data.List ( mapAccumL )
 import qualified Data.List.NonEmpty as NE
 import Data.List.NonEmpty ( NonEmpty(..) )
-import Data.Maybe ( isNothing, fromMaybe )
+import Data.Maybe ( isNothing, isJust, fromMaybe )
 import qualified Data.Set as Set ( difference, fromList, toList, null )
 
 {- | @rnSourceDecl@ "renames" declarations.
@@ -1539,18 +1539,22 @@ rnTyClDecl (SynDecl { tcdLName = tycon, tcdTyVars = tyvars,
 
 -- "data", "newtype" declarations
 -- both top level and (for an associated type) in an instance decl
-rnTyClDecl (DataDecl { tcdLName = tycon, tcdTyVars = tyvars,
-                       tcdFixity = fixity, tcdDataDefn = defn })
+rnTyClDecl (DataDecl _ _ _ _ (XHsDataDefn _)) =
+  panic "rnTyClDecl: DataDecl with XHsDataDefn"
+rnTyClDecl (DataDecl
+    { tcdLName = tycon, tcdTyVars = tyvars,
+      tcdFixity = fixity,
+      tcdDataDefn = defn@HsDataDefn{ dd_ND = new_or_data
+                                   , dd_kindSig = kind_sig} })
   = do { tycon' <- lookupLocatedTopBndrRn tycon
        ; let kvs = extractDataDefnKindVars defn
              doc = TyDataCtx tycon
        ; traceRn "rntycl-data" (ppr tycon <+> ppr kvs)
        ; bindHsQTyVars doc Nothing Nothing kvs tyvars $ \ tyvars' no_rhs_kvs ->
     do { (defn', fvs) <- rnDataDefn doc defn
-          -- See Note [Complete user-supplied kind signatures] in HsDecls
-       ; cusks_enabled <- xoptM LangExt.CUSKs
-       ; let cusk = cusks_enabled && hsTvbAllKinded tyvars' && no_rhs_kvs
-             rn_info = DataDeclRn { tcdDataCusk = cusk
+       ; cusk <- dataDeclHasCUSK
+           tyvars' new_or_data no_rhs_kvs (isJust kind_sig)
+       ; let rn_info = DataDeclRn { tcdDataCusk = cusk
                                   , tcdFVs      = fvs }
        ; traceRn "rndata" (ppr tycon <+> ppr cusk <+> ppr no_rhs_kvs)
        ; return (DataDecl { tcdLName    = tycon'
@@ -1626,6 +1630,42 @@ rnTyClDecl (ClassDecl { tcdCtxt = context, tcdLName = lcls,
 
 rnTyClDecl (XTyClDecl _) = panic "rnTyClDecl"
 
+-- Does the data type declaration include a CUSK?
+dataDeclHasCUSK :: LHsQTyVars pass -> NewOrData -> Bool -> Bool -> RnM Bool
+dataDeclHasCUSK tyvars new_or_data no_rhs_kvs has_kind_sig = do
+  { -- See Note [Unlifted Newtypes and CUSKs], and for a broader
+    -- picture, see Note [Implementation of UnliftedNewtypes].
+  ; unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes
+  ; let non_cusk_newtype
+          | NewType <- new_or_data =
+              unlifted_newtypes && not has_kind_sig
+          | otherwise = False
+    -- See Note [CUSKs: complete user-supplied kind signatures] in HsDecls
+  ; cusks_enabled <- xoptM LangExt.CUSKs
+  ; return $ cusks_enabled && hsTvbAllKinded tyvars &&
+             no_rhs_kvs && not non_cusk_newtype
+  }
+
+{- Note [Unlifted Newtypes and CUSKs]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When unlifted newtypes are enabled, a newtype must have a kind signature
+in order to be considered have a CUSK. This is because the flow of
+kind inference works differently. Consider:
+
+  newtype Foo = FooC Int
+
+When UnliftedNewtypes is disabled, we decide that Foo has kind
+`TYPE 'LiftedRep` without looking inside the data constructor. So, we
+can say that Foo has a CUSK. However, when UnliftedNewtypes is enabled,
+we fill in the kind of Foo as a metavar that gets solved by unification
+with the kind of the field inside FooC (that is, Int, whose kind is
+`TYPE 'LiftedRep`). But since we have to look inside the data constructors
+to figure out the kind signature of Foo, it does not have a CUSK.
+
+See Note [Implementation of UnliftedNewtypes] for where this fits in to
+the broader picture of UnliftedNewtypes.
+-}
+
 -- "type" and "type instance" declarations
 rnTySyn :: HsDocContext -> LHsType GhcPs -> RnM (LHsType GhcRn, FreeVars)
 rnTySyn doc rhs = rnLHsType doc rhs
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index 759830e97f..02b888703d 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -2015,11 +2015,11 @@ mkExpectedActualMsg ty1 ty2 ct@(TypeEqOrigin { uo_actual = act
     level = m_level `orElse` TypeLevel
 
     occurs_check_error
-      | Just act_tv <- tcGetTyVar_maybe act
-      , act_tv `elemVarSet` tyCoVarsOfType exp
+      | Just tv <- tcGetTyVar_maybe ty1
+      , tv `elemVarSet` tyCoVarsOfType ty2
       = True
-      | Just exp_tv <- tcGetTyVar_maybe exp
-      , exp_tv `elemVarSet` tyCoVarsOfType act
+      | Just tv <- tcGetTyVar_maybe ty2
+      , tv `elemVarSet` tyCoVarsOfType ty1
       = True
       | otherwise
       = False
@@ -2043,13 +2043,17 @@ mkExpectedActualMsg ty1 ty2 ct@(TypeEqOrigin { uo_actual = act
         -> empty
 
     thing_msg = case maybe_thing of
-                  Just thing -> \_ -> quotes thing <+> text "is"
-                  Nothing    -> \vowel -> text "got a" <>
-                                          if vowel then char 'n' else empty
+                  Just thing -> \_ levity ->
+                    quotes thing <+> text "is" <+> levity
+                  Nothing    -> \vowel levity ->
+                    text "got a" <>
+                    (if vowel then char 'n' else empty) <+>
+                    levity <+>
+                    text "type"
     msg2 = sep [ text "Expecting a lifted type, but"
-               , thing_msg True, text "unlifted" ]
+               , thing_msg True (text "unlifted") ]
     msg3 = sep [ text "Expecting an unlifted type, but"
-               , thing_msg False, text "lifted" ]
+               , thing_msg False (text "lifted") ]
     msg4 = maybe_num_args_msg $$
            sep [ text "Expected a type, but"
                , maybe (text "found something with kind")
diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs
index eb65d1e093..d5c600dda8 100644
--- a/compiler/typecheck/TcEvidence.hs
+++ b/compiler/typecheck/TcEvidence.hs
@@ -30,6 +30,7 @@ module TcEvidence (
 
   -- TcCoercion
   TcCoercion, TcCoercionR, TcCoercionN, TcCoercionP, CoercionHole,
+  TcMCoercion,
   Role(..), LeftOrRight(..), pickLR,
   mkTcReflCo, mkTcNomReflCo, mkTcRepReflCo,
   mkTcTyConAppCo, mkTcAppCo, mkTcFunCo,
@@ -42,7 +43,7 @@ module TcEvidence (
   mkTcKindCo,
   tcCoercionKind, coVarsOfTcCo,
   mkTcCoVarCo,
-  isTcReflCo, isTcReflexiveCo,
+  isTcReflCo, isTcReflexiveCo, isTcGReflMCo, tcCoToMCo,
   tcCoercionRole,
   unwrapIP, wrapIP
   ) where
@@ -98,6 +99,7 @@ type TcCoercion  = Coercion
 type TcCoercionN = CoercionN    -- A Nominal          coercion ~N
 type TcCoercionR = CoercionR    -- A Representational coercion ~R
 type TcCoercionP = CoercionP    -- a phantom coercion
+type TcMCoercion = MCoercion
 
 mkTcReflCo             :: Role -> TcType -> TcCoercion
 mkTcSymCo              :: TcCoercion -> TcCoercion
@@ -133,6 +135,7 @@ tcCoercionKind         :: TcCoercion -> Pair TcType
 tcCoercionRole         :: TcCoercion -> Role
 coVarsOfTcCo           :: TcCoercion -> TcTyCoVarSet
 isTcReflCo             :: TcCoercion -> Bool
+isTcGReflMCo           :: TcMCoercion -> Bool
 
 -- | This version does a slow check, calculating the related types and seeing
 -- if they are equal.
@@ -168,8 +171,12 @@ tcCoercionKind         = coercionKind
 tcCoercionRole         = coercionRole
 coVarsOfTcCo           = coVarsOfCo
 isTcReflCo             = isReflCo
+isTcGReflMCo           = isGReflMCo
 isTcReflexiveCo        = isReflexiveCo
 
+tcCoToMCo :: TcCoercion -> TcMCoercion
+tcCoToMCo = coToMCo
+
 {-
 %************************************************************************
 %*                                                                      *
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 5965170a55..f2a7950450 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -2122,8 +2122,6 @@ bindExplicitTKBndrs_Q_Skol, bindExplicitTKBndrs_Q_Tv
 bindExplicitTKBndrs_Q_Skol ctxt_kind = bindExplicitTKBndrsX (tcHsQTyVarBndr ctxt_kind newSkolemTyVar)
 bindExplicitTKBndrs_Q_Tv   ctxt_kind = bindExplicitTKBndrsX (tcHsQTyVarBndr ctxt_kind newTyVarTyVar)
 
--- | Used during the "kind-checking" pass in TcTyClsDecls only,
--- and even then only for data-con declarations.
 bindExplicitTKBndrsX
     :: (HsTyVarBndr GhcRn -> TcM TcTyVar)
     -> [LHsTyVarBndr GhcRn]
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index 9642756b99..25c598df6b 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -472,8 +472,7 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = hs_ty, cid_binds = binds
                                   , cid_datafam_insts = adts }))
   = setSrcSpan loc                      $
     addErrCtxt (instDeclCtxt1 hs_ty)  $
-    do  { traceTc "tcLocalInstDecl" (ppr hs_ty)
-        ; dfun_ty <- tcHsClsInstType (InstDeclCtxt False) hs_ty
+    do  { dfun_ty <- tcHsClsInstType (InstDeclCtxt False) hs_ty
         ; let (tyvars, theta, clas, inst_tys) = tcSplitDFunTy dfun_ty
              -- NB: tcHsClsInstType does checkValidInstance
 
@@ -660,10 +659,10 @@ tcDataFamInstDecl mb_clsinfo
        ; gadt_syntax <- dataDeclChecks fam_name new_or_data hs_ctxt hs_cons
           -- Do /not/ check that the number of patterns = tyConArity fam_tc
           -- See [Arity of data families] in FamInstEnv
-
        ; (qtvs, pats, res_kind, stupid_theta)
              <- tcDataFamHeader mb_clsinfo fam_tc imp_vars mb_bndrs
                                 fixity hs_ctxt hs_pats m_ksig hs_cons
+                                new_or_data
 
        -- Eta-reduce the axiom if possible
        -- Quite tricky: see Note [Eta-reduction for data families]
@@ -679,13 +678,26 @@ tcDataFamInstDecl mb_clsinfo
                  -- first, so there is no reason to suppose that the eta_tvs
                  -- (obtained from the pats) are at the end (#11148)
 
-       -- Eta-expand the representation tycon until it has reult kind *
+       -- Eta-expand the representation tycon until it has result
+       -- kind `TYPE r`, for some `r`. If UnliftedNewtypes is not enabled, we
+       -- go one step further and ensure that it has kind `TYPE 'LiftedRep`.
+       --
        -- See also Note [Arity of data families] in FamInstEnv
        -- NB: we can do this after eta-reducing the axiom, because if
        --     we did it before the "extra" tvs from etaExpandAlgTyCon
        --     would always be eta-reduced
        ; (extra_tcbs, final_res_kind) <- etaExpandAlgTyCon full_tcbs res_kind
-       ; checkTc (tcIsLiftedTypeKind final_res_kind) (badKindSig True res_kind)
+       ; unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes
+       ; let allowUnlifted = unlifted_newtypes && new_or_data == NewType
+         -- With UnliftedNewtypes, we allow kinds other than Type, but they
+         -- must still be of the form `TYPE r` since we don't want to accept
+         -- Constraint or Nat. See Note [Implementation of UnliftedNewtypes].
+       ; checkTc
+           (if allowUnlifted
+              then tcIsRuntimeTypeKind final_res_kind
+              else tcIsLiftedTypeKind final_res_kind
+           )
+           (badKindSig True res_kind)
        ; let extra_pats  = map (mkTyVarTy . binderVar) extra_tcbs
              all_pats    = pats `chkAppend` extra_pats
              orig_res_ty = mkTyConApp fam_tc all_pats
@@ -703,9 +715,10 @@ tcDataFamInstDecl mb_clsinfo
 
        ; (rep_tc, axiom) <- fixM $ \ ~(rec_rep_tc, _) ->
            do { data_cons <- tcExtendTyVarEnv qtvs $
-                             -- For H98 decls, the tyvars scope
-                             -- over the data constructors
-                             tcConDecls rec_rep_tc ty_binders orig_res_ty hs_cons
+                  -- For H98 decls, the tyvars scope
+                  -- over the data constructors
+                  tcConDecls rec_rep_tc new_or_data ty_binders final_res_kind
+                             orig_res_ty hs_cons
 
               ; rep_tc_name <- newFamInstTyConName lfam_name pats
               ; axiom_name  <- newFamInstAxiomName lfam_name [pats]
@@ -722,7 +735,7 @@ tcDataFamInstDecl mb_clsinfo
                       -- NB: Use the full ty_binders from the pats. See bullet toward
                       -- the end of Note [Data type families] in TyCon
                     rep_tc   = mkAlgTyCon rep_tc_name
-                                          ty_binders liftedTypeKind
+                                          ty_binders final_res_kind
                                           (map (const Nominal) ty_binders)
                                           (fmap unLoc cType) stupid_theta
                                           tc_rhs parent
@@ -782,12 +795,14 @@ tcDataFamInstDecl _ _ = panic "tcDataFamInstDecl"
 tcDataFamHeader :: AssocInstInfo -> TyCon -> [Name] -> Maybe [LHsTyVarBndr GhcRn]
                 -> LexicalFixity -> LHsContext GhcRn
                 -> HsTyPats GhcRn -> Maybe (LHsKind GhcRn) -> [LConDecl GhcRn]
+                -> NewOrData
                 -> TcM ([TyVar], [Type], Kind, ThetaType)
 -- The "header" is the part other than the data constructors themselves
 -- e.g.  data instance D [a] :: * -> * where ...
 -- Here the "header" is the bit before the "where"
-tcDataFamHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity hs_ctxt hs_pats m_ksig hs_cons
-  = do { (imp_tvs, (exp_tvs, (stupid_theta, lhs_ty, res_kind)))
+tcDataFamHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity hs_ctxt
+                hs_pats m_ksig hs_cons new_or_data
+  = do { (imp_tvs, (exp_tvs, (stupid_theta, lhs_ty)))
             <- pushTcLevelM_                                $
                solveEqualities                              $
                bindImplicitTKBndrs_Q_Skol imp_vars          $
@@ -799,17 +814,16 @@ tcDataFamHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity hs_ctxt hs_pats m_ksi
                   -- with its parent class
                   ; addConsistencyConstraints mb_clsinfo lhs_ty
 
-                  -- Add constraints from the data constructors
-                  ; mapM_ (wrapLocM_ kcConDecl) hs_cons
-
                   -- Add constraints from the result signature
                   ; res_kind <- tc_kind_sig m_ksig
+                  -- Add constraints from the data constructors
+                  ; mapM_ (wrapLocM_ (kcConDecl new_or_data res_kind)) hs_cons
                   ; lhs_ty <- checkExpectedKind_pp pp_lhs lhs_ty lhs_kind res_kind
-                  ; return (stupid_theta, lhs_ty, res_kind) }
+                  ; return (stupid_theta, lhs_ty) }
 
        -- See TcTyClsDecls Note [Generalising in tcFamTyPatsGuts]
        -- This code (and the stuff immediately above) is very similar
-       -- to that in tcFamTyInstEqnGuts.  Maybe we should abstract the
+       -- to that in tcTyFamInstEqnGuts.  Maybe we should abstract the
        -- common code; but for the moment I concluded that it's
        -- clearer to duplicate it.  Still, if you fix a bug here,
        -- check there too!
@@ -819,22 +833,33 @@ tcDataFamHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity hs_ctxt hs_pats m_ksi
 
        -- Zonk the patterns etc into the Type world
        ; (ze, qtvs)   <- zonkTyBndrs qtvs
-       ; lhs_ty       <- zonkTcTypeToTypeX ze lhs_ty
-       ; res_kind     <- zonkTcTypeToTypeX ze res_kind
+              -- See Note [Unifying data family kinds] about the discardCast
+       ; lhs_ty       <- zonkTcTypeToTypeX ze (discardCast lhs_ty)
        ; stupid_theta <- zonkTcTypesToTypesX ze stupid_theta
 
        -- Check that type patterns match the class instance head
-       ; let pats = unravelFamInstPats lhs_ty
-       ; return (qtvs, pats, res_kind, stupid_theta) }
+       -- The call to splitTyConApp_maybe here is just an inlining of
+       -- the body of unravelFamInstPats.
+       ; pats <- case splitTyConApp_maybe lhs_ty of
+           Just (_, pats) -> pure pats
+           Nothing -> pprPanic "tcDataFamHeader" (ppr lhs_ty)
+       ; return (qtvs, pats, typeKind lhs_ty, stupid_theta) }
+          -- See Note [Unifying data family kinds] about why we need typeKind here
   where
     fam_name  = tyConName fam_tc
     data_ctxt = DataKindCtxt fam_name
     pp_lhs    = pprHsFamInstLHS fam_name mb_bndrs hs_pats fixity hs_ctxt
     exp_bndrs = mb_bndrs `orElse` []
 
-    -- See Note [Result kind signature for a data family instance]
+    -- See Note [Implementation of UnliftedNewtypes] in TcTyClsDecls, wrinkle (2).
     tc_kind_sig Nothing
-      = return liftedTypeKind
+      = do { unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes
+           ; if unlifted_newtypes && new_or_data == NewType
+               then newOpenTypeKind
+               else pure liftedTypeKind
+           }
+
+    -- See Note [Result kind signature for a data family instance]
     tc_kind_sig (Just hs_kind)
       = do { sig_kind <- tcLHsKindSig data_ctxt hs_kind
            ; let (tvs, inner_kind) = tcSplitForAllTys sig_kind
@@ -852,6 +877,36 @@ we actually have a place to put the regeneralised variables.
 Thus: skolemise away. cf. Inst.deeplySkolemise and TcUnify.tcSkolemise
 Examples in indexed-types/should_compile/T12369
 
+Note [Unifying data family kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we kind-check a newtype instance with -XUnliftedNewtypes, we must
+unify the kind of the data family with any declared kind in the instance
+declaration. For example:
+
+  data Color = Red | Blue
+  type family Interpret (x :: Color) :: RuntimeRep where
+    Interpret 'Red = 'IntRep
+    Interpret 'Blue = 'WordRep
+  data family Foo (x :: Color) :: TYPE (Interpret x)
+  newtype instance Foo 'Red :: TYPE IntRep where
+    FooRedC :: Int# -> Foo 'Red
+
+We end up unifying `TYPE (Interpret 'Red)` (the kind of Foo, instantiated
+with 'Red) and `TYPE IntRep` (the declared kind of the instance). This
+unification succeeds, resulting in a coercion. The big question: what to
+do with this coercion? Answer: nothing! A kind annotation on a newtype instance
+is always redundant (except, perhaps, in that it helps guide unification). We
+have a definitive kind for the data family from the data family declaration,
+and so we learn nothing really new from the kind signature on an instance.
+We still must perform this unification (done in the call to checkExpectedKind
+toward the beginning of tcDataFamHeader), but the result is unhelpful. If there
+is a cast, it will wrap the lhs_ty, and so we just drop it before splitting the
+lhs_ty to reveal the underlying patterns. Because of the potential of dropping
+a cast like this, we just use typeKind in the result instead of propagating res_kind
+from above.
+
+This Note is wrinkle (3) in Note [Implementation of UnliftedNewtypes] in TcTyClsDecls.
+
 Note [Eta-reduction for data families]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index fdb956aedd..31274fa05f 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -80,6 +80,7 @@ module TcMType (
   zonkCt, zonkSkolemInfo,
 
   tcGetGlobalTyCoVars,
+  skolemiseUnboundMetaTyVar,
 
   ------------------------------
   -- Levity polymorphism
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index a181377b62..d16be28773 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -30,9 +30,7 @@ import GhcPrelude
 
 import Bag
 import Class         ( Class, classKey, classTyCon )
-import DynFlags      ( WarningFlag ( Opt_WarnMonomorphism )
-                     , WarnReason ( Reason )
-                     , DynFlags( solverIterations ) )
+import DynFlags
 import HsExpr        ( UnboundVar(..) )
 import Id            ( idType, mkLocalId )
 import Inst
@@ -229,12 +227,16 @@ simpl_top :: WantedConstraints -> TcS WantedConstraints
 simpl_top wanteds
   = do { wc_first_go <- nestTcS (solveWantedsAndDrop wanteds)
                             -- This is where the main work happens
-       ; try_tyvar_defaulting wc_first_go }
+       ; dflags <- getDynFlags
+       ; try_tyvar_defaulting dflags wc_first_go }
   where
-    try_tyvar_defaulting :: WantedConstraints -> TcS WantedConstraints
-    try_tyvar_defaulting wc
+    try_tyvar_defaulting :: DynFlags -> WantedConstraints -> TcS WantedConstraints
+    try_tyvar_defaulting dflags wc
       | isEmptyWC wc
       = return wc
+      | insolubleWC wc
+      , gopt Opt_PrintExplicitRuntimeReps dflags -- See Note [Defaulting insolubles]
+      = try_class_defaulting wc
       | otherwise
       = do { free_tvs <- TcS.zonkTyCoVarsAndFVList (tyCoVarsOfWCList wc)
            ; let meta_tvs = filter (isTyVar <&&> isMetaTyVar) free_tvs
@@ -252,7 +254,7 @@ simpl_top wanteds
 
     try_class_defaulting :: WantedConstraints -> TcS WantedConstraints
     try_class_defaulting wc
-      | isEmptyWC wc
+      | isEmptyWC wc || insolubleWC wc -- See Note [Defaulting insolubles]
       = return wc
       | otherwise  -- See Note [When to do type-class defaulting]
       = do { something_happened <- applyDefaultingRules wc
@@ -518,6 +520,50 @@ solveWantedsAndDrop, not simpl_top, so that we do no defaulting.
 This is ambiguous of course, but we don't want to default the
 (Num alpha) constraint to (Num Int)!  Doing so gives a defaulting
 warning, but no error.
+
+Note [Defaulting insolubles]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If a set of wanteds is insoluble, we have no hope of accepting the
+program. Yet we do not stop constraint solving, etc., because we may
+simplify the wanteds to produce better error messages. So, once
+we have an insoluble constraint, everything we do is just about producing
+helpful error messages.
+
+Should we default in this case or not? Let's look at an example (tcfail004):
+
+  (f,g) = (1,2,3)
+
+With defaulting, we get a conflict between (a0,b0) and (Integer,Integer,Integer).
+Without defaulting, we get a conflict between (a0,b0) and (a1,b1,c1). I (Richard)
+find the latter more helpful. Several other test cases (e.g. tcfail005) suggest
+similarly. So: we should not do class defaulting with insolubles.
+
+On the other hand, RuntimeRep-defaulting is different. Witness tcfail078:
+
+  f :: Integer i => i
+  f =               0
+
+Without RuntimeRep-defaulting, we GHC suggests that Integer should have kind
+TYPE r0 -> Constraint and then complains that r0 is actually untouchable
+(presumably, because it can't be sure if `Integer i` entails an equality).
+If we default, we are told of a clash between (* -> Constraint) and Constraint.
+The latter seems far better, suggesting we *should* do RuntimeRep-defaulting
+even on insolubles.
+
+But, evidently, not always. Witness UnliftedNewtypesInfinite:
+
+  newtype Foo = FooC (# Int#, Foo #)
+
+This should fail with an occurs-check error on the kind of Foo (with -XUnliftedNewtypes).
+If we default RuntimeRep-vars, we get
+
+  Expecting a lifted type, but ‘(# Int#, Foo #)’ is unlifted
+
+which is just plain wrong.
+
+Conclusion: we should do RuntimeRep-defaulting on insolubles only when the user does not
+want to hear about RuntimeRep stuff -- that is, when -fprint-explicit-runtime-reps
+is not set.
 -}
 
 ------------------
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index fc14b9605b..9d2aea8d15 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -37,6 +37,7 @@ import TcTyDecls
 import TcClassDcl
 import {-# SOURCE #-} TcInstDcls( tcInstDecls1 )
 import TcDeriv (DerivInfo)
+import TcUnify ( unifyKind )
 import TcHsType
 import ClsInst( AssocInstInfo(..) )
 import TcMType
@@ -1030,9 +1031,15 @@ getInitialKind cusk
                                          , dd_ND = new_or_data } })
   = do  { let flav = newOrDataToFlavour new_or_data
         ; tc <- kcLHsQTyVars name flav cusk ktvs $
-                case m_sig of
-                   Just ksig -> tcLHsKindSig (DataKindCtxt name) ksig
-                   Nothing   -> return liftedTypeKind
+                -- See Note [Implementation of UnliftedNewtypes]
+                do { unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes
+                   ; case m_sig of
+                       Just ksig -> tcLHsKindSig (DataKindCtxt name) ksig
+                       Nothing
+                         |  NewType <- new_or_data
+                         ,  unlifted_newtypes -> newOpenTypeKind
+                         |  otherwise -> pure liftedTypeKind
+                   }
         ; return [tc] }
 
 getInitialKind cusk (FamDecl { tcdFam = decl })
@@ -1127,8 +1134,13 @@ kcTyClDecl :: TyClDecl GhcRn -> TcM ()
 kcTyClDecl (DataDecl { tcdLName    = (dL->L _ name)
                      , tcdDataDefn = defn })
   | HsDataDefn { dd_cons = cons@((dL->L _ (ConDeclGADT {})) : _)
-               , dd_ctxt = (dL->L _ []) } <- defn
-  = mapM_ (wrapLocM_ kcConDecl) cons
+               , dd_ctxt = (dL->L _ [])
+               , dd_ND = new_or_data } <- defn
+  = do { tyCon <- kcLookupTcTyCon name
+         -- See Note [Implementation of UnliftedNewtypes] STEP 2
+       ; (_, final_res_kind) <- etaExpandAlgTyCon (tyConBinders tyCon) (tyConResKind tyCon)
+       ; mapM_ (wrapLocM_ (kcConDecl new_or_data final_res_kind)) cons
+       }
     -- hs_tvs and dd_kindSig already dealt with in getInitialKind
     -- This must be a GADT-style decl,
     --        (see invariants of DataDefn declaration)
@@ -1136,10 +1148,14 @@ kcTyClDecl (DataDecl { tcdLName    = (dL->L _ name)
     --        ConDecls bind all their own variables
     --    (b) dd_ctxt is not allowed for GADT-style decls, so we can ignore it
 
-  | HsDataDefn { dd_ctxt = ctxt, dd_cons = cons } <- defn
+  | HsDataDefn { dd_ctxt = ctxt
+               , dd_cons = cons
+               , dd_ND = new_or_data } <- defn
   = bindTyClTyVars name $ \ _ _ ->
-    do  { _ <- tcHsContext ctxt
-        ; mapM_ (wrapLocM_ kcConDecl) cons }
+    do { _ <- tcHsContext ctxt
+       ; tyCon <- kcLookupTcTyCon name
+       ; mapM_ (wrapLocM_ (kcConDecl new_or_data (tyConResKind tyCon))) cons
+       }
 
 kcTyClDecl (SynDecl { tcdLName = dL->L _ name, tcdRhs = rhs })
   = bindTyClTyVars name $ \ _ res_kind ->
@@ -1172,23 +1188,66 @@ kcTyClDecl (DataDecl _ _ _ _ (XHsDataDefn _)) = panic "kcTyClDecl"
 kcTyClDecl (XTyClDecl _)                            = panic "kcTyClDecl"
 
 -------------------
-kcConDecl :: ConDecl GhcRn -> TcM ()
-kcConDecl (ConDeclH98 { con_name = name, con_ex_tvs = ex_tvs
-                      , con_mb_cxt = ex_ctxt, con_args = args })
+
+-- | Unify the kind of the first type provided with the newtype's kind, if
+-- -XUnliftedNewtypes is enabled and the NewOrData indicates Newtype. If there
+-- is more than one type provided, do nothing: the newtype is in error, and this
+-- will be caught in validity checking (which will give a better error than we can
+-- here.)
+unifyNewtypeKind :: DynFlags
+                 -> NewOrData
+                 -> [LHsType GhcRn]   -- user-written argument types, should be just 1
+                 -> [TcType]          -- type-checked argument types, should be just 1
+                 -> TcKind            -- expected kind of newtype
+                 -> TcM [TcType]      -- casted argument types (should be just 1)
+                                      --  result = orig_arg |> kind_co
+                                      -- where kind_co :: orig_arg_ki ~N expected_ki
+unifyNewtypeKind dflags NewType [hs_ty] [tc_ty] ki
+  | xopt LangExt.UnliftedNewtypes dflags
+  = do { traceTc "unifyNewtypeKind" (ppr hs_ty $$ ppr tc_ty $$ ppr ki)
+       ; co <- unifyKind (Just (unLoc hs_ty)) (typeKind tc_ty) ki
+       ; return [tc_ty `mkCastTy` co] }
+  -- See comments above: just do nothing here
+unifyNewtypeKind _ _ _ arg_tys _ = return arg_tys
+
+-- Type check the types of the arguments to a data constructor.
+-- This includes doing kind unification if the type is a newtype.
+-- See Note [Implementation of UnliftedNewtypes] for why we need
+-- the first two arguments.
+kcConArgTys :: NewOrData -> Kind -> [LHsType GhcRn] -> TcM ()
+kcConArgTys new_or_data res_kind arg_tys = do
+  { arg_tc_tys <- mapM (tcHsOpenType . getBangType) arg_tys
+    -- See Note [Implementation of UnliftedNewtypes], STEP 2
+  ; dflags <- getDynFlags
+  ; discardResult $
+      unifyNewtypeKind dflags new_or_data arg_tys arg_tc_tys res_kind
+  }
+
+-- Kind check a data constructor. In additional to the data constructor,
+-- we also need to know about whether or not its corresponding type was
+-- declared with data or newtype, and we need to know the result kind of
+-- this type. See Note [Implementation of UnliftedNewtypes] for why
+-- we need the first two arguments.
+kcConDecl ::
+     NewOrData -- Was the corresponding type declared with data or newtype?
+  -> Kind -- The result kind of the corresponding type constructor
+  -> ConDecl GhcRn -- The data constructor
+  -> TcM ()
+kcConDecl new_or_data res_kind (ConDeclH98
+  { con_name = name, con_ex_tvs = ex_tvs
+  , con_mb_cxt = ex_ctxt, con_args = args })
   = addErrCtxt (dataConCtxtName [name]) $
     discardResult                   $
     bindExplicitTKBndrs_Tv ex_tvs $
     do { _ <- tcHsMbContext ex_ctxt
-       ; traceTc "kcConDecl {" (ppr name $$ ppr args)
-       ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys args)
-       ; traceTc "kcConDecl }" (ppr name)
+       ; kcConArgTys new_or_data res_kind (hsConDeclArgTys args)
+         -- We don't need to check the telescope here, because that's
+         -- done in tcConDecl
        }
-              -- We don't need to check the telescope here, because that's
-              -- done in tcConDecl
 
-kcConDecl (ConDeclGADT { con_names = names
-                       , con_qvars = qtvs, con_mb_cxt = cxt
-                       , con_args = args, con_res_ty = res_ty })
+kcConDecl new_or_data res_kind (ConDeclGADT
+    { con_names = names, con_qvars = qtvs, con_mb_cxt = cxt
+    , con_args = args, con_res_ty = res_ty })
   | HsQTvs { hsq_ext = implicit_tkv_nms
            , hsq_explicit = explicit_tkv_nms } <- qtvs
   = -- Even though the data constructor's type is closed, we
@@ -1204,11 +1263,11 @@ kcConDecl (ConDeclGADT { con_names = names
     bindExplicitTKBndrs_Tv explicit_tkv_nms $
         -- Why "_Tv"?  See Note [Kind-checking for GADTs]
     do { _ <- tcHsMbContext cxt
-       ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys args)
+       ; kcConArgTys new_or_data res_kind (hsConDeclArgTys args)
        ; _ <- tcHsOpenType res_ty
        ; return () }
-kcConDecl (XConDecl _) = panic "kcConDecl"
-kcConDecl (ConDeclGADT _ _ _ (XLHsQTyVars _) _ _ _ _) = panic "kcConDecl"
+kcConDecl _ _ (ConDeclGADT _ _ _ (XLHsQTyVars _) _ _ _ _) = panic "kcConDecl"
+kcConDecl _ _ (XConDecl _) = panic "kcConDecl"
 
 {-
 Note [Recursion and promoting data constructors]
@@ -1354,6 +1413,112 @@ For wired-in things we simply ignore the declaration
 and take the wired-in information.  That avoids complications.
 e.g. the need to make the data constructor worker name for
      a constraint tuple match the wired-in one
+
+Note [Implementation of UnliftedNewtypes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Expected behavior of UnliftedNewtypes:
+
+* Proposal: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0013-unlifted-newtypes.rst
+* Discussion: https://github.com/ghc-proposals/ghc-proposals/pull/98
+
+What follows is a high-level overview of the implementation of the
+proposal.
+
+STEP 1: Getting the initial kind, as done by getInitialKind. We have
+two sub-cases (assuming we have a newtype and -XUnliftedNewtypes is enabled):
+
+* With a CUSK: no change in kind-checking; the tycon is given the kind
+  the user writes, whatever it may be.
+
+* Without a CUSK: If there is no kind signature, the tycon is given
+  a kind `TYPE r`, for a fresh unification variable `r`.
+
+STEP 2: Kind-checking, as done by kcTyClDecl. This step is skipped for CUSKs.
+The key function here is kcConDecl, which looks at an individual constructor
+declaration. In the unlifted-newtypes case (i.e., -XUnliftedNewtypes and,
+indeed, we are processing a newtype), we call unifyNewtypeKind, which is a
+thin wrapper around unifyKind, unifying the kind of the one argument and the
+result kind of the newtype tycon.
+
+Examples of newtypes affected by STEP 2, assuming -XUnliftedNewtypes is
+enabled (we use r0 to denote a unification variable):
+
+newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
++ kcConDecl unifies (TYPE r0) with (TYPE rep), where (TYPE r0)
+  is the kind that getInitialKind invented for (Foo rep).
+
+data Color = Red | Blue
+type family Interpret (x :: Color) :: RuntimeRep where
+  Interpret 'Red = 'IntRep
+  Interpret 'Blue = 'WordRep
+data family Foo (x :: Color) :: TYPE (Interpret x)
+newtype instance Foo 'Red = FooRedC Int#
++ kcConDecl unifies TYPE (Interpret 'Red) with TYPE 'IntRep
+
+Note that, in the GADT case, we might have a kind signature with arrows
+(newtype XYZ a b :: Type -> Type where ...). We want only the final
+component of the kind for checking in kcConDecl, so we call etaExpandAlgTyCon
+in kcTyClDecl.
+
+STEP 3: Type-checking (desugaring), as done by tcTyClDecl. The key function
+here is tcConDecl. Once again, we must call unifyNewtypeKind, for two reasons:
+
+  A. It is possible that a GADT has a CUSK. (Note that this is *not*
+     possible for H98 types. Recall that CUSK types don't go through
+     kcTyClDecl, so we might not have done this kind check.
+  B. We need to produce the coercion to put on the argument type
+     if the kinds are different (for both H98 and GADT).
+
+Example of (B):
+
+type family F a where
+  F Int = LiftedRep
+
+newtype N :: TYPE (F Int) where
+  MkN :: Int -> N
+
+We really need to have the argument to MkN be (Int |> TYPE (sym axF)), where
+axF :: F Int ~ LiftedRep. That way, the argument kind is the same as the
+newtype kind, which is the principal correctness condition for newtypes.
+This call to unifyNewtypeKind is what produces that coercion.
+
+Note that this is possible in the H98 case only for a data family, because
+the H98 syntax doesn't permit a kind signature on the newtype itself.
+
+
+1. In tcFamDecl1, we suppress a tcIsLiftedTypeKind check if
+   UnliftedNewtypes is on. This allows us to write things like:
+     data family Foo :: TYPE 'IntRep
+
+2. In a newtype instance (with -XUnliftedNewtypes), if the user does
+   not write a kind signature, we want to allow the possibility that
+   the kind is not Type, so we use newOpenTypeKind instead of liftedTypeKind.
+   This is done in tcDataFamHeader in TcInstDcls. Example:
+
+       data family Bar (a :: RuntimeRep) :: TYPE a
+       newtype instance Bar 'IntRep = BarIntC Int#
+       newtype instance Bar 'WordRep :: TYPE 'WordRep where
+         BarWordC :: Word# -> Bar 'WordRep
+
+   The data instance corresponding to IntRep does not specify a kind signature,
+   so tc_kind_sig just returns `TYPE r0` (where `r0` is a fresh metavariable).
+   The data instance corresponding to WordRep does have a kind signature, so
+   we use that kind signature.
+
+3. A data family and its newtype instance may be declared with slightly
+   different kinds. See Note [Unifying data family kinds] in TcInstDcls.
+
+There's also a change in the renamer:
+
+* In RnSource.rnTyClDecl, enabling UnliftedNewtypes changes what is means
+  for a newtype to have a CUSK. This is necessary since UnliftedNewtypes
+  means that, for newtypes without kind signatures, we must use the field
+  inside the data constructor to determine the result kind.
+  See Note [Unlifted Newtypes and CUSKs] for more detail.
+
+For completeness, it was also neccessary to make coerce work on
+unlifted types, resolving #13595.
+
 -}
 
 tcTyClDecl :: RolesInfo -> LTyClDecl GhcRn -> TcM TyCon
@@ -1709,11 +1874,18 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info
   --   Type or a kind-variable
   -- For the latter, consider
   --   data family D a :: forall k. Type -> k
+  -- When UnliftedNewtypes is enabled, we loosen this restriction
+  -- on the return kind. See Note [Implementation of UnliftedNewtypes], wrinkle (1).
   ; let (_, final_res_kind) = splitPiTys res_kind
-  ; checkTc (tcIsLiftedTypeKind final_res_kind
-             || isJust (tcGetCastedTyVar_maybe final_res_kind))
-            (badKindSig False res_kind)
-
+  ; unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes
+  ; checkTc
+      (  (if unlifted_newtypes
+            then tcIsRuntimeTypeKind final_res_kind
+            else tcIsLiftedTypeKind final_res_kind
+         )
+      || isJust (tcGetCastedTyVar_maybe final_res_kind)
+      )
+      (badKindSig False res_kind)
   ; tc_rep_name <- newTyConRepName tc_name
   ; let tycon = mkFamilyTyCon tc_name binders
                               res_kind
@@ -1860,10 +2032,16 @@ tcDataDefn roles_info
 
        ; tcg_env <- getGblEnv
        ; (extra_bndrs, final_res_kind) <- etaExpandAlgTyCon tycon_binders res_kind
-
        ; let hsc_src = tcg_src tcg_env
-       ; unless (mk_permissive_kind hsc_src cons) $
-         checkTc (tcIsLiftedTypeKind final_res_kind) (badKindSig True res_kind)
+       ; unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes
+       ; let allowUnlifted = unlifted_newtypes && new_or_data == NewType
+       ; unless (mk_permissive_kind hsc_src cons || allowUnlifted) $
+           checkTc
+             (if allowUnlifted
+                then tcIsRuntimeTypeKind final_res_kind
+                else tcIsLiftedTypeKind final_res_kind
+             )
+             (badKindSig True res_kind)
 
        ; stupid_tc_theta <- pushTcLevelM_ $ solveEqualities $ tcHsContext ctxt
        ; stupid_theta    <- zonkTcTypesToTypes stupid_tc_theta
@@ -1877,8 +2055,13 @@ tcDataDefn roles_info
              { let final_bndrs = tycon_binders `chkAppend` extra_bndrs
                    res_ty      = mkTyConApp tycon (mkTyVarTys (binderVars final_bndrs))
                    roles       = roles_info tc_name
-
-             ; data_cons <- tcConDecls tycon final_bndrs res_ty cons
+             ; data_cons <- tcConDecls
+                              tycon
+                              new_or_data
+                              final_bndrs
+                              final_res_kind
+                              res_ty
+                              cons
              ; tc_rhs    <- mk_tc_rhs hsc_src tycon data_cons
              ; tc_rep_nm <- newTyConRepName tc_name
              ; return (mkAlgTyCon tc_name
@@ -1976,11 +2159,9 @@ tcTyFamInstEqn fam_tc mb_clsinfo
              vis_pats  = numVisibleArgs hs_pats
        ; checkTc (vis_pats == vis_arity) $
          wrongNumberOfParmsErr vis_arity
-
        ; (qtvs, pats, rhs_ty) <- tcTyFamInstEqnGuts fam_tc mb_clsinfo
                                       imp_vars (mb_expl_bndrs `orElse` [])
                                       hs_pats hs_rhs_ty
-
        -- Don't print results they may be knot-tied
        -- (tcFamInstEqnGuts zonks to Type)
        ; return (mkCoAxBranch qtvs [] [] pats rhs_ty
@@ -2015,7 +2196,7 @@ indexed-types/should_compile/T12369 for an example.
 So, the kind-checker must return the new skolems and args (that is, Type
 or (Type -> Type) for the equations above) and the instantiated kind.
 
-Note [Generalising in tcFamTyPatsGuts]
+Note [Generalising in tcTyFamInstEqnGuts]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we have something like
   type instance forall (a::k) b. F t1 t2 = rhs
@@ -2073,7 +2254,7 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty
                      ; rhs_ty <- tcCheckLHsType hs_rhs_ty rhs_kind
                      ; return (lhs_ty, rhs_ty) }
 
-       -- See Note [Generalising in tcFamTyPatsGuts]
+       -- See Note [Generalising in tcTyFamInstEqnGuts]
        -- This code (and the stuff immediately above) is very similar
        -- to that in tcDataFamHeader.  Maybe we should abstract the
        -- common code; but for the moment I concluded that it's
@@ -2130,15 +2311,12 @@ unravelFamInstPats :: TcType -> [TcType]
 unravelFamInstPats fam_app
   = case splitTyConApp_maybe fam_app of
       Just (_, pats) -> pats
-      Nothing        -> WARN( True, bad_lhs fam_app ) []
+      Nothing -> panic "unravelFamInstPats: Ill-typed LHS of family instance"
         -- The Nothing case cannot happen for type families, because
         -- we don't call unravelFamInstPats until we've solved the
-        -- equalities.  For data families I wasn't quite as convinced
-        -- so I've let it as a warning rather than a panic.
-  where
-    bad_lhs fam_app
-      = hang (text "Ill-typed LHS of family instance")
-           2 (debugPprType fam_app)
+        -- equalities. For data families, it shouldn't happen either,
+        -- we need to fail hard and early if it does. See trac issue #15905
+        -- for an example of this happening.
 
 addConsistencyConstraints :: AssocInstInfo -> TcType -> TcM ()
 -- In the corresponding positions of the class and type-family,
@@ -2295,25 +2473,26 @@ consUseGadtSyntax _                                = False
                  -- All constructors have same shape
 
 -----------------------------------
-tcConDecls :: KnotTied TyCon -> [KnotTied TyConBinder] -> KnotTied Type
-           -> [LConDecl GhcRn] -> TcM [DataCon]
-  -- Why both the tycon tyvars and binders? Because the tyvars
-  -- have all the names and the binders have the visibilities.
-tcConDecls rep_tycon tmpl_bndrs res_tmpl
+tcConDecls :: KnotTied TyCon -> NewOrData
+           -> [TyConBinder] -> TcKind   -- binders and result kind of tycon
+           -> KnotTied Type -> [LConDecl GhcRn] -> TcM [DataCon]
+tcConDecls rep_tycon new_or_data tmpl_bndrs res_kind res_tmpl
   = concatMapM $ addLocM $
-    tcConDecl rep_tycon (mkTyConTagMap rep_tycon) tmpl_bndrs res_tmpl
+    tcConDecl rep_tycon (mkTyConTagMap rep_tycon)
+              tmpl_bndrs res_kind res_tmpl new_or_data
     -- It's important that we pay for tag allocation here, once per TyCon,
     -- See Note [Constructor tag allocation], fixes #14657
 
 tcConDecl :: KnotTied TyCon          -- Representation tycon. Knot-tied!
           -> NameEnv ConTag
-          -> [KnotTied TyConBinder] -> KnotTied Type
-                 -- Return type template (with its template tyvars)
-                 --    (tvs, T tys), where T is the family TyCon
+          -> [TyConBinder] -> TcKind   -- tycon binders and result kind
+          -> KnotTied Type
+                 -- Return type template (T tys), where T is the family TyCon
+          -> NewOrData
           -> ConDecl GhcRn
           -> TcM [DataCon]
 
-tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
+tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data
           (ConDeclH98 { con_name = name
                       , con_ex_tvs = explicit_tkv_nms
                       , con_mb_cxt = hs_ctxt
@@ -2337,7 +2516,12 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
                  ; btys <- tcConArgs hs_args
                  ; field_lbls <- lookupConstructorFields (unLoc name)
                  ; let (arg_tys, stricts) = unzip btys
-                 ; return (ctxt, arg_tys, field_lbls, stricts)
+                 ; dflags <- getDynFlags
+                 ; final_arg_tys <-
+                     unifyNewtypeKind dflags new_or_data
+                                      (hsConDeclArgTys hs_args)
+                                      arg_tys res_kind
+                 ; return (ctxt, final_arg_tys, field_lbls, stricts)
                  }
 
          -- exp_tvs have explicit, user-written binding sites
@@ -2393,7 +2577,9 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
        ; mapM buildOneDataCon [name]
        }
 
-tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
+tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data
+  -- NB: don't use res_kind here, as it's ill-scoped. Instead, we get
+  -- the res_kind by typechecking the result type.
           (ConDeclGADT { con_names = names
                        , con_qvars = qtvs
                        , con_mb_cxt = cxt, con_args = hs_args
@@ -2412,13 +2598,19 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
               bindExplicitTKBndrs_Skol explicit_tkv_nms $
               do { ctxt <- tcHsMbContext cxt
                  ; btys <- tcConArgs hs_args
-                 ; res_ty <- tcHsLiftedType hs_res_ty
-                 ; field_lbls <- lookupConstructorFields name
                  ; let (arg_tys, stricts) = unzip btys
-                 ; return (ctxt, arg_tys, res_ty, field_lbls, stricts)
+                 ; res_ty <- tcHsOpenType hs_res_ty
+                   -- See Note [Implementation of unlifted newtypes]
+                 ; dflags <- getDynFlags
+                 ; final_arg_tys <-
+                     unifyNewtypeKind dflags new_or_data
+                                      (hsConDeclArgTys hs_args)
+                                      arg_tys (typeKind res_ty)
+                 ; field_lbls <- lookupConstructorFields name
+                 ; return (ctxt, final_arg_tys, res_ty, field_lbls, stricts)
                  }
        ; imp_tvs <- zonkAndScopedSort imp_tvs
-       ; let user_tvs = imp_tvs ++ exp_tvs
+       ; let user_tvs      = imp_tvs ++ exp_tvs
 
        ; tkvs <- kindGeneralize (mkSpecForAllTys user_tvs $
                                  mkPhiTy ctxt $
@@ -2471,9 +2663,9 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
        ; traceTc "tcConDecl 2" (ppr names)
        ; mapM buildOneDataCon names
        }
-tcConDecl _ _ _ _ (ConDeclGADT _ _ _ (XLHsQTyVars _) _ _ _ _)
+tcConDecl _ _ _ _ _ _ (ConDeclGADT _ _ _ (XLHsQTyVars _) _ _ _ _)
   = panic "tcConDecl"
-tcConDecl _ _ _ _ (XConDecl _) = panic "tcConDecl"
+tcConDecl _ _ _ _ _ _ (XConDecl _) = panic "tcConDecl"
 
 tcConIsInfixH98 :: Name
              -> HsConDetails (LHsType GhcRn) (Located [LConDeclField GhcRn])
@@ -2580,11 +2772,10 @@ errors reported in one pass.  See #7175, and #10836.
 rejigConRes :: [KnotTied TyConBinder] -> KnotTied Type    -- Template for result type; e.g.
                                   -- data instance T [a] b c ...
                                   --      gives template ([a,b,c], T [a] b c)
-                                  -- Type must be of kind *!
             -> [TyVar]            -- The constructor's inferred type variables
             -> [TyVar]            -- The constructor's user-written, specified
                                   -- type variables
-            -> KnotTied Type      -- res_ty type must be of kind *
+            -> KnotTied Type      -- res_ty
             -> ([TyVar],          -- Universal
                 [TyVar],          -- Existential (distinct OccNames from univs)
                 [TyVar],          -- The constructor's rejigged, user-written,
@@ -2613,9 +2804,7 @@ rejigConRes tmpl_bndrs res_tmpl dc_inferred_tvs dc_specified_tvs res_ty
         -- So we return ( [a,b,z], [x,y]
         --              , [], [x,y,z]
         --              , [a~(x,y),b~z], <arg-subst> )
-  | Just subst <- ASSERT( isLiftedTypeKind (tcTypeKind res_ty) )
-                  ASSERT( isLiftedTypeKind (tcTypeKind res_tmpl) )
-                  tcMatchTy res_tmpl res_ty
+  | Just subst <- tcMatchTy res_tmpl res_ty
   = let (univ_tvs, raw_eqs, kind_subst) = mkGADTVars tmpl_tvs dc_tvs subst
         raw_ex_tvs = dc_tvs `minusList` univ_tvs
         (arg_subst, substed_ex_tvs) = substTyVarBndrs kind_subst raw_ex_tvs
@@ -3153,8 +3342,13 @@ checkValidDataCon dflags existential_ok tc con
 
           -- Check all argument types for validity
         ; checkValidType ctxt (dataConUserType con)
-        ; mapM_ (checkForLevPoly empty)
-                (dataConOrigArgTys con)
+
+          -- If we are dealing with a newtype, we allow levity polymorphism
+          -- regardless of whether or not UnliftedNewtypes is enabled. A
+          -- later check in checkNewDataCon handles this, producing a
+          -- better error message than checkForLevPoly would.
+        ; unless (isNewTyCon tc)
+            (mapM_ (checkForLevPoly empty) (dataConOrigArgTys con))
 
           -- Extra checks for newtype data constructors
         ; when (isNewTyCon tc) (checkNewDataCon con)
@@ -3237,8 +3431,13 @@ checkNewDataCon con
   = do  { checkTc (isSingleton arg_tys) (newtypeFieldErr con (length arg_tys))
               -- One argument
 
-        ; checkTc (not (isUnliftedType arg_ty1)) $
-          text "A newtype cannot have an unlifted argument type"
+        ; unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes
+        ; let allowedArgType =
+                unlifted_newtypes || isLiftedType_maybe arg_ty1 == Just True
+        ; checkTc allowedArgType $ vcat
+          [ text "A newtype cannot have an unlifted argument type"
+          , text "Perhaps you intended to use UnliftedNewtypes"
+          ]
 
         ; check_con (null eq_spec) $
           text "A newtype constructor must have a return type of form T a1 ... an"
diff --git a/compiler/typecheck/TcTypeable.hs b/compiler/typecheck/TcTypeable.hs
index cf7700a98f..3488957366 100644
--- a/compiler/typecheck/TcTypeable.hs
+++ b/compiler/typecheck/TcTypeable.hs
@@ -17,7 +17,7 @@ import GhcPrelude
 import BasicTypes ( Boxity(..), neverInlinePragma, SourceText(..) )
 import TcBinds( addTypecheckedBinds )
 import IfaceEnv( newGlobalBinder )
-import TyCoRep( Type(..), TyLit(..) )
+import TyCoRep( Type(..), TyLit(..), isLiftedTypeKind )
 import TcEnv
 import TcEvidence ( mkWpTyApps )
 import TcRnMonad
@@ -426,12 +426,14 @@ tyConIsTypeable tc =
 -- polytypes and types containing casts (which may be, for instance, a type
 -- family).
 typeIsTypeable :: Type -> Bool
--- We handle types of the form (TYPE rep) specifically to avoid
--- looping on (tyConIsTypeable RuntimeRep)
+-- We handle types of the form (TYPE LiftedRep) specifically to avoid
+-- looping on (tyConIsTypeable RuntimeRep). We used to consider (TYPE rr)
+-- to be typeable without inspecting rr, but this exhibits bad behavior
+-- when rr is a type family.
 typeIsTypeable ty
   | Just ty' <- coreView ty         = typeIsTypeable ty'
 typeIsTypeable ty
-  | isJust (kindRep_maybe ty)       = True
+  | isLiftedTypeKind ty             = True
 typeIsTypeable (TyVarTy _)          = True
 typeIsTypeable (AppTy a b)          = typeIsTypeable a && typeIsTypeable b
 typeIsTypeable (FunTy _ a b)        = typeIsTypeable a && typeIsTypeable b
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index 8e4efbac50..81331e0b8e 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -62,7 +62,7 @@ module Coercion (
         pickLR,
 
         isGReflCo, isReflCo, isReflCo_maybe, isGReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe,
-        isReflCoVar_maybe,
+        isReflCoVar_maybe, isGReflMCo, coToMCo,
 
         -- ** Coercion variables
         mkCoVar, isCoVar, coVarName, setCoVarName, setCoVarUnique,
@@ -592,6 +592,11 @@ isReflexiveCo_maybe co
   = Nothing
   where (Pair ty1 ty2, r) = coercionKindRole co
 
+coToMCo :: Coercion -> MCoercion
+coToMCo c = if isReflCo c
+  then MRefl
+  else MCo c
+
 {-
 %************************************************************************
 %*                                                                      *
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index ff4501985e..f12a75f89a 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -59,6 +59,7 @@ module Type (
         getRuntimeRep_maybe, kindRep_maybe, kindRep,
 
         mkCastTy, mkCoercionTy, splitCastTy_maybe,
+        discardCast,
 
         userTypeError_maybe, pprUserTypeErrorTy,
 
@@ -137,6 +138,7 @@ module Type (
         -- ** Finding the kind of a type
         typeKind, tcTypeKind, isTypeLevPoly, resultIsLevPoly,
         tcIsLiftedTypeKind, tcIsConstraintKind, tcReturnsConstraintKind,
+        tcIsRuntimeTypeKind,
 
         -- ** Common Kind
         liftedTypeKind,
@@ -1277,6 +1279,21 @@ tyConBindersTyCoBinders = map to_tyb
     to_tyb (Bndr tv (NamedTCB vis)) = Named (Bndr tv vis)
     to_tyb (Bndr tv (AnonTCB af))   = Anon af (varType tv)
 
+-- | Drop the cast on a type, if any. If there is no
+-- cast, just return the original type. This is rarely what
+-- you want. The CastTy data constructor (in TyCoRep) has the
+-- invariant that another CastTy is not inside. See the
+-- data constructor for a full description of this invariant.
+-- Since CastTy cannot be nested, the result of discardCast
+-- cannot be a CastTy.
+discardCast :: Type -> Type
+discardCast (CastTy ty _) = ASSERT(not (isCastTy ty)) ty
+  where
+  isCastTy CastTy{} = True
+  isCastTy _        = False
+discardCast ty            = ty
+
+
 {-
 --------------------------------------------------------------------
                             CoercionTy
@@ -1827,6 +1844,17 @@ tcIsLiftedTypeKind ty
   | otherwise
   = False
 
+-- | Is this kind equivalent to @TYPE r@ (for some unknown r)?
+--
+-- This considers 'Constraint' to be distinct from @*@.
+tcIsRuntimeTypeKind :: Kind -> Bool
+tcIsRuntimeTypeKind ty
+  | Just (tc, _) <- tcSplitTyConApp_maybe ty    -- Note: tcSplit here
+  , tc `hasKey` tYPETyConKey
+  = True
+  | otherwise
+  = False
+
 tcReturnsConstraintKind :: Kind -> Bool
 -- True <=> the Kind ultimately returns a Constraint
 --   E.g.  * -> Constraint