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

 You're right that in the current state of affairs,
 generativity+injectivity imply matchability. But (until Phab:D202 lands)
 generativity also implies injectivity and vice versa. What characteristics
 to track separately is one of the challenges here...

 Suppose units-of-measure annotations were represented by a type headed
 `UnitExp`. `UnitExp` would not be injective, because it would take as
 arguments information about the different units and their powers, and this
 information has a non-trivial equational theory. However, `UnitExp` would,
 assumedly, be generative, in that no non-`UnitExp`s would ever be the same
 as a `UnitExp`. I don't know exactly what this means to the issue above,
 but it's an example of something that's generative but not injective.

 Yes, I completely agree about distinguishing based on equational theory.
 And the `data family` case is quite interesting, I think, because it shows
 how these concepts can be combined in unusual ways: data families are
 generative+injective, but yet have a non-trivial and extensible equational
 theory. If they didn't already exist, I would probably say this point in
 the space didn't exist! So there's something to be learned from them.

 Also, in case I haven't made this clear: these musings probably don't
 belong in this ticket, as I don't think these ideas should hold anything
 up about empty closed type families. But I'm hoping this leads to a
 slightly cleaner solution down the road.

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