Advice implementing new constraint entailment rules

[Matthew Pickering]

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