#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):
What Adam really wants here is the ability to create new type-level constants at arbitrary kind.
Is it? Open datakinds would be nice, but `Symbol` and `*` already give us quite a lot of wriggle room. My real problem is more in creating type-level function symbols without any equational theory, which (with Phab:D841 at least) goes like this: {{{ data Unit type family Mul (u :: Unit) (v :: Unit) :: Unit where }}} In particular, to avoid conflict with plugin-generated axioms, `Mul` * must be saturated; * is not injective, so `Mul u v ~ Mul v u` does not imply `u ~ v`; * cannot be used in patterns; * cannot be given any instances by the user (this is the only condition not satisfied by an open type family). I don't quite understand how your proposal would work for this case. What does it mean to declare `Weird` as a constant in a closed kind? Note that giving `Mul` kind `Unit -> Unit -> Unit` is no good, because that means it is injective (at least unless we add another flavour of type-level function space). In any case, adding a whole new declaration form feels like rather more work than my needs justify. Phab:D841 is a relatively simple change (deleting 7 lines of code, in its original incarnation before distinguishing abstract/empty CTFs) that is consistent with the way type families currently work. No matter how much we might wish it otherwise, type families are very different from term- level functions. I'm happy to see a fix for #9636, but preferably in a backwards-compatible way. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9840#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler