• Tobias Dammers's avatar
    Turn "inaccessible code" error into a warning · 08073e16
    Tobias Dammers authored
    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
    Test Plan: ./validate
    Reviewers: bgamari
    Reviewed By: bgamari
    Subscribers: rwbarton, thomie, carter
    GHC Trac Issues: #11066
    Differential Revision: https://phabricator.haskell.org/D4744
TcErrors.hs 124 KB