<div dir="ltr"><div>The revised example I gave earlier in the thread:</div><div><br></div><div>``` haskell</div><div>class C k where comp' :: k b c -> k a b -> k a c</div><div><br></div><div>instance C (->) where comp' = (.)</div><div><br></div><div>-- Late-inlining version to enable rewriting.</div><div>comp :: C k => k b c -> k a b -> k a c</div><div>comp = comp'</div><div>{-# INLINE [0] comp #-}</div><div><br></div><div>morph :: (a -> b) -> k a b</div><div>morph = error "morph: undefined"</div><div><br></div><div>{-# RULES "morph/(.)" forall f g. morph (g `comp` f) = morph g `comp` morph f #-}</div><div><br></div><div>-- • Could not deduce (C k) arising from a use of ‘comp’</div><div>-- from the context: C (->)</div><div>-- bound by the RULE "morph/(.)"</div><div>```</div><div><br></div><div>A hypothetical generated Core rule (tweaked slightly from Joachim's note):</div><div><br></div><div>``` haskell</div><div>forall (@ k) (@ b) (@ c) (@ a)</div><div> ($dC :: C (->))</div><div> (f :: a -> b) (g :: b -> c).</div><div> morph @ k @ a @ c (comp @ (->) @ b @ c @ a $dC g f)</div><div> = comp @ k @ b @ c @ a</div><div> $dC'</div><div> (morph @ k @ b @ c g)</div><div> (morph @ k @ a @ b f)</div><div> where</div><div> $dC' :: C k</div><div>```</div><div><br></div><div>The new bit here is that `$dC'` is not found via matching in the LHS, but rather by instance resolution from `k`, which does appear explicitly in the LHS. If `C k` cannot be solved, the rule fails. The "where" clause here lists the dictionary variables to be instantiated by instance resolution rather than matching.</div><div><br></div><div>-- Conal</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Oct 3, 2017 at 8:01 AM, Simon Peyton Jones <span dir="ltr"><<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div lang="EN-GB" link="blue" vlink="purple">
<div class="m_-2421057577520805254WordSection1">
<p class="MsoNormal"><span style="font-size:12.0pt">But synthesising from what?<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt">And currently no: there is no type-class dictionary synthesis after the type checker. Not impossible I suppose, but one more fragility: a rule does not fire because some synthesis thing didn’t happen. Maybe
give an as-simple-as-poss example of what you have in mind, now you understand the situation better? With all the type and dictionary abstractions written explicitly…<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt">S<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt"><u></u> <u></u></span></p>
<div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt">
<div>
<div style="border:none;border-top:solid #e1e1e1 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span lang="EN-US">From:</span></b><span lang="EN-US"> <a href="mailto:conal.elliott@gmail.com" target="_blank">conal.elliott@gmail.com</a> [mailto:<a href="mailto:conal.elliott@gmail.com" target="_blank">conal.elliott@gmail.<wbr>com</a>]
<b>On Behalf Of </b>Conal Elliott<br>
<b>Sent:</b> 03 October 2017 15:56<br>
<b>To:</b> Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>></span></p><div><div class="h5"><br>
<b>Subject:</b> Re: GHC rewrite rule type-checking failure<u></u><u></u></div></div><p></p>
</div>
</div><div><div class="h5">
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
Thanks, Simon. Your explanation make sense to me. Do you think that the rewrite rule mechanism could be enhanced to try synthesizing the needed dictionaries after LHS matching and before RHS instantiation? I'm doing as much now in my compiling-to-categories
plugin, but without the convenience of using concrete syntax for the rules.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
Regard, - Conal<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
On Tue, Oct 3, 2017 at 12:27 AM, Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>> wrote:<u></u><u></u></p>
<blockquote style="border:none;border-left:solid #cccccc 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt">* Is it feasible for GHC to combine the constraints needed LHS and RHS to form an applicability condition?<u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:12.0pt">I don’t think so.</span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:12.0pt"> </span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:12.0pt">Remember that a rewrite rule literally rewrites LHS to RHS. It does not conjure up any new dictionaries out of thin air. In your example, (D k b)
is needed in the result of the rewrite. Where can it come from? Only from something matched on the left.</span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:12.0pt"> </span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:12.0pt">So GHC treats any dictionaries matched on the left as “givens” and tries to solve the ones matched on the left. If it fails you get the sort of error
you see.</span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:12.0pt"> </span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:12.0pt">One way to see this is to write out the rewrite rule you want, complete with all its dictionary arguments. Can you do that?</span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:12.0pt"> </span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:12.0pt">Simon</span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:12.0pt"> </span><u></u><u></u></p>
<div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt">
<div>
<div style="border:none;border-top:solid #e1e1e1 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span lang="EN-US">From:</span></b><span lang="EN-US"> Glasgow-haskell-users [mailto:<a href="mailto:glasgow-haskell-users-bounces@haskell.org" target="_blank">glasgow-haskell-users-<wbr>bounces@haskell.org</a>]
<b>On Behalf Of </b>Conal Elliott<br>
<b>Sent:</b> 03 October 2017 01:03<br>
<b>To:</b> Joachim Breitner <<a href="mailto:mail@joachim-breitner.de" target="_blank">mail@joachim-breitner.de</a>><br>
<b>Cc:</b> <a href="mailto:glasgow-haskell-users@haskell.org" target="_blank">glasgow-haskell-users@haskell.<wbr>org</a><br>
<b>Subject:</b> Re: GHC rewrite rule type-checking failure</span><u></u><u></u></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <u></u><u></u></p>
<div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt">Thanks very much for the reply, Joachim.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt">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.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt">My questions:<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt">* Is it feasible for GHC to combine the constraints needed LHS and RHS to form an applicability condition?<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt">* Is there any way I can make the needed constraints explicit in my rewrite rules?<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt">* Are there any other work-arounds that would enable writing such RHS-constrained rules?<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt">Regards, -- Conal<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt">``` haskell<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"><span style="font-family:"Courier New"">{-# OPTIONS_GHC -Wall #-}</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"><span style="font-family:"Courier New"">-- Demonstrate a type checking failure with rewrite rules</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"><span style="font-family:"Courier New"">module RuleFail where</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"><span style="font-family:"Courier New"">class C k where comp' :: k b c -> k a b -> k a c</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"><span style="font-family:"Courier New"">instance C (->) where comp' = (.)</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"><span style="font-family:"Courier New"">-- Late-inlining version to enable rewriting.</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"><span style="font-family:"Courier New"">comp :: C k => k b c -> k a b -> k a c</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"><span style="font-family:"Courier New"">comp = comp'</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"><span style="font-family:"Courier New"">{-# INLINE [0] comp #-}</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"><span style="font-family:"Courier New"">morph :: (a -> b) -> k a b</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"><span style="font-family:"Courier New"">morph = error "morph: undefined"</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"><span style="font-family:"Courier New"">{-# RULES "morph/(.)" forall f g. morph (g `comp` f) = morph g `comp` morph f #-}</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"><span style="font-family:"Courier New"">-- • Could not deduce (C k) arising from a use of ‘comp’</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"><span style="font-family:"Courier New"">-- from the context: C (->)</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"><span style="font-family:"Courier New"">-- bound by the RULE "morph/(.)"</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt">```<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"> <u></u><u></u></p>
</div>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"> <u></u><u></u></p>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt">On Mon, Oct 2, 2017 at 3:52 PM, Joachim Breitner <<a href="mailto:mail@joachim-breitner.de" target="_blank">mail@joachim-breitner.de</a>> wrote:<u></u><u></u></p>
<blockquote style="border:none;border-left:solid #cccccc 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-top:5.0pt;margin-right:0cm;margin-bottom:5.0pt">
<p class="MsoNormal" style="margin-bottom:6.0pt">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>
morph = error "morph: undefined"<br>
<br>
but I fear that this work-around is not acceptable to you.<br>
<br>
Joachim<br>
<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>
> ______________________________<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="https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fglasgow-haskell-users&data=02%7C01%7Csimonpj%40microsoft.com%7C3da5c75572694bab31aa08d509f25936%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636425858847457302&sdata=6dcqjyAYmKXKwZzQQExmWl1cJlCySmP1EvdjA03O19M%3D&reserved=0" target="_blank">
http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/glasgow-<wbr>haskell-users</a><br>
<span class="m_-2421057577520805254m-8194542347041746917hoenzb"><span style="color:#888888">--</span></span><span style="color:#888888"><br>
<span class="m_-2421057577520805254m-8194542347041746917hoenzb">Joachim Breitner</span><br>
<span class="m_-2421057577520805254m-8194542347041746917hoenzb"> <a href="mailto:mail@joachim-breitner.de" target="_blank">
mail@joachim-breitner.de</a></span><br>
<span class="m_-2421057577520805254m-8194542347041746917hoenzb"> <a href="https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joachim-breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7C3da5c75572694bab31aa08d509f25936%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636425858847457302&sdata=Uoe%2Bw8T3VMFLRsFY%2B8nacXIV0pUQOyCe4iHz%2FS5kGrA%3D&reserved=0" target="_blank">
http://www.joachim-breitner.<wbr>de/</a></span></span><u></u><u></u></p>
</blockquote>
</div>
<p class="MsoNormal" style="margin-bottom:6.0pt"> <u></u><u></u></p>
</div>
</div>
</div>
</div>
</div>
</div>
</blockquote>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
</div></div></div>
</div>
</div>
</blockquote></div><br></div>