[GHC] #6018: Injective type families

[GHC]

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

Comment (by jstolarek):

 I spent some time recently thinking about this one. It is not clear to me
 what should happen when we know that a type family `F` is injective. It
 would certainly allow us to infer from `(F a ~ F b)` that `a ~ b` (modulo
 corner cases). So instead of first reducing injective type family
 application and then working on the result we could instead reason about
 type family's arguments. We could even invert type families. Is there
 anything else we could reason about with injective type families?

 The discussion here is only about open type families (obviously, closed
 type families were not implemented two years ago). I guess that now this
 change would affect both open and closed type families?

 Replying to [comment:2 simonpj]:
 > Some functions might be injective in one argument but not another.  For
 example:
 > {{{
 >   F a b ~ F c d   ===>    a ~ c
 >                 but not   b ~ d
 > }}}
 That is not true according to the mathematical definition of injectivity
 (as stated in [comment:29 comment 29]). Unless we want to introduce
 definition of type families injective only in some of the arguments,
 [http://haskell.1045720.n5.nabble.com/Injective-type-families-
 tp3385084p3385684.html as proposed by Iavor].

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