GHC rewrite rule type-checking failure
Conal Elliott
conal at conal.net
Tue Oct 17 02:47:49 UTC 2017
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 <simonpj at microsoft.com>
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:* conal.elliott at gmail.com [mailto:conal.elliott at gmail.com] *On
> Behalf Of *Conal Elliott
> *Sent:* 12 October 2017 20:02
> *To:* Simon Peyton Jones <simonpj at microsoft.com>
> *Cc:* ghc-devs at haskell.org
>
> *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 <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/20171016/dde841d0/attachment-0001.html>
More information about the ghc-devs
mailing list