Hi,

This has been discussed before: http://haskell.1045720.n5.nabble.com/Data-Kinds-and-superfluous-in-my-opinion-constraints-contexts-td5689436.html

Feel free to open a feature request for this. I think it's something we should consider
addressing, but at the moment it's not immediately clear how to do it.


Cheers,
Pedro

On Thu, Jun 7, 2012 at 7:32 PM, ex falso <0slemi0@gmail.com> wrote:
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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe