<div dir="ltr"><div style="font-size:16px">Hi Joachim. Thanks very much for the suggestions and the `-ddump-rules` view. I wouldn't want to make people write `morph` rules for all combinations of operations (like `(.)`) and categories, but perhaps as you suggest those rules can be generated automatically.<br></div><div style="font-size:16px"><br></div><div style="font-size:16px">Regards, - Conal</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Oct 3, 2017 at 7:52 AM, 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,<br>
<span class=""><br>
<br>
Am Montag, den 02.10.2017, 17:03 -0700 schrieb Conal Elliott:<br>
> My questions:<br>
><br>
> *   Is it feasible for GHC to combine the constraints needed LHS and RHS to form an applicability condition?<br>
> *   Is there any way I can make the needed constraints explicit in my rewrite rules?<br>
> *   Are there any other work-arounds that would enable writing such RHS-constrained rules?<br>
<br>
</span>if you are fine writing one RULE per _instance_ of C, the following<br>
works:<br>
<br>
<br>
    {-# LANGUAGE ExplicitForAll, TypeApplications #-}<br>
    {-# OPTIONS_GHC -Wall #-}<br>
<span class="">    module RuleFail where<br>
    class C k where comp' :: k b c -> k a b -> k a c<br>
<br>
    instance C (->) where comp' = (.)<br>
</span>    instance C (,) where comp' (_,a) (c,_) = (c,a)<br>
<span class=""><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>
</span>    morph :: forall k a b. (a -> b) -> k a b<br>
    morph _ = error "morph: undefined"<br>
    {-# NOINLINE morph #-}<br>
<br>
    {-# RULES "morph/(.)/->"  forall f g. morph @(->) (g `comp` f) = morph g `comp` morph f #-}<br>
    {-# RULES "morph/(.)/(,)" forall f g. morph @(,) (g `comp` f) =<br>
<span class="">    morph g `comp` morph f #-}<br>
<br>
<br>
</span>Let’s look at the rules:<br>
<br>
    $ ghc -O -c -ddump-rules RuleFail.hs<br>
<br>
    ==================== Tidy Core rules ====================<br>
    "morph/(.)/(,)" [ALWAYS]<br>
        forall (@ b)<br>
               (@ b1)<br>
               (@ a)<br>
               ($dC :: C (->))<br>
               (f :: a -> b)<br>
               (g :: b -> b1).<br>
          morph @ (,) @ a @ b1 (comp @ (->) @ b @ b1 @ a $dC g f)<br>
          = comp<br>
              @ (,)<br>
              @ b<br>
              @ b1<br>
              @ a<br>
              $fC(,)<br>
              (morph @ (,) @ b @ b1 g)<br>
              (morph @ (,) @ a @ b f)<br>
    "morph/(.)/->" [ALWAYS]<br>
        forall (@ b)<br>
               (@ b1)<br>
               (@ a)<br>
               ($dC :: C (->))<br>
               (f :: a -> b)<br>
               (g :: b -> b1).<br>
          morph @ (->) @ a @ b1 (comp @ (->) @ b @ b1 @ a $dC g f)<br>
          = comp<br>
              @ (->)<br>
              @ b<br>
              @ b1<br>
              @ a<br>
              $dC<br>
              (morph @ (->) @ b @ b1 g)<br>
              (morph @ (->) @ a @ b f)<br>
<br>
    As you can see, by specializing the rule to a specific k, GHC can<br>
    include the concrete instance dictionary (here, $fC(,)) _in the rule_<br>
    so it does not have to appear on the LHS. This is pretty much how<br>
    specialization works.<br>
<br>
    Is that a viable work-around for you? It involves boilerplate code, but<br>
    nothing that cannot be explained in the documentation. (Or maybe TH can<br>
    create such rules?)<br>
<br>
<br>
    If this idiom turns out to be useful, I wonder if there is a case for<br>
    -rules specified in type classes that get instantiated upon every<br>
    instance, e.g.<br>
<span class=""><br>
    class C k where<br>
        comp' :: k b c -> k a b -> k a c<br>
</span>        {-# RULES "morph/(.)/(,)" forall f g. morph @k (g `comp` f) = morph g `comp` morph f #-}<br>
<br>
<br>
    Greetings,<br>
    Joachim<br>
<div class="HOEnZb"><div class="h5">    --<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>
</div></div></blockquote></div><br></div>