Type checker plugins

[Simon Peyton Jones]

| 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.

Actually it would be worth pausing.  If you get the latest Unflattening is now done by getInertUnsolved, which itself is called by solveFlatWanteds, immediately after calling solveFlats.  And solveFlats (which used to be called solveInteract) is where Iavor has the plugin interface.

In short, if you'd like to see unflattened constraints, rather than flattened ones, that would be easy.

Unflattening yourself is inadvisable.  The unflattening code in getInertUnsolved is quite remarkably tricky and it took me some time get it right.  (I have to write a long Note before committing it to head.)

All this is in the just-committed wip/new-flatten-skolems-Aug14 branch

Simon

| -----Original Message-----
| From: Adam Gundry [mailto:adam at well-typed.com]
| Sent: 16 October 2014 21:50
| To: Eric Seidel; Simon Peyton Jones
| Cc: Iavor Diatchki; glasgow-haskell-users at haskell.org
| Subject: Re: Type checker plugins
| 
| 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/