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

 I guess `Any` isn't really a nullary type family since the `k` argument is
 invisible. So,  the special case that needs to be handled to make this
 work is "all empty type families, regardless of arity". But I think it
 could be done a little more broadly. Playing with the type checker, I
 found that this compiles:

 {{{#!haskell
 {-# language DataKinds #-}
 {-# language TypeFamilies #-}
 module TypeEqualities where
 type family Foo (b :: Bool) :: Bool
 foo :: (Foo 'True ~ 'True, Foo 'True ~ Foo 'False) => Int
 foo = 5
 }}}

 My interpretation of this is that type family applications that do not
 reduce are not considered apart from anything. The behavior that would
 help me is for non-reducing type family applications with constant
 arguments to be considered apart from everything except for themselves.
 Using the above example, `Foo 'True ~ Foo 'True` would typecheck, but `Foo
 'True ~ 'True` and `Foo 'True ~ Foo 'False` would both be rejected. In
 bulleted form, the requirement I listed are:

 * Non-reducing (or stuck)
 * Constant arguments (yes: `Foo 'True`, no: `Foo x`)

 I'm not sure if this is introduces inconsistencies or has any negative
 side effects.

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