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

49 files changed, 1050 insertions, 87 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
diff --git a/docs/users_guide/9.8.1-notes.rst b/docs/users_guide/9.8.1-notes.rst
index 0f0848765f..9f2d51d329 100644
--- a/docs/users_guide/9.8.1-notes.rst
+++ b/docs/users_guide/9.8.1-notes.rst
@@ -93,6 +93,21 @@ Compiler
   with each other, communicating via the system semaphore specified by
   the flag argument.
 
+- GHC Proposal `#433
+  <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0433-unsatisfiable.rst>`_
+  has been implemented. This adds the class ``Unsatisfiable :: ErrorMessage -> Constraint``
+  to the ``GHC.TypeError`` module. Constraints of the form ``Unsatisfiable msg``
+  provide a mechanism for custom type errors that reports the errors in a more
+  predictable behaviour than ``TypeError``, as these constraints are
+  handled purely during constraint solving.
+
+  For example: ::
+
+      instance Unsatisfiable (Text "There is no Eq instance for functions") => Eq (a -> b) where
+        (==) = unsatisfiable
+
+  This allows errors to be reported when users use the instance, even when
+  type errors are being deferred.
 
 GHCi
 ~~~~
diff --git a/libraries/base/GHC/TypeError.hs b/libraries/base/GHC/TypeError.hs
index 77df75854b..21f62afad5 100644
--- a/libraries/base/GHC/TypeError.hs
+++ b/libraries/base/GHC/TypeError.hs
@@ -1,16 +1,25 @@
 {-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE MagicHash #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UnboxedTuples #-}
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# OPTIONS_HADDOCK not-home #-}
 
 {-|
-This module exports the TypeError family, which is used to provide custom type
-errors, and the ErrorMessage kind used to define these custom error messages.
-This is a type-level analogue to the term level error function.
+This module exports:
+
+  - The 'TypeError' type family, which is used to provide custom type
+    errors. This is a type-level analogue to the term level error function.
+  - The 'ErrorMessage' kind, used to define custom error messages.
+  - The 'Unsatisfiable' constraint, a more principled variant of 'TypeError'
+    which gives a more predictable way of reporting custom type errors.
 
 @since 4.17.0.0
 -}
@@ -19,15 +28,15 @@ module GHC.TypeError
   ( ErrorMessage (..)
   , TypeError
   , Assert
+  , Unsatisfiable, unsatisfiable
   ) where
 
 import Data.Bool
 import GHC.Num.Integer () -- See Note [Depend on GHC.Num.Integer] in GHC.Base
-import GHC.Types (Constraint, Symbol)
+import GHC.Types (TYPE, Constraint, Symbol)
 
-{-
-Note [Custom type errors]
-~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Custom type errors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 TypeError is used to provide custom type errors, similar to the term-level
 error function. TypeError is somewhat magical: when the constraint solver
 encounters a constraint where the RHS is TypeError, it reports the error to
@@ -85,9 +94,8 @@ infixl 6 :<>:
 -- @since 4.9.0.0
 type family TypeError (a :: ErrorMessage) :: b where
 
-{-
-Note [Getting good error messages from boolean comparisons]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Getting good error messages from boolean comparisons]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We want to write types like
 
   f :: forall (x :: Int) (y :: Int). (x <= y) => T x -> T y
@@ -139,3 +147,50 @@ type family Assert check errMsg where
   Assert 'True _      = ()
   Assert _     errMsg = errMsg
   -- See Note [Getting good error messages from boolean comparisons]
+
+{- Note [The Unsatisfiable constraint]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The class `Unsatisfiable :: ErrorMessage -> Constraint` provides a mechanism
+for custom type errors that reports the errors in a more predictable behaviour
+than `TypeError`, as these constraints are handled purely during constraint solving.
+
+The details are laid out in GHC Proposal #433 (https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0433-unsatisfiable.rst).
+
+See Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors for
+details of the implementation in GHC.
+
+Note [The Unsatisfiable representation-polymorphism trick]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The class method `unsatisfiableLifted :: forall (a::Type). Unsatisfiable msg => a`
+works only for lifted types `a`.  What if we want an unsatisfiable value of type
+`Int#`, say?  The function `unsatisfiable` has a representation-polymoprhic type
+   unsatisfiable :: forall {rep} (msg :: ErrorMessage) (b :: TYPE rep).
+                    Unsatisfiable msg => b
+and yet is defined in terms of `unsatisfiableLifted`.  How? By instantiating
+`unsatisfiableLifted` at type `(##) -> b`, and applying the result to `(##)`.
+Very cunning!
+-}
+
+-- | An unsatisfiable constraint. Similar to 'TypeError' when used at the
+-- 'Constraint' kind, but reports errors in a more predictable manner.
+--
+-- See also the 'unsatisfiable' function.
+--
+-- @since 4.19.0.0@.
+type Unsatisfiable :: ErrorMessage -> Constraint
+class Unsatisfiable msg where
+  unsatisfiableLifted :: a
+
+-- | Prove anything within a context with an 'Unsatisfiable' constraint.
+--
+-- This is useful for filling in instance methods when there is an 'Unsatisfiable'
+-- constraint in the instance head, e.g.:
+--
+-- > instance Unsatisfiable (Text "No Eq instance for functions") => Eq (a -> b) where
+--     (==) = unsatisfiable
+--
+-- @since 4.19.0.0@.
+unsatisfiable :: forall {rep} (msg :: ErrorMessage) (a :: TYPE rep). Unsatisfiable msg => a
+unsatisfiable = unsatisfiableLifted @msg @((##) -> a) (##)
+  -- See Note [The Unsatisfiable representation-polymorphism trick]
+
diff --git a/libraries/base/changelog.md b/libraries/base/changelog.md
index d25888e7fb..bc55cc4977 100644
--- a/libraries/base/changelog.md
+++ b/libraries/base/changelog.md
@@ -20,6 +20,10 @@
   * Add `COMPLETE` pragmas to the `TypeRep`, `SSymbol`, `SChar`, and `SNat` pattern synonyms.
       ([CLC proposal #149](https://github.com/haskell/core-libraries-committee/issues/149))
   * Make `($)` representation polymorphic ([CLC proposal #132](https://github.com/haskell/core-libraries-committee/issues/132))
+  * Implemented [GHC Proposal #433](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0433-unsatisfiable.rst),
+    adding the class `Unsatisfiable :: ErrorMessage -> TypeError`` to `GHC.TypeError`,
+    which provides a mechanism for custom type errors that reports the errors in
+    a more predictable behaviour than ``TypeError``.
 
 ## 4.18.0.0 *March 2023*
   * Shipped with GHC 9.6.1
diff --git a/testsuite/tests/unsatisfiable/T11503_Unsat.hs b/testsuite/tests/unsatisfiable/T11503_Unsat.hs
new file mode 100644
index 0000000000..a685daf066
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/T11503_Unsat.hs
@@ -0,0 +1,52 @@
+{-# LANGUAGE Haskell2010 #-}
+
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T11503_Unsat where
+
+import GHC.TypeError
+  ( Unsatisfiable, ErrorMessage(..) )
+import GHC.TypeNats
+  ( Nat, type (+), type (<=?) )
+import Data.Kind
+  ( Constraint, Type )
+
+-- Example 1: from #11503
+
+type NotInt :: Type -> Constraint
+type family NotInt a where
+  NotInt Int = Unsatisfiable (Text "That's Int, silly.")
+  NotInt _   = (() :: Constraint)
+
+data T a where
+  MkT1 :: a -> T a
+  MkT2 :: NotInt a => T a
+
+foo :: T Int -> Int
+foo (MkT1 x) = x
+-- Should not have any pattern match warnings for MkT2.
+
+-- Example 2: from #20180
+
+type Assert :: Bool -> Constraint -> Constraint
+type family Assert check errMsg where
+  Assert 'True  _errMsg = ()
+  Assert _check errMsg  = errMsg
+
+type List :: Nat -> Type -> Type
+data List n t where
+  Nil  :: List 0 t
+  (:-) :: t -> List n t -> List (n+1) t
+
+type (<=) :: Nat -> Nat -> Constraint
+type family x <= y where
+  x <= y = Assert (x <=? y) (Unsatisfiable (Text "Impossible!"))
+
+head' :: 1 <= n => List n t -> t
+head' (x :- _) = x
+-- Should not have any pattern match warnings for Nil.
diff --git a/testsuite/tests/unsatisfiable/T14141_Unsat.hs b/testsuite/tests/unsatisfiable/T14141_Unsat.hs
new file mode 100644
index 0000000000..8be3b41960
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/T14141_Unsat.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE Haskell2010 #-}
+
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T14141_Unsat where
+
+import GHC.TypeError
+import Data.Kind
+  ( Constraint, Type )
+
+-- Example 1: from #14141
+
+data D where
+  MkD :: C => D
+
+type C :: Constraint
+type family C where
+    C = Unsatisfiable ('Text "error")
+
+f :: D -> ()
+f MkD = ()
+
+-- Example 2: from #16377
+
+type F :: Type -> Constraint
+type family F a :: Constraint
+type instance F Int  = ()
+type instance F Char = Unsatisfiable  ('Text "Nope")
+
+data T where
+  A :: F Int  => T
+  B :: F Char => T
+
+exhaustive :: T -> ()
+exhaustive A = ()
+exhaustive B = ()
diff --git a/testsuite/tests/unsatisfiable/T14141_Unsat.stderr b/testsuite/tests/unsatisfiable/T14141_Unsat.stderr
new file mode 100644
index 0000000000..d71928917f
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/T14141_Unsat.stderr
@@ -0,0 +1,8 @@
+
+T14141_Unsat.hs:26:1: warning: [GHC-94210] [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match has inaccessible right hand side
+    In an equation for ‘f’: f MkD = ...
+
+T14141_Unsat.hs:41:1: warning: [GHC-53633] [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘exhaustive’: exhaustive B = ...
diff --git a/testsuite/tests/unsatisfiable/T14339_Unsat.hs b/testsuite/tests/unsatisfiable/T14339_Unsat.hs
new file mode 100644
index 0000000000..ffa0c141ab
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/T14339_Unsat.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T14339_Unsat where
+
+import GHC.TypeError
+
+newtype Foo = Foo Int
+
+class Bar a where
+  bar :: a
+
+instance (Unsatisfiable (Text "Boo")) => Bar Foo where
+  bar = undefined
+
+newtype Baz1 = Baz1 Foo
+
+
+-- should be ok
+deriving instance Unsatisfiable (Text "Shouldn't see this") => Bar Baz1
+
+-- should emit the error "Boo"
+newtype Baz2 = Baz2 Foo
+  deriving Bar
diff --git a/testsuite/tests/unsatisfiable/T14339_Unsat.stderr b/testsuite/tests/unsatisfiable/T14339_Unsat.stderr
new file mode 100644
index 0000000000..c24a421eb8
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/T14339_Unsat.stderr
@@ -0,0 +1,4 @@
+
+T14339_Unsat.hs:25:12: error: [GHC-22250]
+    • Boo
+    • When deriving the instance for (Bar Baz2)
diff --git a/testsuite/tests/unsatisfiable/T15232_Unsat.hs b/testsuite/tests/unsatisfiable/T15232_Unsat.hs
new file mode 100644
index 0000000000..c8a55e2be3
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/T15232_Unsat.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+
+module T15232_Unsat where
+
+import GHC.TypeError
+
+class C a where f :: a -> a
+instance {-# OVERLAPPING #-} C Int where f _ = 42
+instance {-# OVERLAPPABLE #-} Unsatisfiable ( 'Text "Only Int is supported" ) => C a where f = undefined
+
+main :: IO ()
+main = print $ f (42::Int)
diff --git a/testsuite/tests/unsatisfiable/T22696_Unsat.stderr b/testsuite/tests/unsatisfiable/T22696_Unsat.stderr
new file mode 100644
index 0000000000..26b5362362
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/T22696_Unsat.stderr
@@ -0,0 +1,4 @@
+
+T22696_Unsat.hs:25:12: error: [GHC-22250]
+    • Boo
+    • When deriving the instance for (Bar Baz2)
diff --git a/testsuite/tests/unsatisfiable/UnsatClassMethods.hs b/testsuite/tests/unsatisfiable/UnsatClassMethods.hs
new file mode 100644
index 0000000000..f0543df7ab
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatClassMethods.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE DataKinds #-}
+
+module UnsatClassMethods where
+
+import GHC.TypeError
+
+-- Easy version
+
+class Cls a where
+  method :: a -> a -> a
+
+instance Unsatisfiable (Text "Not allowed for Bool") => (Cls Bool)
+
+
+-- Trickier version
+
+class C a where
+  {-# MINIMAL (method1, method3, method4) | (method2, method3, method4) | (method1, method2, method4) #-}
+  method1 :: a -> a
+  method1 = method2
+  method2 :: a -> a
+  method2 = method1
+  method3 :: a -> a
+  method3 = method2 . method1
+
+  method4 :: a -> a -> a
+
+instance Unsatisfiable (Text "Not allowed for Int") => (C Int) where
+  method3 = error "not implemented"
diff --git a/testsuite/tests/unsatisfiable/UnsatDefault.hs b/testsuite/tests/unsatisfiable/UnsatDefault.hs
new file mode 100644
index 0000000000..5593fa092e
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatDefault.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+
+module UnsatDefault where
+
+import GHC.TypeError
+
+class C a where
+  method :: a
+  default method :: Unsatisfiable (Text "Please define the method manually. You can try...") => a
+  method = unsatisfiable
+
+
+instance C Int
diff --git a/testsuite/tests/unsatisfiable/UnsatDefault.stderr b/testsuite/tests/unsatisfiable/UnsatDefault.stderr
new file mode 100644
index 0000000000..b4db515840
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatDefault.stderr
@@ -0,0 +1,6 @@
+
+UnsatDefault.hs:14:10: error: [GHC-22250]
+    • Please define the method manually. You can try...
+    • In the expression: UnsatDefault.$dmmethod @(Int)
+      In an equation for ‘method’: method = UnsatDefault.$dmmethod @(Int)
+      In the instance declaration for ‘C Int’
diff --git a/testsuite/tests/unsatisfiable/UnsatDefer.hs b/testsuite/tests/unsatisfiable/UnsatDefer.hs
new file mode 100644
index 0000000000..8169fc2483
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatDefer.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE DataKinds #-}
+
+{-# OPTIONS_GHC -Wno-deferred-type-errors #-}
+
+module Main where
+
+import GHC.TypeError
+
+-- This test makes sure we don't end up with duplication of error messages
+-- when adding Unsatisfiable contexts to classes with superclasses.
+
+-- Test 1: we add an Unsatisfiable context to both the class and its superclass.
+
+class ReflexiveEq a where
+    reflexiveEq :: a -> a -> Bool
+
+type DoubleMsg = Text "Equality is not reflexive on Double"
+instance Unsatisfiable DoubleMsg => ReflexiveEq Double
+
+foo = reflexiveEq 0 (0 :: Double)
+
+main :: IO ()
+main = print foo
diff --git a/testsuite/tests/unsatisfiable/UnsatDefer.stderr b/testsuite/tests/unsatisfiable/UnsatDefer.stderr
new file mode 100644
index 0000000000..fa802c3b3d
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatDefer.stderr
@@ -0,0 +1,5 @@
+UnsatDefer.exe: UnsatDefer.hs:20:7: error: [GHC-22250]
+    • Equality is not reflexive on Double
+    • In the expression: reflexiveEq 0 (0 :: Double)
+      In an equation for ‘foo’: foo = reflexiveEq 0 (0 :: Double)
+(deferred type error)
diff --git a/testsuite/tests/unsatisfiable/UnsatFunDeps.hs b/testsuite/tests/unsatisfiable/UnsatFunDeps.hs
new file mode 100644
index 0000000000..1abf8910af
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatFunDeps.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module UnsatFunDeps where
+
+import GHC.TypeError
+
+class C a b | a -> b
+instance Unsatisfiable (Text "No") => C a b
diff --git a/testsuite/tests/unsatisfiable/UnsatInstance.hs b/testsuite/tests/unsatisfiable/UnsatInstance.hs
new file mode 100644
index 0000000000..c95089cb17
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatInstance.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE DataKinds #-}
+
+module UnsatInstance where
+
+import GHC.TypeError
+
+instance Unsatisfiable (Text "hello")
diff --git a/testsuite/tests/unsatisfiable/UnsatInstance.stderr b/testsuite/tests/unsatisfiable/UnsatInstance.stderr
new file mode 100644
index 0000000000..d79574e73b
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatInstance.stderr
@@ -0,0 +1,4 @@
+
+UnsatInstance.hs:7:10: error: [GHC-97044]
+    • Class ‘Unsatisfiable’ does not support user-specified instances.
+    • In the instance declaration for ‘Unsatisfiable (Text "hello")’
diff --git a/testsuite/tests/unsatisfiable/UnsatPMWarnings.hs b/testsuite/tests/unsatisfiable/UnsatPMWarnings.hs
new file mode 100644
index 0000000000..13a6ee3e6e
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatPMWarnings.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module UnsatPMWarnings where
+
+import Data.Kind
+import Data.Void
+import GHC.TypeError
+
+data MyGADT a where
+  MyInt :: MyGADT Int
+
+type IsBool :: Type -> Constraint
+type family IsBool a where
+  IsBool Bool = ()
+  IsBool a    = Unsatisfiable (Text "Must be Bool")
+
+foo :: IsBool a => MyGADT a -> Void
+foo x = case x of {}
diff --git a/testsuite/tests/unsatisfiable/Unsatisfiable1.hs b/testsuite/tests/unsatisfiable/Unsatisfiable1.hs
new file mode 100644
index 0000000000..357cd296a1
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/Unsatisfiable1.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE DataKinds #-}
+
+module Unsatisfiable1 where
+
+import GHC.TypeError ( Unsatisfiable, unsatisfiable, ErrorMessage(Text) )
+
+type Msg = Text "Cannot call 'uncallable'."
+
+uncallable :: Unsatisfiable Msg => ()
+uncallable = unsatisfiable @Msg
+
+uncallable' :: Unsatisfiable Msg => ()
+uncallable' = uncallable
+
+-------------------------------------
+
+unusual :: Unsatisfiable Msg => Char
+unusual = 42  -- no error
+
+k :: Unsatisfiable (Text "No") => ()
+k = uncallable  -- no error
diff --git a/testsuite/tests/unsatisfiable/Unsatisfiable2.hs b/testsuite/tests/unsatisfiable/Unsatisfiable2.hs
new file mode 100644
index 0000000000..88241a7e46
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/Unsatisfiable2.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE DataKinds #-}
+
+module Unsatisfiable2 where
+
+import GHC.TypeError
+import Data.Type.Bool ( If )
+import Data.Kind
+import Data.Proxy
+
+
+type ExpectTrue x = If x (() :: Constraint) (Unsatisfiable (Text "Input was False!"))
+
+h1 :: ExpectTrue x => proxy x -> ()
+h1 _ = ()
+
+h2 :: If x (() :: Constraint) (Unsatisfiable (Text "Input was False!")) => proxy x -> ()
+h2 _ = ()
+
+eg11 _ = h1 (Proxy @True)
+eg12 p = h1 p
+eg21 _ = h2 (Proxy @True)
+eg22 p = h2 p
diff --git a/testsuite/tests/unsatisfiable/UnsatisfiableFail1.hs b/testsuite/tests/unsatisfiable/UnsatisfiableFail1.hs
new file mode 100644
index 0000000000..70e2b78ac5
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatisfiableFail1.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE DataKinds #-}
+
+module UnsatisfiableFail1 where
+
+import GHC.TypeError
+
+type Msg = Text "Cannot call 'uncallable'."
+
+uncallable :: Unsatisfiable Msg => ()
+uncallable = unsatisfiable @Msg
+
+rejected = uncallable
diff --git a/testsuite/tests/unsatisfiable/UnsatisfiableFail1.stderr b/testsuite/tests/unsatisfiable/UnsatisfiableFail1.stderr
new file mode 100644
index 0000000000..9babaf7aea
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatisfiableFail1.stderr
@@ -0,0 +1,5 @@
+
+UnsatisfiableFail1.hs:12:12: error: [GHC-22250]
+    • Cannot call 'uncallable'.
+    • In the expression: uncallable
+      In an equation for ‘rejected’: rejected = uncallable
diff --git a/testsuite/tests/unsatisfiable/UnsatisfiableFail2.hs b/testsuite/tests/unsatisfiable/UnsatisfiableFail2.hs
new file mode 100644
index 0000000000..07309c25a4
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatisfiableFail2.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE DataKinds #-}
+
+module UnsatisfiableFail2 where
+
+import GHC.TypeError
+import Data.Type.Bool ( If )
+import Data.Kind
+import Data.Proxy
+
+type ExpectTrue x = If x (() :: Constraint) (Unsatisfiable (Text "Input was False!"))
+
+h :: ExpectTrue x => proxy x -> ()
+h _ = ()
+
+eg3 _ = h (Proxy @False)  -- error
diff --git a/testsuite/tests/unsatisfiable/UnsatisfiableFail2.stderr b/testsuite/tests/unsatisfiable/UnsatisfiableFail2.stderr
new file mode 100644
index 0000000000..04c9574f49
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatisfiableFail2.stderr
@@ -0,0 +1,5 @@
+
+UnsatisfiableFail2.hs:15:9: error: [GHC-22250]
+    • Input was False!
+    • In the expression: h (Proxy @False)
+      In an equation for ‘eg3’: eg3 _ = h (Proxy @False)
diff --git a/testsuite/tests/unsatisfiable/UnsatisfiableFail3.hs b/testsuite/tests/unsatisfiable/UnsatisfiableFail3.hs
new file mode 100644
index 0000000000..90befcd5a9
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatisfiableFail3.hs
@@ -0,0 +1,43 @@
+{-# LANGUAGE DataKinds #-}
+
+module UnsatisfiableFail3 where
+
+import GHC.TypeError
+
+
+-- This test makes sure we don't end up with duplication of error messages
+-- when adding Unsatisfiable contexts to classes with superclasses.
+
+-- Test 1: we add an Unsatisfiable context to both the class and its superclass.
+
+class Eq a => ReflexiveEq a where
+    reflexiveEq :: a -> a -> Bool
+    reflexiveEq = (==)
+
+instance Unsatisfiable (Text "Can't compare functions with (==)") => Eq (a -> b) where
+  (==) = unsatisfiable
+
+instance Unsatisfiable (Text "Can't compare functions with reflexiveEq") => ReflexiveEq (a -> b)
+
+type DoubleMsg = Text "Equality is not reflexive on Double"
+instance Unsatisfiable DoubleMsg => ReflexiveEq Double where
+    reflexiveEq = unsatisfiable @DoubleMsg
+
+foo = reflexiveEq 0 (0 :: Double)
+
+bar = reflexiveEq (\ (x :: Int) -> x + 1)
+
+
+-- Test 2: we add an Unsatisfiable context to the class, but not the superclass.
+
+class Eq a => ReflexiveEq' a where
+    reflexiveEq' :: a -> a -> Bool
+    reflexiveEq' = (==)
+
+instance Unsatisfiable (Text "Can't compare functions with reflexiveEq'") => ReflexiveEq' (a -> b)
+instance Unsatisfiable DoubleMsg => ReflexiveEq' Double where
+    reflexiveEq' = unsatisfiable @DoubleMsg
+
+foo' = reflexiveEq' 0 (0 :: Double)
+
+bar' = reflexiveEq' (\ (x :: Int) -> x + 1)
diff --git a/testsuite/tests/unsatisfiable/UnsatisfiableFail3.stderr b/testsuite/tests/unsatisfiable/UnsatisfiableFail3.stderr
new file mode 100644
index 0000000000..5db0db1c04
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatisfiableFail3.stderr
@@ -0,0 +1,21 @@
+
+UnsatisfiableFail3.hs:26:7: error: [GHC-22250]
+    • Equality is not reflexive on Double
+    • In the expression: reflexiveEq 0 (0 :: Double)
+      In an equation for ‘foo’: foo = reflexiveEq 0 (0 :: Double)
+
+UnsatisfiableFail3.hs:28:7: error: [GHC-22250]
+    • Can't compare functions with reflexiveEq
+    • In the expression: reflexiveEq (\ (x :: Int) -> x + 1)
+      In an equation for ‘bar’: bar = reflexiveEq (\ (x :: Int) -> x + 1)
+
+UnsatisfiableFail3.hs:41:8: error: [GHC-22250]
+    • Equality is not reflexive on Double
+    • In the expression: reflexiveEq' 0 (0 :: Double)
+      In an equation for ‘foo'’: foo' = reflexiveEq' 0 (0 :: Double)
+
+UnsatisfiableFail3.hs:43:8: error: [GHC-22250]
+    • Can't compare functions with reflexiveEq'
+    • In the expression: reflexiveEq' (\ (x :: Int) -> x + 1)
+      In an equation for ‘bar'’:
+          bar' = reflexiveEq' (\ (x :: Int) -> x + 1)
diff --git a/testsuite/tests/unsatisfiable/UnsatisfiableFail4.hs b/testsuite/tests/unsatisfiable/UnsatisfiableFail4.hs
new file mode 100644
index 0000000000..070c621d4e
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatisfiableFail4.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE DataKinds, PartialTypeSignatures #-}
+
+module UnsatisfiableFail4 where
+
+import GHC.TypeError
+
+data D = MkD
+
+-- Check that we don't try to solve errors in kinds using Unsatisfiable.
+
+instance Unsatisfiable (Text "msg") => Eq D where
+  _ == _ = let y :: Maybe Maybe
+               y = unsatisfiable
+           in unsatisfiable
+
+instance Unsatisfiable (Text "msg") => Ord D where
+  compare _ _
+    = let y :: _ => Maybe Maybe
+          y = unsatisfiable
+      in unsatisfiable
diff --git a/testsuite/tests/unsatisfiable/UnsatisfiableFail4.stderr b/testsuite/tests/unsatisfiable/UnsatisfiableFail4.stderr
new file mode 100644
index 0000000000..5ce4735a42
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatisfiableFail4.stderr
@@ -0,0 +1,22 @@
+
+UnsatisfiableFail4.hs:12:27: error: [GHC-83865]
+    • Expecting one more argument to ‘Maybe’
+      Expected a type, but ‘Maybe’ has kind ‘* -> *’
+    • In the first argument of ‘Maybe’, namely ‘Maybe’
+      In the type signature: y :: Maybe Maybe
+      In the expression:
+        let
+          y :: Maybe Maybe
+          y = unsatisfiable
+        in unsatisfiable
+
+UnsatisfiableFail4.hs:18:27: error: [GHC-83865]
+    • Expecting one more argument to ‘Maybe’
+      Expected a type, but ‘Maybe’ has kind ‘* -> *’
+    • In the first argument of ‘Maybe’, namely ‘Maybe’
+      In the type signature: y :: _ => Maybe Maybe
+      In the expression:
+        let
+          y :: _ => Maybe Maybe
+          y = unsatisfiable
+        in unsatisfiable
diff --git a/testsuite/tests/unsatisfiable/all.T b/testsuite/tests/unsatisfiable/all.T
new file mode 100644
index 0000000000..2358c7eabc
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/all.T
@@ -0,0 +1,19 @@
+
+test('Unsatisfiable1', normal, compile, [''])
+test('Unsatisfiable2', normal, compile, [''])
+test('UnsatisfiableFail1', normal, compile_fail, [''])
+test('UnsatisfiableFail2', normal, compile_fail, [''])
+test('UnsatisfiableFail3', normal, compile_fail, [''])
+test('UnsatisfiableFail4', normal, compile_fail, [''])
+
+test('UnsatClassMethods', normal, compile, ['-Werror=missing-methods'])
+test('UnsatDefault', normal, compile_fail, [''])
+test('UnsatDefer', exit_code(1), compile_and_run, ['-fdefer-type-errors'])
+test('UnsatFunDeps', normal, compile, [''])
+test('UnsatInstance', normal, compile_fail, [''])
+test('UnsatPMWarnings', normal, compile, ['-Woverlapping-patterns -Wincomplete-patterns'])
+
+test('T11503_Unsat', normal, compile, ['-Woverlapping-patterns -Wincomplete-patterns'])
+test('T14141_Unsat', normal, compile, ['-Woverlapping-patterns -Wincomplete-patterns'])
+test('T14339_Unsat', normal, compile_fail, [''])
+test('T15232_Unsat', normal, compile, ['-Wredundant-constraints'])