The language Fun  is a typed polymorphic lambda calculus with a notion of subtyping and quantifiers ranging over subtypes of a given type. In this paper we show that it is consistent to allow recursive type definitions in Fun, by constructing an interpretation of types as partial equivalence relations of a special kind, terms being interpreted as equivalence classes, modulo such relations, of elements of a model for an underlying untyped language. © 1991.
Cardone, F. (1991). Recursive types for Fun. Theoretical Computer Science, 83(1), 39–56. https://doi.org/10.1016/0304-3975(91)90038-4