Re: Type checker plugins

16 Oct 2014

      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  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@haskell.org] On Behalf Of Adam Gundry
|  Sent: 16 October 2014 11:59
|  To: Iavor Diatchki
|  Cc: glasgow-haskell-users@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/