Thanks very much for the reply, Joachim.
Oops! I flubbed the example. I really `morph` to distribute over an application of `comp`. New code below (and attached). You're right that I wouldn't want to restrict the type of `morph`, since each `morph` *rule* imposes its own restrictions.
My questions:
* Is it feasible for GHC to combine the constraints needed LHS and RHS to form an applicability condition?
* Is there any way I can make the needed constraints explicit in my rewrite rules?
* Are there any other work-arounds that would enable writing such RHS-constrained rules?
Regards, -- Conal
``` haskell
{-# OPTIONS_GHC -Wall #-}
-- Demonstrate a type checking failure with rewrite rules
module RuleFail where
class C k where comp' :: k b c -> k a b -> k a c
instance C (->) where comp' = (.)
-- Late-inlining version to enable rewriting.
comp :: C k => k b c -> k a b -> k a c
comp = comp'
{-# INLINE [0] comp #-}
morph :: (a -> b) -> k a b
morph = error "morph: undefined"
{-# RULES "morph/(.)" forall f g. morph (g `comp` f) = morph g `comp` morph f #-}
-- • Could not deduce (C k) arising from a use of ‘comp’
-- from the context: C (->)
-- bound by the RULE "morph/(.)"
```