[GHC] #16278: Exhaustivity checking GADT with free variables

[GHC]

#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