[GHC] #7080: Make RULES and SPECIALISE more consistent

[GHC]

#7080: Make RULES and SPECIALISE more consistent
---------------------------------+------------------------------------------
    Reporter:  simonpj           |       Owner:                  
        Type:  bug               |      Status:  new             
    Priority:  normal            |   Milestone:  _|_             
   Component:  Compiler          |     Version:  7.4.2           
    Keywords:                    |          Os:  Unknown/Multiple
Architecture:  Unknown/Multiple  |     Failure:  None/Unknown    
  Difficulty:  Unknown           |    Testcase:                  
   Blockedby:                    |    Blocking:                  
     Related:                    |  
---------------------------------+------------------------------------------
 This [http://www.haskell.org/pipermail/glasgow-haskell-
 users/2012-July/022580.html glasgow-haskell-users email thread] describes
 the inconsistency between RULES and SPECIALISE pragmas. Consider
 {{{
 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  #-}

 {-# SPECIALISE f :: Monoid w => a -> Writer w a #-}
 }}}
 Here, the SPECIALISE pragma is accepted, but the RULE is rejected thus:
 {{{
     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"
 }}}
 Rejecting the RULE 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 exactly
 {{{
 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.  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.

 But
  * It's odd that the behaviour is inconsistent
  * The SPECIALISE rule is pretty fragile, beause it'll only match if the
 argument dictionary is constructed exactly as shown.

 It's not clear to me what, if anything, to do about this, but this ticket
 records the issue.

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7080>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler