Is Space-Efficient Polymorphic Gradual Typing Possible?

Gradual typing, proposed by Siek and Taha, is a way to combine static and dynamic typing in a single programming language. Since its inception, researchers have studied techniques for efficient implementation. In this paper, we study the problem of space-efficient gradual typing in the presence of parametric polymorphism. We develop a polymorphic extension of the coercion calculus, an intermediate language for gradual typing. Then, we show that it cannot be made space-efficient by following the previous approaches, due to subtle interaction with dynamic sealing, a standard technique to ensure parametricity in polymorphic gradual typing.