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
