Constraint implication

Andrew Martin andrew.thaddeus at
Thu Dec 28 14:56:24 UTC 2017

I agree that this would be cool. Here is some other discussion of this

   - A research paper proving its soundness:
   - Responses on reddit:
   - A very dated GHC issue:

Many people seem to want this, but to my knowledge, no one has any plans to
work on it any time soon. I would not be surprised if it actually ended up
getting implemented one day. It could replace everything in
Data.Functor.Classes as well as half of the stuff from Data.Exists in my
`quantification` package.

On Wed, Dec 27, 2017 at 2:50 AM, Ryan Reich <ryan.reich at> wrote:

> The Constraint kind appears to lack an interface to an important
> capability that is already part of the type checker: constraint
> implication.  Namely, the ability to provide a witness for the statement
> "constraint c1 implies constraint c2" or, more importantly, "for all a,
> constraint (c1 a) implies constraint (c2 a)", where c1 and c2 are now
> constraint-valued type functions (and possibly even for constraint
> functions with multiple parameters).  It seems to me that this can follow
> the pattern of the "magic" Coercible type class and the (non-magic)
> Coercion data type; it provides the programmer with an analogous value to
> this example that can be obtained in apparently no other way.
> _______________________________________________
> Libraries mailing list
> Libraries at

-Andrew Thaddeus Martin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>

More information about the Libraries mailing list