A type checker plugin for row types

Thu Sep 14 18:12:39 UTC 2017

Here are my stabs at answers to two of your questions.

> • When/where exactly do Derived constraints arise? I'm not recognizing them in the OutsideIn paper.

I agree with others' comments on this point, but perhaps I can expand. A Derived constraint is essentially a Wanted constraint, but one where there is no need for evidence. They arise for several reasons:

- If we have Ord a as a Wanted, then we'll get Eq a (a superclass constraint) as a Derived. While GHC has no need for an Eq a dictionary, perhaps solving the Eq a constraint will help us solve the Ord a constraint. So the Eq a is Derived.

- Functional dependencies and type family dependencies give rise to Derived constraints. That is, if we have class C a b | a -> b, instance C Int Bool, and [W] C Int a, then we'll get [D] a ~ Bool.

- GHC says that Wanteds cannot rewrite Wanteds. That is, if we have [W] a ~ Bool and [W] a ~ Int, we *don't* want GHC to simplify to [W] Int ~ Bool and then report that. It's very confusing to users! However, sometimes, (I don't have an example) we need Wanteds to rewrite Wanteds in order to make progress. So GHC clones Wanteds into Deriveds, and says that Deriveds *can* rewrite Deriveds. Perhaps after a lot of rewriting, some variables will unify, and then GHC can make progress on the Wanteds. Of course, all this cloning would be non-performant, so GHC essentially does a copy-on-write implementation, where many constraints are [WD], both Wanted and Derived.

While Deriveds *arise* for several reasons, they contribute back to the world in only one: unification. That is, the whole point of Deriveds is so that GHC will discover [D] a ~ Int and then set a := Int.

> • GHC has various kinds of variable and skolem (e.g. signature skolem) that I'm not recognizing in the OutsideIn paper. Is there a comprehensive discussion of them all?

I'm unaware of one, but here are some pointers.

- A skolem tends to be a user-written type variable, unifiable with no other. If you have a declaration (id :: a -> b; id x = x), GHC will reject because it won't unify a with b. a and b are skolems.

- GHC also has "super-skolems", which have a slightly different behavior w.r.t. instances. See Note [Binding when looking up instances] in InstEnv. I've never had to care about this distinction.

- GHC has several different types of unification variables (= metavars).

  * A TauTv is your regular, run-of-the-mill unification variable. It can unify only with monotypes.

  * A SigTv is a metavar that can unify only with another variable. See Note [Signature skolems] in TcType for examples of why this is useful. (Editorial comment: I think the design around SigTvs is wrong, because generally there is a set of variables a given SigTv should not unify with. But GHC doesn't track this info.)

  * FlatMetaTvs and FlatSkolTvs are an implementation detail of how GHC deals with type families. They are documented in Note [The flattening story] in TcFlatten.

I think that's it, but feel free to ask if you run into more.

(In case you're wondering, I didn't really look over the design you're proposing. I leave that to others.)

Good luck!
Richard

> On Sep 11, 2017, at 9:48 AM, Ben Gamari <ben at smart-cactus.org> wrote:
> 
> On September 11, 2017 9:34:15 AM GMT+01:00, Adam Gundry <adam at 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 at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> 
> It would be great if someone could extract the conclusion of this thread into a Note. Clearly there is a hole in the current state of our source documentation.
> 
> Cheers,
> 
> - Ben
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs