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 <simo...@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- >> | boun...@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/ _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
