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 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 On Behalf Of Matthew | Pickering | Sent: 05 March 2020 08:16 | To: GHC developers | 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@haskell.org | https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.hask | ell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc- | devs&data=02%7C01%7Csimonpj%40microsoft.com%7C52ec5ca4f50c496b25e808d7 | c0dd8534%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637189929963530670&a | mp;sdata=0T2O%2FaAcIU9Yl61x2uPzl4zUG4P3jl6iA97baIDlSsM%3D&reserved=0

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 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 | Sent: 27 March 2020 22:33 | To: Simon Peyton Jones | Cc: GHC developers | 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 | 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 On Behalf Of Matthew | > | Pickering | > | Sent: 05 March 2020 08:16 | > | To: GHC developers | > | 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@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