[GHC] #10832: Generalize injective type families

[GHC]

#10832: Generalize injective type families
-------------------------------------+-------------------------------------
        Reporter:  jstolarek         |                Owner:  jstolarek
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.11
  checker)                           |             Keywords:  TypeFamilies,
      Resolution:                    |  InjectiveFamilies
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #6018             |  Differential Rev(s):  Phab:D1287
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by lexi.lambda):

 I might have a use case for this, but I’m not smart enough to understand
 if my problem would be solved by this feature or not. Basically, I have a
 type family for type-level append:


 {{{
 #!hs
 type family xs :++: ys where
   '[]  :++: ys = ys
   (x ': xs) :++: ys = x ': (xs :++: ys)
 }}}

 This family is not injective, but if you know the result and one of the
 two inputs, you can deduce the other one. Therefore, I would like to be
 able to write the dependency annotation `r xs -> ys, r ys -> xs`.

 I have written a function that uses `:++:` in its type signature, which
 currently looks like this:

 {{{
 #!hs
 forall g r a f. (forall v. f v -> Eff (g :++: r) v) -> Eff (f ': r) a ->
 Eff (g :++: r) a
 }}}

 Currently, this signature is ambiguous. However, notably, we know `r`, and
 in the location this function is used, we also know `g :++: r`. Therefore,
 my hope is that with this feature, I could use this function, and `g`
 could be inferred. Currently, however, I have to use `TypeApplications` to
 pick `g` explicitly, even though the type seems “obvious” to the
 programmer at its use site (since it very explicitly duplicates type
 information in an adjacent top-level annotation).

 I don’t know enough to know if such an annotation would actually allow
 such a thing or not, or if this is even applicable in my use case, but I
 thought I would offer the example anyway, since it sounds like this
 feature is in need of motivating examples. (I can also try and come up
 with a smaller, self-contained example if I’m not totally off base and
 that would, in fact, be relevant/helpful.)

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