<p dir="ltr">Ah, yes, derived constraints.  The mapping to logic I have in my mind is as follows:</p>
<p dir="ltr">Given = assumption, used in proofs<br>
Wanted = goal, needs proof<br>
Derived = implied by assumptions and goals</p>
<p dir="ltr">A derived constraint may be used to instantiate touchable unification variables, and guarantees that in doing so we are not loosing any generally.</p>
<p dir="ltr">Consider, for example, a wanted: `(x + 5) ~ 8`.  From this we can generate a new derived constraint `x ~ 3`, which would allow GHC to instantiate `x` to 3.  </p>
<p dir="ltr">A derived constraint could also be used to detect that the current set of goals is inconsistent, for example if we got a derived constraint equivalent to False, we would immediately know that the current set of goals has no solution.</p>
<p dir="ltr">-Iavor</p>
<br><div class="gmail_quote"><div dir="ltr">On Mon, Sep 11, 2017, 9:35 AM Adam Gundry <<a href="mailto:adam@well-typed.com">adam@well-typed.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Nick,<br>
<br>
This is great work, and I look forward to seeing the code once it is<br>
ready. I've had a quick glance over your wiki page, and thought I should<br>
send you some initial comments, though it deserves deeper attention<br>
which I will try to find time to give it. :-)<br>
<br>
I don't see a reference to Iavor's paper "Improving Haskell Types with<br>
SMT" (<a href="http://yav.github.io/publications/improving-smt-types.pdf" rel="noreferrer" target="_blank">http://yav.github.io/publications/improving-smt-types.pdf</a>). If<br>
you've not come across it, it might give a useful alternative<br>
perspective on how plugins work, especially with regard to derived<br>
constraints.<br>
<br>
The following is based on my faulty memory, so apologies if it is out of<br>
date or misleading...<br>
<br>
> When/where exactly do Derived constraints arise?<br>
<br>
Suppose I have a class with an equality superclass<br>
<br>
    class a ~ b => C a b<br>
<br>
and a wanted constraint `C alpha Int`, for some touchable variable<br>
`alpha`. This leads to a derived constraint `alpha ~ Int` thanks to the<br>
superclass (derived means we don't actually need evidence for it in<br>
order to build the core term, but solving it might help fill in some<br>
touchable variables).  Sorry if this is obvious and not exact enough!<br>
<br>
> When do touchables "naturally" arise in Given constraints?<br>
<br>
Do you mean "touchable" or "unification variable" here (and elsewhere?).<br>
A skolem is always untouchable, but the converse is not true.<br>
<br>
I think that unification variables can arise in Given constraints, but<br>
that they will always be untouchable. Suppose we have defined<br>
<br>
    f :: forall a b . ((a ~ b) => a -> b) -> Int<br>
<br>
(never mind that it is ambiguous) and consider type-checking the call `f<br>
id`. We end up checking `id` against type `a -> b` with given `a ~ b`<br>
where `a` and `b` are unification variables. They must be untouchable,<br>
however, otherwise we might unify them, which would be wrong.<br>
<br>
Hope this helps,<br>
<br>
Adam<br>
<br>
<br>
On 10/09/17 23:24, Nicolas Frisby wrote:<br>
> Hi all. I've been spending my free time for the last couple months on a<br>
> type checker plugin for row types. The free time waxes and wanes;<br>
> sending an email like this one was my primary goal for the past couple<br>
> weeks.<br>
><br>
> At the very least, I hoped this project would let me finally get some<br>
> hands on experience with OutsideIn. And I definitely have. But I've also<br>
> made more progress than I anticipated, and I think the plugin is<br>
> starting to have legs!<br>
><br>
> I haven't uploaded the code yet to github -- it's not quite ready to<br>
> share. But I did do a write up on the dev wiki.<br>
><br>
><br>
> <a href="https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain" rel="noreferrer" target="_blank">https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain</a><br>
><br>
> I would really appreciate and questions, comments, and --- boy, oh boy<br>
> --- answers.<br>
><br>
> I hope to upload within a week or so, and I'll update that wiki page and<br>
> reply to this email when I do.<br>
><br>
> Thanks very much. -Nick<br>
><br>
> P.S. -- I've CC'd and BCC'd people who I anticipate would be<br>
> specifically interested in this (e.g. plugins, row types, etc). Please<br>
> feel free to forward to others that come to mind; I know some inboxes<br>
> abjectly can't afford default list traffic.<br>
><br>
> P.P.S. -- One hold up for the upload is: which license? I intend to<br>
> release under BSD3, mainly to match GHC since one ideal scenario would<br>
> involve being packaged with/integrated into GHC. But my brief recent<br>
> research suggests that the Apache license might be more conducive to<br>
> eventual widespread adoption. If you'd be willing to advise or even just<br>
> refer me to other write ups, please feel free to email me directly or to<br>
> start a separate thread on a more appropriate distribution list (CC'ing<br>
> me, please). Thanks again.<br>
<br>
<br>
--<br>
Adam Gundry, Haskell Consultant<br>
Well-Typed LLP, <a href="http://www.well-typed.com/" rel="noreferrer" target="_blank">http://www.well-typed.com/</a><br>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div>