On polymorphic gradual typing https://dl.acm.org/citation.cfm?id=3136534.3110284 漸進的型付けの多相型の拡張の話。 ∀X.X→X 〜 ★→★ のように多相型と非多相型がcompatibleになるようにしないといけないが、すべての非多相型に対してそれを許すと System F の保守的な拡張にならないので、動的型★が一回以上出現する非多相型のときだけ許す、というのを読んで、「そんなアドホックな……」と思ったけど、読み進めるとちゃんと整理された形になって各種の性質が証明されていくのが面白かった。