Advice implementing new constraint entailment rules

[Matthew Pickering]

Where exactly do you mean about "stepping inside an implication"?

For the program foo = [|| show ||]

My first attempt to use implication constraints was to create an
implication with G = [] W = [Show a @ 2] and then canonicalise to
remove CodeC constraints. I hope the evidence would get directly
written into the right place and hence be stage correct but we still
generate stage incorrect let bindings. For example:

foo d = let dShow = $$d in [|| let dShow' = dShow in show dShow' ||]

I need

foo d = [|| let dShow = $$d in show dShow ||]

The other possibilities I could think of based on your hint are:

* Capture Ws when leaving a quote, and create a quote with G = [Show a
@ 2] W = [CodeC (Show a) @ 1] (and have no canonicalisation step).
This doesn't seem much different to what I already have.
* When stepping inside an implication which increase the stage, look
in the inert set for any `CodeC` constraints and create givens for the
next stage by applying splices.

A call would be good to clear this up.

Cheers,

Matt

On Mon, Mar 30, 2020 at 11:31 PM Simon Peyton Jones
<simonpj at microsoft.com> wrote:
>
> Do you know about implication constraints?  If not, look back at the OutsideIn(X) paper.
>
> An implication constraint carries with it the place to put its Given bindings: see the ic_binds field of Constraint.Implication.  And that is exactly what you want.
>
> I suspect you'll want an implication to carry a stage, as well as its skolem vars and givens.   When stepping inside an implication that would trigger the unwapping of CodeC constraints from outside.
>
> We could have a Skype call to discuss if you like
>
> Simon
>
> | -----Original Message-----
> | From: Matthew Pickering <matthewtpickering at gmail.com>
> | Sent: 27 March 2020 22:33
> | To: Simon Peyton Jones <simonpj at microsoft.com>
> | Cc: GHC developers <ghc-devs at haskell.org>
> | Subject: Re: Advice implementing new constraint entailment rules
> |
> | I have made some progress towards the implementation but am stuck on how
> | to get the right desugaring.
> |
> | For example if the source program is
> |
> | foo :: CodeC (Show a) => Code (a -> String) foo = [| show |]
> |
> | Then the current approach is to canonicalise all the constraints to remove
> | the `CodeC`. The issue with this I have found is that the evidence gets
> | bound in the wrong place:
> |
> | ```
> | foo d = let d' = $d in [| show d' |]
> | ```
> |
> | It should rather be
> |
> | ```
> | foo d = [| let d' = $d in show d' |]
> | ```
> |
> | Now I am trying to think of ways to make the evidence binding be bound in
> | the right place. So there are a few things I thought of,
> |
> | 1. Attempt to float evidence bindings back inwards to the right level
> | after they are solved, this doesn't feel great as they are floated
> | outwards already.
> | 2. Don't canonicalise the constraints in the normal manner, when leaving
> | the context of a quote, capture the wanted constraints (in this example
> | Show a) and emit a (CodeC (Show a)) constraint whilst inserting the
> | evidence binding inside the quote.
> |
> | I prefer option 2 but inside `WantedConstraints` there are `Ct`s which may
> | be already canonicalised. Trying a few examples shows me that the `Show a`
> | constraint in this example is not canonicalised already but it feels a bit
> | dirty to dig into a `Ct` to find non canonical constraints to re-emit.
> |
> | Any hints about how to make sure the evidence is bound in the correct
> | place?
> |
> | Matt
> |
> | On Thu, Mar 5, 2020 at 9:24 AM Simon Peyton Jones <simonpj at microsoft.com>
> | wrote:
> | >
> | > Hi Matt
> | >
> | > I think you are right to say that we need to apply proper staging to the
> | constraint solver.   But I don't understand your constraint rewriting
> | rules.
> | >
> | > Before moving to the implementation, could we discuss the specification?
> | You already have some typeset rules in a paper of some kind, which I
> | commented on some time ago.  Could you elaborate those rules with class
> | constraints?  Then we'd have something tangible to debate.
> | >
> | > Thanks
> | >
> | > Simon
> | >
> | > |  -----Original Message-----
> | > |  From: ghc-devs <ghc-devs-bounces at haskell.org> On Behalf Of Matthew
> | > | Pickering
> | > |  Sent: 05 March 2020 08:16
> | > |  To: GHC developers <ghc-devs at haskell.org>
> | > |  Subject: Advice implementing new constraint entailment rules
> | > |
> | > |  Hello,
> | > |
> | > |  I am attempting to implement two new constraint entailment rules
> | > | which  dictate how to implement a new constraint form "CodeC" can be
> | > | used to  satisfy constraints.
> | > |
> | > |  The main idea is that all constraints store the level they they are
> | > | introduced and required (in the Template Haskell sense of level) and
> | > | that only constraints of the right level can be used.
> | > |
> | > |  The "CodeC" constraint form allows the level of constraints to be
> | > | manipulated.
> | > |
> | > |  Therefore the two rules
> | > |
> | > |  In order to implement this I want to add two constraint rewriting
> | > | rules in the following way:
> | > |
> | > |  1. If in a given, `CodeC C @ n` ~> `C @ n+1`  2. If in a wanted
> | > | `CodeC C @ n` -> `C @ n - 1`
> | > |
> | > |  Can someone give me some pointers about the specific part of the
> | > | constraint solver where I should add these rules? I am unsure if
> | > | this  rewriting of wanted constraints already occurs or not.
> | > |
> | > |  Cheers,
> | > |
> | > |  Matt
> | > |  _______________________________________________
> | > |  ghc-devs mailing list
> | > |  ghc-devs at haskell.org
> | > |
> | > | https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmai
> | > | l.hask
> | > |  ell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-
> | > |
> | > | devs&data=02%7C01%7Csimonpj%40microsoft.com%7C52ec5ca4f50c496b25
> | > | e808d7
> | > | c0dd8534%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C63718992996353
> | > | 0670&a
> | > |
> | > | mp;sdata=0T2O%2FaAcIU9Yl61x2uPzl4zUG4P3jl6iA97baIDlSsM%3D&reserv
> | > | ed=0