On Thu, Jun 07, 2012 at 07:32:45PM +0100, ex falso wrote:
we always have to put the class restriction (TupleLength l) there, even though all possible type constructors of [*] have a TupleLength instance defined!
Yes, and this is a feature, for at least two reasons. First: to the extent that Haskell's type system corresponds to a logic, it corresponds to a constructive one. Types/propositions are inhabited/proved by explicit terms/evidence. But this request (and [1]) essentially boil down to a desire for double negation elimination: if there *can't* *not* be a certain instance, then the compiler should infer that there *is* one. This seems weird to me (though perhaps I've just drunk too much of the constructivism kool-aid). Second, on a more practical level, the ability to omit class constraints like this would make reasoning about types much more non-local and difficult, since a type like foo :: Bar a -> Baz may or may not implicitly expand to something like foo :: SomeClass a => Bar a -> Baz (which could have important implications for things like inlining, sharing, etc. -- cf the monomorphism restriction), but figuring out whether it does or not requires knowing (a) the definition of Bar and all the instances that are in scope, and (b) whether or not SomeClass's methods ever get called from foo (or anything it calls, recursively). I'd much rather explicitly write the SomeClass constraint if I want it, and be guaranteed that it won't be added if I don't. In summary, these constraints may be "superfluous" in a strictly logical sense, but (a) not in the kind of logic that Haskell uses, and (b) the pain and suffering caused by removing them would far outweigh the tiny bit of typing that would be saved. -Brent [1] http://haskell.1045720.n5.nabble.com/Data-Kinds-and-superfluous-in-my-opinio...