Replying to [comment:105 dorchard]:

...

what about adding a kind of injectives `>->`? e.g.`* >-> *`is the kind of injective type functions

This is very much along the lines of what Jan and I proposed in our "Promoting Functions to Type Families" paper ([http://www.cis.upenn.edu/~eir/papers/2014/promotion/promotion.pdf here]). Not exactly, I think. At the moment `->` kind classifies term-level functions (non-injective, non-generative, can be partially applied), type constructors (injective, generative, can be partially applied) and type families (non-injective, non-generative, cannot be partially applied). In our paper we proposed a new kind to classify type functions (families)

GHC assumes all function types (that is, types with kinds that are

#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 jstolarek): Replying to [comment:108 goldfire]: that are still non-injective and non-generative but can be partially applied just like term-level functions. We addressed the problem of partial application, not injectivity. headed by `->`) are ''generative'' and ''injective''. (...) Thus, the kind `->` denotes a generative, injective function. Are you sure? I would say this is true only for type constructors but perhaps I'm missing something. (I am assuming that also `->` classifies type families although, as you point out, this is not entirely accurate.) Anyway, I can imagine introducing a new kind to distinguish between injective and non-injective applications but, given that we might want a new kind to distinguish between things that can and can't be partially applied at the type level, this does not seem like a good choice. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/6018#comment:109 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler