Refactor the kind-checking of tyvar binders