<div dir="ltr">I agree that this would be cool. Here is some other discussion of this topic:<div><ul><li>A research paper proving its soundness: <a href="http://i.cs.hku.hk/~bruno/papers/hs2017.pdf">http://i.cs.hku.hk/~bruno/papers/hs2017.pdf</a></li><li>Responses on reddit: <a href="https://www.reddit.com/r/haskell/comments/6me3sv/quantified_class_constraints_pdf/">https://www.reddit.com/r/haskell/comments/6me3sv/quantified_class_constraints_pdf/</a></li><li>A very dated GHC issue: <a href="https://ghc.haskell.org/trac/ghc/ticket/2893">https://ghc.haskell.org/trac/ghc/ticket/2893</a></li></ul><div>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.</div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Dec 27, 2017 at 2:50 AM, Ryan Reich <span dir="ltr"><<a href="mailto:ryan.reich@gmail.com" target="_blank">ryan.reich@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>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.<br></div></div>
<br>______________________________<wbr>_________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/libraries</a><br>
<br></blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature">-Andrew Thaddeus Martin</div>
</div>