GHC rewrite rule type-checking failure

[Conal Elliott]

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.

Regards, - Conal

On Tue, Oct 3, 2017 at 7:52 AM, Joachim Breitner <mail at joachim-breitner.de>
wrote:

> Hi,
>
>
> Am Montag, den 02.10.2017, 17:03 -0700 schrieb Conal Elliott:
> > 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?
>
> if you are fine writing one RULE per _instance_ of C, the following
> works:
>
>
>     {-# LANGUAGE ExplicitForAll, TypeApplications #-}
>     {-# OPTIONS_GHC -Wall #-}
>     module RuleFail where
>     class C k where comp' :: k b c -> k a b -> k a c
>
>     instance C (->) where comp' = (.)
>     instance C (,) where comp' (_,a) (c,_) = (c,a)
>
>     -- Late-inlining version to enable rewriting.
>     comp :: C k => k b c -> k a b -> k a c
>     comp = comp'
>     {-# INLINE [0] comp #-}
>
>     morph :: forall k a b. (a -> b) -> k a b
>     morph _ = error "morph: undefined"
>     {-# NOINLINE morph #-}
>
>     {-# RULES "morph/(.)/->"  forall f g. morph @(->) (g `comp` f) = morph
> g `comp` morph f #-}
>     {-# RULES "morph/(.)/(,)" forall f g. morph @(,) (g `comp` f) =
>     morph g `comp` morph f #-}
>
>
> Let’s look at the rules:
>
>     $ ghc -O -c -ddump-rules RuleFail.hs
>
>     ==================== Tidy Core rules ====================
>     "morph/(.)/(,)" [ALWAYS]
>         forall (@ b)
>                (@ b1)
>                (@ a)
>                ($dC :: C (->))
>                (f :: a -> b)
>                (g :: b -> b1).
>           morph @ (,) @ a @ b1 (comp @ (->) @ b @ b1 @ a $dC g f)
>           = comp
>               @ (,)
>               @ b
>               @ b1
>               @ a
>               $fC(,)
>               (morph @ (,) @ b @ b1 g)
>               (morph @ (,) @ a @ b f)
>     "morph/(.)/->" [ALWAYS]
>         forall (@ b)
>                (@ b1)
>                (@ a)
>                ($dC :: C (->))
>                (f :: a -> b)
>                (g :: b -> b1).
>           morph @ (->) @ a @ b1 (comp @ (->) @ b @ b1 @ a $dC g f)
>           = comp
>               @ (->)
>               @ b
>               @ b1
>               @ a
>               $dC
>               (morph @ (->) @ b @ b1 g)
>               (morph @ (->) @ a @ b f)
>
>     As you can see, by specializing the rule to a specific k, GHC can
>     include the concrete instance dictionary (here, $fC(,)) _in the rule_
>     so it does not have to appear on the LHS. This is pretty much how
>     specialization works.
>
>     Is that a viable work-around for you? It involves boilerplate code, but
>     nothing that cannot be explained in the documentation. (Or maybe TH can
>     create such rules?)
>
>
>     If this idiom turns out to be useful, I wonder if there is a case for
>     -rules specified in type classes that get instantiated upon every
>     instance, e.g.
>
>     class C k where
>         comp' :: k b c -> k a b -> k a c
>         {-# RULES "morph/(.)/(,)" forall f g. morph @k (g `comp` f) =
> morph g `comp` morph f #-}
>
>
>     Greetings,
>     Joachim
>     --
>     Joachim Breitner
>   mail at joachim-breitner.de
>   http://www.joachim-breitner.de/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20171003/a42a3583/attachment.html>