+mkRightCoercions :: Int -> Coercion -> [Coercion]
+-- ^ As 'mkRightCoercion', but finds the 'Coercion's available on the right side of @n@
+-- nested application 'Coercion's, manufacturing new left or right cooercions as necessary
+-- if suffficiently many are not directly available.
+mkRightCoercions n co
+ = go n co []
+ where
+ go n co acc
+ | n > 0
+ = case splitAppCoercion_maybe co of
+ Just (co1,co2) -> go (n-1) co1 (co2:acc)
+ Nothing -> go (n-1) (mkCoercion leftCoercionTyCon [co]) (mkCoercion rightCoercionTyCon [co]:acc)
+ | otherwise
+ = acc
+
+
+mkInstCoercion :: Coercion -> Type -> Coercion
+-- ^ Instantiates a 'Coercion' with a 'Type' argument. If possible, it immediately performs
+-- the resulting beta-reduction, otherwise it creates a suspended instantiation.