[GHC] #9840: Permit empty closed type families

[GHC]

#9840: Permit empty closed type families
-------------------------------------+-------------------------------------
        Reporter:  adamgundry        |                   Owner:
            Type:  feature request   |                  Status:  patch
        Priority:  normal            |               Milestone:
       Component:  Compiler (Type    |                 Version:  7.8.3
  checker)                           |                Keywords:
      Resolution:                    |            Architecture:
Operating System:  Unknown/Multiple  |  Unknown/Multiple
 Type of failure:  None/Unknown      |               Test Case:
      Blocked By:                    |                Blocking:
 Related Tickets:  #8028             |  Differential Revisions:  Phab:D841
-------------------------------------+-------------------------------------

Comment (by adamgundry):

 Thanks, Richard, it's good to try to simplify and bring order to these; I
 hadn't realised what a can of worms I was opening with this feature
 request!

 In the interests of simplicity, is it actually necessary to distinguish
 "matchability" from generativity+injectivity? In particular, if `Any`
 remains non-generative (as at present) then I think the distinction
 collapses. The only case this matters is if we needed to conclude `f ~ Any
 : forall k . k` from `f @k0 ~ Any @k0 : k0`; but do we?

 I think it's perhaps also helpful to divide things up along the lines of
 where their equational theory comes from (considering only nominal roles
 for now):
  * trivial equational theory (`data`, `newtype`, `class`)
  * equational theory specified at declaration site (`type`, closed `type
 family`)
  * special equational theory either built-in or provided via plugin (type
 lits operators, what I want)
  * open equational theory that can be extended anywhere (open `type
 family`, `data family`)

 (The `data family` case is slightly strange, because the equational theory
 can be extended anywhere, but only in a very limited way.)

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