<div dir="auto">I believe the answer is currently no. As I understand it, the entire instance resolution mechanism drops away after type checking and is therefore not available to the simplifier. So if you need to add a constraint on the RHS of a rule, I think you're mostly out of luck. The only thing I can think of is that you can look at what the specializer does and try to look around to find the right dictionary, but that sounds hard and brittle. OTOH, I'm not an expert, so maybe there's something major I've missed.</div><div class="gmail_extra"><br><div class="gmail_quote">On Oct 2, 2017 8:04 PM, "Conal Elliott" <<a href="mailto:conal@conal.net">conal@conal.net</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><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> morph = error "morph: undefined"<br>
<br>
</span> but I fear that this work-around is not acceptable to you.<br>
<br>
Joachim<br>
<span><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" target="_blank">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-bi<wbr>n/mailman/listinfo/glasgow-has<wbr>kell-users</a><br>
<span class="m_7631919057000341027HOEnZb"><font color="#888888">--<br>
Joachim Breitner<br>
<a href="mailto:mail@joachim-breitner.de" target="_blank">mail@joachim-breitner.de</a><br>
<a href="http://www.joachim-breitner.de/" rel="noreferrer" target="_blank">http://www.joachim-breitner.de<wbr>/</a><br>
</font></span></blockquote></div><br></div>
<br>______________________________<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>
<br></blockquote></div></div>