Detect TypeError when checking for insolubility

We detect insoluble Givens by making getInertInsols
take into account TypeError constraints, on top of insoluble equalities
such as Int ~ Bool (which it already took into account).

This allows pattern matches with insoluble contexts to be reported
as redundant (tyOracle calls tcCheckGivens which calls getInertInsols).

As a bonus, we get to remove a workaround in Data.Typeable.Internal:
we can directly use a NotApplication type family, as opposed to
needing to cook up an insoluble equality constraint.

Fixes #11503 #14141 #16377 #20180

4 files changed, 116 insertions, 16 deletions

diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index dc95a6a81d..51ab0fca2a 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -583,7 +583,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics
     -- report1: ones that should *not* be suppressed by
     --          an insoluble somewhere else in the tree
     -- It's crucial that anything that is considered insoluble
-    -- (see GHC.Tc.Utils.insolubleCt) is caught here, otherwise
+    -- (see GHC.Tc.Utils.insolublWantedCt) is caught here, otherwise
     -- we might suppress its error message, and proceed on past
     -- type checking to get a Lint error later
     report1 = [ ("custom_error", unblocked is_user_type_error, True,  mkUserTypeErrorReporter)
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index f645e4d49c..e2ea2f59de 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -806,9 +806,74 @@ simplifyDefault theta
        ; return (isEmptyWC unsolved) }
 
 ------------------
+{- Note [Pattern match warnings with insoluble Givens]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A pattern match on a GADT can introduce new type-level information, which needs
+to be analysed in order to get the expected pattern match warnings.
+
+For example:
+
+> type IsBool :: Type -> Constraint
+> type family IsBool a where
+>   IsBool Bool = ()
+>   IsBool b    = b ~ Bool
+>
+> data T a where
+>   MkTInt  :: Int -> T Int
+>   MkTBool :: IsBool b => b -> T b
+>
+> f :: T Int -> Int
+> f (MkTInt i) = i
+
+The pattern matching performed by `f` is complete: we can't ever call
+`f (MkTBool b)`, as type-checking that application would require producing
+evidence for `Int ~ Bool`, which can't be done.
+
+The pattern match checker uses `tcCheckGivens` to accumulate all the Given
+constraints, and relies on `tcCheckGivens` to return Nothing if the
+Givens become insoluble.   `tcCheckGivens` in turn relies on `insolubleCt`
+to identify these insoluble constraints.  So the precise definition of
+`insolubleCt` has a big effect on pattern match overlap warnings.
+
+To detect this situation, we check whether there are any insoluble Given
+constraints. In the example above, the insoluble constraint was an
+equality constraint, but it is also important to detect custom type errors:
+
+> type NotInt :: Type -> Constraint
+> type family NotInt a where
+>   NotInt Int = TypeError (Text "That's Int, silly.")
+>   NotInt _   = ()
+>
+> data R a where
+>   MkT1 :: a -> R a
+>   MkT2 :: NotInt a => R a
+>
+> foo :: R Int -> Int
+> foo (MkT1 x) = x
+
+To see that we can't call `foo (MkT2)`, we must detect that `NotInt Int` is insoluble
+because it is a custom type error.
+Failing to do so proved quite inconvenient for users, as evidence by the
+tickets #11503 #14141 #16377 #20180.
+Test cases: T11503, T14141.
+
+Examples of constraints that tcCheckGivens considers insoluble:
+  - Int ~ Bool,
+  - Coercible Float Word,
+  - TypeError msg.
+
+Non-examples:
+  - constraints which we know aren't satisfied,
+    e.g. Show (Int -> Int) when no such instance is in scope,
+  - Eq (TypeError msg),
+  - C (Int ~ Bool), with @class C (c :: Constraint)@.
+-}
+
 tcCheckGivens :: InertSet -> Bag EvVar -> TcM (Maybe InertSet)
 -- ^ Return (Just new_inerts) if the Givens are satisfiable, Nothing if definitely
--- contradictory
+-- contradictory.
+--
+-- See Note [Pattern match warnings with insoluble Givens] above.
 tcCheckGivens inerts given_ids = do
   (sat, new_inerts) <- runTcSInerts inerts $ do
     traceTcS "checkGivens {" (ppr inerts <+> ppr given_ids)
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index 5796e2bd6a..b957b0ed0c 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -824,10 +824,16 @@ getInnermostGivenEqLevel = do { inert <- getInertCans
                               ; return (inert_given_eq_lvl inert) }
 
 getInertInsols :: TcS Cts
--- Returns insoluble equality constraints
--- specifically including Givens
+-- Returns insoluble equality constraints and TypeError constraints,
+-- specifically including Givens.
+--
+-- 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.
+--
+-- See Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver.
 getInertInsols = do { inert <- getInertCans
-                    ; return (filterBag insolubleEqCt (inert_irreds inert)) }
+                    ; return $ filterBag insolubleCt (inert_irreds inert) }
 
 getInertGivens :: TcS [Ct]
 -- Returns the Given constraints in the inert set
diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index 0567211bfb..7c7b2df772 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -43,7 +43,7 @@ module GHC.Tc.Types.Constraint (
         isSolvedWC, andWC, unionsWC, mkSimpleWC, mkImplicWC,
         addInsols, dropMisleading, addSimples, addImplics, addHoles,
         tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples,
-        tyCoVarsOfWCList, insolubleCt, insolubleEqCt,
+        tyCoVarsOfWCList, insolubleWantedCt, insolubleEqCt, insolubleCt,
         isDroppableCt, insolubleImplic,
         arisesFromGivens,
 
@@ -1129,7 +1129,7 @@ dropMisleading :: WantedConstraints -> WantedConstraints
 --   for why this function is so strange, treating the 'simples'
 --   and the implications differently.  Sigh.
 dropMisleading (WC { wc_simple = simples, wc_impl = implics, wc_holes = holes })
-  = WC { wc_simple = filterBag insolubleCt simples
+  = WC { wc_simple = filterBag insolubleWantedCt simples
        , wc_impl   = mapBag drop_implic implics
        , wc_holes  = filterBag isOutOfScopeHole holes }
   where
@@ -1158,19 +1158,20 @@ insolubleImplic ic = isInsolubleStatus (ic_status ic)
 
 insolubleWC :: WantedConstraints -> Bool
 insolubleWC (WC { wc_impl = implics, wc_simple = simples, wc_holes = holes })
-  =  anyBag insolubleCt simples
+  =  anyBag insolubleWantedCt simples
   || anyBag insolubleImplic implics
   || anyBag isOutOfScopeHole holes  -- See Note [Insoluble holes]
 
-insolubleCt :: Ct -> Bool
+insolubleWantedCt :: Ct -> Bool
 -- Definitely insoluble, in particular /excluding/ type-hole constraints
--- Namely: a) an equality constraint
---         b) that is insoluble
---         c) and does not arise from a Given
-insolubleCt ct
-  | not (insolubleEqCt ct) = False
-  | arisesFromGivens ct    = False              -- See Note [Given insolubles]
-  | otherwise              = True
+-- Namely:
+--   a) an insoluble constraint as per 'insolubleCt', i.e. either
+--        - an insoluble equality constraint (e.g. Int ~ Bool), or
+--        - a custom type error constraint, TypeError msg :: Constraint
+--   b) that does not arise from a Given
+--
+-- See Note [Given insolubles].
+insolubleWantedCt ct = insolubleCt ct && not (arisesFromGivens ct)
 
 insolubleEqCt :: Ct -> Bool
 -- Returns True of /equality/ constraints
@@ -1190,6 +1191,34 @@ insolubleEqCt :: Ct -> Bool
 insolubleEqCt (CIrredCan { cc_reason = reason }) = isInsolubleReason reason
 insolubleEqCt _                                  = False
 
+-- | Returns True of equality constraints that are definitely insoluble,
+-- as well as TypeError constraints.
+-- Can return 'True' for Given constraints, unlike 'insolubleWantedCt'.
+--
+-- This function is critical for accurate pattern-match overlap warnings.
+-- See Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver
+--
+-- Note that this does not traverse through the constraint to find
+-- 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'
+  -- for constraints that are definitely insoluble.
+  --
+  -- 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]
 isOutOfScopeHole :: Hole -> Bool