Pattern synonym used in an expression context could have different constraints to pattern used in a pattern context

The two directions of an explicitly-bidirectional pattern might have utterly different class constraints. After all, the two directions are specified by quite different code. Suppose that

• Pattern P (used in a pattern) requires constraints CR, and provides constraints CP
• Constructor P (used in an expression) requires constraints CE

Then I think the only required relationship is this: CP must be provable from CE (since CP is packaged up in a P-object).

Currently, CE := CP + CR.