Inacessible branch should be warning - otherwise breaks type soundness?
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,..."