Eh, generics kinda do introduce a subtyping relation already. It's just that HM's Gen rule of e: σ implies e: ∀α.σ is restrictive enough that this subtyping relation can be checked (and inferred) by using just unification which is quite an amazing result.