#9568: Type classes that fully cover closed kinds -------------------------------------+------------------------------------- Reporter: dmcclean | Owner: Type: feature request | Status: new Priority: lowest | Milestone: ⊥ Component: Compiler (Type | Version: 7.8.3 checker) | Operating System: Keywords: | Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: Difficulty: Unknown | None/Unknown Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- When we have a closed kind (I think data kinds may be the only ones that are closed?), and a type class that takes only that kind as a parameter, and we have instances of the typeclass for every type in the kind, it would be nice if we didn't have to list it in the context of every function that uses it. Example: in `GHC.TypeLits`, this relationship exists between `Nat` and `KnownNat`, `Symbol` and `KnownSymbol`. It also arises in many of my uses of data kinds, because I often end up with a `KnownX` class that provides term-level things related to whatever the type is. The constraints tend to end up everywhere, which is noisy. As far as I can tell they don't really carry any information: a `KnownNat n` constraint where `n :: Nat` should be able to be discharged in the same way that something like `Show Bool` is, because regardless of which `n` we pick we know there will be an instance. (This is trickier for closed kinds like `Nat` and `Symbol` than for user- defined ones through the data kinds feature, because the former are inhabited by infinitely many types.) Perhaps we could have a pragma to inform the compiler that this situation exists for a certain typeclass, which the compiler could check in finite cases (like the ones arising for user-defined data kinds) by enumerating all the cases. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9568 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler