Commit 08073e16 authored by Tobias Dammers's avatar Tobias Dammers 🦈 Committed by Ben Gamari

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
parent 4d800448
......@@ -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
......
......@@ -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)
......
......@@ -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.
......
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
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,
......
......@@ -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,
......
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)
......@@ -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, [''])
......
......@@ -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,
......
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’
......
......@@ -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, [''])
......
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,
......
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:
......
......@@ -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, [''])
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment