Type checker plugins

[Adam Gundry]

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?

Thanks,

Adam


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. 
> 
> Eric
> 
> 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. 
>>
>> Simon
>>
>> |  -----Original Message-----
>> |  From: Glasgow-haskell-users [mailto:glasgow-haskell-users-
>> |  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/