GHC rewrite rule type-checking failure

[Joachim Breitner]

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 --------------
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/98a7763a/attachment.sig>