#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 adamgundry): Thanks, Richard, it's good to try to simplify and bring order to these; I hadn't realised what a can of worms I was opening with this feature request! In the interests of simplicity, is it actually necessary to distinguish "matchability" from generativity+injectivity? In particular, if `Any` remains non-generative (as at present) then I think the distinction collapses. The only case this matters is if we needed to conclude `f ~ Any : forall k . k` from `f @k0 ~ Any @k0 : k0`; but do we? I think it's perhaps also helpful to divide things up along the lines of where their equational theory comes from (considering only nominal roles for now): * trivial equational theory (`data`, `newtype`, `class`) * equational theory specified at declaration site (`type`, closed `type family`) * special equational theory either built-in or provided via plugin (type lits operators, what I want) * open equational theory that can be extended anywhere (open `type family`, `data family`) (The `data family` case is slightly strange, because the equational theory can be extended anywhere, but only in a very limited way.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9840#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler