[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 andrewthad):

 Thanks for the insights!  I’m not certain that GHC replaces the
 polymorphic type variable with Any  before the exhaustiveness check
 happens. (Although I suspect it does).  If it does, then is  unfortunate
 that we end up doing an apartness check for `'Send` an `Any` when what
 should actually happen is an apartness  check for `'Send` and `forall (s
 :: Send). s` (talking about the second example where I omitted the type
 annotation).

  You make a good argument that teaching the compiler  about apartness
 involving type families in the general case  is difficult  or maybe in
 possible.  But  there are more specific cases where deciding apartness is
 a more tractable problem.  You could consider  only non-recursive type
 families,  only type families that don’t mention other  type families,
 nullary type families,  or the combination of all three (aka Any). From
 what I’ve found in the GHC wiki,  it looks like the apartness check  is an
 approximation anyway.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16278#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler