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

[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 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