Recursive subtyping revealed