[GHC] #6018: Injective type families

[GHC]

#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 dfeuer):

 I don't see the problem with letting injective families call other type
 families as long as there is no recursion—can't GHC follow all paths to
 the end when necessary, and use injectivity "lemmas" when possible for
 efficiency? Or does this end up not being useful/efficient/possible for
 some reason?

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