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>
author: Andrew Martin <andrew.thaddeus@gmail.com> 2019-05-12 09:23:25 -0400
committer: Marge Bot <ben+marge-bot@smart-cactus.org> 2019-06-14 10:48:13 -0400
commit: effdd948056923f3bc03688c24d7e0339d6272f5 (patch)
tree: 02a3cb68ce1680db89c8440ba8beea808cbf4a11
parent: 3bc6df3223f62a8366e2e4267bac23aa08e6a939 (diff)
download: haskell-effdd948056923f3bc03688c24d7e0339d6272f5.tar.gz
113 files changed, 1522 insertions, 202 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
diff --git a/docs/users_guide/8.10.1-notes.rst b/docs/users_guide/8.10.1-notes.rst
index fde1451250..dfbb8f9224 100644
--- a/docs/users_guide/8.10.1-notes.rst
+++ b/docs/users_guide/8.10.1-notes.rst
@@ -10,6 +10,8 @@ following sections.
 Highlights
 ----------
 
+- The `UnliftedNewtypes` extension.
+
 Full details
 ------------
 
@@ -83,6 +85,11 @@ Language
         type forall a (f :: forall k. k -> Type).
              T a f = f Int
 
+- A new extension :extension:`UnliftedNewtypes` that relaxes restrictions
+  around what kinds of types can appear inside of the data constructor
+  for a `newtype`. This was proposed in
+  `GHC proposal #13 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0013-unlifted-newtypes.rst>`__.
+             
 Compiler
 ~~~~~~~~
 
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index fdc3b2cafa..36e29c5253 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -178,6 +178,10 @@ There are some restrictions on the use of primitive types:
 
          newtype A = MkA Int#
 
+   However, this restriction can be relaxed by enabling
+   :extension:`-XUnliftedNewtypes`.  The `section on unlifted newtypes
+   <#unlifted-newtypes>`__ details the behavior of such types.
+
 -  You cannot bind a variable with an unboxed type in a *top-level*
    binding.
 
@@ -359,6 +363,77 @@ layout for a sum type works like this:
   as the ``Bool``-like ``(# (# #) | (# #) #)``, the unboxed sum layout only
   has an ``Int32`` tag field (i.e., the whole thing is represented by an integer).
 
+.. _unlifted-newtypes:
+
+Unlifted Newtypes
+-----------------
+
+.. extension:: UnliftedNewtypes
+    :shortdesc: Enable unlifted newtypes.
+
+    :since: 8.10.1
+
+    Enable the use of newtypes over types with non-lifted runtime representations.
+
+``-XUnliftedNewtypes`` relaxes the restrictions around what types can appear inside
+of a `newtype`. For example, the type ::
+
+    newtype A = MkA Int#
+
+is accepted when this extension is enabled. This creates a type
+``A :: TYPE 'IntRep`` and a data constructor ``MkA :: Int# -> A``.
+Although the kind of ``A`` is inferred by GHC, there is nothing visually
+distictive about this type that indicated that is it not of kind ``Type``
+like newtypes typically are. `GADTSyntax <#gadt-style>`__ can be used to
+provide a kind signature for additional clarity ::
+
+    newtype A :: TYPE 'IntRep where
+      MkA :: Int# -> A
+
+The ``Coercible`` machinery works with unlifted newtypes just like it does with
+lifted types. In either of the equivalent formulations of ``A`` given above,
+users would additionally have access to a coercion between ``A`` and ``Int#``.
+
+As a consequence of the
+`levity-polymorphic binder restriction <#levity-polymorphic-restrictions>`__,
+levity-polymorphic fields are disallowed in data constructors
+of data types declared using ``data``. However, since ``newtype`` data
+constructor application is implemented as a coercion instead of as function
+application, this restriction does not apply to the field inside a ``newtype``
+data constructor. Thus, the type checker accepts ::
+
+    newtype Identity# :: forall (r :: RuntimeRep). TYPE r -> TYPE r where
+      MkIdentity# :: forall (r :: RuntimeRep) (a :: TYPE r). a -> Identity# a
+
+And with `UnboxedSums <#unboxed-sums>`__ enabled ::
+
+    newtype Maybe# :: forall (r :: RuntimeRep). TYPE r -> TYPE (SumRep '[r, TupleRep '[]]) where
+      MkMaybe# :: forall (r :: RuntimeRep) (a :: TYPE r). (# a | (# #) #) -> Maybe# a
+
+This extension also relaxes some of the restrictions around data families.
+It must be enabled in modules where either of the following occur:
+
+- A data family is declared with a kind other than ``Type``. Both ``Foo``
+  and ``Bar``, defined below, fall into this category:
+  ::
+     class Foo a where
+       data FooKey a :: TYPE 'IntRep
+     class Bar (r :: RuntimeRep) where
+       data BarType r :: TYPE r
+
+- A ``newtype instance`` is written with a kind other than ``Type``. The
+  following instances of ``Foo`` and ``Bar`` as defined above fall into
+  this category.
+  ::
+     instance Foo Bool where
+       newtype FooKey Bool = FooKeyBoolC Int#
+     instance Bar 'WordRep where
+       newtype BarType 'WordRep = BarTypeWordRepC Word#
+
+This extension impacts the determination of whether or not a newtype has
+a Complete User-Specified Kind Signature (CUSK). The exact impact is specified
+`the section on CUSKs <#complete-kind-signatures>`__.
+
 .. _syntax-extns:
 
 Syntactic extensions
@@ -9097,6 +9172,20 @@ signature" for a type constructor? These are the forms:
      data T2 :: forall k. k -> Type  -- CUSK: `k` is bound explicitly
      data T3 :: forall (k :: Type). k -> Type   -- still a CUSK
 
+-  For a newtype, the rules are the same as they are for a data type
+   unless `UnliftedNewtypes <#unboxed-newtypes>`__ is enabled.
+   With `UnliftedNewtypes <#unboxed-newtypes>`__, the type constructor
+   only has a CUSK if a kind signature is present. As with a datatype
+   with a top-level ``::``, all kind variables must introduced after
+   the ``::`` must be explicitly quantified ::
+
+       {-# LANGUAGE UnliftedNewtypes #-}
+       newtype N1 where                 -- No; missing kind signature
+       newtype N2 :: TYPE 'IntRep where -- Yes; kind signature present
+       newtype N3 (a :: Type) where     -- No; missing kind signature
+       newtype N4 :: k -> Type where    -- No; `k` is not explicitly quantified
+       newtype N5 :: forall (k :: Type). k -> Type where -- Yes; good signature
+
 -  For a class, every type variable must be annotated with a kind.
 
 -  For a type synonym, every type variable and the result type must all
@@ -9617,6 +9706,8 @@ thus say that ``->`` has type
 ``TYPE r1 -> TYPE r2 -> TYPE 'LiftedRep``. The result is always lifted
 because all functions are lifted in GHC.
 
+.. _levity-polymorphic-restrictions:
+
 No levity-polymorphic variables or arguments
 --------------------------------------------
 
diff --git a/libraries/base/Control/Category.hs b/libraries/base/Control/Category.hs
index e8184956f2..96f0c33aed 100644
--- a/libraries/base/Control/Category.hs
+++ b/libraries/base/Control/Category.hs
@@ -23,7 +23,7 @@ module Control.Category where
 import qualified GHC.Base (id,(.))
 import Data.Type.Coercion
 import Data.Type.Equality
-import GHC.Prim (coerce)
+import Data.Coerce (coerce)
 
 infixr 9 .
 infixr 1 >>>, <<<
diff --git a/libraries/base/Data/Coerce.hs b/libraries/base/Data/Coerce.hs
index 9bd7f9a41a..3785b8a104 100644
--- a/libraries/base/Data/Coerce.hs
+++ b/libraries/base/Data/Coerce.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE Unsafe #-}
 {-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE MagicHash #-}
 
 -----------------------------------------------------------------------------
 -- |
@@ -21,9 +22,11 @@
 
 module Data.Coerce
         ( -- * Safe coercions
-          coerce, Coercible,
+          coerce, Coercible
         ) where
 import GHC.Prim (coerce)
 import GHC.Types (Coercible)
 
-import GHC.Base () -- for build ordering; see Notes in GHC.Base for more info
+-- The import of GHC.Base is for build ordering; see Notes in GHC.Base for
+-- more info.
+import GHC.Base ()
diff --git a/libraries/base/Data/Type/Coercion.hs b/libraries/base/Data/Type/Coercion.hs
index b757682a62..694bedec01 100644
--- a/libraries/base/Data/Type/Coercion.hs
+++ b/libraries/base/Data/Type/Coercion.hs
@@ -8,6 +8,7 @@
 {-# LANGUAGE NoImplicitPrelude   #-}
 {-# LANGUAGE PolyKinds           #-}
 {-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE MagicHash           #-}
 
 -----------------------------------------------------------------------------
 -- |
diff --git a/libraries/base/GHC/Base.hs b/libraries/base/GHC/Base.hs
index 6fd2ff735b..2649146816 100644
--- a/libraries/base/GHC/Base.hs
+++ b/libraries/base/GHC/Base.hs
@@ -1156,7 +1156,6 @@ The rules for map work like this.
 
 {-# RULES "map/coerce" [1] map coerce = coerce #-}
 
-
 ----------------------------------------------
 --              append
 ----------------------------------------------
diff --git a/libraries/base/changelog.md b/libraries/base/changelog.md
index a9f6fcf272..3c12e7c511 100644
--- a/libraries/base/changelog.md
+++ b/libraries/base/changelog.md
@@ -9,6 +9,12 @@
     to detect values `<= maxBound::Word` that were incorrectly encoded using
     the `NatJ#` constructor.
 
+  * The type of `coerce` has been generalized. It is now runtime-representation
+    polymorphic:
+    `forall {r :: RuntimeRep} (a :: TYPE r) (b :: TYPE r). Coercible a b => a -> b`.
+    The type argument `r` is marked as `Inferred` to prevent it from
+    interfering with visible type application.
+
 ## 4.13.0.0 *TBA*
   * Bundled with GHC *TBA*
 
diff --git a/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs b/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
index ac47e165ff..ef1d5c9f9f 100644
--- a/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
+++ b/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
@@ -49,6 +49,7 @@ data Extension
    | AllowAmbiguousTypes
    | UnboxedTuples
    | UnboxedSums
+   | UnliftedNewtypes
    | BangPatterns
    | TypeFamilies
    | TypeFamilyDependencies
diff --git a/libraries/ghc-prim/GHC/Types.hs b/libraries/ghc-prim/GHC/Types.hs
index 9f2d3bc15b..7d4e62c381 100644
--- a/libraries/ghc-prim/GHC/Types.hs
+++ b/libraries/ghc-prim/GHC/Types.hs
@@ -282,7 +282,7 @@ class a ~ b
 --      by Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones and Stephanie Weirich.
 --
 --      @since 4.7.0.0
-class Coercible a b
+class Coercible (a :: k) (b :: k)
   -- See also Note [The equality types story] in TysPrim
 
 {- *********************************************************************
diff --git a/testsuite/tests/codeGen/should_fail/T13233.stderr b/testsuite/tests/codeGen/should_fail/T13233.stderr
index c3683138f8..1531abed8e 100644
--- a/testsuite/tests/codeGen/should_fail/T13233.stderr
+++ b/testsuite/tests/codeGen/should_fail/T13233.stderr
@@ -1,23 +1,22 @@
 
 T13233.hs:14:11: error:
-    Cannot use primitive with levity-polymorphic arguments:
+    Cannot use function with levity-polymorphic arguments:
       GHC.Prim.(#,#) :: a -> a -> (# a, a #)
     Levity-polymorphic arguments:
       a :: TYPE rep
       a :: TYPE rep
 
 T13233.hs:22:16: error:
-    Cannot use primitive with levity-polymorphic arguments:
-      GHC.Prim.(#,#) :: forall (rep1 :: RuntimeRep) (rep2 :: RuntimeRep) (a :: TYPE
-                                                                                 rep1) (b :: TYPE
-                                                                                               rep2).
+    Cannot use function with levity-polymorphic arguments:
+      GHC.Prim.(#,#) :: forall (rep1 :: RuntimeRep) (rep2 :: RuntimeRep)
+                               (a :: TYPE rep1) (b :: TYPE rep2).
                         a -> b -> (# a, b #)
     Levity-polymorphic arguments:
       a :: TYPE rep1
       b :: TYPE rep2
 
 T13233.hs:27:10: error:
-    Cannot use primitive with levity-polymorphic arguments:
+    Cannot use function with levity-polymorphic arguments:
       mkWeak# :: a
                  -> b
                  -> (State# RealWorld -> (# State# RealWorld, c #))
diff --git a/testsuite/tests/driver/T4437.hs b/testsuite/tests/driver/T4437.hs
index 09caa7f3c4..c432e4b90e 100644
--- a/testsuite/tests/driver/T4437.hs
+++ b/testsuite/tests/driver/T4437.hs
@@ -39,6 +39,7 @@ expectedGhcOnlyExtensions :: [String]
 expectedGhcOnlyExtensions = ["RelaxedLayout",
                              "AlternativeLayoutRule",
                              "AlternativeLayoutRuleTransitional",
+                             "UnliftedNewtypes",
                              "CUSKs",
                              "ImportQualifiedPost"]
 
diff --git a/testsuite/tests/driver/recomp006/recomp006.stderr b/testsuite/tests/driver/recomp006/recomp006.stderr
index 25b48f375f..84549b6e62 100644
--- a/testsuite/tests/driver/recomp006/recomp006.stderr
+++ b/testsuite/tests/driver/recomp006/recomp006.stderr
@@ -1,7 +1,6 @@
 
 A.hs:8:8:
-    Couldn't match expected type ‘Int’
-                with actual type ‘(Integer, Integer)’
+    Couldn't match expected type ‘Int’ with actual type ‘(a0, b0)’
     In the expression: (2, 3)
     In the expression: (1, (2, 3))
     In an equation for ‘f’: f = (1, (2, 3))
diff --git a/testsuite/tests/ffi/should_run/UnliftedNewtypesByteArrayOffset.hs b/testsuite/tests/ffi/should_run/UnliftedNewtypesByteArrayOffset.hs
new file mode 100644
index 0000000000..8e0aaeef50
--- /dev/null
+++ b/testsuite/tests/ffi/should_run/UnliftedNewtypesByteArrayOffset.hs
@@ -0,0 +1,47 @@
+{-# language ForeignFunctionInterface #-}
+{-# language GADTSyntax #-}
+{-# language KindSignatures #-}
+{-# language MagicHash #-}
+{-# language UnboxedTuples #-}
+{-# language UnliftedFFITypes #-}
+{-# language UnliftedNewtypes #-}
+
+{-# OPTIONS_GHC -O2 #-}
+
+import Data.Kind (Type)
+import Data.Word
+import GHC.Exts
+import GHC.IO
+import GHC.Word
+
+foreign import ccall unsafe "head_bytearray"
+  c_head_bytearray_a :: MutableByteArray# RealWorld -> IO Word8
+foreign import ccall unsafe "head_bytearray"
+  c_head_bytearray_b :: MyArray# -> IO Word8
+
+newtype MyArray# :: TYPE 'UnliftedRep where
+  MyArray# :: MutableByteArray# RealWorld -> MyArray#
+
+data MutableByteArray :: Type where
+  MutableByteArray :: MutableByteArray# RealWorld -> MutableByteArray
+
+main :: IO ()
+main = do
+  ba@(MutableByteArray ba#) <- luckySingleton
+  print =<< readByteArray ba 0
+  print =<< c_head_bytearray_a ba#
+  print =<< c_head_bytearray_b (MyArray# ba#)
+
+readByteArray :: MutableByteArray -> Int -> IO Word8
+readByteArray (MutableByteArray b#) (I# i#) = IO $ \s0 ->
+  case readWord8Array# b# i# s0 of
+    (# s1, w #) -> (# s1, W8# w #)
+
+-- Create a new mutable byte array of length 1 with the sole byte
+-- set to the 105.
+luckySingleton :: IO MutableByteArray
+luckySingleton = IO $ \s0 -> case newByteArray# 1# s0 of
+  (# s1, marr# #) -> case writeWord8Array# marr# 0# 105## s1 of
+    s2 -> (# s2, MutableByteArray marr# #)
+
+
diff --git a/testsuite/tests/ffi/should_run/UnliftedNewtypesByteArrayOffset.stdout b/testsuite/tests/ffi/should_run/UnliftedNewtypesByteArrayOffset.stdout
new file mode 100644
index 0000000000..b9c7be5412
--- /dev/null
+++ b/testsuite/tests/ffi/should_run/UnliftedNewtypesByteArrayOffset.stdout
@@ -0,0 +1,3 @@
+105
+105
+105
diff --git a/testsuite/tests/ffi/should_run/UnliftedNewtypesByteArrayOffset_c.c b/testsuite/tests/ffi/should_run/UnliftedNewtypesByteArrayOffset_c.c
new file mode 100644
index 0000000000..38f1043105
--- /dev/null
+++ b/testsuite/tests/ffi/should_run/UnliftedNewtypesByteArrayOffset_c.c
@@ -0,0 +1,5 @@
+#include <stdint.h>
+
+uint8_t head_bytearray (uint8_t *arr) {
+  return arr[0];
+}
diff --git a/testsuite/tests/ffi/should_run/all.T b/testsuite/tests/ffi/should_run/all.T
index f692d2d04a..fa78c56b80 100644
--- a/testsuite/tests/ffi/should_run/all.T
+++ b/testsuite/tests/ffi/should_run/all.T
@@ -208,3 +208,5 @@ test('PrimFFIInt16', [omit_ways(['ghci'])], compile_and_run, ['PrimFFIInt16_c.c'
 test('PrimFFIWord16', [omit_ways(['ghci'])], compile_and_run, ['PrimFFIWord16_c.c'])
 
 test('T493', [omit_ways(['ghci'])], compile_and_run, ['T493_c.c'])
+
+test('UnliftedNewtypesByteArrayOffset', [omit_ways(['ghci'])], compile_and_run, ['UnliftedNewtypesByteArrayOffset_c.c'])
diff --git a/testsuite/tests/module/mod130.stderr b/testsuite/tests/module/mod130.stderr
index 26528b148a..9e41bcdc42 100644
--- a/testsuite/tests/module/mod130.stderr
+++ b/testsuite/tests/module/mod130.stderr
@@ -1,5 +1,5 @@
 
 mod130.hs:7:5: error:
-    Variable not in scope: (<) :: Integer -> Int -> Int
+    Variable not in scope: (<) :: t0 -> Int -> Int
     Perhaps you want to remove ‘<’ from the explicit hiding list
     in the import of ‘Prelude’ (mod130.hs:4:1-33).
diff --git a/testsuite/tests/module/mod147.stderr b/testsuite/tests/module/mod147.stderr
index 39bf7d2dc7..0a4e3fd662 100644
--- a/testsuite/tests/module/mod147.stderr
+++ b/testsuite/tests/module/mod147.stderr
@@ -1,3 +1,2 @@
 
-mod147.hs:6:5: error:
-    Data constructor not in scope: D :: Integer -> t
+mod147.hs:6:5: error: Data constructor not in scope: D :: t0 -> t
diff --git a/testsuite/tests/polykinds/T14561.stderr b/testsuite/tests/polykinds/T14561.stderr
index d39dec4d7b..05814f387c 100644
--- a/testsuite/tests/polykinds/T14561.stderr
+++ b/testsuite/tests/polykinds/T14561.stderr
@@ -1,5 +1,5 @@
 
 T14561.hs:12:9: error:
-    Cannot use primitive with levity-polymorphic arguments:
+    Cannot use function with levity-polymorphic arguments:
       unsafeCoerce# :: a -> a
     Levity-polymorphic arguments: a :: TYPE r
diff --git a/testsuite/tests/rename/should_fail/T15607.stderr b/testsuite/tests/rename/should_fail/T15607.stderr
index 9bc84f42f7..4c1111eef9 100644
--- a/testsuite/tests/rename/should_fail/T15607.stderr
+++ b/testsuite/tests/rename/should_fail/T15607.stderr
@@ -1,5 +1,5 @@
 
 T15607.hs:6:10: error:
-    • Variable not in scope: pure :: Integer -> t
+    • Variable not in scope: pure :: t0 -> t
     • Perhaps you want to remove ‘pure’ from the explicit hiding list
       in the import of ‘Prelude’ (T15607.hs:4:1-36).
diff --git a/testsuite/tests/safeHaskell/ghci/p4.stderr b/testsuite/tests/safeHaskell/ghci/p4.stderr
index a0dc5c319e..1d416eba39 100644
--- a/testsuite/tests/safeHaskell/ghci/p4.stderr
+++ b/testsuite/tests/safeHaskell/ghci/p4.stderr
@@ -4,6 +4,6 @@
     No module named ‘System.IO.Unsafe’ is imported.
 
 <interactive>:6:9: error:
-    Variable not in scope: x :: IO Integer -> t
+    Variable not in scope: x :: IO b0 -> t
 
 <interactive>:7:1: error: Variable not in scope: y
diff --git a/testsuite/tests/safeHaskell/ghci/p6.stderr b/testsuite/tests/safeHaskell/ghci/p6.stderr
index 2e68cd9a60..6213243bb0 100644
--- a/testsuite/tests/safeHaskell/ghci/p6.stderr
+++ b/testsuite/tests/safeHaskell/ghci/p6.stderr
@@ -6,5 +6,5 @@
         foreign import ccall safe "sin" c_sin :: Double -> Double
 
 <interactive>:12:1: error:
-    • Variable not in scope: c_sin :: Integer -> t
+    • Variable not in scope: c_sin :: t0 -> t
     • Perhaps you meant ‘c_sin'’ (line 7)
diff --git a/testsuite/tests/typecheck/should_compile/UnlifNewUnify.hs b/testsuite/tests/typecheck/should_compile/UnlifNewUnify.hs
new file mode 100644
index 0000000000..d32eed4ef1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/UnlifNewUnify.hs
@@ -0,0 +1,35 @@
+{-# Language CPP                   #-}
+{-# Language QuantifiedConstraints #-}
+{-# Language TypeApplications      #-}
+{-# Language PolyKinds             #-}
+{-# Language TypeOperators         #-}
+{-# Language DataKinds             #-}
+{-# Language TypeFamilies          #-}
+{-# Language TypeSynonymInstances  #-}
+{-# Language FlexibleInstances     #-}
+{-# Language GADTs                 #-}
+{-# Language UndecidableInstances  #-}
+{-# Language MultiParamTypeClasses #-}
+{-# Language FlexibleContexts      #-}
+{-# LANGUAGE UnliftedNewtypes      #-}
+
+module Bug where
+import Data.Coerce
+import Data.Kind
+
+type Cat ob = ob -> ob -> Type
+
+type Obj = Type
+
+class
+  Ríki (obj :: Obj) where
+  type (-->) :: obj -> obj -> Type
+
+  ið :: a --> (a::obj)
+
+data Op a = Op a
+
+type family UnOp op where UnOp ('Op obj) = obj
+
+newtype Y :: Cat (Op a) where
+  Y :: (UnOp b --> UnOp a) -> Y a b
diff --git a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesDifficultUnification.hs b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesDifficultUnification.hs
new file mode 100644
index 0000000000..de831f9200
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesDifficultUnification.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module UnliftedNewtypesDifficultUnification where
+
+import GHC.Exts
+import Data.Kind
+
+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#
+
+newtype Quux :: TYPE (Interpret Red) where
+  MkQ :: Int# -> Quux
+
+newtype instance Foo 'Blue :: TYPE WordRep where
+  MkFB :: Word# -> Foo 'Blue
+
+type family Lower (x :: Type) :: RuntimeRep where
+  Lower Int = IntRep
+  Lower Word = WordRep
+
+data family Bar (x :: Color) :: TYPE (Interpret x)
+
+newtype instance Bar 'Red :: TYPE (Lower Int) where
+  MkBR :: Int# -> Bar 'Red
diff --git a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesForall.hs b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesForall.hs
new file mode 100644
index 0000000000..68221cb510
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesForall.hs
@@ -0,0 +1,10 @@
+{-# Language RankNTypes #-}
+{-# Language KindSignatures #-}
+{-# Language PolyKinds #-}
+{-# Language UnliftedNewtypes #-}
+
+module UnliftedNewtypesForall where
+
+import GHC.Exts
+
+newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
diff --git a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesGnd.hs b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesGnd.hs
new file mode 100644
index 0000000000..d664801a08
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesGnd.hs
@@ -0,0 +1,20 @@
+{-# language DataKinds #-}
+{-# language DerivingStrategies #-}
+{-# language GeneralizedNewtypeDeriving #-}
+{-# language KindSignatures #-}
+{-# language MagicHash #-}
+{-# language PolyKinds #-}
+{-# language UnliftedNewtypes #-}
+
+module UnliftedNewtypesGnd where
+
+import GHC.Exts (Int#,TYPE,RuntimeRep(IntRep),isTrue#,(==#))
+
+class LevityEq (a :: TYPE 'IntRep) where
+  levityEq :: a -> a -> Bool
+
+instance LevityEq Int# where
+  levityEq x y = isTrue# (x ==# y)
+
+newtype Foo = Foo Int#
+  deriving newtype (LevityEq)
diff --git a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesLPFamily.hs b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesLPFamily.hs
new file mode 100644
index 0000000000..1b8a18fc7c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesLPFamily.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE ExplicitForAll, PolyKinds, TypeFamilies, GADTs, UnliftedNewtypes #-}
+
+module UnliftedNewtypesLPFamily where
+
+import GHC.Exts
+
+data family DF (a :: k) :: k
+
+newtype instance DF (a :: TYPE r) where
+  MkDF :: forall (r :: RuntimeRep) (a :: TYPE r). a -> DF a
diff --git a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnassociatedFamily.hs b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnassociatedFamily.hs
new file mode 100644
index 0000000000..60f97bdd53
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnassociatedFamily.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE UnboxedTuples #-}
+
+module UnliftedNewtypesUnassociatedFamily where
+
+import GHC.Int (Int(I#))
+import GHC.Word (Word(W#))
+import GHC.Exts (Int#,Word#)
+import GHC.Exts (TYPE,RuntimeRep(LiftedRep,IntRep,WordRep,TupleRep))
+
+data family DFT (r :: RuntimeRep) :: TYPE r
+newtype instance DFT 'IntRep = MkDFT1 Int#
+newtype instance DFT 'WordRep = MkDFT2 Word#
+newtype instance DFT ('TupleRep '[ 'IntRep, 'WordRep])
+  = MkDFT3 (# Int#, Word# #)
+data instance DFT 'LiftedRep = MkDFT4 | MkDFT5
+
+data family DF :: TYPE (r :: RuntimeRep)
+newtype instance DF = MkDF1 Int#
+newtype instance DF = MkDF2 Word#
+newtype instance DF = MkDF3 (# Int#, Word# #)
+data instance DF = MkDF4 | MkDF5
diff --git a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnifySig.hs b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnifySig.hs
new file mode 100644
index 0000000000..9f5b984025
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnifySig.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTSyntax #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module UnliftedNewtypesUnassociatedFamily where
+
+import GHC.Int (Int(I#))
+import GHC.Exts (Int#,Word#,RuntimeRep(IntRep))
+import GHC.Exts (TYPE)
+
+type KindOf (a :: TYPE k) = k
+data family D (a :: TYPE r) :: TYPE r
+newtype instance D a = MkWordD Word#
+newtype instance D a :: TYPE (KindOf a) where
+  MkIntD :: forall (a :: TYPE 'IntRep). Int# -> D a
diff --git a/testsuite/tests/typecheck/should_compile/VtaCoerce.hs b/testsuite/tests/typecheck/should_compile/VtaCoerce.hs
new file mode 100644
index 0000000000..ab8d7082f7
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/VtaCoerce.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE RankNTypes, TypeApplications #-}
+
+module VtaCoerce where
+
+import Data.Coerce (coerce)
+
+newtype Age = Age Int
+
+convert :: Int -> Age
+convert = coerce @Int @Age
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 850b271140..d0f54c0eca 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -470,6 +470,7 @@ test('T10562', normal, compile, [''])
 test('T10564', normal, compile, [''])
 test('Vta1', normal, compile, [''])
 test('Vta2', normal, compile, [''])
+test('VtaCoerce', normal, compile, [''])
 test('PushHRIf', normal, compile, [''])
 test('T10632', normal, compile, ['-Wredundant-constraints'])
 test('T10642', normal, compile, [''])
@@ -674,3 +675,10 @@ test('T16411', normal, compile, [''])
 test('T16609', normal, compile, [''])
 test('T505', normal, compile, [''])
 test('T12928', normal, compile, [''])
+test('UnliftedNewtypesGnd', normal, compile, [''])
+test('UnliftedNewtypesUnassociatedFamily', normal, compile, [''])
+test('UnliftedNewtypesUnifySig', normal, compile, [''])
+test('UnliftedNewtypesForall', normal, compile, [''])
+test('UnlifNewUnify', normal, compile, [''])
+test('UnliftedNewtypesLPFamily', normal, compile, [''])
+test('UnliftedNewtypesDifficultUnification', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_compile/tc211.stderr b/testsuite/tests/typecheck/should_compile/tc211.stderr
index 3342cf72e3..ccc3da6fb0 100644
--- a/testsuite/tests/typecheck/should_compile/tc211.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc211.stderr
@@ -1,7 +1,7 @@
 
 tc211.hs:20:8: error:
     • Couldn't match expected type ‘forall a. a -> a’
-                  with actual type ‘a3 -> a3’
+                  with actual type ‘a9 -> a9’
     • In the expression:
           (:) ::
             (forall a. a -> a) -> [forall a. a -> a] -> [forall a. a -> a]
@@ -32,7 +32,7 @@ tc211.hs:25:20: error:
 
 tc211.hs:62:18: error:
     • Couldn't match expected type ‘forall a. a -> a’
-                  with actual type ‘a2 -> a2’
+                  with actual type ‘a6 -> a6’
     • In the expression:
           Cons ::
             (forall a. a -> a)
@@ -70,10 +70,10 @@ tc211.hs:68:8: error:
                 (\ x -> x) Nil
 
 tc211.hs:76:9: error:
-    • Couldn't match type ‘forall a5. a5 -> a5’ with ‘a4 -> a4’
+    • Couldn't match type ‘forall a11. a11 -> a11’ with ‘a10 -> a10’
       Expected type: List (forall a. a -> a)
-                     -> (forall a. a -> a) -> a4 -> a4
-        Actual type: List (a4 -> a4) -> (a4 -> a4) -> a4 -> a4
+                     -> (forall a. a -> a) -> a10 -> a10
+        Actual type: List (a10 -> a10) -> (a10 -> a10) -> a10 -> a10
     • In the expression:
           foo2 ::
             List (forall a. a -> a) -> (forall a. a -> a) -> (forall a. a -> a)
diff --git a/testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr
index 355bfe959c..1c108f719b 100644
--- a/testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr
@@ -68,7 +68,8 @@ valid_hole_fits.hs:24:9: warning: [-Wtyped-holes (in -Wdefault)]
            (and originally defined at ValidHoleFits.hs:4:12-22))
 
 valid_hole_fits.hs:27:5: warning: [-Wtyped-holes (in -Wdefault)]
-    • Found hole: _ :: Integer -> Maybe Integer
+    • Found hole: _ :: t0 -> Maybe Integer
+      Where: ‘t0’ is an ambiguous type variable
     • In the expression: _
       In the expression: _ 2
       In an equation for ‘k’: k = _ 2
diff --git a/testsuite/tests/typecheck/should_fail/T10971d.stderr b/testsuite/tests/typecheck/should_fail/T10971d.stderr
index c5ad886683..5cf339bd8d 100644
--- a/testsuite/tests/typecheck/should_fail/T10971d.stderr
+++ b/testsuite/tests/typecheck/should_fail/T10971d.stderr
@@ -1,14 +1,12 @@
 
 T10971d.hs:4:14: error:
-    • Couldn't match expected type ‘[a0]’
-                  with actual type ‘Maybe Integer’
+    • Couldn't match expected type ‘[a0]’ with actual type ‘Maybe a2’
     • In the first argument of ‘f’, namely ‘(Just 1)’
       In the second argument of ‘($)’, namely ‘f (Just 1)’
       In a stmt of a 'do' block: print $ f (Just 1)
 
 T10971d.hs:5:19: error:
-    • Couldn't match expected type ‘[Integer]’
-                  with actual type ‘Maybe Integer’
+    • Couldn't match expected type ‘[b1]’ with actual type ‘Maybe a3’
     • In the second argument of ‘g’, namely ‘(Just 5)’
       In the second argument of ‘($)’, namely ‘g (+ 1) (Just 5)’
       In a stmt of a 'do' block: print $ g (+ 1) (Just 5)
diff --git a/testsuite/tests/typecheck/should_fail/T12729.stderr b/testsuite/tests/typecheck/should_fail/T12729.stderr
index 39dac1116f..fafa6316c3 100644
--- a/testsuite/tests/typecheck/should_fail/T12729.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12729.stderr
@@ -1,10 +1,12 @@
 
 T12729.hs:8:4: error:
     • A newtype cannot have an unlifted argument type
+      Perhaps you intended to use UnliftedNewtypes
     • In the definition of data constructor ‘MkA’
       In the newtype declaration for ‘A’
 
 T12729.hs:10:13: error:
     • A newtype cannot have an unlifted argument type
+      Perhaps you intended to use UnliftedNewtypes
     • In the definition of data constructor ‘MkB’
       In the newtype declaration for ‘B’
diff --git a/testsuite/tests/typecheck/should_fail/T13902.stderr b/testsuite/tests/typecheck/should_fail/T13902.stderr
index c3d07edfd1..2794ae25ec 100644
--- a/testsuite/tests/typecheck/should_fail/T13902.stderr
+++ b/testsuite/tests/typecheck/should_fail/T13902.stderr
@@ -1,7 +1,6 @@
 
 T13902.hs:8:5: error:
-    • Couldn't match expected type ‘Integer -> Int’
-                  with actual type ‘Int’
+    • Couldn't match expected type ‘t0 -> Int’ with actual type ‘Int’
     • The expression ‘f @Int’ is applied to two arguments,
       but its type ‘Int -> Int’ has only one
       In the expression: f @Int 42 5
diff --git a/testsuite/tests/typecheck/should_fail/T15883.hs b/testsuite/tests/typecheck/should_fail/T15883.hs
new file mode 100644
index 0000000000..29ccbc835a
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15883.hs
@@ -0,0 +1,9 @@
+{-# Language KindSignatures #-}
+{-# Language PolyKinds #-}
+{-# Language RankNTypes #-}
+
+module T15883 where
+
+import GHC.Exts
+
+newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
diff --git a/testsuite/tests/typecheck/should_fail/T15883.stderr b/testsuite/tests/typecheck/should_fail/T15883.stderr
new file mode 100644
index 0000000000..4bfbc615e6
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15883.stderr
@@ -0,0 +1,5 @@
+T15883.hs:9:19:
+     A newtype cannot have an unlifted argument type
+      Perhaps you intended to use UnliftedNewtypes
+      In the definition of data constructor ‘MkFoo’
+      In the newtype declaration for ‘Foo’
diff --git a/testsuite/tests/typecheck/should_fail/T15883b.hs b/testsuite/tests/typecheck/should_fail/T15883b.hs
new file mode 100644
index 0000000000..82613943a7
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15883b.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module T15883b where
+
+import GHC.Exts
+
+newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
+deriving stock instance Eq (Foo LiftedRep)
diff --git a/testsuite/tests/typecheck/should_fail/T15883b.stderr b/testsuite/tests/typecheck/should_fail/T15883b.stderr
new file mode 100644
index 0000000000..a89403d4af
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15883b.stderr
@@ -0,0 +1,5 @@
+T15883b.hs:14:1:
+     Can't make a derived instance of
+        ‘Eq (Foo 'LiftedRep)’ with the stock strategy:
+        Don't know how to derive ‘Eq’ for type ‘forall a. a’
+     In the stand-alone deriving instance for ‘Eq (Foo LiftedRep)’
diff --git a/testsuite/tests/typecheck/should_fail/T15883c.hs b/testsuite/tests/typecheck/should_fail/T15883c.hs
new file mode 100644
index 0000000000..bd031540c2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15883c.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module T15883c where
+
+import GHC.Exts
+
+newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
+deriving stock instance Ord (Foo LiftedRep)
diff --git a/testsuite/tests/typecheck/should_fail/T15883c.stderr b/testsuite/tests/typecheck/should_fail/T15883c.stderr
new file mode 100644
index 0000000000..5444f5d6c8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15883c.stderr
@@ -0,0 +1,5 @@
+T15883c.hs:14:1:                 
+     Can't make a derived instance of
+        ‘Ord (Foo 'LiftedRep)’ with the stock strategy:
+        Don't know how to derive ‘Ord’ for type ‘forall a. a’
+     In the stand-alone deriving instance for ‘Ord (Foo LiftedRep)’
diff --git a/testsuite/tests/typecheck/should_fail/T15883d.hs b/testsuite/tests/typecheck/should_fail/T15883d.hs
new file mode 100644
index 0000000000..fd86c5cab3
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15883d.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module T15883d where
+
+import GHC.Exts
+
+newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
+deriving stock instance Show (Foo LiftedRep)
+
diff --git a/testsuite/tests/typecheck/should_fail/T15883d.stderr b/testsuite/tests/typecheck/should_fail/T15883d.stderr
new file mode 100644
index 0000000000..b080ff6544
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15883d.stderr
@@ -0,0 +1,5 @@
+T15883d.hs:14:1:
+     Can't make a derived instance of
+        ‘Show (Foo 'LiftedRep)’ with the stock strategy:
+        Don't know how to derive ‘Show’ for type ‘forall a. a’
+     In the stand-alone deriving instance for ‘Show (Foo LiftedRep)’
diff --git a/testsuite/tests/typecheck/should_fail/T15883e.hs b/testsuite/tests/typecheck/should_fail/T15883e.hs
new file mode 100644
index 0000000000..bb1dcacf92
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15883e.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module T15883e where
+
+import GHC.Exts
+import Data.Data (Data)
+
+newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
+deriving stock instance Data (Foo LiftedRep)
+
+
diff --git a/testsuite/tests/typecheck/should_fail/T15883e.stderr b/testsuite/tests/typecheck/should_fail/T15883e.stderr
new file mode 100644
index 0000000000..05e07f0307
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15883e.stderr
@@ -0,0 +1,5 @@
+T15883e.hs:16:1:
+     Can't make a derived instance of
+        ‘Data (Foo 'LiftedRep)’ with the stock strategy:
+        Don't know how to derive ‘Data’ for type ‘forall a. a’
+     In the stand-alone deriving instance for ‘Data (Foo LiftedRep)’
diff --git a/testsuite/tests/typecheck/should_fail/T8603.stderr b/testsuite/tests/typecheck/should_fail/T8603.stderr
index d22d13f92b..ec991bc39f 100644
--- a/testsuite/tests/typecheck/should_fail/T8603.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8603.stderr
@@ -1,7 +1,7 @@
 
 T8603.hs:33:17: error:
     • Couldn't match type ‘RV a1’ with ‘StateT s RV a0’
-      Expected type: [Integer] -> StateT s RV a0
+      Expected type: [a2] -> StateT s RV a0
         Actual type: t0 ((->) [a1]) (RV a1)
     • The function ‘lift’ is applied to two arguments,
       but its type ‘([a1] -> RV a1) -> t0 ((->) [a1]) (RV a1)’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesCoerceFail.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesCoerceFail.hs
new file mode 100644
index 0000000000..f5fd1092ca
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesCoerceFail.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module Goof where
+
+import GHC.Exts (coerce)
+import GHC.Types (RuntimeRep,TYPE,Coercible)
+
+goof :: forall (rep :: RuntimeRep) (x :: TYPE rep) (y :: TYPE rep).
+  Coercible x y => x -> y
+goof = coerce
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesCoerceFail.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesCoerceFail.stderr
new file mode 100644
index 0000000000..638dc80ff8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesCoerceFail.stderr
@@ -0,0 +1,5 @@
+UnliftedNewtypesCoerceFail.hs:15:8:
+    Cannot use function with levity-polymorphic arguments:
+      coerce :: x -> y
+    Levity-polymorphic arguments: x :: TYPE rep
+
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesConstraintFamily.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesConstraintFamily.hs
new file mode 100644
index 0000000000..530b1f5241
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesConstraintFamily.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MagicHash #-}
+
+module UnliftedNewtypesConstraintFamily where
+
+import Data.Kind (Type,Constraint)
+
+data family D (a :: Type) :: Constraint
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesConstraintFamily.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesConstraintFamily.stderr
new file mode 100644
index 0000000000..9c6816b3c1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesConstraintFamily.stderr
@@ -0,0 +1,5 @@
+UnliftedNewtypesConstraintFamily.hs:11:1:
+     Kind signature on data type declaration has non-*
+      and non-variable return kind
+        Constraint
+     In the data family declaration for ‘D’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFail.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFail.hs
new file mode 100644
index 0000000000..f37549ed76
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFail.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE UnliftedNewtypes #-}
+
+main :: IO ()
+main = return ()
+
+newtype Baz = Baz (Show Int)
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFail.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFail.stderr
new file mode 100644
index 0000000000..58b7d65d31
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFail.stderr
@@ -0,0 +1,5 @@
+UnliftedNewtypesFail.hs:6:20:
+     Expected a type, but ‘Show Int’ has kind ‘Constraint’
+     In the type ‘(Show Int)’
+      In the definition of data constructor ‘Baz’
+      In the newtype declaration for ‘Baz’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.hs
new file mode 100644
index 0000000000..0306a11c9f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module UnliftedNewtypesFamilyKindFail1 where
+
+import Data.Kind (Type)
+
+data family DF (a :: Type) :: 5
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.stderr
new file mode 100644
index 0000000000..13c9836c43
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.stderr
@@ -0,0 +1,4 @@
+UnliftedNewtypesFamilyKindFail1.hs:11:31:
+     Expected a type, but ‘5’ has kind ‘GHC.Types.Nat’
+     In the kind ‘5’
+      In the data family declaration for ‘DF’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.hs
new file mode 100644
index 0000000000..a2baf8ca5c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MagicHash #-}
+
+module UnliftedNewtypesFamilyKindFail2 where
+
+import Data.Kind (Type)
+
+data family F k :: k
+newtype instance F 5 = MkF (F 5)
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr
new file mode 100644
index 0000000000..57c4a3c2e9
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr
@@ -0,0 +1,11 @@
+UnliftedNewtypesFamilyKindFail2.hs:12:20:
+     Expected a type, but ‘5’ has kind ‘GHC.Types.Nat’
+     In the first argument of ‘F’, namely ‘5’
+      In the newtype instance declaration for ‘F’
+
+UnliftedNewtypesFamilyKindFail2.hs:12:31:
+     Expected a type, but ‘5’ has kind ‘GHC.Types.Nat’
+     In the first argument of ‘F’, namely ‘5’
+      In the type ‘(F 5)’
+      In the definition of data constructor ‘MkF’
+
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInfinite.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInfinite.hs
new file mode 100644
index 0000000000..644943e398
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInfinite.hs
@@ -0,0 +1,9 @@
+{-# language MagicHash #-}
+{-# language UnboxedTuples #-}
+{-# language UnliftedNewtypes #-}
+
+module UnliftedNewtypesInfinite where
+
+import GHC.Exts (Int#)
+
+newtype Foo = FooC (# Int#, Foo #)
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInfinite.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInfinite.stderr
new file mode 100644
index 0000000000..65db9f5a84
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInfinite.stderr
@@ -0,0 +1,6 @@
+
+UnliftedNewtypesInfinite.hs:9:15: error:
+    • Occurs check: cannot construct the infinite kind:
+        t0 ~ 'GHC.Types.TupleRep '[ 'GHC.Types.IntRep, t0]
+    • In the definition of data constructor ‘FooC’
+      In the newtype declaration for ‘Foo’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.hs
new file mode 100644
index 0000000000..8f1f9b4c65
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE GADTSyntax #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE TypeFamilies #-}
+module UnliftedNewtypesInstanceFail where
+
+import GHC.Exts
+
+class Foo a where
+  data Bar a :: TYPE 'IntRep
+
+instance Foo Bool where
+  newtype Bar Bool :: TYPE 'WordRep where
+    BarBoolC :: Word# -> Bar Bool
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.stderr
new file mode 100644
index 0000000000..3fb2814dab
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.stderr
@@ -0,0 +1,5 @@
+UnliftedNewtypesInstanceFail.hs:13:3:
+     Expected kind ‘TYPE 'WordRep’,
+        but ‘Bar Bool’ has kind ‘TYPE 'IntRep’
+     In the newtype instance declaration for ‘Bar’
+      In the instance declaration for ‘Foo Bool’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.hs
new file mode 100644
index 0000000000..f5d134e3b1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeInType #-}
+
+module UnliftedNewtypesLevityBinder where
+
+import GHC.Types (RuntimeRep,TYPE,Coercible)
+
+newtype Ident :: forall (r :: RuntimeRep). TYPE r -> TYPE r where
+  IdentC :: forall (r :: RuntimeRep) (a :: TYPE r). a -> Ident a
+
+bad :: forall (r :: RuntimeRep) (a :: TYPE r). a -> Ident a
+bad = IdentC
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr
new file mode 100644
index 0000000000..90cf5b23aa
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr
@@ -0,0 +1,4 @@
+UnliftedNewtypesLevityBinder.hs:16:7:
+    Cannot use function with levity-polymorphic arguments:
+      UnliftedNewtypesLevityBinder.IdentC :: a -> Ident a
+    Levity-polymorphic arguments: a :: TYPE r
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKind.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKind.hs
new file mode 100644
index 0000000000..6c085267db
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKind.hs
@@ -0,0 +1,12 @@
+{-# language MagicHash #-}
+{-# language GADTSyntax #-}
+{-# language KindSignatures #-}
+{-# language UnliftedNewtypes #-}
+
+module UnliftedNewtypesMismatchedKind where
+
+import Data.Kind (Type)
+import GHC.Exts
+
+newtype T :: Type where
+  MkT :: Int# -> T
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKind.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKind.stderr
new file mode 100644
index 0000000000..1d3cb50f90
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKind.stderr
@@ -0,0 +1,4 @@
+UnliftedNewtypesMismatchedKind.hs:12:3:
+     Expecting a lifted type, but ‘Int#’ is unlifted
+     In the definition of data constructor ‘MkT’
+      In the newtype declaration for ‘T’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKindRecord.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKindRecord.hs
new file mode 100644
index 0000000000..255643a69d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKindRecord.hs
@@ -0,0 +1,11 @@
+{-# language GADTSyntax #-}
+{-# language KindSignatures #-}
+{-# language MagicHash #-}
+{-# language UnliftedNewtypes #-}
+
+module UnliftedNewtypesMismatchedKindRecord where
+
+import GHC.Exts
+
+newtype Foo :: TYPE 'IntRep where
+  FooC :: { getFoo :: Word# } -> Foo
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKindRecord.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKindRecord.stderr
new file mode 100644
index 0000000000..2530a438ab
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKindRecord.stderr
@@ -0,0 +1,5 @@
+UnliftedNewtypesMismatchedKindRecord.hs:11:3:
+     Expected kind ‘TYPE 'IntRep’,
+        but ‘Word#’ has kind ‘TYPE 'WordRep’
+     In the definition of data constructor ‘FooC’
+      In the newtype declaration for ‘Foo’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMultiFieldGadt.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMultiFieldGadt.hs
new file mode 100644
index 0000000000..81a2041d2b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMultiFieldGadt.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+-- In tcConDecl, there is a place where a panic can happen if
+-- a newtype has multiple fields. This test is here to make
+-- sure that the appropriate validity checks happen before
+-- we get to the panic. See Note [Kind-checking the field type].
+
+module UnliftedNewtypesMultiFieldGadt where
+
+import GHC.Exts
+import Data.Kind
+
+newtype Foo :: TYPE 'IntRep where
+  FooC :: Bool -> Char -> Foo
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMultiFieldGadt.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMultiFieldGadt.stderr
new file mode 100644
index 0000000000..70493e0d96
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMultiFieldGadt.stderr
@@ -0,0 +1,5 @@
+UnliftedNewtypesMultiFieldGadt.hs:19:3:
+     The constructor of a newtype must have exactly one field
+        but ‘FooC’ has two
+     In the definition of data constructor ‘FooC’
+      In the newtype declaration for ‘Foo’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesNotEnabled.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesNotEnabled.hs
new file mode 100644
index 0000000000..6c6aadccc8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesNotEnabled.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE MagicHash #-}
+
+module UnliftedNewtypesNotEnabled
+  ( Baz(..)
+  ) where
+
+import GHC.Exts (Int#)
+
+newtype Baz = Baz Int#
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesNotEnabled.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesNotEnabled.stderr
new file mode 100644
index 0000000000..37496c4edd
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesNotEnabled.stderr
@@ -0,0 +1,5 @@
+UnliftedNewtypesNotEnabled.hs:9:15:
+     A newtype cannot have an unlifted argument type
+      Perhaps you intended to use UnliftedNewtypes
+     In the definition of data constructor ‘Baz’
+      In the newtype declaration for ‘Baz’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.hs
new file mode 100644
index 0000000000..6c1959e035
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MagicHash #-}
+
+module UnliftedNewtypesOverlap where
+
+import GHC.Exts (TYPE)
+
+data family DF :: TYPE r
+data instance DF = MkDF4 | MkDF5
+newtype instance DF = MkDF6 Int
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.stderr
new file mode 100644
index 0000000000..808e8c0f60
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.stderr
@@ -0,0 +1,4 @@
+UnliftedNewtypesOverlap.hs:12:15:
+    Conflicting family instance declarations:
+      DF -- Defined at UnliftedNewtypesOverlap.hs:12:15
+      DF -- Defined at UnliftedNewtypesOverlap.hs:13:18
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 5be507edbf..7ee15ebc4c 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -518,3 +518,21 @@ test('T16456', normal, compile_fail, ['-fprint-explicit-foralls'])
 test('T16627', normal, compile_fail, [''])
 test('T502', normal, compile_fail, [''])
 test('T16517', normal, compile_fail, [''])
+test('T15883', normal, compile_fail, [''])
+test('T15883b', normal, compile_fail, [''])
+test('T15883c', normal, compile_fail, [''])
+test('T15883d', normal, compile_fail, [''])
+test('T15883e', normal, compile_fail, [''])
+test('UnliftedNewtypesFail', normal, compile_fail, [''])
+test('UnliftedNewtypesNotEnabled', normal, compile_fail, [''])
+test('UnliftedNewtypesCoerceFail', normal, compile_fail, [''])
+test('UnliftedNewtypesInstanceFail', normal, compile_fail, [''])
+test('UnliftedNewtypesInfinite', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
+test('UnliftedNewtypesLevityBinder', normal, compile_fail, [''])
+test('UnliftedNewtypesOverlap', normal, compile_fail, [''])
+test('UnliftedNewtypesFamilyKindFail1', normal, compile_fail, [''])
+test('UnliftedNewtypesFamilyKindFail2', normal, compile_fail, [''])
+test('UnliftedNewtypesConstraintFamily', normal, compile_fail, [''])
+test('UnliftedNewtypesMismatchedKind', normal, compile_fail, [''])
+test('UnliftedNewtypesMismatchedKindRecord', normal, compile_fail, [''])
+test('UnliftedNewtypesMultiFieldGadt', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/mc24.stderr b/testsuite/tests/typecheck/should_fail/mc24.stderr
index 7f016283b1..06a9c51690 100644
--- a/testsuite/tests/typecheck/should_fail/mc24.stderr
+++ b/testsuite/tests/typecheck/should_fail/mc24.stderr
@@ -1,8 +1,8 @@
 
 mc24.hs:10:31: error:
-    • Couldn't match type ‘[a0]’ with ‘[a] -> m [a]’
-      Expected type: (a -> Integer) -> [a] -> m [a]
-        Actual type: [a0] -> [a0]
+    • Couldn't match type ‘[a1]’ with ‘[a] -> m [a]’
+      Expected type: (a -> a0) -> [a] -> m [a]
+        Actual type: [a1] -> [a1]
     • Possible cause: ‘take’ is applied to too many arguments
       In the expression: take 2
       In a stmt of a monad comprehension: then group by x using take 2
diff --git a/testsuite/tests/typecheck/should_fail/tcfail004.stderr b/testsuite/tests/typecheck/should_fail/tcfail004.stderr
index 7bf64d841a..9d6657e651 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail004.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail004.stderr
@@ -1,7 +1,7 @@
 
 tcfail004.hs:3:9: error:
     • Couldn't match expected type ‘(a, b)’
-                  with actual type ‘(Integer, Integer, Integer)’
+                  with actual type ‘(a0, b0, c0)’
     • In the expression: (1, 2, 3)
       In a pattern binding: (f, g) = (1, 2, 3)
     • Relevant bindings include
diff --git a/testsuite/tests/typecheck/should_fail/tcfail005.stderr b/testsuite/tests/typecheck/should_fail/tcfail005.stderr
index 56db4cf58b..d206505cdc 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail005.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail005.stderr
@@ -1,7 +1,6 @@
 
 tcfail005.hs:3:9: error:
-    • Couldn't match expected type ‘[a]’
-                  with actual type ‘(Integer, Char)’
+    • Couldn't match expected type ‘[a]’ with actual type ‘(a0, Char)’
     • In the expression: (1, 'a')
       In a pattern binding: (h : i) = (1, 'a')
     • Relevant bindings include
diff --git a/testsuite/tests/typecheck/should_fail/tcfail079.stderr b/testsuite/tests/typecheck/should_fail/tcfail079.stderr
index 78d14f9c35..769b8335ed 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail079.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail079.stderr
@@ -1,5 +1,5 @@
-
 tcfail079.hs:9:19: error:
     • A newtype cannot have an unlifted argument type
+      Perhaps you intended to use UnliftedNewtypes
     • In the definition of data constructor ‘Unboxed’
       In the newtype declaration for ‘Unboxed’
diff --git a/testsuite/tests/typecheck/should_fail/tcfail140.stderr b/testsuite/tests/typecheck/should_fail/tcfail140.stderr
index 85217315ca..924e14081b 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail140.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail140.stderr
@@ -1,7 +1,6 @@
 
 tcfail140.hs:10:7: error:
-    • Couldn't match expected type ‘Integer -> t’
-                  with actual type ‘Int’
+    • Couldn't match expected type ‘t0 -> t’ with actual type ‘Int’
     • The function ‘f’ is applied to two arguments,
       but its type ‘Int -> Int’ has only one
       In the expression: f 3 9
@@ -9,8 +8,7 @@ tcfail140.hs:10:7: error:
     • Relevant bindings include bar :: t (bound at tcfail140.hs:10:1)
 
 tcfail140.hs:12:10: error:
-    • Couldn't match expected type ‘Integer -> t’
-                  with actual type ‘Int’
+    • Couldn't match expected type ‘t1 -> t’ with actual type ‘Int’
     • The operator ‘f’ takes two arguments,
       but its type ‘Int -> Int’ has only one
       In the expression: 3 `f` 4
diff --git a/testsuite/tests/typecheck/should_fail/tcfail159.stderr b/testsuite/tests/typecheck/should_fail/tcfail159.stderr
index 412ba47d3f..706b3afa32 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail159.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail159.stderr
@@ -1,6 +1,6 @@
 
 tcfail159.hs:9:11: error:
-    • Expecting a lifted type, but got an unlifted
+    • Expecting a lifted type, but got an unlifted type
     • In the pattern: ~(# p, q #)
       In a case alternative: ~(# p, q #) -> p
       In the expression: case h x of { ~(# p, q #) -> p }
diff --git a/testsuite/tests/typecheck/should_fail/tcfail189.stderr b/testsuite/tests/typecheck/should_fail/tcfail189.stderr
index f23243bdd0..f33d1e37f6 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail189.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail189.stderr
@@ -1,8 +1,8 @@
 
 tcfail189.hs:10:31: error:
-    • Couldn't match type ‘[a0]’ with ‘[a] -> [[a]]’
-      Expected type: (a -> Integer) -> [a] -> [[a]]
-        Actual type: [a0] -> [a0]
+    • Couldn't match type ‘[a1]’ with ‘[a] -> [[a]]’
+      Expected type: (a -> a0) -> [a] -> [[a]]
+        Actual type: [a1] -> [a1]
     • Possible cause: ‘take’ is applied to too many arguments
       In the expression: take 2
       In a stmt of a list comprehension: then group by x using take 2
diff --git a/testsuite/tests/typecheck/should_fail/tcfail206.stderr b/testsuite/tests/typecheck/should_fail/tcfail206.stderr
index 51fbbb3825..7c97fc02af 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail206.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail206.stderr
@@ -7,9 +7,9 @@ tcfail206.hs:5:5: error:
       In an equation for ‘a’: a = (, True)
 
 tcfail206.hs:8:5: error:
-    • Couldn't match type ‘(Integer, Int)’ with ‘Bool -> (Int, Bool)’
+    • Couldn't match type ‘(t1, Int)’ with ‘Bool -> (Int, Bool)’
       Expected type: Int -> Bool -> (Int, Bool)
-        Actual type: Int -> (Integer, Int)
+        Actual type: Int -> (t1, Int)
     • In the expression: (1,)
       In an equation for ‘b’: b = (1,)
 
@@ -34,10 +34,10 @@ tcfail206.hs:14:5: error:
       In an equation for ‘d’: d = (# , True #)
 
 tcfail206.hs:17:5: error:
-    • Couldn't match type ‘(# Integer, Int #)’
+    • Couldn't match type ‘(# t0, Int #)’
                      with ‘Bool -> (# Int, Bool #)’
       Expected type: Int -> Bool -> (# Int, Bool #)
-        Actual type: Int -> (# Integer, Int #)
+        Actual type: Int -> (# t0, Int #)
     • In the expression: (# 1, #)
       In an equation for ‘e’: e = (# 1, #)
 
diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesCoerceRun.hs b/testsuite/tests/typecheck/should_run/UnliftedNewtypesCoerceRun.hs
new file mode 100644
index 0000000000..53905a302a
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesCoerceRun.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE GADTSyntax #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE UnboxedSums #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeFamilies #-}
+
+import GHC.Int (Int(I#))
+import GHC.Word (Word(W#))
+import GHC.Exts (Int#,Word#,(+#))
+import GHC.Types
+import Data.Coerce (coerce)
+
+main :: IO ()
+main = do
+  print (I# (coerce (Foo 5#)))
+
+newtype Foo = Foo Int#
diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesCoerceRun.stdout b/testsuite/tests/typecheck/should_run/UnliftedNewtypesCoerceRun.stdout
new file mode 100644
index 0000000000..7ed6ff82de
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesCoerceRun.stdout
@@ -0,0 +1 @@
+5
diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesDependentFamilyRun.hs b/testsuite/tests/typecheck/should_run/UnliftedNewtypesDependentFamilyRun.hs
new file mode 100644
index 0000000000..a6331b8329
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesDependentFamilyRun.hs
@@ -0,0 +1,32 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTSyntax #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+import GHC.Int (Int(I#))
+import GHC.Word (Word(W#))
+import GHC.Exts (Int#,Word#)
+import Data.Proxy (Proxy(..))
+import GHC.Exts (TYPE,RuntimeRep(..))
+
+main :: IO ()
+main = case method (Proxy :: Proxy 'IntRep) of
+  BarIntC y -> case method (Proxy :: Proxy 'WordRep) of
+    BarWordC z -> do
+      print (I# y)
+      print (W# z)
+
+class Foo (a :: RuntimeRep) where
+  data Bar a :: TYPE a
+  method :: Proxy a -> Bar a
+
+instance Foo 'IntRep where
+  newtype instance Bar 'IntRep = BarIntC Int#
+  method _ = BarIntC 5#
+
+instance Foo 'WordRep where
+  newtype instance Bar 'WordRep :: TYPE 'WordRep where
+    BarWordC :: Word# -> Bar 'WordRep
+  method _ = BarWordC 7##
diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesDependentFamilyRun.stdout b/testsuite/tests/typecheck/should_run/UnliftedNewtypesDependentFamilyRun.stdout
new file mode 100644
index 0000000000..b3172d1242
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesDependentFamilyRun.stdout
@@ -0,0 +1,2 @@
+5
+7
diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesFamilyRun.hs b/testsuite/tests/typecheck/should_run/UnliftedNewtypesFamilyRun.hs
new file mode 100644
index 0000000000..b0fdc88dbb
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesFamilyRun.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE GADTSyntax #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+
+import GHC.Int (Int(I#))
+import GHC.Word (Word(W#))
+import GHC.Exts (Int#,Word#)
+import GHC.Types
+
+main :: IO ()
+main = do
+  print (method 5 (BarIntC 6#))
+  print (method 13 (BarWordC 9#))
+
+class Foo a where
+  data Bar a :: TYPE 'IntRep
+  method :: a -> Bar a -> a
+
+instance Foo Int where
+  newtype Bar Int = BarIntC Int#
+  method x (BarIntC y) = x + I# y
+
+instance Foo Word where
+  newtype Bar Word = BarWordC Int#
+  method x (BarWordC y) = x - fromIntegral (I# y)
diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesFamilyRun.stdout b/testsuite/tests/typecheck/should_run/UnliftedNewtypesFamilyRun.stdout
new file mode 100644
index 0000000000..dfa5ffdccf
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesFamilyRun.stdout
@@ -0,0 +1,2 @@
+11
+4
diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesIdentityRun.hs b/testsuite/tests/typecheck/should_run/UnliftedNewtypesIdentityRun.hs
new file mode 100644
index 0000000000..f81367268b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesIdentityRun.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE GADTSyntax #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE UnboxedSums #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeFamilies #-}
+
+import GHC.Int (Int(I#))
+import GHC.Word (Word(W#))
+import GHC.Exts (Int#,Word#,(+#))
+import GHC.Types
+
+main :: IO ()
+main = case (IdentityC 5#) of
+  IdentityC x -> case ex of
+    IdentityC y -> do
+      print (I# x)
+      print y
+      print (maybeInt# 12 increment# (Maybe# (# 42# | #)))
+      print (maybeInt# 27 increment# (Maybe# (# | (# #) #)))
+
+newtype Identity :: forall (r :: RuntimeRep). TYPE r -> TYPE r where
+  IdentityC :: forall (r :: RuntimeRep) (a :: TYPE r). a -> Identity a
+
+newtype Maybe# :: forall (r :: RuntimeRep).
+    TYPE r -> TYPE (SumRep '[r, TupleRep '[]]) where
+  Maybe# :: forall (r :: RuntimeRep) (a :: TYPE r). (# a | (# #) #) -> Maybe# a
+
+maybeInt# :: a -> (Int# -> a) -> Maybe# Int# -> a
+maybeInt# def _ (Maybe# (# | (# #) #)) = def
+maybeInt# _   f (Maybe# (# i | #)) = f i
+
+increment# :: Int# -> Int
+increment# i = I# (i +# 1#)
+
+ex :: Identity Bool
+ex = IdentityC True
diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesIdentityRun.stdout b/testsuite/tests/typecheck/should_run/UnliftedNewtypesIdentityRun.stdout
new file mode 100644
index 0000000000..e5835b0b94
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesIdentityRun.stdout
@@ -0,0 +1,4 @@
+5
+True
+43
+27
diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesRun.hs b/testsuite/tests/typecheck/should_run/UnliftedNewtypesRun.hs
new file mode 100644
index 0000000000..b6c07396bf
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesRun.hs
@@ -0,0 +1,46 @@
+{-# LANGUAGE GADTSyntax #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE RankNTypes #-}
+
+import GHC.Int (Int(I#))
+import GHC.Word (Word(W#))
+import GHC.Exts (Int#,Word#)
+import GHC.Types
+
+main :: IO ()
+main = do
+  let a = idIntRep (FooC 6#)
+      b = idWordRep (BarC 7##)
+      c = idWordRep (PatC 3##)
+      d = idIntRep (DarthC 5#)
+  print (I# (getFoo a))
+  print (W# (case b of BarC w -> w))
+  print (W# (case c of PatC w -> w))
+  print (I# (case d of DarthC w -> w))
+  print (A1 13#)
+  print (A2 15##)
+
+newtype Darth = DarthC Int#
+
+newtype Foo = FooC { getFoo :: Int# }
+
+newtype Bar :: TYPE 'WordRep where
+  BarC :: Word# -> Bar
+
+newtype Pat where
+  PatC :: Word# -> Pat
+
+data A1 :: Type where
+  A1 :: Int# -> A1
+  deriving (Show)
+
+data A2 = A2 Word#
+  deriving (Show)
+
+idIntRep :: forall (a :: TYPE 'IntRep). a -> a
+idIntRep x = x
+
+idWordRep :: forall (a :: TYPE 'WordRep). a -> a
+idWordRep x = x
diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesRun.stdout b/testsuite/tests/typecheck/should_run/UnliftedNewtypesRun.stdout
new file mode 100644
index 0000000000..df8e8ed83d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesRun.stdout
@@ -0,0 +1,6 @@
+6
+7
+3
+5
+A1 13#
+A2 15##
diff --git a/testsuite/tests/typecheck/should_run/all.T b/testsuite/tests/typecheck/should_run/all.T
index 598d467b7e..05fddcb0b0 100755
--- a/testsuite/tests/typecheck/should_run/all.T
+++ b/testsuite/tests/typecheck/should_run/all.T
@@ -135,3 +135,8 @@ test('T14218', normal, compile_and_run, [''])
 test('T14236', normal, compile_and_run, [''])
 test('T14925', normal, compile_and_run, [''])
 test('T14341', normal, compile_and_run, [''])
+test('UnliftedNewtypesRun', normal, compile_and_run, [''])
+test('UnliftedNewtypesFamilyRun', normal, compile_and_run, [''])
+test('UnliftedNewtypesDependentFamilyRun', normal, compile_and_run, [''])
+test('UnliftedNewtypesIdentityRun', normal, compile_and_run, [''])
+test('UnliftedNewtypesCoerceRun', normal, compile_and_run, [''])
author	Andrew Martin <andrew.thaddeus@gmail.com>	2019-05-12 09:23:25 -0400
committer	Marge Bot <ben+marge-bot@smart-cactus.org>	2019-06-14 10:48:13 -0400
commit	effdd948056923f3bc03688c24d7e0339d6272f5 (patch)
tree	02a3cb68ce1680db89c8440ba8beea808cbf4a11
parent	3bc6df3223f62a8366e2e4267bac23aa08e6a939 (diff)
download	haskell-effdd948056923f3bc03688c24d7e0339d6272f5.tar.gz