[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 adamgundry):

 Replying to [comment:30 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.

 Doesn't an empty closed type family serve the same purpose? The first
 encoding seems simply wrong, because it implies that `Gcd` is injective.

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