Opened 5 years ago

Last modified 5 months ago

#7080 new bug

Make RULES and SPECIALISE more consistent

Reported by: simonpj Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.4.2
Keywords: Specialise Cc: tkn.akio@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Runtime performance bug Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

This 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.

Change History (3)

comment:1 Changed 5 years ago by akio

Cc: tkn.akio@… added

I experienced a situation where I wanted to write rules like this. I think it would be very useful if the rule was accepted, and worked by finding whatever (Monoid w) dictionary that is in scope. But perhaps I am asking too much of the simplifier?

comment:2 Changed 22 months ago by thomie

Type of failure: None/UnknownRuntime performance bug

comment:3 Changed 5 months ago by simonpj

Keywords: Specialise added
Note: See TracTickets for help on using tickets.