[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
      Resolution:                    |             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:                    |
-------------------------------------+-------------------------------------
Description changed by rrnewton:

Old description:

> 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,"

New description:

 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#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler