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