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 <m...@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 > m...@joachim-breitner.de > http://www.joachim-breitner.de/ >
RuleFail.hs
Description: Binary data
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users