<div dir="ltr"><div>Thanks very much for the reply, Joachim.</div><div><br></div><div>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.</div><div><br></div><div>My questions:</div><div><br></div><div>* Is it feasible for GHC to combine the constraints needed LHS and RHS to form an applicability condition?</div><div>* Is there any way I can make the needed constraints explicit in my rewrite rules?</div><div>* Are there any other work-arounds that would enable writing such RHS-constrained rules?</div><div><br></div><div>Regards, -- Conal</div><div><br></div><div>``` haskell</div><div><font face="monospace, monospace">{-# OPTIONS_GHC -Wall #-}</font></div><div><font face="monospace, monospace">-- Demonstrate a type checking failure with rewrite rules</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">module RuleFail where</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">class C k where comp' :: k b c -> k a b -> k a c</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">instance C (->) where comp' = (.)</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">-- Late-inlining version to enable rewriting.</font></div><div><font face="monospace, monospace">comp :: C k => k b c -> k a b -> k a c</font></div><div><font face="monospace, monospace">comp = comp'</font></div><div><font face="monospace, monospace">{-# INLINE [0] comp #-}</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">morph :: (a -> b) -> k a b</font></div><div><font face="monospace, monospace">morph = error "morph: undefined"</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">{-# RULES "morph/(.)" forall f g. morph (g `comp` f) = morph g `comp` morph f #-}</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">-- • Could not deduce (C k) arising from a use of ‘comp’</font></div><div><font face="monospace, monospace">-- from the context: C (->)</font></div><div><font face="monospace, monospace">-- bound by the RULE "morph/(.)"</font></div><div>```</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Oct 2, 2017 at 3:52 PM, Joachim Breitner <span dir="ltr"><<a href="mailto:mail@joachim-breitner.de" target="_blank">mail@joachim-breitner.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Conal,<br>
<br>
The difference is that the LHS of the first rule is mentions the `C k`<br>
constraint (probably unintentionally):<br>
<br>
*RuleFail> :t morph comp<br>
morph comp :: C k => k1 (k b c) (k a b -> k a c)<br>
<br>
but the LHS of the second rule side does not:<br>
<br>
*RuleFail> :t morph addC<br>
morph addC :: Num b => k (b, b) b<br>
<br>
<br>
<br>
A work-around is to add the constraint to `morph`:<br>
<br>
morph :: D k b => (a -> b) -> k a b<br>
<span class=""> morph = error "morph: undefined"<br>
<br>
</span> but I fear that this work-around is not acceptable to you.<br>
<br>
Joachim<br>
<span class=""><br>
Am Montag, den 02.10.2017, 14:25 -0700 schrieb Conal Elliott:<br>
> -- Demonstrate a type checking failure with rewrite rules<br>
><br>
> module RuleFail where<br>
><br>
> class C k where comp' :: k b c -> k a b -> k a c<br>
><br>
> instance C (->) where comp' = (.)<br>
><br>
> -- Late-inlining version to enable rewriting.<br>
> comp :: C k => k b c -> k a b -> k a c<br>
> comp = comp'<br>
> {-# INLINE [0] comp #-}<br>
><br>
> morph :: (a -> b) -> k a b<br>
> morph = error "morph: undefined"<br>
><br>
> {-# RULES "morph/(.)" morph comp = comp #-} -- Fine<br>
<br>
<br>
<br>
> class D k a where addC' :: k (a,a) a<br>
><br>
> instance Num a => D (->) a where addC' = uncurry (+)<br>
><br>
> -- Late-inlining version to enable rewriting.<br>
> addC :: D k a => k (a,a) a<br>
> addC = addC'<br>
> {-# INLINE [0] addC #-}<br>
><br>
> {-# RULES "morph/addC" morph addC = addC #-} -- Fail<br>
><br>
> -- • Could not deduce (D k b) arising from a use of ‘addC’<br>
> -- from the context: D (->) b<br>
><br>
> -- Why does GHC infer the (C k) constraint for the first rule but not (D k b)<br>
> -- for the second rule?<br>
><br>
</span>> ______________________________<wbr>_________________<br>
> Glasgow-haskell-users mailing list<br>
> <a href="mailto:Glasgow-haskell-users@haskell.org">Glasgow-haskell-users@haskell.<wbr>org</a><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/glasgow-<wbr>haskell-users</a><br>
<span class="HOEnZb"><font color="#888888">--<br>
Joachim Breitner<br>
<a href="mailto:mail@joachim-breitner.de">mail@joachim-breitner.de</a><br>
<a href="http://www.joachim-breitner.de/" rel="noreferrer" target="_blank">http://www.joachim-breitner.<wbr>de/</a><br>
</font></span></blockquote></div><br></div>