Advice implementing new constraint entailment rules

[Matthew Pickering]

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