GHC rewrite rule type-checking failure

Next Topic
 
classic Classic list List threaded Threaded
10 messages Options
Reply | Threaded
Open this post in threaded view
|

GHC rewrite rule type-checking failure

Conal Elliott
I'm running into type checking problem with GHC rewrite rules in GHC 8.0.2, illustrated in the code below. The first rule type-checks, but the second triggers the type error mentioned in the comment following the rule definition. I'd expect both rules to type-check, adding the needed constraints to the applicability condition for the rule.

Is GHC's behavior intended (and perhaps necessary), or a bug?

Thanks,  -- Conal

Code (also attached):


{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}

{-# OPTIONS_GHC -Wall #-}

-- Demonstrate a type checking failure with rewrite rules

module RuleFail where

class C k where comp' :: k b c -> k a b -> k a c

instance C (->) where comp' = (.)

-- Late-inlining version to enable rewriting.
comp :: C k => k b c -> k a b -> k a c
comp = comp'
{-# INLINE [0] comp #-}

morph :: (a -> b) -> k a b
morph = error "morph: undefined"

{-# RULES "morph/(.)" morph comp = comp #-}  -- Fine

class D k a where addC' :: k (a,a) a

instance Num a => D (->) a where addC' = uncurry (+)

-- Late-inlining version to enable rewriting.
addC :: D k a => k (a,a) a
addC = addC'
{-# INLINE [0] addC #-}

{-# RULES "morph/addC" morph addC = addC #-}  -- Fail

-- • Could not deduce (D k b) arising from a use of ‘addC’
--   from the context: D (->) b

-- Why does GHC infer the (C k) constraint for the first rule but not (D k b)
-- for the second rule?


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

RuleFail.hs (1K) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: GHC rewrite rule type-checking failure

Joachim Breitner-2
Hi Conal,

The difference is that the LHS of the first rule is mentions the `C k`
constraint (probably unintentionally):

*RuleFail> :t morph comp
morph comp :: C k => k1 (k b c) (k a b -> k a c)

but the LHS of the second rule side does not:

*RuleFail> :t morph addC
morph addC :: Num b => k (b, b) b



A work-around is to add the constraint to `morph`:

    morph :: D k b => (a -> b) -> k a b
    morph = error "morph: undefined"

    but I fear that this work-around is not acceptable to you.

    Joachim

    Am Montag, den 02.10.2017, 14:25 -0700 schrieb Conal Elliott:
    > -- Demonstrate a type checking failure with rewrite rules

>
> module RuleFail where
>
> class C k where comp' :: k b c -> k a b -> k a c
>
> instance C (->) where comp' = (.)
>
> -- Late-inlining version to enable rewriting.
> comp :: C k => k b c -> k a b -> k a c
> comp = comp'
> {-# INLINE [0] comp #-}
>
> morph :: (a -> b) -> k a b
> morph = error "morph: undefined"
>
> {-# RULES "morph/(.)" morph comp = comp #-}  -- Fine


> class D k a where addC' :: k (a,a) a
>
> instance Num a => D (->) a where addC' = uncurry (+)
>
> -- Late-inlining version to enable rewriting.
> addC :: D k a => k (a,a) a
> addC = addC'
> {-# INLINE [0] addC #-}
>
> {-# RULES "morph/addC" morph addC = addC #-}  -- Fail
>
> -- • Could not deduce (D k b) arising from a use of ‘addC’
> --   from the context: D (->) b
>
> -- Why does GHC infer the (C k) constraint for the first rule but not (D k b)
> -- for the second rule?
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
--
Joachim Breitner
  [hidden email]
  http://www.joachim-breitner.de/

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

signature.asc (849 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: GHC rewrite rule type-checking failure

Conal Elliott
Thanks very much for the reply, Joachim.

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.

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?

Regards, -- Conal

``` haskell
{-# OPTIONS_GHC -Wall #-}
-- Demonstrate a type checking failure with rewrite rules

module RuleFail where

class C k where comp' :: k b c -> k a b -> k a c

instance C (->) where comp' = (.)

-- Late-inlining version to enable rewriting.
comp :: C k => k b c -> k a b -> k a c
comp = comp'
{-# INLINE [0] comp #-}

morph :: (a -> b) -> k a b
morph = error "morph: undefined"

{-# RULES "morph/(.)" forall f g. morph (g `comp` f) = morph g `comp` morph f #-}

-- • Could not deduce (C k) arising from a use of ‘comp’
--   from the context: C (->)
--     bound by the RULE "morph/(.)"
```


On Mon, Oct 2, 2017 at 3:52 PM, Joachim Breitner <[hidden email]> wrote:
Hi Conal,

The difference is that the LHS of the first rule is mentions the `C k`
constraint (probably unintentionally):

*RuleFail> :t morph comp
morph comp :: C k => k1 (k b c) (k a b -> k a c)

but the LHS of the second rule side does not:

*RuleFail> :t morph addC
morph addC :: Num b => k (b, b) b



A work-around is to add the constraint to `morph`:

    morph :: D k b => (a -> b) -> k a b
    morph = error "morph: undefined"

    but I fear that this work-around is not acceptable to you.

    Joachim

    Am Montag, den 02.10.2017, 14:25 -0700 schrieb Conal Elliott:
    > -- Demonstrate a type checking failure with rewrite rules
>
> module RuleFail where
>
> class C k where comp' :: k b c -> k a b -> k a c
>
> instance C (->) where comp' = (.)
>
> -- Late-inlining version to enable rewriting.
> comp :: C k => k b c -> k a b -> k a c
> comp = comp'
> {-# INLINE [0] comp #-}
>
> morph :: (a -> b) -> k a b
> morph = error "morph: undefined"
>
> {-# RULES "morph/(.)" morph comp = comp #-}  -- Fine



> class D k a where addC' :: k (a,a) a
>
> instance Num a => D (->) a where addC' = uncurry (+)
>
> -- Late-inlining version to enable rewriting.
> addC :: D k a => k (a,a) a
> addC = addC'
> {-# INLINE [0] addC #-}
>
> {-# RULES "morph/addC" morph addC = addC #-}  -- Fail
>
> -- • Could not deduce (D k b) arising from a use of ‘addC’
> --   from the context: D (->) b
>
> -- Why does GHC infer the (C k) constraint for the first rule but not (D k b)
> -- for the second rule?
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
--
Joachim Breitner
  [hidden email]
  http://www.joachim-breitner.de/


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

RuleFail.hs (808 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: GHC rewrite rule type-checking failure

David Feuer
I believe the answer is currently no. As I understand it, the entire instance resolution mechanism drops away after type checking and is therefore not available to the simplifier. So if you need to add a constraint on the RHS of a rule, I think you're mostly out of luck. The only thing I can think of is that you can look at what the specializer does and try to look around to find the right dictionary, but that sounds hard and brittle. OTOH, I'm not an expert, so maybe there's something major I've missed.

On Oct 2, 2017 8:04 PM, "Conal Elliott" <[hidden email]> wrote:
Thanks very much for the reply, Joachim.

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.

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?

Regards, -- Conal

``` haskell
{-# OPTIONS_GHC -Wall #-}
-- Demonstrate a type checking failure with rewrite rules

module RuleFail where

class C k where comp' :: k b c -> k a b -> k a c

instance C (->) where comp' = (.)

-- Late-inlining version to enable rewriting.
comp :: C k => k b c -> k a b -> k a c
comp = comp'
{-# INLINE [0] comp #-}

morph :: (a -> b) -> k a b
morph = error "morph: undefined"

{-# RULES "morph/(.)" forall f g. morph (g `comp` f) = morph g `comp` morph f #-}

-- • Could not deduce (C k) arising from a use of ‘comp’
--   from the context: C (->)
--     bound by the RULE "morph/(.)"
```


On Mon, Oct 2, 2017 at 3:52 PM, Joachim Breitner <[hidden email]> wrote:
Hi Conal,

The difference is that the LHS of the first rule is mentions the `C k`
constraint (probably unintentionally):

*RuleFail> :t morph comp
morph comp :: C k => k1 (k b c) (k a b -> k a c)

but the LHS of the second rule side does not:

*RuleFail> :t morph addC
morph addC :: Num b => k (b, b) b



A work-around is to add the constraint to `morph`:

    morph :: D k b => (a -> b) -> k a b
    morph = error "morph: undefined"

    but I fear that this work-around is not acceptable to you.

    Joachim

    Am Montag, den 02.10.2017, 14:25 -0700 schrieb Conal Elliott:
    > -- Demonstrate a type checking failure with rewrite rules
>
> module RuleFail where
>
> class C k where comp' :: k b c -> k a b -> k a c
>
> instance C (->) where comp' = (.)
>
> -- Late-inlining version to enable rewriting.
> comp :: C k => k b c -> k a b -> k a c
> comp = comp'
> {-# INLINE [0] comp #-}
>
> morph :: (a -> b) -> k a b
> morph = error "morph: undefined"
>
> {-# RULES "morph/(.)" morph comp = comp #-}  -- Fine



> class D k a where addC' :: k (a,a) a
>
> instance Num a => D (->) a where addC' = uncurry (+)
>
> -- Late-inlining version to enable rewriting.
> addC :: D k a => k (a,a) a
> addC = addC'
> {-# INLINE [0] addC #-}
>
> {-# RULES "morph/addC" morph addC = addC #-}  -- Fail
>
> -- • Could not deduce (D k b) arising from a use of ‘addC’
> --   from the context: D (->) b
>
> -- Why does GHC infer the (C k) constraint for the first rule but not (D k b)
> -- for the second rule?
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
--
Joachim Breitner
  [hidden email]
  http://www.joachim-breitner.de/


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

RE: GHC rewrite rule type-checking failure

Haskell - Glasgow-haskell-users mailing list
In reply to this post by Conal Elliott

*   Is it feasible for GHC to combine the constraints needed LHS and RHS to form an applicability condition?

I don’t think so.

 

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.

 

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.

 

One way to see this is to write out the rewrite rule you want, complete with all its dictionary arguments. Can you do that?

 

Simon

 

From: Glasgow-haskell-users [mailto:[hidden email]] On Behalf Of Conal Elliott
Sent: 03 October 2017 01:03
To: Joachim Breitner <[hidden email]>
Cc: [hidden email]
Subject: Re: GHC rewrite rule type-checking failure

 

Thanks very much for the reply, Joachim.

 

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.

 

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?

 

Regards, -- Conal

 

``` haskell

{-# OPTIONS_GHC -Wall #-}

-- Demonstrate a type checking failure with rewrite rules

 

module RuleFail where

 

class C k where comp' :: k b c -> k a b -> k a c

 

instance C (->) where comp' = (.)

 

-- Late-inlining version to enable rewriting.

comp :: C k => k b c -> k a b -> k a c

comp = comp'

{-# INLINE [0] comp #-}

 

morph :: (a -> b) -> k a b

morph = error "morph: undefined"

 

{-# RULES "morph/(.)" forall f g. morph (g `comp` f) = morph g `comp` morph f #-}

 

-- • Could not deduce (C k) arising from a use of ‘comp’

--   from the context: C (->)

--     bound by the RULE "morph/(.)"

```

 

 

On Mon, Oct 2, 2017 at 3:52 PM, Joachim Breitner <[hidden email]> wrote:

Hi Conal,

The difference is that the LHS of the first rule is mentions the `C k`
constraint (probably unintentionally):

*RuleFail> :t morph comp
morph comp :: C k => k1 (k b c) (k a b -> k a c)

but the LHS of the second rule side does not:

*RuleFail> :t morph addC
morph addC :: Num b => k (b, b) b



A work-around is to add the constraint to `morph`:

    morph :: D k b => (a -> b) -> k a b
    morph = error "morph: undefined"

    but I fear that this work-around is not acceptable to you.

    Joachim

    Am Montag, den 02.10.2017, 14:25 -0700 schrieb Conal Elliott:
    > -- Demonstrate a type checking failure with rewrite rules
>
> module RuleFail where
>
> class C k where comp' :: k b c -> k a b -> k a c
>
> instance C (->) where comp' = (.)
>
> -- Late-inlining version to enable rewriting.
> comp :: C k => k b c -> k a b -> k a c
> comp = comp'
> {-# INLINE [0] comp #-}
>
> morph :: (a -> b) -> k a b
> morph = error "morph: undefined"
>
> {-# RULES "morph/(.)" morph comp = comp #-}  -- Fine



> class D k a where addC' :: k (a,a) a
>
> instance Num a => D (->) a where addC' = uncurry (+)
>
> -- Late-inlining version to enable rewriting.
> addC :: D k a => k (a,a) a
> addC = addC'
> {-# INLINE [0] addC #-}
>
> {-# RULES "morph/addC" morph addC = addC #-}  -- Fail
>
> -- • Could not deduce (D k b) arising from a use of ‘addC’
> --   from the context: D (->) b
>
> -- Why does GHC infer the (C k) constraint for the first rule but not (D k b)
> -- for the second rule?
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
--
Joachim Breitner
  [hidden email]
  http://www.joachim-breitner.de/

 


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: GHC rewrite rule type-checking failure

Joachim Breitner-2
In reply to this post by Conal Elliott
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
  [hidden email]
  http://www.joachim-breitner.de/

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

signature.asc (849 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: 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 <[hidden email]> 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
  [hidden email]
  http://www.joachim-breitner.de/


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: GHC rewrite rule type-checking failure

Joachim Breitner-2
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 <[hidden email]> 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
> >   [hidden email]
> >   http://www.joachim-breitner.de/
>
>
--
Joachim Breitner
  [hidden email]
  http://www.joachim-breitner.de/

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

signature.asc (849 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: GHC rewrite rule type-checking failure

Conal Elliott
Thanks for the suggestion, Joachim.

Since I'm writing a core-to-core plugin anyway, it wasn't so hard for me to implement all of these n*m rules (for n operations and m instances) at once via a "built-in" rewrite rule that explicitly manipulates Core expressions. Doing so is probably also considerably more efficient than matching against many rewrite rules (whether generated manually or automatically), at least the way rewrite rule matching is currently implemented. As you & I discussed at ICFP, I'm looking for ways to reduce the complexity of the plugin to make it easier to maintain and extend, and I thought that dictionary synthesis from rewrite rules might be one.

Regards,
-- Conal

On Tue, Oct 3, 2017 at 8:49 AM, Joachim Breitner <[hidden email]> wrote:
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 <[hidden email]> 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
> >   [hidden email]
> >   http://www.joachim-breitner.de/
>
>
--
Joachim Breitner
  [hidden email]
  http://www.joachim-breitner.de/


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: GHC rewrite rule type-checking failure

Joachim Breitner-2
Hi,

I think creating your rules as built-in rules is a good way to go.

You could reduce the complexity somewhat by generating all n*m rules as
“normal” rules in the plugin when you see the instancs. This way, the
plugin does not have to do anything when you want the rule to actually
file (…and maybe the plugin does not have to be loaded at all). But I
am not sure if it is worth the effort. And the built-in rules are more
efficient, as you say.

Greetings,
Joachim

Am Dienstag, den 03.10.2017, 09:01 -0700 schrieb Conal Elliott:

> Thanks for the suggestion, Joachim.
>
> Since I'm writing a core-to-core plugin anyway, it wasn't so hard for
> me to implement all of these n*m rules (for n operations and m
> instances) at once via a "built-in" rewrite rule that explicitly
> manipulates Core expressions. Doing so is probably also considerably
> more efficient than matching against many rewrite rules (whether
> generated manually or automatically), at least the way rewrite rule
> matching is currently implemented. As you & I discussed at ICFP, I'm
> looking for ways to reduce the complexity of the plugin to make it
> easier to maintain and extend, and I thought that dictionary
> synthesis from rewrite rules might be one.
>
> Regards,
> -- Conal
>
> On Tue, Oct 3, 2017 at 8:49 AM, Joachim Breitner <[hidden email]> wrote:
> > 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 <[hidden email]> 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
> > > >   [hidden email]
> > > >   http://www.joachim-breitner.de/
> > >
> > >
> > --
> > Joachim Breitner
> >   [hidden email]
> >   http://www.joachim-breitner.de/
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
--
Joachim Breitner
  [hidden email]
  http://www.joachim-breitner.de/

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

signature.asc (849 bytes) Download Attachment