Just a few old observations I've made from implementing these things into type systems of my own:
1.) An internal hom for the category of constraints is admissible:
(|-) :: Constraint -> Constraint -> Constraint
models entailment, and effectively brings into scope a local rule, but global instance resolution isn't lost if this is only produced from existing instances.
To your point, this is analogous to the (:-) :: Constraint -> Constraint -> * external hom for the category of constraints provided by my constraints package, but it is internal, with all of the appropriate CCC operations.
2.) Quantification over constraints is also admissible.
Neither one compromises the "thinness" of the category of constraints that provides us global coherence of instance resolution
In this case the property that if D is thin, so is [C,D]. forall here can quantify over any other kind you want.
Unfortunately, neither implemented in Haskell.
You'd need both of them to be able to talk about constraints like (forall a. Eq a |- Eq (f a)).
Together could eliminate, morally, the entire Data.Functor.Classes mess. (That said, as implemented those classes are a bit stronger than the quantified form)
3.) Constraint also admits a sum type, (\/) but it acts more like a least upper bound than an either.
It is much easier to talk about in the category of constraints using the first part above.
Given (p |- r, q |- r), (p \/ q) |- r and vice versa.
The key to keeping the category of constraints thin is that you can't case analyze on it, its more like if you look at, say, Ord [a] \/ Eq a you can get to any constraint that you could get to given the intersection of both, not using the particulars of either. e.g. its morally as powerful as Eq [a] in this case.
Getting this stuff into GHC is the tricky part!
-Edward