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