[GHC] #6018: Injective type families

[GHC]

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

Comment (by dorchard):

 Hi,
 Sorry to throw in a late thought, but what about adding a kind of
 injectives `>->`? e.g.`* >-> *`is the kind of injective type functions (as
 proved by the compiler, and perhaps as explicitly annotated by the user).
 This would provide a way to propagate
 the injectivity information within the type checker, and could also be an
 alternative (replacement?) for using the functional dependency syntax here
 (although, I think that syntax makes a lot of sense). I suppose it is not
 currently possible to specify this for a type family, unless kind
 signatures on type family names were possible, e.g.

 {{{
     type family (Id :: * >-> *) a where Id a = a
 }}}
 but this wouldn't be hard to add I don't think.

 Note that data family could then be given the injective kind too. This
 might provide some simplification in the type checker? I don't know for
 sure though.
 Just a thought, but thought it worth mentioning.

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