Implicit vs explicit subtyping
The short answer is "to verify additional properties of existing code".  Longer answer follows.

I am not sure "implicit" vs "explicit" is good terminology.  This distinction is sometimes called "structural" vs "nominal" subtyping.  Then there is also a second distinction in the possible interpretations of structural subtyping (described shortly).  Note that all three interpretations of subtyping really are orthogonal, and so it doesn't really make sense to compare them against each other, rather than understanding the uses of each.

The main operational distinction in interpreting a structural subtyping relation A &lt;: B is whether it is witnessed by a real coercion with (runtime/compiletime) computational content, or whether it can be witnessed by the identity coercion.  If the former, the important theoretical property that has to hold is "coherence", i.e., if there are multiple ways to show that A is a substructural subtype of B, each of the accompanying coercions have to have the same computational content.

The link you gave seems to have the second interpretation of structural subtyping in mind, where A &lt;: B can be witnessed by the identity coercion.  This is sometimes called a "subset interpretation" of subtyping, taking the naive view that a type represents a set of values, and so A &lt;: B just in case every value of type A is also a value of type B.  It is also sometimes called "refinement typing", and a good paper to read for the original motivation is Freeman &amp; Pfenning's Refinement types for ML.  For a more recent incarnation in F#, you can read Bengston et al, Refinement types for secure implementations.  The basic idea is to take an existing programming language that may (or may not) already have types but in which types do not guarantee all that much (e.g., only memory safety), and consider a second layer of types selecting subsets of programs with additional, more precise properties.

(Now, I would argue that the mathematical theory behind this interpretation of subtyping is still not as well understood as it should be, and perhaps that is because its uses are not as widely appreciated as they should be.  One problem is that the "set of values" interpretation of types is too naive, and so sometimes it is abandoned rather than refined.  For another argument that this interpretation of subtyping deserves more mathematical attention, read the introduction to Paul Taylor's Subspaces in Abstract Stone Duality.)