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

 * I think it's very straightforward to allow injectivity of form `r ->
 <subset of args>`.  That is, the rhs is unconstrained but the lhs must be
 `r`.

  * So injectivity isn't a binary property; rather it's a `Bool` per
 argument.  Making this list a field of `SynTyCon` is probably right, with
 ordinary synonyms being all false.

  * We are not (at least for now) changing System FC.  So the only effect
 of injectivity is to add extra "Derived" unification constraints, very
 much like functional dependencies.  If we see
 {{{
  [W] F t ~ F s
 }}}
   then we don't decopose it.  Instead we add
 {{{
  [D] t ~ s
 }}}
   That guides inference, but does not produce proof terms.  So, no,
 nothing to do with `isDecomposableTyCon`.  Much more like the
 `try_improvement` code in `TcInteract.doTopReactFunEq`.

  * I don't understand the discussion of `Map`.  Are you perhaps discussing
 how to verify some (not shown here) implementation of a closed type family
 `Map` is in fact injective?

  * Verifying injectivity for open families: if the RHSs unify then the
 LHSs should be identical under that substitution. Eg
 {{{
   type instance F a Int = a -> Int
   type instance F Int a = Int -> a
 }}}
   These are consistent (and hence allowed) and are injective in both
 arguments.

  * My brain is too small to think about verifying injectivity for closed
 families. Richard?

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