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%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