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

 The equations defining a head-injective function all have RHSs with
 different heads. What appears below the heads does not matter. Here is an
 example:

 {{{#!hs
 type family F a where
   F (Just x) = True
   F Nothing  = False
 }}}

 This function is ''not'' injective: `F (Just 1) ~ F (Just 2)`. Yet, it is
 head-injective. If the type-inferencer knows that `F x ~ True`, it can
 then refine `x ~ Just y` for some fresh unification variable `y`. This
 improvement may be enough to make further progress.

 Of course, injectivity does not imply head-injectivity. Consider

 {{{#!hs
   type family G a where
     G True  = Just 1
     G False = Just 2
 }}}

 This function is injective but not head-injective. So, implementing only
 head-injectivity will miss this case. But, perhaps we can refine the
 notion of head-injectivity simply to mean that the RHSs don't unify.

 The reason I'm bringing this up is that head-injectivity is, as I
 understand it, implemented in Agda and used during type inference. It
 intrigues me to think that we can make progress in the case of `F`, a non-
 injective function.

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