GHC rewrite rules with class constraints

Question

I've added the following rewrite rule to conduit without issue:

{-# RULES "ConduitM: lift x >>= f" forall m f.
    lift m >>= f = ConduitM (PipeM (liftM (unConduitM . f) m))
  #-}

I'm trying to add a similar rewrite rules for liftIO as well

{-# RULES "ConduitM: liftIO x >>= f" forall m f.
    liftIO m >>= f = ConduitM (PipeM (liftM (unConduitM . f) (liftIO m)))
  #-}

However, when I try to do so, I get the following error messages from GHC:

Data/Conduit/Internal/Conduit.hs:1025:84:
    Could not deduce (Monad m) arising from a use of ‘liftM’
    from the context (Monad (ConduitM i o m), MonadIO (ConduitM i o m))
      bound by the RULE "ConduitM: liftIO x >>= f"
      at Data/Conduit/Internal/Conduit.hs:1025:11-118
    Possible fix:
      add (Monad m) to the context of the RULE "ConduitM: liftIO x >>= f"
    In the first argument of ‘PipeM’, namely
      ‘(liftM (unConduitM . f) (liftIO m))’
    In the first argument of ‘ConduitM’, namely
      ‘(PipeM (liftM (unConduitM . f) (liftIO m)))’
    In the expression:
      ConduitM (PipeM (liftM (unConduitM . f) (liftIO m)))

Data/Conduit/Internal/Conduit.hs:1025:108:
    Could not deduce (MonadIO m) arising from a use of ‘liftIO’
    from the context (Monad (ConduitM i o m), MonadIO (ConduitM i o m))
      bound by the RULE "ConduitM: liftIO x >>= f"
      at Data/Conduit/Internal/Conduit.hs:1025:11-118
    Possible fix:
      add (MonadIO m) to the context of
        the RULE "ConduitM: liftIO x >>= f"
    In the second argument of ‘liftM’, namely ‘(liftIO m)’
    In the first argument of ‘PipeM’, namely
      ‘(liftM (unConduitM . f) (liftIO m))’
    In the first argument of ‘ConduitM’, namely
      ‘(PipeM (liftM (unConduitM . f) (liftIO m)))’

I'm unaware of any syntax that would let me specify such context to a rewrite rule. Is there a way to achieve this?

Bibliophile

Answer 1

You can specify the types of the arguments with constraints in the rule, like

{-# RULES "ConduitM: liftIO x >>= f" forall m (f :: (Monad n, MonadIO n) => CounduitM i o n r).
    liftIO m >>= f = ConduitM (PipeM (liftM (unConduitM . f) (liftIO m)))
  #-}

(I haven't tested it, since I haven't the involved package installed, but as far as I understand the types involved, that should work, I think.)

Tripping

Answer 2

I was trying to figure out how to achieve similar effect of adding a constraint into a rewrite rule. Using the same syntax I was able to get GHC to compile, but apparently, in this case, the rewrite rule will simply never fire.

Here is a simple example:

#!/usr/bin/env stack
-- stack --resolver lts-7.14 exec -- ghc -O -ddump-rule-firings
module Main where

import Prelude as P
import System.Environment (getArgs)


class Num e => Power e where
  (^:) :: Integral a => e -> a -> e

instance Power Double where
  (^:) x y = go 0 1 where
    go n acc | n < y = go (n+1) (acc*x)
             | n > y = go (n-1) (acc/x)
             | otherwise = acc

main :: IO ()
main = do
  [xStr] <- getArgs
  let x = read xStr :: Double
  print (x ^ 24)

{-# RULES
 "1. Test ^" forall (x :: Power x => x) n. x ^ n = x ^: n;
 "2. Test ^" forall x n. (x :: Double) ^ n = x ^: n 
 #-} 

Even if the second rule is removed, first rule will never fire. Here is a similar SO question that answers why it doesn't fire: GHC rewrite rule specialising a function for a type class

Urinal