Turn "inaccessible code" error into a warning
authorTobias Dammers <tdammers@gmail.com>
Sun, 3 Jun 2018 03:23:22 +0000 (23:23 -0400)
committerBen Gamari <ben@smart-cactus.org>
Sun, 3 Jun 2018 03:23:39 +0000 (23:23 -0400)
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

14 files changed:
compiler/main/DynFlags.hs
compiler/typecheck/TcErrors.hs
docs/users_guide/using-warnings.rst
testsuite/tests/gadt/T3651.stderr
testsuite/tests/gadt/T7293.stderr
testsuite/tests/gadt/T7294.stderr
testsuite/tests/gadt/T7558.stderr
testsuite/tests/gadt/all.T
testsuite/tests/ghci/scripts/Defer02.stderr
testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr
testsuite/tests/typecheck/should_fail/all.T
testsuite/tests/typecheck/should_fail/tcfail167.stderr
testsuite/tests/typecheck/should_run/Typeable1.stderr
testsuite/tests/typecheck/should_run/all.T

index 558fa99..b9141f9 100644 (file)
@@ -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
index 1df6cd6..fb60ba3 100644 (file)
@@ -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)
index b72ae42..87ddcda 100644 (file)
@@ -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.
index 14216eb..62e3bf1 100644 (file)
@@ -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
index 40b8a04..664f9a0 100644 (file)
@@ -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,
index 2782b8a..63b3e0e 100644 (file)
@@ -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,
index f3d7436..29d7fa6 100644 (file)
@@ -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)
index 321d67e..2721031 100644 (file)
@@ -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, [''])
index 5aa67f0..33c82bb 100644 (file)
@@ -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,
index 6abb044..613d92b 100644 (file)
@@ -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’
index 86099ea..3a7f2c4 100644 (file)
@@ -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, [''])
index 3700a76..8ca5dc9 100644 (file)
@@ -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,
index 63f02db..77d2604 100644 (file)
@@ -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:
index b7f37b7..3344d4c 100755 (executable)
@@ -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, [''])