Hello, On Thu, Oct 16, 2014 at 3:58 AM, Adam Gundry <a...@well-typed.com> wrote:
> > > 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? > One thing that occurred to me about this: when constraints are "flattened", it is easy for a plugin to pick-out only the one that it cares about. If things were fully unflattened, this would not be the case... For example, if I have a constraint: (2 + F a) ~ F a + F a In the flattened form, this will become: (F a ~ f1, 2 + f1 ~ f2, f1 + f2 ~ f3, f2 ~ f3) So, the type-nats plugin would pick out: (2 + f1 ~ f2, f1 + f2 ~ f3, f2 ~ f3), and ignore (F a ~ f1), as it knows nothing about arbitrary type functions. So, if we want to do un-flattening, I think we should do it only on those constraints that are of interest to 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). > > Yeah, we should probably pass-in all constraints, inlcluding derived ones. The reason it is not like that is pretty much historical now. So I'll have a go at making this change. -Iavor > > > > - 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