[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 simonpj):

 (GHC does, in effect, use narrowing, I believe.)

 Let's stand back a bit.  What are we trying to achieve.  Here is the
 Number 1 Goal: if the type inference engine is trying to prove `F a ~ F
 beta`, where `a` is a skolem constant and `beta` is a unification
 variable, is it justified in fixing `beta := a`?  If `F` is not injective
 the answer is "no".  If it's injective, the answer is "yes".  We have
 multiple examples of the need for this.

 More generally, our goal is to use injectivity to guide the decision about
 what type a unification varaible stands for.  Injectivity also allows
 other such opportunities, beyond the Number 1 Goal above.  Suppose `F` is
 injective, and we have
 {{{
 F Int = True
 }}}
 Then if we have `F beta ~ True` we can deduce `beta := Int`.

 Richard raises further possiblities: possibly-partial information about
 the result might allow us to deduce possibly-partial information about the
 arguments.  That is the stuff about head-injectivity and it seems to be
 potentially very complicated.  Take a closed type family.  If I tell you
 something (but perhaps not everything) about the result, perhaps you can
 tell me something (but perhaps not everything) about the argument.  I
 don't know how clever you might be here, or how to declare the cleverness
 in an "injectivity signature" for open families.

 But we have no actual use-caes for anything except Number 1 Goal, for
 equalities of form `F t1 ~ F t2`. It seems that equalities of form `F t1 ~
 some-type` offer potential opportunities, but I don't see a sweet spot.

 Simon

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