[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:  Phab:D202   |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Replying to [comment:75 jstolarek]:
 > Good question. I have not considered such case earlier. Here are some
 thoughts:
 >
 > Currently your `Map` function will work only for type constructors
 because unsaturated type families are not allowed. These are certainly
 injective.
 >
 > First step in my current outline of the algorithm that decides whether a
 type family is injective or not says: "If a RHS contains a call to a type
 family we conclude that the type family is not injective. I am not certain
 if this extends to self-recursion -- see discussion below." This would
 lead to conclusion that `Map` is not injective because `Map` calls itself.
 >
 > Now let's say I manage to find a way to allow self-recursion (see
 discussion on the wiki page). I'm left with the problematic call to `f`.
 As stated earlier currently this must be an injective type constructor. So
 it seems that declaring `Map` injective should be safe because type
 constructors are generative and it seems possible to deduce `f`, `a` and
 `b` from `Map f [a, b] ~ [Maybe Int, Maybe Char]`. At the moment I have no
 idea how to formulate an algorithm for such a deduction. Could this be
 done by the current constraint solver?

 This should just work with the algorithm already stated. (Except for the
 self-recursion bit, which I responded to on the wiki page.) Unification
 should do the work for you.

 >
 > What if we were allowed to have partially applied type families (say,
 because we've implemented ideas from singletons) and `f` could be a type
 family? Would knowing that `f` is injective allow us to declare `Map` as
 injective? Injectivity says you can deduce LHS from RHS but I think that
 it would not be a good idea to try to solve `Map f [a, b] ~ [Int, Char]`.
 And so the restriction on not having calls to type families on the RHS
 would rightly declare `Map` as not injective. So if we had partially
 applied type families and thus `f` was allowed to be either a type
 constructor a type family we should declare `Map` as not injective. This
 contrasts with earlier paragraph, where knowing that `f` must be a type
 constructor allowed us to declare `Map` as injective.
 >
 > Does that make sense?

 No. Under the singletons work, we gave a different kind to non-injective
 functions, so Gabor's kind -- using `->`, not any other arrow -- requires
 an injective argument.

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