Erasable coercions in System F-eta, also known as retyping functions, are
well-typed eta-expansions of the identity. They may change the type of terms
without changing their behavior and can thus be erased before
reduction. Coercions in F-eta can model subtyping of known types and some
displacement of quantifiers, but not subtyping assumptions nor certain forms
of delayed type instantiation. We generalize F-eta by allowing abstraction
over retyping functions. We follow a general approach where computing with
coercions can be seen as computing in the lambda-calculus but keeping track
of which parts of terms are coercions. We obtain a language where coercions
do not contribute to the reduction but may block it and are thus not
erasable. We recover erasable coercions by choosing a weak reduction
strategy and restricting coercion abstraction to value-forms or by
restricting abstraction to coercions that are polymorphic in their domain or
codomain. The latter variant subsumes F-eta, F-sub, and MLF in a unified
framework.