Use a specific Reduction datatype instead of `(Type,Coercion)`
As I discovered in !5909 (merged), introducing a datatype data Reduction = Reduction Coercion !Type for use in the rewriter, replacing pairs (Type, Coercion) has several benefits:
- improved performance in rewriting of type families (around 2.5% improvement in
T9872), - improved consistency around orientation of rewritings, as a
Reductionis always left-to-right (the coercion's RHS type is always the type stored in the 'Reduction').
@rae suggested that this could be taken much further. His idea is to introduce combinators that work purely on the level of Reductions, e.g. mkReflRedn, mkTransRedn, mkTyConAppRedn, etc. This means that other parts of the code won't have to worry about getting the orientations right (e.g. whether to use mkCoherenceRightCo or mkCoherenceLeftCo).