Variable types (à la System F) are not templates, though one can think of them as type schemata. A template
id(x: T) -> T {
return 2;
}
will only fail when applied, say, to a string.
By contrast variable types enforce universality throughout (in fact, there is an interpretation of System F in which the identity \(\Lambda.a.\lambda x^\alpha. x^\alpha\) consists of one point). Concretely, the Haskell function
id :: a -> a
id x = x
has one sensible implementation.[1] The implementation is clarified precisely by the generality of the interface. Universality (recalling free objects in category theory) in type systems is more than sorting into boxes, “catch errors at compile time rather than runtime.”
[1] a -> a has only two inhabitants, the other is \_ -> let x = x in x, which enters an infinite loop for all inputs.
