#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