Hi, i've been using DataKinds for a while and there seems to be a recurring annoyance that could be possibly eliminated with a language extension. It goes something like this: data Tuple (l :: [*]) where Unit :: Tuple '[] Comma :: a -> Tuple as -> Tuple (a ': as) data Proxy k = Proxy class TupleLength (l :: [*]) where tupleLength :: Proxy l -> Integer instance TupleLength '[] where tupleLength _ = 0 instance (TupleLength as) => TupleLength '(a : as) where tupleLength _ = 1 + tupleLength (Proxy :: Proxy as) so far so good. but now if we want to use TupleLength: printLength :: (TupleLength l) => Tuple l -> IO () printLength t = print $ tupleLength t we always have to put the class restriction (TupleLength l) there, even though all possible type constructors of [*] have a TupleLength instance defined! If we had a way to signal that all ty constrs are catered for then the compiler could check this, and deduce that l::[*] is always an instance. Well that's the hypothesis. Of course this would only make sense for kinds with finite no. of ty constructors, namely DataKinds-lifted types. Does this make sense? ex