#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): I'm afraid something smells a little off here. I agree that we should permit empty closed type families -- that's not a problem. But I'm not convinced that empty CTFs are the solution to Adam's problem. What Adam really wants here is the ability to create new type-level constants at arbitrary kind. An empty CTF fits the bill, but there's something strange about it. Despite my early objections, I've come to agree with Lennart's viewpoint in #9636 that a CTF that is known to be unable to reduce is a strange beast that should probably be disallowed. Here is a simple proposal: {{{ type constant Unit :: * -- kind annotation required; types of kind * are promoted to kinds -- this is essentially indistinguishable from `data Unit` type constant Meter :: Unit -- Here, we can define a new constant of a non-* kind. This is very useful! type constant Second :: Unit -- We can even pattern-match on these constants: type family UnitToString (x :: Unit) :: Symbol where UnitToString Meter = "m" UnitToString Second = "m" type constant Weird :: Nat -> Bool -- This is OK to declare. But we *cannot* pattern-match on it, because the return -- kind is closed. }}} This last example may be controversial, but I think it's OK. The others are less controversial in my opinion. What this essentially does is allow for ''open'' datakinds. Once these constants are declared, then a plugin can define an equational theory over them. Unfortunately, this is a much bigger change than just allowing empty CTFs. But it somehow smells better to me. Thoughts? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9840#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler