Turn "inaccessible code" error into a warning

With GADTs, it is possible to write programs such that the type
constraints make some code branches inaccessible.

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

Clearly, the `Just Refl` case cannot ever be reached, because the `Foo1`
and `Foo2` constructors say `t ~ Char` and `u ~ Int`, while the `Refl`
constructor essentially mandates `t ~ u`, and thus `Char ~ Int`.

Previously, GHC would reject such programs entirely; however, in
practice this is too harsh. Accepting such code does little harm, since
attempting to use the "impossible" code will still produce errors down
the chain, while rejecting it means we cannot legally write or generate
such code at all.

Hence, we turn the error into a warning, and provide
`-Winaccessible-code` to control GHC's behavior upon encountering this
situation.

Test Plan: ./validate

Reviewers: bgamari

Reviewed By: bgamari

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #11066

Differential Revision: https://phabricator.haskell.org/D4744

11 files changed, 32 insertions, 41 deletions

diff --git a/testsuite/tests/gadt/T3651.stderr b/testsuite/tests/gadt/T3651.stderr
index 14216eb149..62e3bf16d7 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 40b8a04333..664f9a09df 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 2782b8a1f2..63b3e0e3ef 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 f3d74362a5..29d7fa65a3 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 321d67e9e8..27210312c3 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 5aa67f06c3..33c82bbfd7 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 6abb044c8e..613d92b837 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 86099ea026..3a7f2c415b 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 3700a7656c..8ca5dc9b80 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 63f02dbeb6..77d26041c3 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 b7f37b7507..3344d4c372 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, [''])