#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 simonpj): It certainly sounds wrong for GHC to reject a branch as inaccessible (i.e. definitely cannot be executed) when it actually ''can'' be executed. Can you make an example that doesn't depend on relatively sophisticated package? I tried {{{ {-# LANGUAGE FlexibleContexts, TypeFamilies, TypeApplications #-} module T11066 where import Data.Typeable type family F a foo:: Typeable (F Bool) => () foo = case eqT @Int @(F Bool) of Just Refl -> () _ -> () }}} thinking that GHC might claim that `F Bool ~ Int` is inaccesible; but it's accepted just fine. You do not say which version of the compiler you are using. A milder version of the problem is if the branch really is inaccessible, but you want to accept it anyway for some reason -- e.g. it's produced by `deriving`. But that is not what you are bothered about here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler