ShiqiCao, please refer to the Coq file. I am not overly familiar with type systems including subtyping, as you see I was even confused about the standard notation; but I like things being formal,
and at a first glance my intuition for subtyping would be this:
Inductive subtype (a b : Set) : Set :=
| ST : (a -> b) -> subtype a b.
In plain words, this says: we can demonstrate that A is a subtype of B by providing a function (as in math) from A to B. That is, A contains all the information in B and more.
that a sound type system would be significantly more complex, and I would argue you do not need to expose any of the additional complexity to the user.
For example, to avoid the need for variance annotation on generics, you could simply exclude rules that depend on it from the formalized subtyping relation. It is a strategy works quite well - when the compiler is in doubt, assume a NO answer. In the limit,
of subtyping fails to infer safety, the user inserts an explicit cast.
I have a strong preference for an explicit cast, because in this setup a compiling cast-free program gives me a static guarantee there will be no type errors. In current TypeScript the fact a program compiles tells me nothing about type errors - they can
still manifest themselves for certain runs of the program.