[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
In Curry-style type systems, it is possible for a term to have two different types; in the setting that I am interested in (Cedille) it is possible to define a type of "Cast S T" witnessing that all terms of type S also have type T, which in turn induces a form of subtyping S <: T. I would like to know whether anyone knows about or can point me to work related to the following two subjects: 1. type systems in which the subtyping judgment is replaced by a type (like Cast) and where subtyping inference rules elaborate terms with inserted coercions (Luo's "Coercive Subtyping" is closely related in this second respect) 2. the connection between subtyping and positivity checking for recursive types. To expand on this, let F be some type-scheme of kind Type -> Type. Often (such as when working with inductive data-types as least fixpoints of functors) one is interested in restricting F to be positive. With Cast as the notion of subtyping, this requirement can be stated as the existence of a proof / function of type X <: Y -> F X <: F Y, in effect allowing one to replace the usual detailed account of positivity checking with a set of (elaborating) subtyping rules and saying "F is positive iff F X <: F Y is derivable assuming X <: Y is in the context". Maybe this second observation isn't very deep, but nonetheless I could not find any work reducing positivity checking to a subtyping problem, and wanted to know if someone else has also made this connection. Thanks,
