[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
      Operating System:              |     Architecture:  Unknown/Multiple
  Unknown/Multiple                   |       Difficulty:  Unknown
       Type of failure:              |       Blocked By:
  None/Unknown                       |  Related Tickets:  #4259
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by heisenbug):

 Replying to [comment:48 goldfire]:
 > A conversation with Ulf Norell (the first implementor of Agda) led to
 this interesting thought: We may not want injectivity -- we may want a
 weaker property, which I'll term "head-injectivity".
 >

 So when our goal is to make progress from the target expression towards
 the source expression, what hinders us to follow Omega and use narrowing
 to obtain the head? Tim Sheard has a nice 2006 paper on how to do it. It
 is really powerful and we could insist that exactly one solution exists.

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