Advice implementing new constraint entailment rules

Simon Peyton Jones simonpj at
Thu Mar 5 09:24:02 UTC 2020

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.



|  -----Original Message-----
|  From: ghc-devs <ghc-devs-bounces at> On Behalf Of Matthew
|  Pickering
|  Sent: 05 March 2020 08:16
|  To: GHC developers <ghc-devs at>
|  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
|  devs&
|  c0dd8534%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637189929963530670&a
|  mp;sdata=0T2O%2FaAcIU9Yl61x2uPzl4zUG4P3jl6iA97baIDlSsM%3D&reserved=0

More information about the ghc-devs mailing list