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

[GHC]

#11066: Inacessible branch should be warning - otherwise breaks type soundness?
-------------------------------------+-------------------------------------
           Reporter:  rrnewton       |             Owner:
               Type:  bug            |            Status:  new
           Priority:  high           |         Milestone:
          Component:  Compiler       |           Version:  7.10.2
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 GHC 7.10.2 reports inaccessible branches as a type error, and I think
 this is really a bug.

 First, the implicit thinking seems to be "why would a user want to
 write inaccessible cases, they'd be crazy!".  But that only applies to
 human-written code.  Program generators can have a great deal of
 trouble avoiding this error, unless they replicate the GHC type
 checker to predict the problem and prune branches.  (That's why we are
 hitting this error and are stuck.)

 Second, it seems like this is a problem for type soundness.  See the
 attached program where "step1" typechecks but "step2" does not.  And yet,
 the operational semantics should allow step1 to reduce to step2.

 Indeed, in the "GADTs meet their match" paper it seems like the intent
 was to warn for these inaccessible cases, not error.  For example, the
 paper contains the language:

   "If we warn that a right-hand side of a non-redundant clause is
 inaccessible,"

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