GHC rewrite rule type-checking failure

[Joachim Breitner]

Hi,

Now that I think about it: You can probably even generate these rules
in a core2core pass that looks for instances of C, and then adds the
rules to the mod_guts. That would solve the problem neatly, I’d say.

Greetings,
Joachim


Am Dienstag, den 03.10.2017, 08:45 -0700 schrieb 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/
> 
> 
-- 
Joachim Breitner
  mail at joachim-breitner.de
  http://www.joachim-breitner.de/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20171003/b5411564/attachment-0001.sig>