Type checker plugins

[Adam Gundry]

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/