Dependent Types

A Dependent Type is one whose members can be describe by a predicate depending on other values.
In your case, it is Index (xs: List a) = { i ∈ PositiveInt | i < |xs| }.
As you can deduce from the i ∈ PositiveInt clause, this is a strict subtype of PositiveInt.

Here's an example programme description using it:

List a = enum
    (::): a -> List a -> List a
    Empty: List a

length: List a -> PositiveInt
length l = f l 0 where
    f (Cons _ xs) n = f xs (n + 1)
    f Empty n = n

Index (xs: List a) = (i: PositiveInt) when i < length xs

get: (xs: List a) -> Index xs -> a
get (Cons x _) 0 = x
get (Cons _ xs) n = get xs (n - 1)

main = do
    let xs = "h" :: "42" :: Empty
    putStrLn (get xs 0) //ok
    putStrLn (get xs 5) //Compiler Error

A question that arises then is that of get "knowing" it will never get Empty as input, at which point one will notice that length: List a -> PositiveInt has not a descriptive enough type.
Indeed: length's correct type is (Empty -> 0) & ((::) -> PositiveInt), which explicitates the fact that Index Empty is not a type existing in the Universe.
How smart a language and implementation has to be to automatically understand and report on those problems then is the realm of Automated Theorem Proving.

Naturally, when a value is not literal, one has to prove it indeed inhabits the type at hand.

let n: Int = userInput in
get xs n

is not a valid programme, for Int is a supertype of { i ∈ Int | i < |xs| }, meaning explicit type narrowing has to be involved:

let n: Int = userInput in
if n < |xs| then
    get xs n
else
    //deal with error

which should be reminiscent of C++'s dynamic_cast, and is already existing practice (you don't just use unsanitised user input as-is, do you?).
This also relates to the realm of Automatic Type Narrowing as featured in Kotlin, TypeScript, and, less automatic, Ceylon.

An other example is that of Min and Max: ∀(a: Comparable). MinMax (x: a, y: a) = { x, y }, which may be used to describe functions such as

MinMax = ∀a. Comparable a => (x: a) -> (y: a) -> (x | y)

max: MinMax
max x y = x > y then x else y

min: MinMax
min x y = x > y then y else x

where x and y are runtime values used as unit types in a union type, where it is guaranteed that for each pair of x and y, min and max both will return precisely either that x or that y, and nothing else.
Naturally the result of min and max is a strict subset of a by virtue of { x ∈ a | f(x) } <: a.

Languages implementing those include, among others, Idris, Agda, Coq, F*, and ATS.