[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:  (none)
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.4.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:                    |
-------------------------------------+-------------------------------------

Comment (by ekmett):

 I'm not particularly wedded to whether I use

 {{{#!hs
 type family Gcd :: Nat -> Nat -> Nat
 }}}

 or

 {{{#!hs
 type family Gcd (n:: Nat) (m::Nat) :: Nat
 }}}

 here.

 The one thing I have in favor (or against, depending on your perspective)
 of the Nat -> Nat -> Nat encoding is that it allows me to preclude the
 user actually defining any ad hoc base cases. Switching to the other
 address the "eta" concern to some extent.

 The main usecase I have sort of mirrors this situation: In the module
 we're in Gcd 3 4 doesn't have a type instance, but that doesn't mean that
 in another context it might not be reducible.

 Say you define the type family in one module:

 {{{#!hs
 module Foo where
 type family Gcd (x :: Nat) (y :: Nat) :: Nat
 }}}

 but refine it later in another:

 {{{#!hs
 module Bar where
 type instance Gcd 3 4 = 1
 }}}

 In Bar, we can perform the reduction, but in Foo we'd get stuck.

 The machinery in Data.Constraint.Nat acts much the same way. We later on
 get into a situation that lets us discharge a stuck constraint.

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