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

1 files changed, 39 insertions, 1 deletions

diff --git a/docs/users_guide/using-warnings.rst b/docs/users_guide/using-warnings.rst
index b72ae4250b..87ddcdabf7 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.