Constraint implication

[Ryan Reich]

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20171226/ee90bc6b/attachment.html>