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 <matthewtpicker...@gmail.com> | Sent: 27 March 2020 22:33 | To: Simon Peyton Jones <simo...@microsoft.com> | Cc: GHC developers <ghc-devs@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 <simo...@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-boun...@haskell.org> On Behalf Of Matthew | > | Pickering | > | Sent: 05 March 2020 08:16 | > | To: GHC developers <ghc-devs@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@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 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs