type checker plugin does not affect inferred type signatures

[Adam Gundry]

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#Callingpluginsfromthetypechecker).

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/