Re: “Ambiguous type variable in the constraint” error in rewrite rule

[Tsuyoshi Ito]

Dear Simon,

Thank you for the investigation, and also thank you for telling me
about the -ddump-rules.

> Ah!  This rule will only match if the LHS is
>
>         f (WriterT w Identity) ($fMonadWriterT w Identity dm $fMonadIdentity)
>
> So it's a nested pattern match.  That makes the LHS match less often; namely only when the dictionary argument to 'f' is an application of $fMonadWriterT, the function that arises from the instance decl
>     instance (Monoid w, Monad m) => Monad (WriterT w m) where

I was expecting that this rule will fire if I use function f in a
larger function of type, say, Monoid w => (Int -> w) -> Writer w ().
But does your finding mean that it will fire less often than this?  (I
tried to see this by myself, but it is difficult for me to test it
because in a small test program, inlining solves everything and I
cannot see the rule firing, and in a large example, I cannot figure
out what is going on from the large core output.)  If so, probably the
SPECIALIZE pragma is not very useful in this case.

> So I hope that explains better what is happening.  If anyone can think of better behaviour, I'm open to suggestions!

I still think that it would be better if the behavior of RULES pragma
is consistent with that of SPECIALIZE pragma, at least to make the
behavior easier to understand.  But if the rule will not fire often
enough, then I do not think that it really matters in practice.

Thanks,
  Tsuyoshi

On Thu, Jul 12, 2012 at 8:41 AM, Simon Peyton-Jones
<simonpj at microsoft.com> wrote:
> The error message is unhelpful.  HEAD reports this:
>
>     Could not deduce (Monoid w) arising from a use of `g'
>     from the context (Monad (WriterT w Identity))
>       bound by the RULE "f->g" at Foo.hs:14:3-14
>     Possible fix: add (Monoid w) to the context of the RULE "f->g"
>     In the expression: g
>     When checking the transformation rule "f->g"
>
> And that is quite right.  On the LHS you have an application
>     f (WriterT w Identity) d
>   where d :: Monad (WriterT w Identity)
>
> Recall that Writer w = WriterT w Identity.
>
> For the rewrite to work you have to rewrite this to
>     g w d'
>   where
>     d' :: Monoid w
>
> Well, how can you get a Monoid w dictionary from a Monad (WriterT w Identity)?
>
>
> I was surprised that the SPECIALISE pragma worked, but here's what it does (you can see with -ddump-rules):
>
>
> ==================== Tidy Core rules ====================
> "SPEC Foo.f" [ALWAYS]
>     forall (@ a) (@ w) ($dMonoid :: Data.Monoid.Monoid w).
>       Foo.f @ a
>             @ (Control.Monad.Trans.Writer.Strict.WriterT
>                  w Data.Functor.Identity.Identity)
>             (Control.Monad.Trans.Writer.Strict.$fMonadWriterT
>                @ w
>                @ Data.Functor.Identity.Identity
>                $dMonoid
>                Data.Functor.Identity.$fMonadIdentity)
>       = Foo.f_f @ a @ w $dMonoid
>
> Ah!  This rule will only match if the LHS is
>
>         f (WriterT w Identity) ($fMonadWriterT w Identity dm $fMonadIdentity)
>
> So it's a nested pattern match.  That makes the LHS match less often; namely only when the dictionary argument to 'f' is an application of $fMonadWriterT, the function that arises from the instance decl
>     instance (Monoid w, Monad m) => Monad (WriterT w m) where
>
> In exchange for matching less often, we now do get access to the (Monoid w) argument.
>
> It is odd that this is inconsistent, I agree.  Here is why. For a RULE, we must have a way to rewrite the LHS to an arbitrarily complicated RHS.  For a SPECIALISE pragma
>     SPECIALISE f :: spec_ty
> where f's type is
>     f :: poly_ty
> we simply ask whether poly_ty is more polymorphic than spec_ty; that is, whether f can appear in a context requiring a value of type spec_ty. If so, we see what arguments f would need to do that, and that's the LHS pattern.
>
>
> So I hope that explains better what is happening.  If anyone can think of better behaviour, I'm open to suggestions!
>
> Simon
>
>
> | -----Original Message-----
> | From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-
> | haskell-users-bounces at haskell.org] On Behalf Of Tsuyoshi Ito
> | Sent: 11 July 2012 04:40
> | To: glasgow-haskell-users at haskell.org
> | Subject: “Ambiguous type variable in the constraint” error in rewrite
> | rule
> |
> | Hello,
> |
> | Why does GHC 7.4.1 reject the rewrite rule in the following code?
> |
> | > module Test where
> | >
> | > import Data.Monoid
> | > import Control.Monad.Writer.Strict
> | >
> | > f :: Monad m => a -> m a
> | > f = return
> | >
> | > g :: Monoid w => a -> Writer w a
> | > g = return
> | >
> | > {-# RULES
> | > "f->g" f = g
> | >   #-}
> |
> | On the line containing the rewrite rule, GHC shows the following error
> | message:
> |
> | Test.hs:13:12:
> |     Ambiguous type variable `w0' in the constraint:
> |       (Monoid w0) arising from a use of `g'
> |     Probable fix: add a type signature that fixes these type
> | variable(s)
> |     In the expression: g
> |     When checking the transformation rule "f->g"
> |
> | Interestingly, the code compiles if the rewrite rule is replaced with
> | the following SPECIALIZE pragma:
> |
> | > {-# SPECIALIZE f :: Monoid w => a -> Writer w a #-}
> |
> | I find this strange because if I am not mistaken, this specialization
> | is handled by using a rewrite rule of the same type as the one which
> | GHC rejects.
> |
> | The following ticket might be related, but I am not sure:
> |     Subclass Specialization in Rewrite Rules
> |     http://hackage.haskell.org/trac/ghc/ticket/6102
> |
> | Best regards,
> |   Tsuyoshi
> |
> | _______________________________________________
> | Glasgow-haskell-users mailing list
> | Glasgow-haskell-users at haskell.org
> | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>