#16278: Exhaustivity checking GADT with free variables -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): The pattern-match coverage checker is only able to conclude that `LocalShutdown` is an unreachable case if it can reason that `Send` and `Any` are //apart// as types (i.e., they can never possibly unify). For whatever reason, GHC appears to be unable to do this, even though `Any` is a closed type family. For most type families, this makes sense—imagine if you had: {{{#!hs type family F :: Send }}} And tried matching on a value of type `SocketException F`. GHC would be completely justified in declaring `LocalShutdown` to be a reachable case here. Even if the module you're writing didn't have any instances for `F`, due to the open-world assumption, it's possible that you might bring in another module later which declares `type instance F = 'Send`. Closed type families add an interesting wrinkle since they're, well, not open. That is, no one can write `type instance Any = 'Send`, so in theory, it should never be the case that `Any ~ 'Send`. That being said, teaching GHC to reason like this for arbitrary closed type families sounds challenging. Consider the following example: {{{#!hs data Nat = Z | S Nat type family Id (a :: k) :: k where Id x = x type family G (a :: Nat) :: k G Z = () G (S n) = Id (G n) }}} Is `G a` ever equal to `'Send`? The answer is no, but determining this requires some nontrivial reasoning. GHC would need to be able to figure out that `G a` cannot ever reduce to `'Send` by a sort of inductive argument. Moreover, GHC would also need to be aware of how `Id`, a different type family, reduces. Bottom line: while I can sympathize with your desire not to write a case for `LocalException`, actually teaching GHC the smarts to reason about this seems quite tricky. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16278#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler