Weirich, StephanieVytiniotis, DimitriosZdancewic, Stephan APeyton Jones, Simon2023-05-222023-05-222011-01-012012-07-17https://repository.upenn.edu/handle/20.500.14332/6632Modular 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.Computer SciencesPresentation