#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