Type checker plugins

[Iavor Diatchki]

Hello,

On Thu, Oct 16, 2014 at 3:58 AM, Adam Gundry <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/20141017/582f0738/attachment.html>