It would still be correct if τi contains a variable that does not belong to α, since this variable would not be generalized in the types of constructors and destructors. (Of course, it would be unsafe to generalize such a variable: for instance, one could then define type g = Cg of α with Cg : ∀ α.  α → g and f : ∀ α, β.  g → (α → β) → β and assign any type to the expression e =def match Cg 1 with Cg yyf (Cg 1) (λ y. y), which reduces to the integer 1.)

Conversely, it is safe, although strange and useless, that α contains superfluous variables. Consider for instance the definition type g(α) = Cg of int. Then g 1 would have type g(α) for any type α.

Note that the latter is allowed in OCaml, while the former is rejected.