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
Reduction
is 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 Reduction
s, 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
).