Re: [GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?

2 Jun 2018

      #11066: Inacessible branch should be warning - otherwise breaks type soundness?
-------------------------------------+-------------------------------------
        Reporter:  rrnewton          |                Owner:  (none)
            Type:  bug               |               Status:  patch
        Priority:  high              |            Milestone:  8.6.1
       Component:  Compiler          |              Version:  7.10.2
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Incorrect         |  Unknown/Multiple
  warning at compile-time            |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #8128, #8740      |  Differential Rev(s):  Phab:D1454,
       Wiki Page:                    |  Phab:D4744
-------------------------------------+-------------------------------------

Comment (by Ben Gamari <ben@…>):

 In [changeset:"08073e16cf672d8009309e4e55d4566af1ecaff4/ghc"
 08073e16/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="08073e16cf672d8009309e4e55d4566af1ecaff4"
 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
 }}}

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066#comment:48>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler