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

 > what's wrong with exponential time here?

 Compilation times. If a type family takes a single argument then obviously
 there is only one possible injectivity condition ("result -> a"). For two
 arguments there are 5 possible injectivity conditions. For 3 this number
 jumps to 19. 4 arguments => 65 combinations. 5 arguments => 211
 combinations. 6 arguments => 665 combinations. Let's assume (for
 illustrative purposes) that verifying (ie. attempting to infer) a single
 injectivity condition for a type family takes 0.01s. Under such
 assumptions inferring all possible injectivity conditions for a type
 family with 6 arguments will take ~6.5s. We can't do that.

 > Is there any patch which would allow me to use injective type families
 in current GHC?

 No. But if all goes well all this discussion here will culminate with such
 a patch :-) In the meantime, if you have any motivating use cases that
 require injectivity to work please share them if you can. This would be
 most helpful.

 I've spent last several days thinking intensely about the design and made
 some progress. Hopefully, I'll incorporate my notes into the wiki page by
 the end of the week. Will get back with some ideas and proposals once this
 happens.

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