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 form 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.