[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 just had a user reach out to me with this error being caused by an open
 type family that couldn't be reduced in a local setting, but which could
 be reduced elsewhere in the program where the extra type instance
 information was available. The irony here is the 'inaccessible' code was
 matching on a `Refl` to prove the existence of this type instance existed
 to the local context.

 Without this being reduced to a merely overly-enthusiastic warning that he
 can opt out of there is no way to fix the problem at present.

 A concrete example of code this currently cripples is the use of
 `Data.Constraint.Nat`.

 http://hackage.haskell.org/package/constraints-0.9.1/docs/Data-Constraint-
 Nat.html

 The user can't use the machinery provided therein to prove in a local
 context that, say `Gcd 3 6` is `3`.

 {{{#!hs
 {-# LANGUAGE GADTs, TypeApplications, DataKinds #-}
 import Data.Constraint
 import Data.Constraint.Nat
 import Data.Proxy
 import Data.Type.Equality
 import GHC.TypeLits

 foo = case sameNat (Proxy @3) (Proxy @(Gcd 3 6)) \\ gcdNat @3 @6 of
   Just Refl -> ()
 }}}

 The `Refl` match there is being rejected as "Inaccessible code" despite
 the fact that if it was allowed to compile, it'd darn well get accessed!

 (This happens even if we weaken the closed type families in that module to
 open type families.)

 There isn't anything special about `Gcd` here. The same issue arises
 trying to write "userspace" proof terms about the (+) provided by
 GHC.TypeLits as if it were an uninterpreted function.

 This may be a case of this being a closely related error where GHC is
 being too eager to claim code inaccessible when it can't reduce a type
 family further in a local context, but its made into a crippling problem
 rather than a useless warning when combined with this issue.

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