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

5 files changed, 23 insertions, 27 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, [''])