高阶多态函数子类型中特异性的定义与比较方法问询

在支持高阶多态的类型系统（如Peyton Jones等人的《Practical Type Inference for Arbitrary-Rank Types》）中，我试图理解子类型中特异性的推理逻辑，但感到十分困惑。以下是两个关键示例：

单态函数类型的子类型关系 #

对于单态函数类型，通常将更具体的类型视为子类型：
(B,C)→(B,C) ⪯ A→A
这符合逻辑——仅适用于配对的函数可用于需要泛型函数的场景。

多态类型的子类型关系 #

但对于多态类型，情况相反：
∀A.A→A ⪯ ∀B,C.(B,C)→(B,C)
尽管右侧类型更具体（量化的实例化可能性更少），却被视为左侧更通用类型的超类型，这看似矛盾。

核心疑问 #

换言之，第一个示例中更具体的函数在左侧（子类型），第二个示例中更具体的多态函数在右侧（超类型）。我理解检查子类型时∀类型的实例化发生在左侧（如Peyton Jones论文所述），但尚未完全理解特异性的定义。

我认为(B,C)→(B,C) ⪯ A→A与A→A ⪯ (B,C)→(B,C)均成立，但是否存在规则可确定更具体的类型？即单态场景下选中(B,C)→(B,C)，多态场景下选中右侧类型？

内容的提问来源于stack exchange，提问作者NisNis