[TYPES] "Constraints as types" paradigm

[Jacques Carette]

I have heard some informal references to a "constraints as types" paradigm.  I have however not been able to find a 
lot of concrete references.  I am aware of HM(X) by Odersky, Sulzmann and Wehr, which certainly takes this idea part 
of the ways [and know of *some* of the follow-up papers].  One could also consider Haskell's type classes as another 
examples of this idea.

However, I am only realy interested in this idea in the absence of an underlying type system with 'principal types' -- 
otherwise there really is no point in moving to constraints, as closed forms are usually more informative than 
implicit definitions, although they tend to be more verbose.  An evocative analogy (for me!) is the difference between 
closed-form solutions to (differential, integral, ...) equations versus a normalized form of the equations themselves; 
although people prefer closed-form solutions, it is algorithmically much(!) easier to find properties of the 
'solution' from the original equations than from the closed-form expression [is my Computer Algebra background showing 
yet?].

Are there people on this list who can turn the vague thoughts above into precise references to written material?

Jacques Carette