[GHC] #6018: Injective type families

[GHC]

#6018: Injective type families
-------------------------------------+-------------------------------------
              Reporter:  lunaris     |            Owner:  jstolarek
                  Type:  feature     |           Status:  new
  request                            |        Milestone:  7.10.1
              Priority:  normal      |          Version:  7.4.1
             Component:  Compiler    |         Keywords:  TypeFamilies,
            Resolution:              |  Injective
      Operating System:              |     Architecture:  Unknown/Multiple
  Unknown/Multiple                   |       Difficulty:  Unknown
       Type of failure:              |       Blocked By:
  None/Unknown                       |  Related Tickets:  #4259
             Test Case:              |
              Blocking:              |
Differential Revisions:  Phab:D202   |
-------------------------------------+-------------------------------------

Comment (by jstolarek):

 A nice syntax proposal showed up on Haskell-cafe. The idea is to allow
 user to actually introduce a variable that names the result:

 {{{#!hs
 type family Id a :: (result :: *) | result -> a where
 type family F a b c :: (d :: *) | d -> a b c
 type family G a b c :: (foo :: *) | foo-> a b where
 type family Plus a b :: (sum :: Nat) | sum a -> b, sum b -> a where
 type family H a b c :: (xyz :: *) | xyz a -> b c, xyz b -> a c
 }}}

 No new keywords, so we get full backwards compatibility. I'm only
 wondering how this would interact with kind signatures for the result,
 which we allow now. Above I assumed that if a programmer wants to name the
 result she must supply a kind annotation. This might be a bit
 inconvenient. On the other hand I think that the range of possible names
 for type variables and kinds is disjoint, so we may actually guess whether
 the user means the kind of the result or its name by looking whether the
 identifier is capitalized. So we could just write:

 {{{#!hs
 type family Id a :: result | result -> a where
 type family F a b c :: d | d -> a b c
 type family G a b c :: foo | foo-> a b where
 type family Plus a b :: sum | sum a -> b, sum b -> a where
 type family H a b c :: xyz | xyz a -> b c, xyz b -> a c
 }}}

 The only caveat I see is that user might accidentally write `type family
 Plus a b :: nat` instead of `type family Plus a b :: Nat` and then get
 some weird compilation errors if the kind signature was essential to make
 the code compile. Still, I like this proposal best of all made so far.

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