[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
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