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
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/