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

1 files changed, 9 insertions, 3 deletions

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