Advice implementing new constraint entailment rules

[Simon Peyton Jones]

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