#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