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

15 files changed, 265 insertions, 75 deletions

diff --git a/compiler/GHC/HsToCore/Pmc/Solver.hs b/compiler/GHC/HsToCore/Pmc/Solver.hs
index e0d5c63698..3caced3468 100644
--- a/compiler/GHC/HsToCore/Pmc/Solver.hs
+++ b/compiler/GHC/HsToCore/Pmc/Solver.hs
@@ -617,6 +617,8 @@ addTyCts nabla@MkNabla{ nabla_ty_st = ty_st } new_ty_cs = do
 
 -- | Add some extra type constraints to the 'TyState'; return 'Nothing' if we
 -- find a contradiction (e.g. @Int ~ Bool@).
+--
+-- See Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver.
 tyOracle :: TyState -> Bag PredType -> DsM (Maybe TyState)
 tyOracle ty_st@(TySt n inert) cts
   | isEmptyBag cts
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
diff --git a/compiler/GHC/Utils/Binary/Typeable.hs b/compiler/GHC/Utils/Binary/Typeable.hs
index b0f4833cbf..7bef358e73 100644
--- a/compiler/GHC/Utils/Binary/Typeable.hs
+++ b/compiler/GHC/Utils/Binary/Typeable.hs
@@ -1,10 +1,9 @@
 {-# LANGUAGE CPP #-}
-{-# LANGUAGE MultiWayIf #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE GADTs #-}
 
 {-# OPTIONS_GHC -O2 -funbox-strict-fields #-}
-{-# OPTIONS_GHC -Wno-orphans #-}
+{-# OPTIONS_GHC -Wno-orphans -Wincomplete-patterns #-}
 #if MIN_VERSION_base(4,16,0)
 #define HAS_TYPELITCHAR
 #endif
@@ -19,7 +18,7 @@ import GHC.Prelude
 
 import GHC.Utils.Binary
 
-import GHC.Exts (TYPE, RuntimeRep(..), VecCount(..), VecElem(..))
+import GHC.Exts (RuntimeRep(..), VecCount(..), VecElem(..))
 #if __GLASGOW_HASKELL__ >= 901
 import GHC.Exts (Levity(Lifted, Unlifted))
 #endif
@@ -49,7 +48,6 @@ getSomeTypeRep bh = do
         1 -> do con <- get bh :: IO TyCon
                 ks <- get bh :: IO [SomeTypeRep]
                 return $ SomeTypeRep $ mkTrCon con ks
-
         2 -> do SomeTypeRep f <- getSomeTypeRep bh
                 SomeTypeRep x <- getSomeTypeRep bh
                 case typeRepKind f of
@@ -68,20 +66,8 @@ getSomeTypeRep bh = do
                        [ "    Applied type: " ++ show f
                        , "    To argument:  " ++ show x
                        ]
-        3 -> do SomeTypeRep arg <- getSomeTypeRep bh
-                SomeTypeRep res <- getSomeTypeRep bh
-                if
-                  | App argkcon _ <- typeRepKind arg
-                  , App reskcon _ <- typeRepKind res
-                  , Just HRefl <- argkcon `eqTypeRep` tYPErep
-                  , Just HRefl <- reskcon `eqTypeRep` tYPErep
-                  -> return $ SomeTypeRep $ Fun arg res
-                  | otherwise -> failure "Kind mismatch" []
         _ -> failure "Invalid SomeTypeRep" []
   where
-    tYPErep :: TypeRep TYPE
-    tYPErep = typeRep
-
     failure description info =
         fail $ unlines $ [ "Binary.getSomeTypeRep: "++description ]
                       ++ map ("    "++) info
@@ -201,10 +187,7 @@ instance Binary TypeLitSort where
           _ -> fail "Binary.putTypeLitSort: invalid tag"
 
 putTypeRep :: BinHandle -> TypeRep a -> IO ()
--- Special handling for TYPE, (->), and RuntimeRep due to recursive kind
--- relations.
--- See Note [Mutually recursive representations of primitive types]
-putTypeRep bh rep
+putTypeRep bh rep -- Handle Type specially since it's so common
   | Just HRefl <- rep `eqTypeRep` (typeRep :: TypeRep Type)
   = put_ bh (0 :: Word8)
 putTypeRep bh (Con' con ks) = do
diff --git a/libraries/base/Data/Typeable/Internal.hs b/libraries/base/Data/Typeable/Internal.hs
index 2a02ec68cb..13853c9301 100644
--- a/libraries/base/Data/Typeable/Internal.hs
+++ b/libraries/base/Data/Typeable/Internal.hs
@@ -95,7 +95,8 @@ import Data.Type.Equality
 import GHC.List ( splitAt, foldl', elem )
 import GHC.Word
 import GHC.Show
-import GHC.TypeLits ( KnownChar, charVal', KnownSymbol, symbolVal', AppendSymbol )
+import GHC.TypeLits ( KnownChar, charVal', KnownSymbol, symbolVal'
+                    , TypeError, ErrorMessage(..) )
 import GHC.TypeNats ( KnownNat, Nat, natVal' )
 import Unsafe.Coerce ( unsafeCoerce )
 
@@ -507,14 +508,16 @@ data AppOrCon (a :: k) where
     IsApp :: forall k k' (f :: k' -> k) (x :: k'). ()
           => TypeRep f %1 -> TypeRep x %1 -> AppOrCon (f x)
     -- See Note [Con evidence]
-    IsCon :: IsApplication a ~ "" => TyCon %1 -> [SomeTypeRep] %1 -> AppOrCon a
+    IsCon :: NotApplication a => TyCon %1 -> [SomeTypeRep] %1 -> AppOrCon a
 
-type family IsApplication (x :: k) :: Symbol where
-  IsApplication (_ _) = "An error message about this unifying with \"\" "
-     `AppendSymbol` "means that you tried to match a TypeRep with Con or "
-     `AppendSymbol` "Con' when the represented type was known to be an "
-     `AppendSymbol` "application."
-  IsApplication _ = ""
+type family NotApplication (x :: k) :: Constraint where
+  NotApplication (f a)
+    = TypeError
+      (     'Text "Cannot match this TypeRep with Con or Con': it is an application:"
+      ':$$: 'Text "  " ':<>: 'ShowType (f a)
+      )
+  NotApplication _
+    = ()
 
 splitApp :: forall k (a :: k). ()
          => TypeRep a
@@ -524,7 +527,7 @@ splitApp (TrApp {trAppFun = f, trAppArg = x}) = IsApp f x
 splitApp rep@(TrFun {trFunArg=a, trFunRes=b}) = IsApp (mkTrApp arr a) b
   where arr = bareArrow rep
 splitApp (TrTyCon{trTyCon = con, trKindVars = kinds})
-  = case unsafeCoerce Refl :: IsApplication a :~: "" of
+  = case unsafeCoerce Refl :: NotApplication a :~: (() :: Constraint) of
       Refl -> IsCon con kinds
 
 -- | Use a 'TypeRep' as 'Typeable' evidence.
@@ -545,7 +548,7 @@ withTypeable rep k = withDict @(TypeRep a) @(Typeable a) rep k
 
 -- | Pattern match on a type constructor
 pattern Con :: forall k (a :: k). ()
-            => IsApplication a ~ "" -- See Note [Con evidence]
+            => NotApplication a -- See Note [Con evidence]
             => TyCon -> TypeRep a
 pattern Con con <- (splitApp -> IsCon con _)
 
@@ -567,7 +570,7 @@ pattern Con con <- (splitApp -> IsCon con _)
 -- @
 --
 pattern Con' :: forall k (a :: k). ()
-             => IsApplication a ~ "" -- See Note [Con evidence]
+             => NotApplication a -- See Note [Con evidence]
              => TyCon -> [SomeTypeRep] -> TypeRep a
 pattern Con' con ks <- (splitApp -> IsCon con ks)
 
@@ -576,30 +579,17 @@ pattern Con' con ks <- (splitApp -> IsCon con ks)
 {-# COMPLETE Fun, App, Con' #-}
 
 {- Note [Con evidence]
-    ~~~~~~~~~~~~~~~~~~~
-
-Matching TypeRep t on Con or Con' fakes up evidence that
-
-  IsApplication t ~ "".
+~~~~~~~~~~~~~~~~~~~~~~
+Matching TypeRep t on Con or Con' fakes up evidence of NotApplication t.
 
 Why should anyone care about the value of strange internal type family?
 Well, almost nobody cares about it, but the pattern checker does!
 For example, suppose we have TypeRep (f x) and we want to get
 TypeRep f and TypeRep x. There is no chance that the Con constructor
 will match, because (f x) is not a constructor, but without the
-IsApplication evidence, omitting it will lead to an incomplete pattern
+NotApplication evidence, omitting it will lead to an incomplete pattern
 warning. With the evidence, the pattern checker will see that
 Con wouldn't typecheck, so everything works out as it should.
-
-Why do we use Symbols? We would really like to use something like
-
-  type family NotApplication (t :: k) :: Constraint where
-    NotApplication (f a) = TypeError ...
-    NotApplication _ = ()
-
-Unfortunately, #11503 means that the pattern checker and type checker
-will fail to actually reject the mistaken patterns. So we describe the
-error in the result type. It's a horrible hack.
 -}
 
 ----------------- Observation ---------------------
diff --git a/testsuite/tests/pmcheck/should_compile/T11503.hs b/testsuite/tests/pmcheck/should_compile/T11503.hs
new file mode 100644
index 0000000000..1309baf91f
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T11503.hs
@@ -0,0 +1,52 @@
+{-# LANGUAGE Haskell2010 #-}
+
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T11503 where
+
+import GHC.TypeLits
+  ( TypeError, 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 = TypeError (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) (TypeError (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/pmcheck/should_compile/T14141.hs b/testsuite/tests/pmcheck/should_compile/T14141.hs
new file mode 100644
index 0000000000..e3df48545c
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T14141.hs
@@ -0,0 +1,42 @@
+{-# LANGUAGE Haskell2010 #-}
+
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T14141 where
+
+import GHC.TypeLits
+  ( TypeError, ErrorMessage(..) )
+import Data.Kind
+  ( Constraint, Type )
+
+-- Example 1: from #14141
+
+data D where
+  MkD :: C => D
+
+type C :: Constraint
+type family C where
+    C = TypeError ('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 = TypeError ('Text "Nope")
+
+data T where
+  A :: F Int  => T
+  B :: F Char => T
+
+exhaustive :: T -> ()
+exhaustive A = ()
+exhaustive B = ()
diff --git a/testsuite/tests/pmcheck/should_compile/T14141.stderr b/testsuite/tests/pmcheck/should_compile/T14141.stderr
new file mode 100644
index 0000000000..32eade4ce0
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T14141.stderr
@@ -0,0 +1,8 @@
+
+T14141.hs:27:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match has inaccessible right hand side
+    In an equation for ‘f’: f MkD = ...
+
+T14141.hs:42:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘exhaustive’: exhaustive B = ...
diff --git a/testsuite/tests/pmcheck/should_compile/T18478.hs b/testsuite/tests/pmcheck/should_compile/T18478.hs
index 6c0fbd9828..5ec331d092 100644
--- a/testsuite/tests/pmcheck/should_compile/T18478.hs
+++ b/testsuite/tests/pmcheck/should_compile/T18478.hs
@@ -505,11 +505,8 @@ type family FailOnNestedBigMapsFound (enabled :: Bool) :: Constraint where
     TypeError ('Text "Nested BigMaps are not allowed")
   FailOnNestedBigMapsFound 'False = ()
 
--- | This is like 'HasNoOp', it raises a more human-readable error
--- when @t@ type is concrete, but GHC cannot make any conclusions
--- from such constraint as it can for 'HasNoOp'.
--- Though, hopefully, it will someday:
--- <https://gitlab.haskell.org/ghc/ghc/issues/11503 #11503>.
+-- | This is like 'HasNoOp', but raises a more human-readable error
+-- when the @t@ type is concrete.
 --
 -- Use this constraint in our eDSL.
 type ForbidOp t = FailOnOperationFound (ContainsOp t)
@@ -523,12 +520,8 @@ type ForbidNestedBigMaps t = FailOnNestedBigMapsFound (ContainsNestedBigMaps t)
 -- | Evidence of that 'HasNoOp' is deducable from 'ForbidOp'.
 forbiddenOpEvi :: forall t. (SingI t, ForbidOp t) :- HasNoOp t
 forbiddenOpEvi = Sub $
-  -- It's not clear now to proof GHC that @HasNoOp t@ is implication of
-  -- @ForbidOp t@, so we use @error@ below and also disable
-  -- "-Wredundant-constraints" extension.
   case checkOpPresence (sing @t) of
     OpAbsent -> Dict
-    OpPresent -> error "impossible"
 
 -- | Reify 'HasNoOp' constraint from 'ForbidOp'.
 --
@@ -544,13 +537,11 @@ forbiddenBigMapEvi :: forall t. (SingI t, ForbidBigMap t) :- HasNoBigMap t
 forbiddenBigMapEvi = Sub $
   case checkBigMapPresence (sing @t) of
     BigMapAbsent -> Dict
-    BigMapPresent -> error "impossible"
 
 forbiddenNestedBigMapsEvi :: forall t. (SingI t, ForbidNestedBigMaps t) :- HasNoNestedBigMaps t
 forbiddenNestedBigMapsEvi = Sub $
   case checkNestedBigMapsPresence (sing @t) of
     NestedBigMapsAbsent -> Dict
-    NestedBigMapsPresent -> error "impossible"
 
 forbiddenBigMap
   :: forall t a.
@@ -572,7 +563,6 @@ forbiddenContractTypeEvi
 forbiddenContractTypeEvi = Sub $
   case checkContractTypePresence (sing @t) of
     ContractAbsent -> Dict
-    ContractPresent -> error "impossible"
 
 -- | Reify 'HasNoContract' constraint from 'ForbidContract'.
 forbiddenContractType
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index 3880ca0756..c732ef5691 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -50,12 +50,16 @@ test('T11822', collect_compiler_stats('bytes allocated',10), compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T11195', collect_compiler_stats('bytes allocated',10), compile,
      ['-package ghc -fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M2G -RTS'])
+test('T11503', [], compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T11984', normal, compile,
     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T14086', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T14098', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T14141', [], compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T14813', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T14899', normal, compile,
diff --git a/testsuite/tests/typecheck/should_compile/TypeRepCon.hs b/testsuite/tests/typecheck/should_compile/TypeRepCon.hs
new file mode 100644
index 0000000000..37e9bfc00b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/TypeRepCon.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE PatternSynonyms #-}
+
+module TypeRepCon1 where
+
+import Type.Reflection
+  ( TypeRep, pattern Con )
+
+-- Simple test of the 'NotApplication' custom type error
+-- in Data.Typeable.Internal.
+
+isApp :: TypeRep (f a) -> Bool
+isApp (Con _) = False -- Should warn about redundant pattern (insoluble Given)
+isApp _       = True
diff --git a/testsuite/tests/typecheck/should_compile/TypeRepCon.stderr b/testsuite/tests/typecheck/should_compile/TypeRepCon.stderr
new file mode 100644
index 0000000000..4bd41fcf3a
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/TypeRepCon.stderr
@@ -0,0 +1,4 @@
+
+TypeRepCon.hs:12:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match has inaccessible right hand side
+    In an equation for ‘isApp’: isApp (Con _) = ...
\ No newline at end of file
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index a275d5196a..83688dbb9b 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -793,3 +793,5 @@ test('T18481a', normal, compile, [''])
 test('T19775', normal, compile, [''])
 test('T17817b', normal, compile, [''])
 test('T20033', normal, compile, [''])
+
+test('TypeRepCon', normal, compile, ['-Woverlapping-patterns'])