Type checker plugins

[Simon Peyton Jones]

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