diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index 558fa9963c5a3e8eaa1d6ef6083279c0bc2123b7..b9141f9e8713ea55f39130c48121e87f5e800136 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -803,6 +803,7 @@ data WarningFlag =
    | Opt_WarnMissingHomeModules           -- Since 8.2
    | Opt_WarnPartialFields                -- Since 8.4
    | Opt_WarnMissingExportList
+   | Opt_WarnInaccessibleCode
    deriving (Eq, Show, Enum)
 
 data Language = Haskell98 | Haskell2010
@@ -3764,6 +3765,7 @@ wWarningFlagsDeps = [
   flagSpec "redundant-constraints"       Opt_WarnRedundantConstraints,
   flagSpec "duplicate-exports"           Opt_WarnDuplicateExports,
   flagSpec "hi-shadowing"                Opt_WarnHiShadows,
+  flagSpec "inaccessible-code"           Opt_WarnInaccessibleCode,
   flagSpec "implicit-prelude"            Opt_WarnImplicitPrelude,
   flagSpec "incomplete-patterns"         Opt_WarnIncompletePatterns,
   flagSpec "incomplete-record-updates"   Opt_WarnIncompletePatternsRecUpd,
@@ -4496,7 +4498,8 @@ standardWarnings -- see Note [Documenting warning flags]
         Opt_WarnUnsupportedLlvmVersion,
         Opt_WarnTabs,
         Opt_WarnUnrecognisedWarningFlags,
-        Opt_WarnSimplifiableClassConstraints
+        Opt_WarnSimplifiableClassConstraints,
+        Opt_WarnInaccessibleCode
       ]
 
 -- | Things you get with -W
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index 1df6cd6750baafd1f6b85d87a7b763699a62125f..fb60ba350bca78d5dc983b0bb01fe87f22835488 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -706,7 +706,7 @@ mkGivenErrorReporter implic ctxt cts
                              Nothing ty1 ty2
 
        ; traceTc "mkGivenErrorReporter" (ppr ct)
-       ; maybeReportError ctxt err }
+       ; reportWarning (Reason Opt_WarnInaccessibleCode) err }
   where
     (ct : _ )  = cts    -- Never empty
     (ty1, ty2) = getEqPredTys (ctPred ct)
diff --git a/docs/users_guide/using-warnings.rst b/docs/users_guide/using-warnings.rst
index b72ae4250bf1bf2c74e25604c08437c170ee09f5..87ddcdabf76df7c4ce86a799eca63d2fe7d380c2 100644
--- a/docs/users_guide/using-warnings.rst
+++ b/docs/users_guide/using-warnings.rst
@@ -33,6 +33,7 @@ generally likely to indicate bugs in your program. These are:
     * :ghc-flag:`-Wunsupported-llvm-version`
     * :ghc-flag:`-Wtabs`
     * :ghc-flag:`-Wunrecognised-warning-flags`
+    * :ghc-flag:`-Winaccessible-code`
 
 The following flags are simple ways to select standard "packages" of warnings:
 
@@ -685,7 +686,7 @@ of ``-W(no-)*``.
     Similar warnings are given for a redundant constraint in an instance
     declaration.
 
-    When turning on, you can suppress it on a per-module basis with 
+    When turning on, you can suppress it on a per-module basis with
     :ghc-flag:`-Wno-redundant-constraints <-Wredundant-constraints>`.
     Occasionally you may specifically want a function to have a more
     constrained signature than necessary, perhaps to leave yourself
@@ -1088,6 +1089,43 @@ of ``-W(no-)*``.
     second pattern overlaps it. More often than not, redundant patterns
     is a programmer mistake/error, so this option is enabled by default.
 
+.. ghc-flag:: -Winaccessible-code
+    :shortdesc: warn about inaccessible code
+    :type: dynamic
+    :reverse: -Wno-inaccessible-code
+    :category:
+
+    .. index::
+       single: inaccessible code, warning
+       single: inaccessible
+
+    By default, the compiler will warn you if types make a branch inaccessible.
+    This generally requires GADTs or similar extensions.
+
+    Take, for example, the following program ::
+
+        {-# LANGUAGE GADTs #-}
+
+        data Foo a where
+         Foo1 :: Foo Char
+         Foo2 :: Foo Int
+
+        data TyEquality a b where
+                Refl :: TyEquality a a
+
+        checkTEQ :: Foo t -> Foo u -> Maybe (TyEquality t u)
+        checkTEQ x y = error "unimportant"
+
+        step2 :: Bool
+        step2 = case checkTEQ Foo1 Foo2 of
+                 Just Refl -> True -- Inaccessible code
+                 Nothing -> False
+
+    The ``Just Refl`` case in ``step2`` is inaccessible, because in order for
+    ``checkTEQ`` to be able to produce a ``Just``, ``t ~ u`` must hold, but
+    since we're passing ``Foo1`` and ``Foo2`` here, it follows that ``t ~
+    Char``, and ``u ~ Int``, and thus ``t ~ u`` cannot hold.
+
 .. ghc-flag:: -Wsimplifiable-class-constraints
     :shortdesc: 2arn about class constraints in a type signature that can
         be simplified using a top-level instance declaration.
diff --git a/testsuite/tests/gadt/T3651.stderr b/testsuite/tests/gadt/T3651.stderr
index 14216eb1499b75dfbd8bb56b6d2b31716bc90cec..62e3bf16d7057c39b8f7cb3131764e7b1b049abd 100644
--- a/testsuite/tests/gadt/T3651.stderr
+++ b/testsuite/tests/gadt/T3651.stderr
@@ -1,21 +1,14 @@
 
-T3651.hs:11:11: error:
-    • Couldn't match type ‘Bool’ with ‘()’
-      Inaccessible code in
-        a pattern with constructor: U :: Z (), in an equation for ‘unsafe1’
-    • In the pattern: U
+T3651.hs:11:15: error:
+    • Couldn't match type ‘()’ with ‘Bool’
+      Expected type: a
+        Actual type: ()
+    • In the expression: ()
       In an equation for ‘unsafe1’: unsafe1 B U = ()
 
-T3651.hs:14:11: error:
-    • Couldn't match type ‘Bool’ with ‘()’
-      Inaccessible code in
-        a pattern with constructor: U :: Z (), in an equation for ‘unsafe2’
-    • In the pattern: U
+T3651.hs:14:15: error:
+    • Couldn't match type ‘()’ with ‘Bool’
+      Expected type: a
+        Actual type: ()
+    • In the expression: ()
       In an equation for ‘unsafe2’: unsafe2 B U = ()
-
-T3651.hs:17:11: error:
-    • Couldn't match type ‘Bool’ with ‘()’
-      Inaccessible code in
-        a pattern with constructor: U :: Z (), in an equation for ‘unsafe3’
-    • In the pattern: U
-      In an equation for ‘unsafe3’: unsafe3 B U = True
diff --git a/testsuite/tests/gadt/T7293.stderr b/testsuite/tests/gadt/T7293.stderr
index 40b8a04333384a5f60ae70ae1cb54c38d43e5e77..664f9a09dfcc6f1c108920769ca26d2e91c1a75b 100644
--- a/testsuite/tests/gadt/T7293.stderr
+++ b/testsuite/tests/gadt/T7293.stderr
@@ -1,5 +1,9 @@
 
-T7293.hs:24:5: error:
+T7293.hs:24:1: error: [-Woverlapping-patterns (in -Wdefault), -Werror=overlapping-patterns]
+    Pattern match is redundant
+    In an equation for ‘nth’: nth Nil _ = ...
+
+T7293.hs:24:5: error: [-Winaccessible-code (in -Wdefault), -Werror=inaccessible-code]
     • Couldn't match type ‘'True’ with ‘'False’
       Inaccessible code in
         a pattern with constructor: Nil :: forall a. Vec a 'Zero,
diff --git a/testsuite/tests/gadt/T7294.stderr b/testsuite/tests/gadt/T7294.stderr
index 2782b8a1f246d4518b18c0142162a2dbc37c4e88..63b3e0e3ef6be60d8c4d43cd8a0e59d47b6c9979 100644
--- a/testsuite/tests/gadt/T7294.stderr
+++ b/testsuite/tests/gadt/T7294.stderr
@@ -3,7 +3,7 @@ T7294.hs:25:1: warning: [-Woverlapping-patterns (in -Wdefault)]
     Pattern match is redundant
     In an equation for ‘nth’: nth Nil _ = ...
 
-T7294.hs:25:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
+T7294.hs:25:5: warning: [-Winaccessible-code (in -Wdefault)]
     • Couldn't match type ‘'True’ with ‘'False’
       Inaccessible code in
         a pattern with constructor: Nil :: forall a. Vec a 'Zero,
diff --git a/testsuite/tests/gadt/T7558.stderr b/testsuite/tests/gadt/T7558.stderr
index f3d74362a59ffcdee1410382fb26c953b0b56b44..29d7fa65a3cb03ebd11396e33d02141ec506f0d7 100644
--- a/testsuite/tests/gadt/T7558.stderr
+++ b/testsuite/tests/gadt/T7558.stderr
@@ -1,11 +1,10 @@
 
-T7558.hs:8:4: error:
+T7558.hs:8:18: error:
     • Occurs check: cannot construct the infinite type: a ~ Maybe a
-      Inaccessible code in
-        a pattern with constructor:
-          MkT :: forall a b. (a ~ Maybe b) => a -> Maybe b -> T a b,
-        in an equation for ‘f’
-    • In the pattern: MkT x y
-      In an equation for ‘f’: f (MkT x y) = [x, y] `seq` True
+    • In the expression: y
+      In the first argument of ‘seq’, namely ‘[x, y]’
+      In the expression: [x, y] `seq` True
     • Relevant bindings include
+        y :: Maybe a (bound at T7558.hs:8:10)
+        x :: a (bound at T7558.hs:8:8)
         f :: T a a -> Bool (bound at T7558.hs:8:1)
diff --git a/testsuite/tests/gadt/all.T b/testsuite/tests/gadt/all.T
index 321d67e9e8f5cef53c67248a7311ce9de4eeeee1..27210312c37af24a653fb383b6043de1c38c8fab 100644
--- a/testsuite/tests/gadt/all.T
+++ b/testsuite/tests/gadt/all.T
@@ -105,7 +105,7 @@ test('T5424', [], multimod_compile, ['T5424', '-v0 -O0'])
 
 test('FloatEq', normal, compile, [''])
 test('T7205', normal, compile, [''])
-test('T7293', normal, compile_fail, [''])
+test('T7293', normal, compile_fail, ['-Werror'])
 test('T7294', normal, compile, [''])
 test('T7321', [], run_command, ['$MAKE -s --no-print-directory T7321'])
 test('T7974', normal, compile, [''])
diff --git a/testsuite/tests/ghci/scripts/Defer02.stderr b/testsuite/tests/ghci/scripts/Defer02.stderr
index 5aa67f06c35747c6f22601846cf23b3328d93b3b..33c82bbfd76a9a3bfd3cc906c1a2239f64aebfeb 100644
--- a/testsuite/tests/ghci/scripts/Defer02.stderr
+++ b/testsuite/tests/ghci/scripts/Defer02.stderr
@@ -21,7 +21,7 @@ Defer01.hs:25:1: warning: [-Woverlapping-patterns (in -Wdefault)]
     Pattern match has inaccessible right hand side
     In an equation for ‘c’: c (C2 x) = ...
 
-Defer01.hs:25:4: warning: [-Wdeferred-type-errors (in -Wdefault)]
+Defer01.hs:25:4: warning: [-Winaccessible-code (in -Wdefault)]
     • Couldn't match type ‘Int’ with ‘Bool’
       Inaccessible code in
         a pattern with constructor: C2 :: Bool -> C Bool,
diff --git a/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr b/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr
index 6abb044c8ea8e60fb7ed2a5c938efabcd877b9c6..613d92b837cfa7d38390f9da2431055332bb6180 100644
--- a/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr
+++ b/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr
@@ -1,13 +1,4 @@
 
-FrozenErrorTests.hs:12:12: error:
-    • Couldn't match type ‘Int’ with ‘Bool’
-      Inaccessible code in
-        a pattern with constructor: MkT3 :: forall a. (a ~ Bool) => T a,
-        in a case alternative
-    • In the pattern: MkT3
-      In a case alternative: MkT3 -> ()
-      In the expression: case x of { MkT3 -> () }
-
 FrozenErrorTests.hs:26:9: error:
     • Occurs check: cannot construct the infinite type: a ~ [a]
         arising from a use of ‘goo1’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 86099ea026d94d80658734f2b104c026edd9ceb5..3a7f2c415b3a9a1a13a5c672457bc1225fbebc2d 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -149,7 +149,7 @@ test('tcfail162', normal, compile_fail, [''])
 test('tcfail164', normal, compile_fail, [''])
 test('tcfail165', normal, compile_fail, [''])
 test('tcfail166', normal, compile_fail, [''])
-test('tcfail167', normal, compile_fail, [''])
+test('tcfail167', normal, compile_fail, ['-Werror'])
 test('tcfail168', normal, compile_fail, [''])
 test('tcfail169', normal, compile_fail, [''])
 test('tcfail170', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tcfail167.stderr b/testsuite/tests/typecheck/should_fail/tcfail167.stderr
index 3700a7656cfbbd436857f844b5f967661ce831f5..8ca5dc9b804760591b3070f58f95dfe89736de90 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail167.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail167.stderr
@@ -1,5 +1,9 @@
 
-tcfail167.hs:14:14: error:
+tcfail167.hs:14:1: error: [-Woverlapping-patterns (in -Wdefault), -Werror=overlapping-patterns]
+    Pattern match is redundant
+    In an equation for ‘inaccessible’: inaccessible C2 = ...
+
+tcfail167.hs:14:14: error: [-Winaccessible-code (in -Wdefault), -Werror=inaccessible-code]
     • Couldn't match type ‘Char’ with ‘Float’
       Inaccessible code in
         a pattern with constructor: C2 :: T Float,
diff --git a/testsuite/tests/typecheck/should_run/Typeable1.stderr b/testsuite/tests/typecheck/should_run/Typeable1.stderr
index 63f02dbeb6070c41f3298e39fa66d52aad434148..77d26041c3cf6a7c37261bda109383dfd2987cef 100644
--- a/testsuite/tests/typecheck/should_run/Typeable1.stderr
+++ b/testsuite/tests/typecheck/should_run/Typeable1.stderr
@@ -1,5 +1,5 @@
 
-Typeable1.hs:22:5: error:
+Typeable1.hs:22:5: error: [-Winaccessible-code (in -Wdefault), -Werror=inaccessible-code]
     • Couldn't match type ‘ComposeK’ with ‘a3 b3’
       Inaccessible code in
         a pattern with pattern synonym:
diff --git a/testsuite/tests/typecheck/should_run/all.T b/testsuite/tests/typecheck/should_run/all.T
index b7f37b7507cebe530f94dd0a7b46585ab5ab20ae..3344d4c372f2d55b2182d90dee67a59115cc1e22 100755
--- a/testsuite/tests/typecheck/should_run/all.T
+++ b/testsuite/tests/typecheck/should_run/all.T
@@ -125,7 +125,7 @@ test('EtaExpandLevPoly', [ omit_ways(['ghci'])
 			 ], compile_and_run, [''])
 
 test('TestTypeableBinary', normal, compile_and_run, [''])
-test('Typeable1', normal, compile_fail, [''])
+test('Typeable1', normal, compile_fail, ['-Werror'])
 test('TypeableEq', normal, compile_and_run, [''])
 test('T13435', normal, compile_and_run, [''])
 test('T11715', exit_code(1), compile_and_run, [''])