Add the Unsatisfiable class

This commit implements GHC proposal #433, adding the Unsatisfiable
class to the GHC.TypeError module. This provides an alternative to
TypeError for which error reporting is more predictable: we report it
when we are reporting unsolved Wanted constraints.

Fixes #14983 #16249 #16906 #18310 #20835

19 files changed, 496 insertions, 77 deletions

diff --git a/compiler/GHC/Builtin/Names.hs b/compiler/GHC/Builtin/Names.hs
index 8671b5521f..d72e911541 100644
--- a/compiler/GHC/Builtin/Names.hs
+++ b/compiler/GHC/Builtin/Names.hs
@@ -503,6 +503,10 @@ basicKnownKeyNames
         , typeErrorVAppendDataConName
         , typeErrorShowTypeDataConName
 
+        -- "Unsatisfiable" constraint
+        , unsatisfiableClassName
+        , unsatisfiableIdName
+
         -- Unsafe coercion proofs
         , unsafeEqualityProofName
         , unsafeEqualityTyConName
@@ -1452,6 +1456,13 @@ typeErrorVAppendDataConName =
 typeErrorShowTypeDataConName =
   dcQual gHC_TYPEERROR (fsLit "ShowType") typeErrorShowTypeDataConKey
 
+-- "Unsatisfiable" constraint
+unsatisfiableClassName, unsatisfiableIdName :: Name
+unsatisfiableClassName =
+  clsQual gHC_TYPEERROR (fsLit "Unsatisfiable") unsatisfiableClassNameKey
+unsatisfiableIdName =
+  varQual gHC_TYPEERROR (fsLit "unsatisfiable") unsatisfiableIdNameKey
+
 -- Unsafe coercion proofs
 unsafeEqualityProofName, unsafeEqualityTyConName, unsafeCoercePrimName,
   unsafeReflDataConName :: Name
@@ -1993,9 +2004,13 @@ uFloatTyConKey  = mkPreludeTyConUnique 161
 uIntTyConKey    = mkPreludeTyConUnique 162
 uWordTyConKey   = mkPreludeTyConUnique 163
 
+-- "Unsatisfiable" constraint
+unsatisfiableClassNameKey :: Unique
+unsatisfiableClassNameKey = mkPreludeTyConUnique 170
+
 -- Custom user type-errors
 errorMessageTypeErrorFamKey :: Unique
-errorMessageTypeErrorFamKey =  mkPreludeTyConUnique 181
+errorMessageTypeErrorFamKey = mkPreludeTyConUnique 181
 
 coercibleTyConKey :: Unique
 coercibleTyConKey = mkPreludeTyConUnique 183
@@ -2548,6 +2563,10 @@ getFieldClassOpKey, setFieldClassOpKey :: Unique
 getFieldClassOpKey = mkPreludeMiscIdUnique 572
 setFieldClassOpKey = mkPreludeMiscIdUnique 573
 
+-- "Unsatisfiable" constraints
+unsatisfiableIdNameKey :: Unique
+unsatisfiableIdNameKey = mkPreludeMiscIdUnique 580
+
 ------------------------------------------------------
 -- ghc-bignum uses 600-699 uniques
 ------------------------------------------------------
diff --git a/compiler/GHC/Builtin/Types.hs b/compiler/GHC/Builtin/Types.hs
index 59970daa3c..7dceb6524e 100644
--- a/compiler/GHC/Builtin/Types.hs
+++ b/compiler/GHC/Builtin/Types.hs
@@ -1999,7 +1999,7 @@ data BoxingInfo b
     --        recall: data Int = I# Int#
     --
     --      BI_Box { bi_data_con = MkInt8Box, bi_inst_con = MkInt8Box @ty
-    --             , bi_boxed_type = Int8Box ty }A
+    --             , bi_boxed_type = Int8Box ty }
     --        recall: data Int8Box (a :: TYPE Int8Rep) = MkIntBox a
 
 boxingDataCon :: Type -> BoxingInfo b
diff --git a/compiler/GHC/Builtin/Types/Prim.hs b/compiler/GHC/Builtin/Types/Prim.hs
index 0335e1cb11..74710077b2 100644
--- a/compiler/GHC/Builtin/Types/Prim.hs
+++ b/compiler/GHC/Builtin/Types/Prim.hs
@@ -759,7 +759,7 @@ Wrinkles
 
 (W2) We need two absent-error Ids, aBSENT_ERROR_ID for types of kind Type, and
      aBSENT_CONSTRAINT_ERROR_ID for vaues of kind Constraint.  Ditto noInlineId
-     vs noInlieConstraintId in GHC.Types.Id.Make; see Note [inlineId magic].
+     vs noInlineConstraintId in GHC.Types.Id.Make; see Note [inlineId magic].
 
 (W3) We need a TypeOrConstraint flag in LitRubbish.
 
@@ -802,7 +802,7 @@ irretrievably overlap with:
 
 Wrinkles
 
-(W1) In GHC.Core.RoughMap.roughMtchTyConName we are careful to map
+(W1) In GHC.Core.RoughMap.roughMatchTyConName we are careful to map
      TYPE and CONSTRAINT to the same rough-map key.  Reason:
      If we insert (F @Constraint tys) into a FamInstEnv, and look
      up (F @Type tys'), we /must/ ensure that the (C @Constraint tys)
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 40fa1ea2df..86f483abca 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -76,6 +76,7 @@ module GHC.Core.Type (
 
         mkCastTy, mkCoercionTy, splitCastTy_maybe,
 
+        ErrorMsgType,
         userTypeError_maybe, pprUserTypeErrorTy,
 
         coAxNthLHS,
@@ -1229,9 +1230,12 @@ isLitTy ty
   | LitTy l <- coreFullView ty = Just l
   | otherwise                  = Nothing
 
+-- | A type of kind 'ErrorMessage' (from the 'GHC.TypeError' module).
+type ErrorMsgType = Type
+
 -- | Is this type a custom user error?
--- If so, give us the kind and the error message.
-userTypeError_maybe :: Type -> Maybe Type
+-- If so, give us the error message.
+userTypeError_maybe :: Type -> Maybe ErrorMsgType
 userTypeError_maybe t
   = do { (tc, _kind : msg : _) <- splitTyConApp_maybe t
           -- There may be more than 2 arguments, if the type error is
@@ -1241,7 +1245,7 @@ userTypeError_maybe t
        ; return msg }
 
 -- | Render a type corresponding to a user type error into a SDoc.
-pprUserTypeErrorTy :: Type -> SDoc
+pprUserTypeErrorTy :: ErrorMsgType -> SDoc
 pprUserTypeErrorTy ty =
   case splitTyConApp_maybe ty of
 
@@ -1267,7 +1271,6 @@ pprUserTypeErrorTy ty =
     -- An unevaluated type function
     _ -> ppr ty
 
-
 {- *********************************************************************
 *                                                                      *
                       FunTy
diff --git a/compiler/GHC/Data/Bag.hs b/compiler/GHC/Data/Bag.hs
index a9b8a669de..14caf3d5b1 100644
--- a/compiler/GHC/Data/Bag.hs
+++ b/compiler/GHC/Data/Bag.hs
@@ -18,7 +18,7 @@ module GHC.Data.Bag (
         concatBag, catBagMaybes, foldBag,
         isEmptyBag, isSingletonBag, consBag, snocBag, anyBag, allBag,
         listToBag, nonEmptyToBag, bagToList, headMaybe, mapAccumBagL,
-        concatMapBag, concatMapBagPair, mapMaybeBag, unzipBag,
+        concatMapBag, concatMapBagPair, mapMaybeBag, mapMaybeBagM, unzipBag,
         mapBagM, mapBagM_, lookupBag,
         flatMapBagM, flatMapBagPairM,
         mapAndUnzipBagM, mapAccumBagLM,
@@ -232,6 +232,17 @@ mapMaybeBag f (UnitBag x)     = case f x of
 mapMaybeBag f (TwoBags b1 b2) = unionBags (mapMaybeBag f b1) (mapMaybeBag f b2)
 mapMaybeBag f (ListBag xs)    = listToBag $ mapMaybe f (toList xs)
 
+mapMaybeBagM :: Monad m => (a -> m (Maybe b)) -> Bag a -> m (Bag b)
+mapMaybeBagM _ EmptyBag        = return EmptyBag
+mapMaybeBagM f (UnitBag x)     = do r <- f x
+                                    return $ case r of
+                                      Nothing -> EmptyBag
+                                      Just y  -> UnitBag y
+mapMaybeBagM f (TwoBags b1 b2) = do r1 <- mapMaybeBagM f b1
+                                    r2 <- mapMaybeBagM f b2
+                                    return $ unionBags r1 r2
+mapMaybeBagM f (ListBag xs)    = listToBag <$> mapMaybeM f (toList xs)
+
 mapBagM :: Monad m => (a -> m b) -> Bag a -> m (Bag b)
 mapBagM _ EmptyBag        = return EmptyBag
 mapBagM f (UnitBag x)     = do r <- f x
diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index cb23c835dc..ed102d9bb5 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -588,6 +588,7 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics
     -- we might suppress its error message, and proceed on past
     -- type checking to get a Lint error later
     report1 = [ ("custom_error", is_user_type_error, True,  mkUserTypeErrorReporter)
+                 -- (Handles TypeError and Unsatisfiable)
 
               , given_eq_spec
               , ("insoluble2",      utterly_wrong,  True, mkGroupReporter mkEqErr)
@@ -643,7 +644,12 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics
     non_tv_eq _ (EqPred NomEq ty1 _) = not (isTyVarTy ty1)
     non_tv_eq _ _                    = False
 
-    is_user_type_error item _ = isUserTypeError (errorItemPred item)
+    -- Catch TypeError and Unsatisfiable.
+    -- Here, we want any nested TypeErrors to bubble up, so we use
+    -- 'containsUserTypeError' and not 'isTopLevelUserTypeError'.
+    --
+    -- See also Note [Implementation of Unsatisfiable constraints], point (F).
+    is_user_type_error item _ = containsUserTypeError (errorItemPred item)
 
     is_homo_equality _ (EqPred _ ty1 ty2)
       = typeKind ty1 `tcEqType` typeKind ty2
@@ -786,8 +792,129 @@ Currently, the constraints to ignore are:
 
    If there is any trouble, checkValidFamInst bleats, aborting compilation.
 
--}
+Note [Implementation of Unsatisfiable constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The Unsatisfiable constraint was introduced in GHC proposal #433 (https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0433-unsatisfiable.rst).
+See Note [The Unsatisfiable constraint] in GHC.TypeError.
+
+Its implementation consists of the following:
+
+  A. The definitions.
+
+     The Unsatisfiable class is defined in GHC.TypeError, in base.
+     It consists of the following definitions:
+
+       type Unsatisfiable :: ErrorMessage -> Constraint
+       class Unsatisfiable msg where
+         unsatisfiableLifted :: a
+
+       unsatisfiable :: forall {rep} (msg :: ErrorMessage) (a :: TYPE rep). Unsatisfiable msg => a
+       unsatisfiable = unsatisfiableLifted @msg @((##) -> a) (##)
+
+     The class TyCon as well as the unsatisfiable Id have known-key Names
+     in GHC; they are not wired-in.
+
+  B. Unsatisfiable instances.
+
+     The Unsatisfiable typeclass has no instances (see GHC.Tc.Instance.Class.matchGlobalInst).
+
+     Users are prevented from writing instances in GHC.Tc.Validity.check_special_inst_head.
+     This is done using the same mechanism as for, say, Coercible or WithDict.
+
+  C. Using [G] Unsatisfiable msg to solve any Wanted.
+
+     In GHC.Tc.Solver.simplifyTopWanteds, after defaulting happens, when an
+     implication contains Givens of the form [G] Unsatisfiable msg, and the
+     implication supports term-level evidence (as per Note [Coercion evidence only]
+     in GHC.Tc.Types.Evidence), we use any such Given to solve all the Wanteds
+     in that implication. See GHC.Tc.Solver.useUnsatisfiableGivens.
+
+     The way we construct the evidence terms is slightly complicated by
+     Type vs Constraint considerations; see Note [Evidence terms from Unsatisfiable Givens]
+     in GHC.Tc.Solver.
+
+     The proposal explains why this happens after defaulting: if there are other
+     ways to solve the Wanteds, we would prefer to use that, as that will make
+     user programs "as defined as possible".
+
+     Wrinkle [Ambiguity]
+
+       We also use an Unsatisfiable Given to solve Wanteds when performing an
+       ambiguity check. See the call to "useUnsatisfiableGivens" in
+       GHC.Tc.Solver.simplifyAmbiguityCheck.
+
+       This is, for example, required to typecheck the definition
+       of "unsatisfiable" itself:
+
+         unsatisfiable :: forall {rep} (msg :: ErrorMessage) (a :: TYPE rep). Unsatisfiable msg => a
+
+       The ambiguity check on this type signature will produce
+
+         [G] Unsatisfiable msg1, [W] Unsatisfiable msg2
+
+       and we want to ensure the Given solves the Wanted, to accept the definition.
+
+       NB:
+
+         An alternative would be to add a functional dependency on Unsatisfiable:
 
+           class Unsatisfiable msg | -> msg
+
+         Then we would unify msg1 and msg2 in the above constraint solving problem,
+         and would be able to solve the Wanted using the Given in the normal way.
+         However, adding such a functional dependency solely for this purpose
+         could have undesirable consequences. For example, one might have
+
+           [W] Unsatisfiable (Text "msg1"), [W] Unsatisfiable (Text "msg2")
+
+         and W-W fundep interaction would produce the insoluble constraint
+
+           [W] "msg1" ~ "msg2"
+
+         which we definitely wouldn't want to report to the user.
+
+  D. Adding "meth = unsatisfiable @msg" method bindings.
+
+     When a class instance has an "Unsatisfiable msg" constraint in its context,
+     and the user has omitted methods (which don't have any default implementations),
+     we add method bindings of the form "meth = unsatisfiable @msg".
+     See GHC.Tc.TyCl.Instance.tcMethods, in particular "tc_default".
+
+     Example:
+
+         class C a where { op :: a -> a }
+         instance Unsatisfiable Msg => C [a] where {}
+
+       elaborates to
+
+         instance Unsatisfiable Msg => C [a] where { op = unsatisfiable @Msg }
+
+       due to the (Unsatisfiable Msg) constraint in the instance context.
+
+     We also switch off the "missing methods" warning in this situation.
+     See "checkMinimalDefinition" in GHC.Tc.TyCl.Instance.tcMethods.
+
+  E. Switching off functional dependency coverage checks when there is
+     an "Unsatisfiable msg" context.
+
+     This is because we want to allow users to rule out certain instances with
+     an "unsatisfiable" error, even when that would violate a functional
+     dependency. For example:
+
+       class C a b | a -> b
+       instance Unsatisfiable (Text "No") => C a b
+
+     See GHC.Tc.Instance.FunDeps.checkInstCoverage.
+
+  F. Error reporting of "Unsatisfiable msg" constraints.
+
+     This is done in GHC.Tc.Errors.reportWanteds: we detect when a constraint
+     is of the form "Unsatisfiable msg" and just emit the custom message
+     as an error to the user.
+
+     This is the only way that "Unsatisfiable msg" constraints are reported,
+     which makes their behaviour much more predictable than TypeError.
+-}
 
 
 --------------------------------------------
@@ -922,10 +1049,15 @@ mkUserTypeErrorReporter ctxt
                         ; addDeferredBinding ctxt err item }
 
 mkUserTypeError :: ErrorItem -> TcSolverReportMsg
-mkUserTypeError item =
-  case getUserTypeErrorMsg (errorItemPred item) of
-    Just msg -> UserTypeError msg
-    Nothing  -> pprPanic "mkUserTypeError" (ppr item)
+mkUserTypeError item
+  | Just msg <- getUserTypeErrorMsg pty
+  = UserTypeError msg
+  | Just msg <- isUnsatisfiableCt_maybe pty
+  = UnsatisfiableError msg
+  | otherwise
+  = pprPanic "mkUserTypeError" (ppr item)
+  where
+    pty = errorItemPred item
 
 mkGivenErrorReporter :: Reporter
 -- See Note [Given errors]
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index 33c67fee79..4152866492 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -3438,6 +3438,8 @@ pprTcSolverReportMsg _ (BadTelescope telescope skols) =
     sorted_tvs = scopedSort skols
 pprTcSolverReportMsg _ (UserTypeError ty) =
   pprUserTypeErrorTy ty
+pprTcSolverReportMsg _ (UnsatisfiableError ty) =
+  pprUserTypeErrorTy ty
 pprTcSolverReportMsg ctxt (ReportHoleError hole err) =
   pprHoleError ctxt hole err
 pprTcSolverReportMsg ctxt
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index e2a69e0ce2..8cdc5eb007 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -150,7 +150,7 @@ import GHC.Core.InstEnv (LookupInstanceErrReason, ClsInst)
 import GHC.Core.PatSyn (PatSyn)
 import GHC.Core.Predicate (EqRel, predTypeEqRel)
 import GHC.Core.TyCon (TyCon, Role)
-import GHC.Core.Type (Kind, Type, ThetaType, PredType)
+import GHC.Core.Type (Kind, Type, ThetaType, PredType, ErrorMsgType)
 import GHC.Driver.Backend (Backend)
 import GHC.Unit.State (UnitState)
 import GHC.Utils.Misc (capitalise, filterOut)
@@ -4482,7 +4482,10 @@ data TcSolverReportMsg
   --   err = ()
   --
   -- Test cases: CustomTypeErrors0{1,2,3,4,5}, T12104.
-  | UserTypeError Type
+  | UserTypeError ErrorMsgType -- ^ the message to report
+
+  -- | Report a Wanted constraint of the form "Unsatisfiable msg".
+  | UnsatisfiableError ErrorMsgType -- ^ the message to report
 
   -- | We want to report an out of scope variable or a typed hole.
   -- See 'HoleError'.
diff --git a/compiler/GHC/Tc/Instance/Class.hs b/compiler/GHC/Tc/Instance/Class.hs
index 00811459c4..349ea1e34c 100644
--- a/compiler/GHC/Tc/Instance/Class.hs
+++ b/compiler/GHC/Tc/Instance/Class.hs
@@ -121,17 +121,18 @@ matchGlobalInst :: DynFlags
                              -- See Note [Shortcut solving: overlap]
                 -> Class -> [Type] -> TcM ClsInstResult
 matchGlobalInst dflags short_cut clas tys
-  | cls_name == knownNatClassName     = matchKnownNat    dflags short_cut clas tys
-  | cls_name == knownSymbolClassName  = matchKnownSymbol dflags short_cut clas tys
-  | cls_name == knownCharClassName    = matchKnownChar   dflags short_cut clas tys
-  | isCTupleClass clas                = matchCTuple                       clas tys
-  | cls_name == typeableClassName     = matchTypeable                     clas tys
-  | cls_name == withDictClassName     = matchWithDict                          tys
-  | clas `hasKey` heqTyConKey         = matchHeteroEquality                    tys
-  | clas `hasKey` eqTyConKey          = matchHomoEquality                      tys
-  | clas `hasKey` coercibleTyConKey   = matchCoercible                         tys
-  | cls_name == hasFieldClassName     = matchHasField    dflags short_cut clas tys
-  | otherwise                         = matchInstEnv     dflags short_cut clas tys
+  | cls_name == knownNatClassName      = matchKnownNat    dflags short_cut clas tys
+  | cls_name == knownSymbolClassName   = matchKnownSymbol dflags short_cut clas tys
+  | cls_name == knownCharClassName     = matchKnownChar   dflags short_cut clas tys
+  | isCTupleClass clas                 = matchCTuple                       clas tys
+  | cls_name == typeableClassName      = matchTypeable                     clas tys
+  | cls_name == withDictClassName      = matchWithDict                          tys
+  | clas `hasKey` heqTyConKey          = matchHeteroEquality                    tys
+  | clas `hasKey` eqTyConKey           = matchHomoEquality                      tys
+  | clas `hasKey` coercibleTyConKey    = matchCoercible                         tys
+  | cls_name == hasFieldClassName      = matchHasField    dflags short_cut clas tys
+  | cls_name == unsatisfiableClassName = return NoInstance -- See (B) in Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors
+  | otherwise                          = matchInstEnv     dflags short_cut clas tys
   where
     cls_name = className clas
 
diff --git a/compiler/GHC/Tc/Instance/FunDeps.hs b/compiler/GHC/Tc/Instance/FunDeps.hs
index 681fd5d9a2..3b4768fb99 100644
--- a/compiler/GHC/Tc/Instance/FunDeps.hs
+++ b/compiler/GHC/Tc/Instance/FunDeps.hs
@@ -37,6 +37,7 @@ import GHC.Core.TyCo.FVs
 import GHC.Core.TyCo.Compare( eqTypes, eqType )
 import GHC.Core.TyCo.Ppr( pprWithExplicitKindsWhen )
 
+import GHC.Tc.Types.Constraint ( isUnsatisfiableCt_maybe )
 import GHC.Tc.Utils.TcType( transSuperClasses )
 
 import GHC.Types.Var.Set
@@ -401,6 +402,15 @@ checkInstCoverage :: Bool   -- Be liberal
 --    Just msg => coverage problem described by msg
 
 checkInstCoverage be_liberal clas theta inst_taus
+  | any (isJust . isUnsatisfiableCt_maybe) theta
+  -- As per [GHC proposal #433](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0433-unsatisfiable.rst),
+  -- we skip checking the coverage condition if there is an "Unsatisfiable"
+  -- constraint in the instance context.
+  --
+  -- See Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors,
+  -- point (E).
+  = IsValid
+  | otherwise
   = allValid (map fundep_ok fds)
   where
     (tyvars, fds) = classTvsFds clas
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index d4dae8e31e..eaa62e44ea 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE MultiWayIf, RecursiveDo #-}
+{-# LANGUAGE MultiWayIf, RecursiveDo, TupleSections #-}
 
 module GHC.Tc.Solver(
        InferMode(..), simplifyInfer, findInferredDiff,
@@ -31,11 +31,15 @@ import GHC.Prelude
 
 import GHC.Data.Bag
 import GHC.Core.Class
+import GHC.Core
+import GHC.Core.DataCon
+import GHC.Core.InstEnv ( Coherence(IsCoherent) )
+import GHC.Core.Make
 import GHC.Driver.Session
-import GHC.Tc.Utils.Instantiate
+import GHC.Data.FastString
 import GHC.Data.List.SetOps
 import GHC.Types.Name
-import GHC.Types.Id( idType )
+import GHC.Types.Id
 import GHC.Utils.Outputable
 import GHC.Builtin.Utils
 import GHC.Builtin.Names
@@ -58,22 +62,25 @@ import GHC.Tc.Utils.TcType
 import GHC.Core.Type
 import GHC.Core.Ppr
 import GHC.Core.TyCon    ( TyConBinder, isTypeFamilyTyCon )
-import GHC.Builtin.Types ( liftedRepTy, liftedDataConTy )
+import GHC.Builtin.Types
 import GHC.Core.Unify    ( tcMatchTyKi )
+import GHC.Unit.Module ( getModule )
 import GHC.Utils.Misc
 import GHC.Utils.Panic
 import GHC.Types.Var
 import GHC.Types.Var.Set
-import GHC.Types.Basic    ( IntWithInf, intGtLimit
-                          , DefaultingStrategy(..), NonStandardDefaultingStrategy(..) )
+import GHC.Types.Basic
+import GHC.Types.Id.Make  ( unboxedUnitExpr )
 import GHC.Types.Error
 import qualified GHC.LanguageExtensions as LangExt
 
 import Control.Monad
+import Control.Monad.Trans.Class        ( lift )
+import Control.Monad.Trans.State.Strict ( StateT(runStateT), put )
 import Data.Foldable      ( toList )
 import Data.List          ( partition )
 import Data.List.NonEmpty ( NonEmpty(..) )
-import GHC.Data.Maybe     ( mapMaybe, isJust )
+import GHC.Data.Maybe     ( mapMaybe )
 
 {-
 *********************************************************************************
@@ -487,7 +494,11 @@ simplifyTopWanteds wanteds
   = do { wc_first_go <- nestTcS (solveWanteds wanteds)
                             -- This is where the main work happens
        ; dflags <- getDynFlags
-       ; try_tyvar_defaulting dflags wc_first_go }
+       ; wc_defaulted <- try_tyvar_defaulting dflags wc_first_go
+
+       -- See Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors,
+       -- point (C).
+       ; useUnsatisfiableGivens wc_defaulted }
   where
     try_tyvar_defaulting :: DynFlags -> WantedConstraints -> TcS WantedConstraints
     try_tyvar_defaulting dflags wc
@@ -539,6 +550,149 @@ simplifyTopWanteds wanteds
       | otherwise
       = defaultCallStacks wc
 
+-- | If an implication contains a Given of the form @Unsatisfiable msg@, use
+-- it to solve all Wanteds within the implication.
+--
+-- This does a complete walk over the implication tree.
+--
+-- See point (C) in Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors.
+useUnsatisfiableGivens :: WantedConstraints -> TcS WantedConstraints
+useUnsatisfiableGivens wc =
+  do { (final_wc, did_work) <- (`runStateT` False) $ go_wc wc
+     ; if did_work
+       then nestTcS (solveWanteds final_wc)
+       else return final_wc }
+  where
+    go_wc (WC { wc_simple = wtds, wc_impl = impls, wc_errors = errs })
+      = do impls' <- mapMaybeBagM go_impl impls
+           return $ WC { wc_simple = wtds, wc_impl = impls', wc_errors = errs }
+    go_impl impl
+      | isSolvedStatus (ic_status impl)
+      = return $ Just impl
+      -- Is there a Given with type "Unsatisfiable msg"?
+      -- If so, use it to solve all other Wanteds.
+      | unsat_given:_ <- mapMaybe unsatisfiableEv_maybe (ic_given impl)
+      = do { put True
+           ; lift $ solveImplicationUsingUnsatGiven unsat_given impl }
+      -- Otherwise, recurse.
+      | otherwise
+      = do { wcs' <- go_wc (ic_wanted impl)
+           ; lift $ setImplicationStatus $ impl { ic_wanted = wcs' } }
+
+-- | Is this evidence variable the evidence for an 'Unsatisfiable' constraint?
+--
+-- If so, return the variable itself together with the error message type.
+unsatisfiableEv_maybe :: EvVar -> Maybe (EvVar, Type)
+unsatisfiableEv_maybe v = (v,) <$> isUnsatisfiableCt_maybe (idType v)
+
+-- | We have an implication with an 'Unsatisfiable' Given; use that Given to
+-- solve all the other Wanted constraints, including those nested within
+-- deeper implications.
+solveImplicationUsingUnsatGiven :: (EvVar, Type) -> Implication -> TcS (Maybe Implication)
+solveImplicationUsingUnsatGiven
+  unsat_given@(given_ev,_)
+  impl@(Implic { ic_wanted = wtd, ic_tclvl = tclvl, ic_binds = ev_binds_var, ic_need_inner = inner })
+  | isCoEvBindsVar ev_binds_var
+  -- We can't use Unsatisfiable evidence in kinds.
+  -- See Note [Coercion evidence only] in GHC.Tc.Types.Evidence.
+  = return $ Just impl
+  | otherwise
+  = do { wcs <- nestImplicTcS ev_binds_var tclvl $ go_wc wtd
+       ; setImplicationStatus $
+         impl { ic_wanted = wcs
+              , ic_need_inner = inner `extendVarSet` given_ev } }
+  where
+    go_wc :: WantedConstraints -> TcS WantedConstraints
+    go_wc wc@(WC { wc_simple = wtds, wc_impl = impls })
+      = do { mapBagM_ go_simple wtds
+           ; impls <- mapMaybeBagM (solveImplicationUsingUnsatGiven unsat_given) impls
+           ; return $ wc { wc_simple = emptyBag, wc_impl = impls } }
+    go_simple :: Ct -> TcS ()
+    go_simple ct = case ctEvidence ct of
+      CtWanted { ctev_pred = pty, ctev_dest = dst }
+        -> do { ev_expr <- unsatisfiableEvExpr unsat_given pty
+              ; setWantedEvTerm dst IsCoherent $ EvExpr ev_expr }
+      _ -> return ()
+
+-- | Create an evidence expression for an arbitrary constraint using
+-- evidence for an "Unsatisfiable" Given.
+--
+-- See Note [Evidence terms from Unsatisfiable Givens]
+unsatisfiableEvExpr :: (EvVar, ErrorMsgType) -> PredType -> TcS EvExpr
+unsatisfiableEvExpr (unsat_ev, given_msg) wtd_ty
+  = do { mod <- getModule
+         -- If we're typechecking GHC.TypeError, return a bogus expression;
+         -- it's only used for the ambiguity check, which throws the evidence away anyway.
+         -- This avoids problems with circularity; where we are trying to look
+         -- up the "unsatisfiable" Id while we are in the middle of typechecking it.
+       ; if mod == gHC_TYPEERROR then return (Var unsat_ev) else
+    do { unsatisfiable_id <- tcLookupId unsatisfiableIdName
+
+         -- See Note [Evidence terms from Unsatisfiable Givens]
+         -- for a description of what evidence term we are constructing here.
+
+       ; let -- (##) -=> wtd_ty
+             fun_ty = mkFunTy visArgConstraintLike ManyTy unboxedUnitTy wtd_ty
+             mkDictBox = case boxingDataCon fun_ty of
+               BI_Box { bi_data_con = mkDictBox } -> mkDictBox
+               _ -> pprPanic "unsatisfiableEvExpr: no DictBox!" (ppr wtd_ty)
+             dictBox = dataConTyCon mkDictBox
+       ; ev_bndr <- mkSysLocalM (fsLit "ct") ManyTy fun_ty
+             -- Dict ((##) -=> wtd_ty)
+       ; let scrut_ty = mkTyConApp dictBox [fun_ty]
+             -- unsatisfiable @{LiftedRep} @given_msg @(Dict ((##) -=> wtd_ty)) unsat_ev
+             scrut =
+               mkCoreApps (Var unsatisfiable_id)
+                 [ Type liftedRepTy
+                 , Type given_msg
+                 , Type scrut_ty
+                 , Var unsat_ev ]
+             -- case scrut of { MkDictBox @((##) -=> wtd_ty)) ct -> ct (# #) }
+             ev_expr =
+               mkWildCase scrut (unrestricted $ scrut_ty) wtd_ty
+               [ Alt (DataAlt mkDictBox) [ev_bndr] $
+                   mkCoreApps (Var ev_bndr) [unboxedUnitExpr]
+               ]
+        ; return ev_expr } }
+
+{- Note [Evidence terms from Unsatisfiable Givens]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+An Unsatisfiable Given constraint, of the form [G] Unsatisfiable msg, should be
+able to solve ANY Wanted constraint whatsoever.
+
+Recall that we have
+
+  unsatisfiable :: forall {rep} (msg :: ErrorMessage) (a :: TYPE rep)
+                .  Unsatisfiable msg => a
+
+We want to use this function, together with the evidence
+[G] unsat_ev :: Unsatisfiable msg, to solve any other constraint [W] wtd_ty.
+
+We could naively think that a valid evidence term for the Wanted might be:
+
+  wanted_ev = unsatisfiable @{rep} @msg @wtd_ty unsat_ev
+
+Unfortunately, this is a kind error: "wtd_ty :: CONSTRAINT rep", but
+"unsatisfiable" expects the third type argument to be of kind "TYPE rep".
+
+Instead, we use a boxing data constructor to box the constraint into a type.
+In the end, we construct the following evidence for the implication:
+
+  [G] unsat_ev :: Unsatisfiable msg
+    ==>
+      [W] wtd_ev :: wtd_ty
+
+  wtd_ev =
+    case unsatisfiable @{LiftedRep} @msg @(Dict ((##) -=> wtd_ty)) unsat_ev of
+      MkDictBox ct -> ct (# #)
+
+Note that we play the same trick with the function arrow -=> that we did
+in order to define "unsatisfiable" in terms of "unsatisfiableLifted", as described
+in Note [The Unsatisfiable representation-polymorphism trick] in base:GHC.TypeError.
+This allows us to indirectly box constraints with different representations
+(such as primitive equality constraints).
+-}
+
 -- | Default any remaining @CallStack@ constraints to empty @CallStack@s.
 defaultCallStacks :: WantedConstraints -> TcS WantedConstraints
 -- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
@@ -845,8 +999,11 @@ last example above.
 simplifyAmbiguityCheck :: Type -> WantedConstraints -> TcM ()
 simplifyAmbiguityCheck ty wanteds
   = do { traceTc "simplifyAmbiguityCheck {" (text "type = " <+> ppr ty $$ text "wanted = " <+> ppr wanteds)
-       ; (final_wc, _) <- runTcS $ solveWanteds wanteds
+       ; (final_wc, _) <- runTcS $ useUnsatisfiableGivens =<< solveWanteds wanteds
              -- NB: no defaulting!  See Note [No defaulting in the ambiguity check]
+             -- Note: we do still use Unsatisfiable Givens to solve Wanteds,
+             -- see Wrinkle [Ambiguity] under point (C) of
+             -- Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors.
 
        ; traceTc "End simplifyAmbiguityCheck }" empty
 
@@ -2785,9 +2942,9 @@ findUnnecessaryGivens info need_inner givens
 
     unused_givens = filterOut is_used givens
 
-    is_used given =   is_type_error given
-                  ||  (given `elemVarSet` need_inner)
-                  ||  (in_instance_decl && is_improving (idType given))
+    is_used given =  is_type_error given
+                  || given `elemVarSet` need_inner
+                  || (in_instance_decl && is_improving (idType given))
 
     minimal_givens = mkMinimalBySCs evVarPred givens
     is_minimal = (`elemVarSet` mkVarSet minimal_givens)
@@ -2796,7 +2953,7 @@ findUnnecessaryGivens info need_inner givens
       | otherwise        = filterOut is_minimal givens
 
     -- See #15232
-    is_type_error = isJust . userTypeError_maybe . idType
+    is_type_error id = isTopLevelUserTypeError (idType id)
 
     is_improving pred -- (transSuperClasses p) does not include p
       = any isImprovementPred (pred : transSuperClasses pred)
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index 49699d865d..bd2e48682f 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -59,7 +59,8 @@ module GHC.Tc.Solver.Monad (
     getTopEnv, getGblEnv, getLclEnv, setLclEnv,
     getTcEvBindsVar, getTcLevel,
     getTcEvTyCoVars, getTcEvBindsMap, setTcEvBindsMap,
-    tcLookupClass, tcLookupId,
+    tcLookupClass, tcLookupId, tcLookupTyCon,
+
 
     -- Inerts
     updInertTcS, updInertCans, updInertDicts, updInertIrreds,
@@ -134,7 +135,9 @@ import qualified GHC.Tc.Utils.Monad    as TcM
 import qualified GHC.Tc.Utils.TcMType  as TcM
 import qualified GHC.Tc.Instance.Class as TcM( matchGlobalInst, ClsInstResult(..) )
 import qualified GHC.Tc.Utils.Env      as TcM
-       ( checkWellStaged, tcGetDefaultTys, tcLookupClass, tcLookupId, topIdLvl
+       ( checkWellStaged, tcGetDefaultTys
+       , tcLookupClass, tcLookupId, tcLookupTyCon
+       , topIdLvl
        , tcInitTidyEnv )
 
 import GHC.Driver.Session
@@ -151,6 +154,8 @@ import GHC.Tc.Types.Origin
 import GHC.Tc.Types.Constraint
 import GHC.Tc.Utils.Unify
 
+import GHC.Builtin.Names ( unsatisfiableClassNameKey )
+
 import GHC.Core.Type
 import GHC.Core.TyCo.Rep as Rep
 import GHC.Core.Coercion
@@ -536,17 +541,25 @@ getInnermostGivenEqLevel :: TcS TcLevel
 getInnermostGivenEqLevel = do { inert <- getInertCans
                               ; return (inert_given_eq_lvl inert) }
 
-getInertInsols :: TcS Cts
--- Returns insoluble equality constraints and TypeError constraints,
--- specifically including Givens.
+-- | Retrieves all insoluble constraints from the inert set,
+-- specifically including Given constraints.
 --
--- Note that this function only inspects irreducible constraints;
--- a DictCan constraint such as 'Eq (TypeError msg)' is not
--- considered to be an insoluble constraint by this function.
+-- This consists of:
 --
--- See Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver.
+--  - insoluble equalities, such as @Int ~# Bool@;
+--  - constraints that are top-level custom type errors, of the form
+--    @TypeError msg@, but not constraints such as @Eq (TypeError msg)@
+--    in which the type error is nested;
+--  - unsatisfiable constraints, of the form @Unsatisfiable msg@.
+--
+-- The inclusion of Givens is important for pattern match warnings, as we
+-- want to consider a pattern match that introduces insoluble Givens to be
+-- redundant (see Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver).
+getInertInsols :: TcS Cts
 getInertInsols = do { inert <- getInertCans
-                    ; return $ filterBag insolubleCt (inert_irreds inert) }
+                    ; let irreds = inert_irreds inert
+                          unsats = findDictsByTyConKey (inert_dicts inert) unsatisfiableClassNameKey
+                    ; return $ unsats `unionBags` filterBag insolubleCt irreds }
 
 getInertGivens :: TcS [Ct]
 -- Returns the Given constraints in the inert set
@@ -1356,6 +1369,9 @@ tcLookupClass c = wrapTcS $ TcM.tcLookupClass c
 tcLookupId :: Name -> TcS Id
 tcLookupId n = wrapTcS $ TcM.tcLookupId n
 
+tcLookupTyCon :: Name -> TcS TyCon
+tcLookupTyCon n = wrapTcS $ TcM.tcLookupTyCon n
+
 -- Any use of this function is a bit suspect, because it violates the
 -- pure veneer of TcS. But it's just about warnings around unused imports
 -- and local constructors (GHC will issue fewer warnings than it otherwise
diff --git a/compiler/GHC/Tc/Solver/Types.hs b/compiler/GHC/Tc/Solver/Types.hs
index 80ca1113a6..648f451eee 100644
--- a/compiler/GHC/Tc/Solver/Types.hs
+++ b/compiler/GHC/Tc/Solver/Types.hs
@@ -4,7 +4,8 @@
 -- | Utility types used within the constraint solver
 module GHC.Tc.Solver.Types (
     -- Inert CDictCans
-    DictMap, emptyDictMap, findDictsByClass, addDict,
+    DictMap, emptyDictMap, addDict,
+    findDictsByTyConKey, findDictsByClass,
     addDictsByClass, delDict, foldDicts, filterDicts, findDict,
     dictsToBag, partitionDicts,
 
@@ -25,6 +26,9 @@ import GHC.Tc.Types.Constraint
 import GHC.Tc.Types.Origin
 import GHC.Tc.Utils.TcType
 
+import GHC.Types.Unique
+import GHC.Types.Unique.DFM
+
 import GHC.Core.Class
 import GHC.Core.Map.Type
 import GHC.Core.Predicate
@@ -140,9 +144,12 @@ findDict m loc cls tys
   = findTcApp m (classTyCon cls) tys
 
 findDictsByClass :: DictMap a -> Class -> Bag a
-findDictsByClass m cls
-  | Just tm <- lookupDTyConEnv m (classTyCon cls) = foldTM consBag tm emptyBag
-  | otherwise                                     = emptyBag
+findDictsByClass m cls = findDictsByTyConKey m (getUnique $ classTyCon cls)
+
+findDictsByTyConKey :: DictMap a -> Unique -> Bag a
+findDictsByTyConKey m tc
+  | Just tm <- lookupUDFM_Directly m tc = foldTM consBag tm emptyBag
+  | otherwise                           = emptyBag
 
 delDict :: DictMap a -> Class -> [Type] -> DictMap a
 delDict m cls tys = delTcApp m (classTyCon cls) tys
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index caae46ce36..f0bfb8b4da 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -6,6 +6,8 @@
 
 
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE TupleSections #-}
 {-# LANGUAGE TypeFamilies #-}
 
 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
@@ -48,6 +50,7 @@ import GHC.Tc.Deriv
 import GHC.Tc.Utils.Env
 import GHC.Tc.Gen.HsType
 import GHC.Tc.Utils.Unify
+import GHC.Builtin.Names ( unsatisfiableIdName )
 import GHC.Core        ( Expr(..), mkApps, mkVarApps, mkLams )
 import GHC.Core.Make   ( nO_METHOD_BINDING_ERROR_ID )
 import GHC.Core.Unfold.Make ( mkInlineUnfoldingWithArity, mkDFunUnfolding )
@@ -1785,6 +1788,9 @@ tcMethods skol_info dfun_id clas tyvars dfun_ev_vars inst_tys
     hs_sig_fn = mkHsSigFun sigs
     inst_loc  = getSrcSpan dfun_id
 
+    unsat_thetas =
+      mapMaybe (\ id -> (id,) <$> isUnsatisfiableCt_maybe (idType id)) dfun_ev_vars
+
     ----------------------
     tc_item :: ClassOpItem -> TcM (Id, LHsBind GhcTc, Maybe Implication)
     tc_item (sel_id, dm_info)
@@ -1813,8 +1819,29 @@ tcMethods skol_info dfun_id clas tyvars dfun_ev_vars inst_tys
            ; (meth_id, _) <- mkMethIds clas tyvars dfun_ev_vars
                                        inst_tys sel_id
            ; dflags <- getDynFlags
-           ; let meth_bind = mkVarBind meth_id $
-                             mkLHsWrap lam_wrapper (error_rhs dflags)
+           ; meth_rhs <-
+               if
+                  -- If the instance has an "Unsatisfiable msg" context,
+                  -- add method bindings that use "unsatisfiable".
+                  --
+                  -- See Note [Implementation of Unsatisfiable constraints],
+                  -- in GHC.Tc.Errors, point (D).
+                  | (theta_id,unsat_msg):_ <- unsat_thetas
+                  -> do { unsat_id <- tcLookupId unsatisfiableIdName
+                        -- Recall that unsatisfiable :: forall {rep} (msg :: ErrorMessage) (a :: TYPE rep). Unsatisfiable msg => a
+                        --
+                        -- So we need to instantiate the forall and pass the dictionary evidence.
+                        ; return $ L inst_loc' $
+                            wrapId
+                            (   mkWpEvApps [EvExpr $ Var theta_id]
+                            <.> mkWpTyApps [getRuntimeRep meth_tau, unsat_msg, meth_tau])
+                            unsat_id }
+
+                  -- Otherwise, add bindings whose RHS is an error
+                  -- "No explicit nor default method for class operation 'meth'".
+                  | otherwise
+                  -> return $ error_rhs dflags
+           ; let meth_bind = mkVarBind meth_id $ mkLHsWrap lam_wrapper meth_rhs
            ; return (meth_id, meth_bind, Nothing) }
       where
         inst_loc' = noAnnSrcSpan inst_loc
@@ -1829,13 +1856,18 @@ tcMethods skol_info dfun_id clas tyvars dfun_ev_vars inst_tys
                                               (unsafeMkByteString (error_string dflags))))
         meth_tau     = classMethodInstTy sel_id inst_tys
         error_string dflags = showSDoc dflags
-                              (hcat [ppr inst_loc, vbar, ppr sel_id ])
+                              (hcat [ppr inst_loc, vbar, quotes (ppr sel_id) ])
         lam_wrapper  = mkWpTyLams tyvars <.> mkWpEvLams dfun_ev_vars
 
     ----------------------
     -- Check if one of the minimal complete definitions is satisfied
     checkMinimalDefinition
-      = whenIsJust (isUnsatisfied methodExists (classMinimalDef clas)) $
+      = when (null unsat_thetas) $
+        -- Don't warn if there is an "Unsatisfiable" constraint in the context.
+        --
+        -- See Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors,
+        -- point (D).
+        whenIsJust (isUnsatisfied methodExists (classMinimalDef clas)) $
         warnUnsatisfiedMinimalDefinition
 
     methodExists meth = isJust (findMethodBind meth binds prag_fn)
diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index 6fc6b235c4..d99f9067df 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -16,7 +16,8 @@ module GHC.Tc.Types.Constraint (
         isPendingScDict, pendingScDict_maybe,
         superClassesMightHelp, getPendingWantedScs,
         isWantedCt, isGivenCt,
-        isUserTypeError, getUserTypeErrorMsg,
+        isTopLevelUserTypeError, containsUserTypeError, getUserTypeErrorMsg,
+        isUnsatisfiableCt_maybe,
         ctEvidence, ctLoc, ctPred, ctFlavour, ctEqRel, ctOrigin,
         ctRewriters,
         ctEvId, wantedEvId_maybe, mkTcEqPredLikeEv,
@@ -118,8 +119,8 @@ import GHC.Core.TyCo.Ppr
 import GHC.Utils.FV
 import GHC.Types.Var.Set
 import GHC.Driver.Session (DynFlags(reductionDepth))
+import GHC.Builtin.Names
 import GHC.Types.Basic
-import GHC.Types.Unique
 import GHC.Types.Unique.Set
 
 import GHC.Utils.Outputable
@@ -134,7 +135,7 @@ import Data.Coerce
 import Data.Monoid ( Endo(..) )
 import qualified Data.Semigroup as S
 import Control.Monad ( msum, when )
-import Data.Maybe ( mapMaybe )
+import Data.Maybe ( mapMaybe, isJust )
 import Data.List.NonEmpty ( NonEmpty )
 
 -- these are for CheckTyEqResult
@@ -957,7 +958,7 @@ Eq (F (TypeError msg))  -- Here the type error is nested under a type-function
 -- | A constraint is considered to be a custom type error, if it contains
 -- custom type errors anywhere in it.
 -- See Note [Custom type errors in constraints]
-getUserTypeErrorMsg :: PredType -> Maybe Type
+getUserTypeErrorMsg :: PredType -> Maybe ErrorMsgType
 getUserTypeErrorMsg pred = msum $ userTypeError_maybe pred
                                   : map getUserTypeErrorMsg (subTys pred)
   where
@@ -971,10 +972,30 @@ getUserTypeErrorMsg pred = msum $ userTypeError_maybe pred
                               Just (_,ts) -> ts
                  (t,ts) -> t : ts
 
-isUserTypeError :: PredType -> Bool
-isUserTypeError pred = case getUserTypeErrorMsg pred of
-                             Just _ -> True
-                             _      -> False
+-- | Is this an user error message type, i.e. either the form @TypeError err@ or
+-- @Unsatisfiable err@?
+isTopLevelUserTypeError :: PredType -> Bool
+isTopLevelUserTypeError pred =
+  isJust (userTypeError_maybe pred) || isJust (isUnsatisfiableCt_maybe pred)
+
+-- | Does this constraint contain an user error message?
+--
+-- That is, the type is either of the form @Unsatisfiable err@, or it contains
+-- a type of the form @TypeError msg@, either at the top level or nested inside
+-- the type.
+containsUserTypeError :: PredType -> Bool
+containsUserTypeError pred =
+  isJust (getUserTypeErrorMsg pred) || isJust (isUnsatisfiableCt_maybe pred)
+
+-- | Is this type an unsatisfiable constraint?
+-- If so, return the error message.
+isUnsatisfiableCt_maybe :: Type -> Maybe ErrorMsgType
+isUnsatisfiableCt_maybe t
+  | Just (tc, [msg]) <- splitTyConApp_maybe t
+  , tc `hasKey` unsatisfiableClassNameKey
+  = Just msg
+  | otherwise
+  = Nothing
 
 isPendingScDict :: Ct -> Bool
 isPendingScDict (CDictCan { cc_pend_sc = f }) = pendingFuel f
@@ -1297,22 +1318,23 @@ insolubleEqCt _                                  = False
 -- nested custom type errors: it only detects @TypeError msg :: Constraint@,
 -- and not e.g. @Eq (TypeError msg)@.
 insolubleCt :: Ct -> Bool
-insolubleCt ct
-  | Just _ <- userTypeError_maybe (ctPred ct)
-  -- Don't use 'isUserTypeErrorCt' here, as that function is too eager:
-  -- the TypeError might appear inside a type family application
-  -- which might later reduce, but we only want to return 'True'
+insolubleCt ct = isTopLevelUserTypeError (ctPred ct) || insolubleEqCt ct
+  where
+  -- NB: 'isTopLevelUserTypeError' detects constraints of the form "TypeError msg"
+  -- and "Unsatisfiable msg". It deliberately does not detect TypeError
+  -- nested in a type (e.g. it does not use "containsUserTypeError"), as that
+  -- would be too eager: the TypeError might appear inside a type family
+  -- application which might later reduce, but we only want to return 'True'
   -- for constraints that are definitely insoluble.
   --
+  -- For example: Num (F Int (TypeError "msg")), where F is a type family.
+  --
   -- Test case: T11503, with the 'Assert' type family:
   --
   -- > type Assert :: Bool -> Constraint -> Constraint
   -- > type family Assert check errMsg where
   -- >   Assert 'True  _errMsg = ()
   -- >   Assert _check errMsg  = errMsg
-  = True
-  | otherwise
-  = insolubleEqCt ct
 
 -- | Does this hole represent an "out of scope" error?
 -- See Note [Insoluble holes]
diff --git a/compiler/GHC/Tc/Utils/Env.hs b/compiler/GHC/Tc/Utils/Env.hs
index b8f9d83912..aa7230108c 100644
--- a/compiler/GHC/Tc/Utils/Env.hs
+++ b/compiler/GHC/Tc/Utils/Env.hs
@@ -462,7 +462,7 @@ tcLookup name = do
     local_env <- getLclTypeEnv
     case lookupNameEnv local_env name of
         Just thing -> return thing
-        Nothing    -> (AGlobal <$> tcLookupGlobal name)
+        Nothing    -> AGlobal <$> tcLookupGlobal name
 
 tcLookupTyVar :: Name -> TcM TcTyVar
 tcLookupTyVar name
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index e7d33c3a80..1a03cd1c4b 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -2542,6 +2542,7 @@ isTerminatingClass cls
             -- Typeable constraints are bigger than they appear due
             -- to kind polymorphism, but we can never get instance divergence this way
     || cls `hasKey` coercibleTyConKey
+    || cls `hasKey` unsatisfiableClassNameKey
 
 allDistinctTyVars :: TyVarSet -> [KindOrType] -> Bool
 -- (allDistinctTyVars tvs tys) returns True if tys are
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index 250811b99e..da51f7245f 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -1503,7 +1503,9 @@ check_special_inst_head dflags is_boot is_sig ctxt clas cls_args
   -- instances for (~), (~~), or Coercible;
   -- but we DO want to allow them in quantified constraints:
   --   f :: (forall a b. Coercible a b => Coercible (m a) (m b)) => ...m...
-  | clas_nm `elem` [ heqTyConName, eqTyConName, coercibleTyConName, withDictClassName ]
+  | clas_nm `elem`
+    [ heqTyConName, eqTyConName, coercibleTyConName
+    , withDictClassName, unsatisfiableClassName ]
   , not quantified_constraint
   = failWithTc $ TcRnSpecialClassInst clas False
 
diff --git a/compiler/GHC/Types/Error/Codes.hs b/compiler/GHC/Types/Error/Codes.hs
index 9c2f7d1dc3..195f6e0608 100644
--- a/compiler/GHC/Types/Error/Codes.hs
+++ b/compiler/GHC/Types/Error/Codes.hs
@@ -300,6 +300,7 @@ type family GhcDiagnosticCode c = n | n -> c where
   -- Constraint solver diagnostic codes
   GhcDiagnosticCode "BadTelescope"                                  = 97739
   GhcDiagnosticCode "UserTypeError"                                 = 64725
+  GhcDiagnosticCode "UnsatisfiableError"                            = 22250
   GhcDiagnosticCode "ReportHoleError"                               = 88464
   GhcDiagnosticCode "UntouchableVariable"                           = 34699
   GhcDiagnosticCode "FixedRuntimeRepError"                          = 55287