[Haskell-cafe] class instances for kinds with finite ty constrs, does this make sense?

[Brent Yorgey]

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-opinion-constraints-contexts-td5689436.html