Advice implementing new constraint entailment rules

[Simon Peyton Jones]

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