GHC rewrite rule type-checking failure

Thu Oct 12 19:02:16 UTC 2017

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 <conal at conal.net> 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 <simonpj at microsoft.com>
> 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:* conal.elliott at gmail.com [mailto:conal.elliott at gmail.com] *On
>> Behalf Of *Conal Elliott
>> *Sent:* 03 October 2017 16:30
>> *To:* Simon Peyton Jones <simonpj at microsoft.com>
>> *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 <simonpj at microsoft.com>
>> 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:* conal.elliott at gmail.com [mailto:conal.elliott at gmail.com] *On
>> Behalf Of *Conal Elliott
>> *Sent:* 03 October 2017 15:56
>> *To:* Simon Peyton Jones <simonpj at microsoft.com>
>>
>>
>> *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 <
>> simonpj at microsoft.com> 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:glasgow-haskell-users-
>> bounces at haskell.org] *On Behalf Of *Conal Elliott
>> *Sent:* 03 October 2017 01:03
>> *To:* Joachim Breitner <mail at joachim-breitner.de>
>> *Cc:* glasgow-haskell-users at haskell.org
>> *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 <
>> mail at joachim-breitner.de> 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
>> > Glasgow-haskell-users at haskell.org
>> > http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>> <https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fglasgow-haskell-users&data=02%7C01%7Csimonpj%40microsoft.com%7C3da5c75572694bab31aa08d509f25936%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636425858847457302&sdata=6dcqjyAYmKXKwZzQQExmWl1cJlCySmP1EvdjA03O19M%3D&reserved=0>
>> --
>> Joachim Breitner
>>   mail at joachim-breitner.de
>>   http://www.joachim-breitner.de/
>> <https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joachim-breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7C3da5c75572694bab31aa08d509f25936%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636425858847457302&sdata=Uoe%2Bw8T3VMFLRsFY%2B8nacXIV0pUQOyCe4iHz%2FS5kGrA%3D&reserved=0>
>>
>>
>>
>>
>>
>>
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20171012/0fcd1a8d/attachment-0001.html>