#9840: Permit empty closed type families -------------------------------------+------------------------------------- Reporter: adamgundry | Owner: Type: feature request | Status: patch Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.3 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #8028 | Differential Revisions: Phab:D841 -------------------------------------+------------------------------------- Comment (by goldfire): You're right that in the current state of affairs, generativity+injectivity imply matchability. But (until Phab:D202 lands) generativity also implies injectivity and vice versa. What characteristics to track separately is one of the challenges here... Suppose units-of-measure annotations were represented by a type headed `UnitExp`. `UnitExp` would not be injective, because it would take as arguments information about the different units and their powers, and this information has a non-trivial equational theory. However, `UnitExp` would, assumedly, be generative, in that no non-`UnitExp`s would ever be the same as a `UnitExp`. I don't know exactly what this means to the issue above, but it's an example of something that's generative but not injective. Yes, I completely agree about distinguishing based on equational theory. And the `data family` case is quite interesting, I think, because it shows how these concepts can be combined in unusual ways: data families are generative+injective, but yet have a non-trivial and extensible equational theory. If they didn't already exist, I would probably say this point in the space didn't exist! So there's something to be learned from them. Also, in case I haven't made this clear: these musings probably don't belong in this ticket, as I don't think these ideas should hold anything up about empty closed type families. But I'm hoping this leads to a slightly cleaner solution down the road. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9840#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler