Lambda the Ultimate

Generative Type Abstraction and Type-level Computation (Extended Version), by Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, Steve Zdancewic:

Modular languages support generative type abstraction, ensuring that an abstract type is distinct from its representation, except inside the implementation where the two are synonymous. We show that this well-established feature is in tension with the non-parametric features of newer type systems, such as indexed type families and GADTs. In this paper we solve the problem by using kinds to distinguish between parametric and non-parametric contexts. The result is directly applicable to Haskell, which is rapidly developing support for type-level computation, but the same issues should arise whenever generativity and non-parametric features are combined.

Type-level computation is becoming more common and more elaborate, thanks to recent extensions such as type families. Other non-parametric features allow the developer to reason about the concrete types used in a computation. Unfortunately, something as simple as a type-based dispatch can be unsound when combined with coercion lifting. This paper solves the tensions between these two useful features using a kind system extended with "roles".

In fact, this isn't the first time coercion lifting has caused trouble. In capability security terminology, coercion lifting is a "rights amplification" operation, and there are previously known examples of seemingly innocuous coercion lifting across an abstraction/implementation boundary resulting in Confused Deputies. There's no discussion of this connection in the paper, and the paper cannot solve the problem discussed at that link, which exposes a much deeper issue than confusing parametric/non-parametric contexts.