In the PoPL 2019 proceedings there are two typographical errors that are corrected as follows:

1. Page 10, displayed definition of Fhcom: second occurrence of M should be M'.

2. Page 15, displayed definition of Fcoe: Tm(Fcoe(alpha)) should be Tm(alpha), referring to the (term expansion of the) underlying type of the identity, rather than to itself.