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

 I'm afraid something smells a little off here.

 I agree that we should permit empty closed type families -- that's not a
 problem. But I'm not convinced that empty CTFs are the solution to Adam's
 problem.

 What Adam really wants here is the ability to create new type-level
 constants at arbitrary kind. An empty CTF fits the bill, but there's
 something strange about it. Despite my early objections, I've come to
 agree with Lennart's viewpoint in #9636 that a CTF that is known to be
 unable to reduce is a strange beast that should probably be disallowed.

 Here is a simple proposal:

 {{{
 type constant Unit :: *
    -- kind annotation required; types of kind * are promoted to kinds
    -- this is essentially indistinguishable from `data Unit`
 type constant Meter :: Unit
    -- Here, we can define a new constant of a non-* kind. This is very
 useful!
 type constant Second :: Unit

 -- We can even pattern-match on these constants:
 type family UnitToString (x :: Unit) :: Symbol where
   UnitToString Meter = "m"
   UnitToString Second = "m"

 type constant Weird :: Nat -> Bool
   -- This is OK to declare. But we *cannot* pattern-match on it, because
 the return
   -- kind is closed.
 }}}

 This last example may be controversial, but I think it's OK. The others
 are less controversial in my opinion. What this essentially does is allow
 for ''open'' datakinds.

 Once these constants are declared, then a plugin can define an equational
 theory over them.

 Unfortunately, this is a much bigger change than just allowing empty CTFs.
 But it somehow smells better to me.

 Thoughts?

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