GHC rewrite rule type-checking failure
Conal Elliott
conal at conal.net
Tue Oct 3 15:45:04 UTC 2017
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/20171003/4013c71e/attachment.html>
More information about the ghc-devs
mailing list