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 y ⇒ y ≡ f (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.