[TYPES] Literature relating subtyping to positivity checking for recursive types?

[Christopher Jenkins]

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,