#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 Differential Revisions: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: Difficulty: Unknown | Blocking: Blocked By: | Related Tickets: #4259 | -------------------------------------+------------------------------------- Comment (by goldfire): I'm still not sold on the concrete syntax involving `result`, despite having introduced that idea myself. I like the `(**)` suggestion here a bit more: http://www.haskell.org/pipermail/ghc-devs/2014-July/005492.html Separately, a change to Core will be necessary to really make this work in all cases. {{{ data X a where MkX :: (F b c ~ a) => b -> c -> X a }}} Say `F` is injective (in both arguments). After pattern-matching on `MkX ... :: X (F Int Bool)`, we will probably want to discover that `b` is `Int` and `c` is `Bool`. To do so, we will need to decompose the `(F b c ~ a)` coercion, using the '''left''' and '''right''' (or perhaps '''nth''') coercion forms. These currently don't work over type families, and for good reason. However, if a type family is injective, then these ''could'' be made to work over type families. With the update to Core, we would probably want to make sure we don't lose type safety, though! All that said, this use case is obscure, and the primary push for injective type families does not seem to require a change to Core. It is worth implementing without this piece. But, the idea came up in conversation, and I thought I should record it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/6018#comment:40 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler