Re: Type checker plugins
Adam Gundry <adam <at> well-typed.com>
2014-10-16 20:49:52 GMT
Thanks Simon, your branch does make it a lot more feasible to unflatten,
so I'll just go ahead and implement that in my plugin for now.
Eric, that's fair enough, and I don't have any concrete use cases for
non-equality constraints at the moment. I'm just keen to minimize the
restrictions placed on plugins, because it is much easier to recompile a
plugin than make changes in GHC itself!
On that note, I still wonder if it would be better to define TcPluginM
as a wrapper around TcS rather than TcM. While in principle TcM should
suffice, in practice GHC sometimes uses TcS for things that a plugin
might want (I've run into TcSMonad.matchFam, which could easily be
implemented in TcM instead). Is there any downside to defining a nice
API in TcPluginM but providing an escape hatch to TcS, not just TcM?
On 16/10/14 16:21, Eric Seidel wrote:
> Our branch is actually based on yours Simon, are there any changes in the past week that we should pull in for
people who want to experiment?
> Adam, we talked about passing other constraints to the plugins, but didn't have a concrete use-case at the
time, so we just kept it as simple as possible. I don't see a reason to hide constraints if, as you say, there
are plugins that may want to solve them.
> Sent from my iPhone
>> On Oct 16, 2014, at 07:08, Simon Peyton Jones <simonpj <at> microsoft.com> wrote:
>> This will become easier, I think. look on wip/new-flatten-skoelms-Aug14. I'm now unflattening after
solving the flat constraints.
>> | -----Original Message-----
>> | From: Glasgow-haskell-users [mailto:glasgow-haskell-
>> | bounces <at> haskell.org] On Behalf Of Adam Gundry
>> | Sent: 16 October 2014 11:59
>> | To: Iavor Diatchki
>> | Cc: glasgow-haskell-users <at> haskell.org
>> | Subject: Re: Type checker plugins
>> | Hi Iavor,
>> | On 13/10/14 21:34, Iavor Diatchki wrote:
>> | > Hello,
>> | >
>> | > We now have an implementation of type-checker with plugin support.
>> | If
>> | > you are interested in trying it out:
>> | >
>> | > - Checkout and build the `wip/tc-plugins` branch of GHC
>> | Thanks, this is great! I'd been working on a similar implementation,
>> | but yours is much better integrated. I am trying to adapt my units of
>> | measure plugin to work with this interface, and work out what else I
>> | need in TcPluginM.
>> | 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?
>> | 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).
>> | Cheers,
>> | Adam
>> | > - 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/