Type checker plugins

[Iavor Diatchki]

Hi,

It shouldn't be hard to do the merge, but I am not sure that I'll have time
to do it before the weekend---I'll give it a go then.

-Iavor

On Tue, Oct 21, 2014 at 9:40 AM, Adam Gundry <adam at well-typed.com> wrote:

> Thanks Iavor, this is really helpful!
>
> If you have a moment to merge Simon's more recent changes on
> wip/new-flatten-skolems-Aug14, I'm keen to try out the new
> unflattening... or I can have a go at the merge if it would help?
>
> You may be right that flattened constraints are easier to work with in
> some cases, so it would be great if the plugin could choose which it
> sees. Unfortunately I'm not sure we can easily unflatten *some*
> constraints, given the way unflattening will work in the new
> getInertUnsolved. One option might be for tcPluginSolve to be called in
> both places, with a boolean parameter.
>
> Cheers,
>
> Adam
>
>
> On 18/10/14 23:33, Iavor Diatchki wrote:
> > Hello,
> >
> > Just a heads up, if anyone is playing around with this:  I just updated
> > the plugin interface a bit.
> >
> > Here are the changes:
> >    - A plugin now gets 3 sets of constraints: given, derived, and wanted
> > (in that order)
> >    - Plugins are now also presented with dictionary constraints (i.e.,
> > you may see equalities, function equalities, and dictionaries)
> >    - A plugin does not need to return all constraints that need to be
> > put back in the inert set.  This is both simpler and more efficient, I
> > think.  So, now a plugin can return one of these two results:
> >       - All is good:  plugin returns some solved constraints, and some
> > new constraints to be processed by the constraint solver. The solved
> > constraints are removed from the inert set, and their evidence variables
> > are defined.  The new work is added to the work list.
> >       - Found contradiction: plugin returns a list of the conflicting
> > constraint; these are removed from the inert set, and re-added as
> > insoluable.
> >
> > Happy hacking,
> > -Iavor
> >
> >
> >
> >
> >
> >
> > On Fri, Oct 17, 2014 at 3:36 PM, Iavor Diatchki
> > <iavor.diatchki at gmail.com <mailto:iavor.diatchki at gmail.com>> wrote:
> >
> >     Hello,
> >
> >     On Thu, Oct 16, 2014 at 3:58 AM, Adam Gundry <adam at well-typed.com
> >     <mailto:adam at well-typed.com>> wrote:
> >
> >
> >
> >         One problem I've run into is transforming the flattened
> >         CFunEqCans into
> >         unflattened form (so the flatten-skolems don't get in the way of
> >         AG-unification). Do you know if there is an easy way to do this,
> >         or do I
> >         need to rebuild the tree manually in the plugin?
> >
> >
> >     One thing that occurred to me about this:  when constraints are
> >     "flattened",
> >     it is easy for a plugin to pick-out only the one that it cares
> >     about.  If things were fully
> >     unflattened, this would not be the case... For example, if I have a
> >     constraint:
> >
> >     (2 + F a) ~ F a + F a
> >
> >     In the flattened form, this will become:
> >     (F a ~ f1, 2 + f1 ~ f2, f1 + f2 ~ f3, f2 ~ f3)
> >
> >     So, the type-nats plugin would pick out: (2 + f1 ~ f2, f1 + f2 ~ f3,
> >     f2 ~ f3),
> >     and ignore (F a ~ f1), as it knows nothing about arbitrary type
> >     functions.
> >
> >     So, if we want to do un-flattening, I think we should do it only on
> >     those constraints
> >     that are of interest to the plugin.
> >
> >
> >
> >
> >         Also, I notice that you are providing only equality constraints
> >         to the
> >         plugin. Is there any reason we can't make other types of
> constraint
> >         available as well? For example, one might want to introduce a
> >         typeclass
> >         with a special solution strategy (cf. Coercible, or the Has
> class in
> >         OverloadedRecordFields).
> >
> >
> >     Yeah, we should probably pass-in all constraints, inlcluding derived
> >     ones.
> >     The reason it is not like that is pretty much historical now.
> >     So I'll have a go at making this change.
> >
> >     -Iavor
> >
> >
> >
> >
> >
> >
> >
> >         >   - As an example, I've extracted my work on using an SMT
> solver at the
> >         > type level as a separate plugin:
> >         >
> >         >       https://github.com/yav/type-nat-solver
> >         >
> >         >    - To see how to invoke a module that uses a plugin, have a
> look in
> >         > `examples/A.hs`.
> >         >      (Currently, the plugin assumes that you have `cvc4`
> installed and
> >         > available in the path).
> >         >
> >         >     - Besides this, we don't have much documentation yet.  For
> hackers:
> >         > we tried to use `tcPlugin` on
> >         >     `TcPlugin` in the names of all things plugin related, so
> you could
> >         > grep for this.  The basic API
> >         >      types and functions are defined in `TcRnTypes` and
> `TcRnMonad`.
> >         >
> >         > Happy hacking,
> >         > -Iavor
>
> --
> Adam Gundry, Haskell Consultant
> Well-Typed LLP, http://www.well-typed.com/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20141022/3e8d7af0/attachment.html>