type checker plugin does not affect inferred type signatures

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

type checker plugin does not affect inferred type signatures

Adam Vogt
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
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: type checker plugin does not affect inferred type signatures

Adam Gundry-2
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/
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: type checker plugin does not affect inferred type signatures

Adam Vogt
Hi Adam,

I've added a README which tries to explain things:
https://github.com/aavogt/HListPlugin

When I produce a wanted constraint from a wanted constraint, things
work as I wanted. Thanks for the suggestion!

Regards,
Adam

On Mon, Feb 16, 2015 at 4:36 AM, Adam Gundry <[hidden email]> wrote:

> 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,
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users