Draft: directed coercions

Work in progress. More to come soon [May 2023].

This MR introduces a slimmer version of coercions, directed coercions, which store fewer types within them. This more compact representation considerably speeds up programs which involve many type family reductions, as the coercion size no longer grows quadratically in the number of reduction steps.