Turn "inaccessible code" error into a warning
ClosedPublic

Authored by tdammers on May 28 2018, 2:48 AM.

Details

Summary

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

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Lint
Automatic diff as part of commit; lint not applicable.
Unit
Automatic diff as part of commit; unit tests not applicable.
tdammers created this revision.May 28 2018, 2:48 AM
tdammers updated this revision to Diff 16580.EditedMay 30 2018, 9:45 AM

Updated to reflect changed output in tests, and adding -Werror to tests that should fail.

bgamari accepted this revision.Jun 2 2018, 5:52 PM

Looks good to me. Thanks!

This revision is now accepted and ready to land.Jun 2 2018, 5:52 PM
This revision was automatically updated to reflect the committed changes.