The proposal: in any type signature, the presence of type variable

x@pat

matches the type specified by pat, and replaces any occurrences of the type variable x with pat. In particular, this might be comparable to defining

type x (free variables in pat) = pat

with scope solely to the right of the as-pattern. Alternately, it might be compared to an equality constraint (x ~ pat).