#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