Hi Adam, It's great to hear that you are trying the plugins functionality, this is exactly the kind of experimentation it's designed for! I'm a little confused about what you're trying to achieve, though. Can you give some examples of code you'd like to be able to write? In general, GHC's type inference algorithm isn't expecting wanted constraints to be produced from givens; confusing things will happen if they are, and it's likely that *less* things will be typeable rather than *more*. Perhaps the plugin infrastructure should prevent you from doing so. It makes sense to produce givens from givens or wanteds from wanteds though. I'd imagine you might want to look for *wanted* constraints (HLength x ~ HLength y) and add an additional *wanted* (SameLength x y). One other thing to note is that plugins are called twice, once to simplify the givens (with empty wanteds), and once to solve the wanteds (https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker#Callingpluginsfrom...). Hope this helps, Adam On 14/02/15 10:31, adam vogt wrote:

Hello,

Using ghc-7.10 rc1, I am trying to write a type checker plugin that adds wanted constraint which helps ghc to infer more types. However, it seems that the wanted constraints I add don't get added to the inferred type of the declaration, so that I get a type error like:

a.hs:1:1: Warning: Could not deduce (SameLength y x) arising from an application from the context (HLength x ~ HLength y) bound by the inferred type of p :: (HLength x ~ HLength y) => Proxy '(y, x) at a.hs:11:1-69

I think ghc should be able to figure out p :: (SameLength x y, HLength x ~ HLength y) => Proxy '(x,y).

The code is self-contained:

git clone https://github.com/aavogt/HListPlugin

cd HListPlugin/ex

make

Is this approach supposed to be possible, or am I supposed to rewrite things such that I only produce CtGivenS from the plugin?

Regards, Adam

-- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/