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 constraintsCR
, and provides constraintsCP
- Constructor
P
(used in an expression) requires constraintsCE
Then I think the only required relationship is this:
CP
must be provable fromCE
(since CP is packaged up in a P-object).
Currently, CE := CP + CR
.