RE: GHC rewrite rule type-checking failure

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

RE: GHC rewrite rule type-checking failure

GHC - devs mailing list

But synthesising from what?

 

And currently no: there is no type-class dictionary synthesis after the type checker.  Not impossible I suppose, but one more fragility: a rule does not fire because some synthesis thing didn’t happen.    Maybe give an as-simple-as-poss example of what you have in mind, now you understand the situation better?   With all the type and dictionary abstractions written explicitly…

 

S

 

From: [hidden email] [mailto:[hidden email]] On Behalf Of Conal Elliott
Sent: 03 October 2017 15:56
To: Simon Peyton Jones <[hidden email]>
Subject: Re: GHC rewrite rule type-checking failure

 

Thanks, Simon. Your explanation make sense to me. Do you think that the rewrite rule mechanism could be enhanced to try synthesizing the needed dictionaries after LHS matching and before RHS instantiation? I'm doing as much now in my compiling-to-categories plugin, but without the convenience of using concrete syntax for the rules.

 

Regard, - Conal

 

 

On Tue, Oct 3, 2017 at 12:27 AM, Simon Peyton Jones <[hidden email]> wrote:

*   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/

 

 


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

Re: GHC rewrite rule type-checking failure

Conal Elliott
The revised example I gave earlier in the thread:

``` haskell
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/(.)"
```

A hypothetical generated Core rule (tweaked slightly from Joachim's note):

``` haskell
forall (@ k) (@ b) (@ c) (@ a)
       ($dC :: C (->))
       (f :: a -> b) (g :: b -> c).
  morph @ k @ a @ c (comp @ (->) @ b @ c @ a $dC g f)
  = comp @ k @ b @ c @ a
      $dC'
      (morph @ k @ b @ c g)
      (morph @ k @ a @ b f)
 where
   $dC' :: C k
```

The new bit here is that `$dC'` is not found via matching in the LHS, but rather by instance resolution from `k`, which does appear explicitly in the LHS. If `C k` cannot be solved, the rule fails. The "where" clause here lists the dictionary variables to be instantiated by instance resolution rather than matching.

-- Conal


On Tue, Oct 3, 2017 at 8:01 AM, Simon Peyton Jones <[hidden email]> wrote:

But synthesising from what?

 

And currently no: there is no type-class dictionary synthesis after the type checker.  Not impossible I suppose, but one more fragility: a rule does not fire because some synthesis thing didn’t happen.    Maybe give an as-simple-as-poss example of what you have in mind, now you understand the situation better?   With all the type and dictionary abstractions written explicitly…

 

S

 

From: [hidden email] [mailto:[hidden email]] On Behalf Of Conal Elliott
Sent: 03 October 2017 15:56
To: Simon Peyton Jones <[hidden email]>


Subject: Re: GHC rewrite rule type-checking failure

 

Thanks, Simon. Your explanation make sense to me. Do you think that the rewrite rule mechanism could be enhanced to try synthesizing the needed dictionaries after LHS matching and before RHS instantiation? I'm doing as much now in my compiling-to-categories plugin, but without the convenience of using concrete syntax for the rules.

 

Regard, - Conal

 

 

On Tue, Oct 3, 2017 at 12:27 AM, Simon Peyton Jones <[hidden email]> wrote:

*   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/

 

 



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

RE: GHC rewrite rule type-checking failure

GHC - devs mailing list
In reply to this post by GHC - devs mailing list

The new bit here is that `$dC'` is not found via matching in the LHS, but rather by instance resolution from `k`, which does appear explicitly in the LHS

 

Well this would be something qualitatively new.  We don’t that ability in rules; and it’s far from clear to me what it would mean anyway.  I suppose that if k was instantiated to a ground type then you might hope to solve it, but what if it was instantiated to some in-scope type variable t, and some variable of type (C t) was in scope.  Should that work too?

 

I’m highly dubious.

 

Happily it sounds as if you are making progress with help from Joachim.

 

Simon

 

From: [hidden email] [mailto:[hidden email]] On Behalf Of Conal Elliott
Sent: 03 October 2017 16:30
To: Simon Peyton Jones <[hidden email]>
Subject: Re: GHC rewrite rule type-checking failure

 

 

The revised example I gave earlier in the thread:

 

``` haskell

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/(.)"

```

 

A hypothetical generated Core rule (tweaked slightly from Joachim's note):

 

``` haskell

forall (@ k) (@ b) (@ c) (@ a)

       ($dC :: C (->))

       (f :: a -> b) (g :: b -> c).

  morph @ k @ a @ c (comp @ (->) @ b @ c @ a $dC g f)

  = comp @ k @ b @ c @ a

      $dC'

      (morph @ k @ b @ c g)

      (morph @ k @ a @ b f)

 where

   $dC' :: C k

```

 

The new bit here is that `$dC'` is not found via matching in the LHS, but rather by instance resolution from `k`, which does appear explicitly in the LHS. If `C k` cannot be solved, the rule fails. The "where" clause here lists the dictionary variables to be instantiated by instance resolution rather than matching.

 

-- Conal

 

 

On Tue, Oct 3, 2017 at 8:01 AM, Simon Peyton Jones <[hidden email]> wrote:

But synthesising from what?

 

And currently no: there is no type-class dictionary synthesis after the type checker.  Not impossible I suppose, but one more fragility: a rule does not fire because some synthesis thing didn’t happen.    Maybe give an as-simple-as-poss example of what you have in mind, now you understand the situation better?   With all the type and dictionary abstractions written explicitly…

 

S

 

From: [hidden email] [mailto:[hidden email]] On Behalf Of Conal Elliott
Sent: 03 October 2017 15:56
To: Simon Peyton Jones <[hidden email]>


Subject: Re: GHC rewrite rule type-checking failure

 

Thanks, Simon. Your explanation make sense to me. Do you think that the rewrite rule mechanism could be enhanced to try synthesizing the needed dictionaries after LHS matching and before RHS instantiation? I'm doing as much now in my compiling-to-categories plugin, but without the convenience of using concrete syntax for the rules.

 

Regard, - Conal

 

 

On Tue, Oct 3, 2017 at 12:27 AM, Simon Peyton Jones <[hidden email]> wrote:

*   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/

 

 

 


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

Re: GHC rewrite rule type-checking failure

Conal Elliott
Thanks for the helpful reply, Simon!

> > The new bit here is that `$dC'` is not found via matching in the LHS, but
> > rather by instance resolution from `k`, which does appear explicitly in
> > the LHS
 
> Well this would be something qualitatively new. We don’t that ability in
> rules; and it’s far from clear to me what it would mean anyway. I suppose
> that if k was instantiated to a ground type then you might hope to solve it,
> but what if it was instantiated to some in-scope type variable t, and some
> variable of type (C t) was in scope. Should that work too?

Yes, we'd want to use in-scope dictionary variables to help solve the needed
constraints in the presence of polymorphism. I've run into exactly this need
in my own manually programmed ("built-in") rewrite rules. Would it be possible
to do so (without deep/pervasive changes to GHC)?

> Happily it sounds as if you are making progress with help from Joachim.

No, I think Joachim agrees that it's impractical to write all of the needed
rule specializations, and that generating then programmatically would be less
convenient than the implementing the built-in rules as I do now.

Cheers, -- Conal

On Wed, Oct 4, 2017 at 2:08 AM, Simon Peyton Jones <[hidden email]> wrote:

The new bit here is that `$dC'` is not found via matching in the LHS, but rather by instance resolution from `k`, which does appear explicitly in the LHS

 

Well this would be something qualitatively new.  We don’t that ability in rules; and it’s far from clear to me what it would mean anyway.  I suppose that if k was instantiated to a ground type then you might hope to solve it, but what if it was instantiated to some in-scope type variable t, and some variable of type (C t) was in scope.  Should that work too?

 

I’m highly dubious.

 

Happily it sounds as if you are making progress with help from Joachim.

 

Simon

 

From: [hidden email] [mailto:[hidden email]] On Behalf Of Conal Elliott
Sent: 03 October 2017 16:30
To: Simon Peyton Jones <[hidden email]>
Subject: Re: GHC rewrite rule type-checking failure

 

 

The revised example I gave earlier in the thread:

 

``` haskell

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/(.)"

```

 

A hypothetical generated Core rule (tweaked slightly from Joachim's note):

 

``` haskell

forall (@ k) (@ b) (@ c) (@ a)

       ($dC :: C (->))

       (f :: a -> b) (g :: b -> c).

  morph @ k @ a @ c (comp @ (->) @ b @ c @ a $dC g f)

  = comp @ k @ b @ c @ a

      $dC'

      (morph @ k @ b @ c g)

      (morph @ k @ a @ b f)

 where

   $dC' :: C k

```

 

The new bit here is that `$dC'` is not found via matching in the LHS, but rather by instance resolution from `k`, which does appear explicitly in the LHS. If `C k` cannot be solved, the rule fails. The "where" clause here lists the dictionary variables to be instantiated by instance resolution rather than matching.

 

-- Conal

 

 

On Tue, Oct 3, 2017 at 8:01 AM, Simon Peyton Jones <[hidden email]> wrote:

But synthesising from what?

 

And currently no: there is no type-class dictionary synthesis after the type checker.  Not impossible I suppose, but one more fragility: a rule does not fire because some synthesis thing didn’t happen.    Maybe give an as-simple-as-poss example of what you have in mind, now you understand the situation better?   With all the type and dictionary abstractions written explicitly…

 

S

 

From: [hidden email] [mailto:[hidden email]] On Behalf Of Conal Elliott
Sent: 03 October 2017 15:56
To: Simon Peyton Jones <[hidden email]>


Subject: Re: GHC rewrite rule type-checking failure

 

Thanks, Simon. Your explanation make sense to me. Do you think that the rewrite rule mechanism could be enhanced to try synthesizing the needed dictionaries after LHS matching and before RHS instantiation? I'm doing as much now in my compiling-to-categories plugin, but without the convenience of using concrete syntax for the rules.

 

Regard, - Conal

 

 

On Tue, Oct 3, 2017 at 12:27 AM, Simon Peyton Jones <[hidden email]> wrote:

*   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/

 

 

 



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

Re: GHC rewrite rule type-checking failure

Conal Elliott
For now, I'm trying to determine whether it possible to use the in-scope dictionary variables for constraint solving from a built-in rewrite rule. I guess (unsure) my question is how to set up a call to `solveWanteds` to take those variables into account when solving a given constraint/predicate.

On Thu, Oct 12, 2017 at 11:07 AM, Conal Elliott <[hidden email]> wrote:
Thanks for the helpful reply, Simon!

> > The new bit here is that `$dC'` is not found via matching in the LHS, but
> > rather by instance resolution from `k`, which does appear explicitly in
> > the LHS
 
> Well this would be something qualitatively new. We don’t that ability in
> rules; and it’s far from clear to me what it would mean anyway. I suppose
> that if k was instantiated to a ground type then you might hope to solve it,
> but what if it was instantiated to some in-scope type variable t, and some
> variable of type (C t) was in scope. Should that work too?

Yes, we'd want to use in-scope dictionary variables to help solve the needed
constraints in the presence of polymorphism. I've run into exactly this need
in my own manually programmed ("built-in") rewrite rules. Would it be possible
to do so (without deep/pervasive changes to GHC)?

> Happily it sounds as if you are making progress with help from Joachim.

No, I think Joachim agrees that it's impractical to write all of the needed
rule specializations, and that generating then programmatically would be less
convenient than the implementing the built-in rules as I do now.

Cheers, -- Conal

On Wed, Oct 4, 2017 at 2:08 AM, Simon Peyton Jones <[hidden email]> wrote:

The new bit here is that `$dC'` is not found via matching in the LHS, but rather by instance resolution from `k`, which does appear explicitly in the LHS

 

Well this would be something qualitatively new.  We don’t that ability in rules; and it’s far from clear to me what it would mean anyway.  I suppose that if k was instantiated to a ground type then you might hope to solve it, but what if it was instantiated to some in-scope type variable t, and some variable of type (C t) was in scope.  Should that work too?

 

I’m highly dubious.

 

Happily it sounds as if you are making progress with help from Joachim.

 

Simon

 

From: [hidden email] [mailto:[hidden email]] On Behalf Of Conal Elliott
Sent: 03 October 2017 16:30
To: Simon Peyton Jones <[hidden email]>
Subject: Re: GHC rewrite rule type-checking failure

 

 

The revised example I gave earlier in the thread:

 

``` haskell

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/(.)"

```

 

A hypothetical generated Core rule (tweaked slightly from Joachim's note):

 

``` haskell

forall (@ k) (@ b) (@ c) (@ a)

       ($dC :: C (->))

       (f :: a -> b) (g :: b -> c).

  morph @ k @ a @ c (comp @ (->) @ b @ c @ a $dC g f)

  = comp @ k @ b @ c @ a

      $dC'

      (morph @ k @ b @ c g)

      (morph @ k @ a @ b f)

 where

   $dC' :: C k

```

 

The new bit here is that `$dC'` is not found via matching in the LHS, but rather by instance resolution from `k`, which does appear explicitly in the LHS. If `C k` cannot be solved, the rule fails. The "where" clause here lists the dictionary variables to be instantiated by instance resolution rather than matching.

 

-- Conal

 

 

On Tue, Oct 3, 2017 at 8:01 AM, Simon Peyton Jones <[hidden email]> wrote:

But synthesising from what?

 

And currently no: there is no type-class dictionary synthesis after the type checker.  Not impossible I suppose, but one more fragility: a rule does not fire because some synthesis thing didn’t happen.    Maybe give an as-simple-as-poss example of what you have in mind, now you understand the situation better?   With all the type and dictionary abstractions written explicitly…

 

S

 

From: [hidden email] [mailto:[hidden email]] On Behalf Of Conal Elliott
Sent: 03 October 2017 15:56
To: Simon Peyton Jones <[hidden email]>


Subject: Re: GHC rewrite rule type-checking failure

 

Thanks, Simon. Your explanation make sense to me. Do you think that the rewrite rule mechanism could be enhanced to try synthesizing the needed dictionaries after LHS matching and before RHS instantiation? I'm doing as much now in my compiling-to-categories plugin, but without the convenience of using concrete syntax for the rules.

 

Regard, - Conal

 

 

On Tue, Oct 3, 2017 at 12:27 AM, Simon Peyton Jones <[hidden email]> wrote:

*   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/

 

 

 




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

RE: GHC rewrite rule type-checking failure

GHC - devs mailing list

For now, I'm trying to determine whether it possible to use the in-scope dictionary variables for constraint solving from a built-in rewrite rule.

 

It would not take deep, pervasive changes.  

 

I suggest that you do /not/ call solveWanteds, but instead make a custom constraint solver.  The constraint solver in the type checker is profoundly influenced by

  • The need to discover suitable instantiations for unification variables
  • The need to generate good error messages
  • The need for nested implication constraints to handle GADTs, skolem escape checks etc

The type checker’s monad is full of junk that you don’t need or want in this simpler context.  Just look at TcRnTypes.TcGblEnv and TcLclEnv.

 

I think you don’t need either of those things here.    I think you probably only want type-class constraints, not equalities (which add a great deal of complexity).

 

You just want to say

  • I’m trying to solve Eq [a].  Ah I have an instance for that.
  • I’m trying to solve Eq a.  Ah, I have an in-scope Id with that type.

In fact, we already have something a bit like this, for ground class constraints.  See TcInteract.shortCutSolver, and Note [Shortcut solving] in that file.  So it’s not hard.   [Mumble mumble: instance decls with variables not bound in the head might be a problem.  But I doubt that’s what you want.]

 

Other thoughts

  • To make this work you’d need access to the top-level class instances in rules.  That’s a change but not a difficult one.  The simplifier already carries around the top-level type-family instances, so you could add the class instances in a similar way..
  • I’m more concerned about how you’d express all this in the concrete syntax of a RULE.  Maybe you don’t need to do that?  It’s all generated thorough the API?
  • Even if you don’t need concrete syntax, you’d still need abstract syntax, some change to the CoreRule data type.  And I’m not sure what exactly that is.

 

I’m unlikely to do all of this myself, but I’m happy advise; but without making a prior commitment to incorporating the result in GHC.  We’d have to see how it goes.

 

Simon

 

From: [hidden email] [mailto:[hidden email]] On Behalf Of Conal Elliott
Sent: 12 October 2017 20:02
To: Simon Peyton Jones <[hidden email]>
Cc: [hidden email]
Subject: Re: GHC rewrite rule type-checking failure

 

For now, I'm trying to determine whether it possible to use the in-scope dictionary variables for constraint solving from a built-in rewrite rule. I guess (unsure) my question is how to set up a call to `solveWanteds` to take those variables into account when solving a given constraint/predicate.

 

On Thu, Oct 12, 2017 at 11:07 AM, Conal Elliott <[hidden email]> wrote:

Thanks for the helpful reply, Simon!

 

> > The new bit here is that `$dC'` is not found via matching in the LHS, but

> > rather by instance resolution from `k`, which does appear explicitly in

> > the LHS

 

> Well this would be something qualitatively new. We don’t that ability in

> rules; and it’s far from clear to me what it would mean anyway. I suppose

> that if k was instantiated to a ground type then you might hope to solve it,

> but what if it was instantiated to some in-scope type variable t, and some

> variable of type (C t) was in scope. Should that work too?

 

Yes, we'd want to use in-scope dictionary variables to help solve the needed

constraints in the presence of polymorphism. I've run into exactly this need

in my own manually programmed ("built-in") rewrite rules. Would it be possible

to do so (without deep/pervasive changes to GHC)?

 

> Happily it sounds as if you are making progress with help from Joachim.

 

No, I think Joachim agrees that it's impractical to write all of the needed

rule specializations, and that generating then programmatically would be less

convenient than the implementing the built-in rules as I do now.

 

Cheers, -- Conal

 

On Wed, Oct 4, 2017 at 2:08 AM, Simon Peyton Jones <[hidden email]> wrote:

The new bit here is that `$dC'` is not found via matching in the LHS, but rather by instance resolution from `k`, which does appear explicitly in the LHS

 

Well this would be something qualitatively new.  We don’t that ability in rules; and it’s far from clear to me what it would mean anyway.  I suppose that if k was instantiated to a ground type then you might hope to solve it, but what if it was instantiated to some in-scope type variable t, and some variable of type (C t) was in scope.  Should that work too?

 

I’m highly dubious.

 

Happily it sounds as if you are making progress with help from Joachim.

 

Simon

 

From: [hidden email] [mailto:[hidden email]] On Behalf Of Conal Elliott
Sent: 03 October 2017 16:30
To: Simon Peyton Jones <[hidden email]>
Subject: Re: GHC rewrite rule type-checking failure

 

 

The revised example I gave earlier in the thread:

 

``` haskell

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/(.)"

```

 

A hypothetical generated Core rule (tweaked slightly from Joachim's note):

 

``` haskell

forall (@ k) (@ b) (@ c) (@ a)

       ($dC :: C (->))

       (f :: a -> b) (g :: b -> c).

  morph @ k @ a @ c (comp @ (->) @ b @ c @ a $dC g f)

  = comp @ k @ b @ c @ a

      $dC'

      (morph @ k @ b @ c g)

      (morph @ k @ a @ b f)

 where

   $dC' :: C k

```

 

The new bit here is that `$dC'` is not found via matching in the LHS, but rather by instance resolution from `k`, which does appear explicitly in the LHS. If `C k` cannot be solved, the rule fails. The "where" clause here lists the dictionary variables to be instantiated by instance resolution rather than matching.

 

-- Conal

 

 

On Tue, Oct 3, 2017 at 8:01 AM, Simon Peyton Jones <[hidden email]> wrote:

But synthesising from what?

 

And currently no: there is no type-class dictionary synthesis after the type checker.  Not impossible I suppose, but one more fragility: a rule does not fire because some synthesis thing didn’t happen.    Maybe give an as-simple-as-poss example of what you have in mind, now you understand the situation better?   With all the type and dictionary abstractions written explicitly…

 

S

 

From: [hidden email] [mailto:[hidden email]] On Behalf Of Conal Elliott
Sent: 03 October 2017 15:56
To: Simon Peyton Jones <[hidden email]>


Subject: Re: GHC rewrite rule type-checking failure

 

Thanks, Simon. Your explanation make sense to me. Do you think that the rewrite rule mechanism could be enhanced to try synthesizing the needed dictionaries after LHS matching and before RHS instantiation? I'm doing as much now in my compiling-to-categories plugin, but without the convenience of using concrete syntax for the rules.

 

Regard, - Conal

 

 

On Tue, Oct 3, 2017 at 12:27 AM, Simon Peyton Jones <[hidden email]> wrote:

*   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/

 

 

 

 

 


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

Re: GHC rewrite rule type-checking failure

Conal Elliott
Thanks for the tips, Simon! I'll first try without extending concrete syntax (for a BuiltinRule). Regards, - Conal

On Fri, Oct 13, 2017 at 3:54 AM, Simon Peyton Jones <[hidden email]> wrote:

For now, I'm trying to determine whether it possible to use the in-scope dictionary variables for constraint solving from a built-in rewrite rule.

 

It would not take deep, pervasive changes.  

 

I suggest that you do /not/ call solveWanteds, but instead make a custom constraint solver.  The constraint solver in the type checker is profoundly influenced by

  • The need to discover suitable instantiations for unification variables
  • The need to generate good error messages
  • The need for nested implication constraints to handle GADTs, skolem escape checks etc

The type checker’s monad is full of junk that you don’t need or want in this simpler context.  Just look at TcRnTypes.TcGblEnv and TcLclEnv.

 

I think you don’t need either of those things here.    I think you probably only want type-class constraints, not equalities (which add a great deal of complexity).

 

You just want to say

  • I’m trying to solve Eq [a].  Ah I have an instance for that.
  • I’m trying to solve Eq a.  Ah, I have an in-scope Id with that type.

In fact, we already have something a bit like this, for ground class constraints.  See TcInteract.shortCutSolver, and Note [Shortcut solving] in that file.  So it’s not hard.   [Mumble mumble: instance decls with variables not bound in the head might be a problem.  But I doubt that’s what you want.]

 

Other thoughts

  • To make this work you’d need access to the top-level class instances in rules.  That’s a change but not a difficult one.  The simplifier already carries around the top-level type-family instances, so you could add the class instances in a similar way..
  • I’m more concerned about how you’d express all this in the concrete syntax of a RULE.  Maybe you don’t need to do that?  It’s all generated thorough the API?
  • Even if you don’t need concrete syntax, you’d still need abstract syntax, some change to the CoreRule data type.  And I’m not sure what exactly that is.

 

I’m unlikely to do all of this myself, but I’m happy advise; but without making a prior commitment to incorporating the result in GHC.  We’d have to see how it goes.

 

Simon

 

From: [hidden email] [mailto:[hidden email]] On Behalf Of Conal Elliott
Sent: 12 October 2017 20:02
To: Simon Peyton Jones <[hidden email]>
Cc: [hidden email]


Subject: Re: GHC rewrite rule type-checking failure

 

For now, I'm trying to determine whether it possible to use the in-scope dictionary variables for constraint solving from a built-in rewrite rule. I guess (unsure) my question is how to set up a call to `solveWanteds` to take those variables into account when solving a given constraint/predicate.

 

On Thu, Oct 12, 2017 at 11:07 AM, Conal Elliott <[hidden email]> wrote:

Thanks for the helpful reply, Simon!

 

> > The new bit here is that `$dC'` is not found via matching in the LHS, but

> > rather by instance resolution from `k`, which does appear explicitly in

> > the LHS

 

> Well this would be something qualitatively new. We don’t that ability in

> rules; and it’s far from clear to me what it would mean anyway. I suppose

> that if k was instantiated to a ground type then you might hope to solve it,

> but what if it was instantiated to some in-scope type variable t, and some

> variable of type (C t) was in scope. Should that work too?

 

Yes, we'd want to use in-scope dictionary variables to help solve the needed

constraints in the presence of polymorphism. I've run into exactly this need

in my own manually programmed ("built-in") rewrite rules. Would it be possible

to do so (without deep/pervasive changes to GHC)?

 

> Happily it sounds as if you are making progress with help from Joachim.

 

No, I think Joachim agrees that it's impractical to write all of the needed

rule specializations, and that generating then programmatically would be less

convenient than the implementing the built-in rules as I do now.

 

Cheers, -- Conal

 

On Wed, Oct 4, 2017 at 2:08 AM, Simon Peyton Jones <[hidden email]> wrote:

The new bit here is that `$dC'` is not found via matching in the LHS, but rather by instance resolution from `k`, which does appear explicitly in the LHS

 

Well this would be something qualitatively new.  We don’t that ability in rules; and it’s far from clear to me what it would mean anyway.  I suppose that if k was instantiated to a ground type then you might hope to solve it, but what if it was instantiated to some in-scope type variable t, and some variable of type (C t) was in scope.  Should that work too?

 

I’m highly dubious.

 

Happily it sounds as if you are making progress with help from Joachim.

 

Simon

 

From: [hidden email] [mailto:[hidden email]] On Behalf Of Conal Elliott
Sent: 03 October 2017 16:30
To: Simon Peyton Jones <[hidden email]>
Subject: Re: GHC rewrite rule type-checking failure

 

 

The revised example I gave earlier in the thread:

 

``` haskell

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/(.)"

```

 

A hypothetical generated Core rule (tweaked slightly from Joachim's note):

 

``` haskell

forall (@ k) (@ b) (@ c) (@ a)

       ($dC :: C (->))

       (f :: a -> b) (g :: b -> c).

  morph @ k @ a @ c (comp @ (->) @ b @ c @ a $dC g f)

  = comp @ k @ b @ c @ a

      $dC'

      (morph @ k @ b @ c g)

      (morph @ k @ a @ b f)

 where

   $dC' :: C k

```

 

The new bit here is that `$dC'` is not found via matching in the LHS, but rather by instance resolution from `k`, which does appear explicitly in the LHS. If `C k` cannot be solved, the rule fails. The "where" clause here lists the dictionary variables to be instantiated by instance resolution rather than matching.

 

-- Conal

 

 

On Tue, Oct 3, 2017 at 8:01 AM, Simon Peyton Jones <[hidden email]> wrote:

But synthesising from what?

 

And currently no: there is no type-class dictionary synthesis after the type checker.  Not impossible I suppose, but one more fragility: a rule does not fire because some synthesis thing didn’t happen.    Maybe give an as-simple-as-poss example of what you have in mind, now you understand the situation better?   With all the type and dictionary abstractions written explicitly…

 

S

 

From: [hidden email] [mailto:[hidden email]] On Behalf Of Conal Elliott
Sent: 03 October 2017 15:56
To: Simon Peyton Jones <[hidden email]>


Subject: Re: GHC rewrite rule type-checking failure

 

Thanks, Simon. Your explanation make sense to me. Do you think that the rewrite rule mechanism could be enhanced to try synthesizing the needed dictionaries after LHS matching and before RHS instantiation? I'm doing as much now in my compiling-to-categories plugin, but without the convenience of using concrete syntax for the rules.

 

Regard, - Conal

 

 

On Tue, Oct 3, 2017 at 12:27 AM, Simon Peyton Jones <[hidden email]> wrote:

*   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/

 

 

 

 

 



_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs