Advice implementing new constraint entailment rules
Simon Peyton Jones
simonpj at microsoft.com
Thu Mar 5 09:24:02 UTC 2020
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.
| -----Original Message-----
| From: ghc-devs <ghc-devs-bounces at haskell.org> On Behalf Of Matthew
| Sent: 05 March 2020 08:16
| To: GHC developers <ghc-devs at haskell.org>
| Subject: Advice implementing new constraint entailment rules
| 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
| 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.
| ghc-devs mailing list
| ghc-devs at haskell.org
More information about the ghc-devs