[commit: ghc] wip/tdammers/T11066: Turn "inaccessible code" error into a warning (2d3e275)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : wip/tdammers/T11066
Link       : http://ghc.haskell.org/trac/ghc/changeset/2d3e275816cb8831e8804217854cae2f1299be6f/ghc

>---------------------------------------------------------------

commit 2d3e275816cb8831e8804217854cae2f1299be6f
Author: Tobias Dammers <tdammers at gmail.com>
Date:   Tue May 8 13:54:28 2018 +0200

    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
    
    GHC Trac issue: #11066


>---------------------------------------------------------------

2d3e275816cb8831e8804217854cae2f1299be6f
 compiler/main/DynFlags.hs           |  5 ++++-
 compiler/typecheck/TcErrors.hs      |  2 +-
 docs/users_guide/using-warnings.rst | 38 +++++++++++++++++++++++++++++++++++++
 3 files changed, 43 insertions(+), 2 deletions(-)

diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index 0406d0e..993d393 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -797,6 +797,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
@@ -3755,6 +3756,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,
@@ -4455,7 +4457,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 1172c0a..177b1b3 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -710,7 +710,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 b72ae42..87ddcda 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:
 
@@ -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.