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 <simo...@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.elli...@gmail.com [mailto:conal.elli...@gmail.com] *On > Behalf Of *Conal Elliott > *Sent:* 03 October 2017 16:30 > *To:* Simon Peyton Jones <simo...@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 <simo...@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.elli...@gmail.com [mailto:conal.elli...@gmail.com] *On > Behalf Of *Conal Elliott > *Sent:* 03 October 2017 15:56 > *To:* Simon Peyton Jones <simo...@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 <simo...@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- > boun...@haskell.org] *On Behalf Of *Conal Elliott > *Sent:* 03 October 2017 01:03 > *To:* Joachim Breitner <m...@joachim-breitner.de> > *Cc:* glasgow-haskell-us...@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 <m...@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-us...@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 > m...@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> > > > > > > >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs