<div dir="ltr">Adam, thanks for:<div><br></div><div>1) The reference to Iavor's paper --- it is a nice more-detailed description of the plugin API/semantics, and the Nelson-Oppen parallel is very illuminating!</div><div><br></div><div>2) Asking "<span style="color:rgb(33,33,33);font-size:13px">Do you mean "touchable" or "unification variable" here and elsewhere?"</span></div><div><br></div><div>That prompted me to finally dig deeper into something, and I've updated/simplified the wiki page accordingly. Basically, I was just using newFlexiTyVar (since it's pretty much the only option in the "official" TcPluginsM interface) without understanding if it's the touchability or the skolem-vs-unification status that was enabling the Given-Given interactions. I'm happy to report that touchability apparently has nothing to do with any of my test cases (including the record and variant library, etc). I'm relieved about that: touchability is a restriction on unification, and my general goal with my plugin architecture is to leave as many of the unification details to GHC's type equality solver as possible.</div><div dir="ltr"><div><br></div><div>Thanks. -Nick<br><br><div class="gmail_quote"><div dir="ltr">On Mon, Sep 11, 2017 at 1:34 AM Adam Gundry <<a href="mailto:adam@well-typed.com" target="_blank">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>
</blockquote></div></div></div></div>