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 <simo...@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 <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