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

 > What Adam really wants here is the ability to create new type-level
 constants at arbitrary kind.

 Is it? Open datakinds would be nice, but `Symbol` and `*` already give us
 quite a lot of wriggle room.

 My real problem is more in creating type-level function symbols without
 any equational theory, which (with Phab:D841 at least) goes like this:

 {{{
 data Unit
 type family Mul (u :: Unit) (v :: Unit) :: Unit where
 }}}

 In particular, to avoid conflict with plugin-generated axioms, `Mul`

  * must be saturated;

  * is not injective, so `Mul u v ~ Mul v u` does not imply `u ~ v`;

  * cannot be used in patterns;

  * cannot be given any instances by the user (this is the only condition
 not satisfied by an open type family).

 I don't quite understand how your proposal would work for this case. What
 does it mean to declare `Weird` as a constant in a closed kind? Note that
 giving `Mul` kind `Unit -> Unit -> Unit` is no good, because that means it
 is injective (at least unless we add another flavour of type-level
 function space). In any case, adding a whole new declaration form feels
 like rather more work than my needs justify.

 Phab:D841 is a relatively simple change (deleting 7 lines of code, in its
 original incarnation before distinguishing abstract/empty CTFs) that is
 consistent with the way type families currently work. No matter how much
 we might wish it otherwise, type families are very different from term-
 level functions.

 I'm happy to see a fix for #9636, but preferably in a backwards-compatible
 way.

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