Subtypes

In some cases, Disco is willing to accept one type in place of another, when this is known to be safe. For example, suppose we have

f : Z -> Z
f(n) = n - 1

x : N
x = 3

XXX