“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

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@haskell.org [mailto:glasgow- | haskell-users-bounces@haskell.org] On Behalf Of Tsuyoshi Ito | Sent: 11 July 2012 04:40 | To: glasgow-haskell-users@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@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

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
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@haskell.org [mailto:glasgow- | haskell-users-bounces@haskell.org] On Behalf Of Tsuyoshi Ito | Sent: 11 July 2012 04:40 | To: glasgow-haskell-users@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@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

| > 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? It probably should fire in that situation, but it's delicate, because it relies on the argument looking exactly like f (WriterT w Identity) ($fMonadWriterT w Identity dm $fMonadIdentity) and it's hard to know whether it will look exactly like that. It's also not immediately clear that this specialisation is a big win, is it? |(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 You can stop "inlining solving everything" in a small test using {-# NOINLINE #-}. Simon
participants (2)
-
Simon Peyton-Jones
-
Tsuyoshi Ito