Type classes that fully cover closed kinds
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.
Trac metadata
Trac field | Value |
---|---|
Version | 7.8.3 |
Type | FeatureRequest |
TypeOfFailure | OtherFailure |
Priority | lowest |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |