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/(.)" ``` On Mon, Oct 2, 2017 at 3:52 PM, Joachim Breitner <mail@joachim-breitner.de> wrote:
Hi Conal,
The difference is that the LHS of the first rule is mentions the `C k` constraint (probably unintentionally):
*RuleFail> :t morph comp morph comp :: C k => k1 (k b c) (k a b -> k a c)
but the LHS of the second rule side does not:
*RuleFail> :t morph addC morph addC :: Num b => k (b, b) b
A work-around is to add the constraint to `morph`:
morph :: D k b => (a -> b) -> k a b morph = error "morph: undefined"
but I fear that this work-around is not acceptable to you.
Joachim
Am Montag, den 02.10.2017, 14:25 -0700 schrieb Conal Elliott: > -- 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/(.)" morph comp = comp #-} -- Fine
class D k a where addC' :: k (a,a) a
instance Num a => D (->) a where addC' = uncurry (+)
-- Late-inlining version to enable rewriting. addC :: D k a => k (a,a) a addC = addC' {-# INLINE [0] addC #-}
{-# RULES "morph/addC" morph addC = addC #-} -- Fail
-- • Could not deduce (D k b) arising from a use of ‘addC’ -- from the context: D (->) b
-- Why does GHC infer the (C k) constraint for the first rule but not (D k b) -- for the second rule?
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/