当我们说T1比T2具有更多的多态性时，我们是什么意思？

正如对OP的注释中所指出的，(undefined :: (forall a . a) -> Int) ( undefined :: (forall a. a -> a) )它不进行类型检查，并且实际上forall a. a -> a并没有比更具多态性forall a. a，因此这里没有矛盾。

另一方面，要进行类型检查，(undefined :: (forall a. a -> Int)) (undefined :: (forall a. a -> a))所以forall a. a -> a必须a在函数类型中包含对吧？看起来似乎违反直觉，但这确实是事实。让我解释。

包含和类型变量

包含（或替代：多态子类型化）的意思是“至少与多态相同”，因此它更像是<=而不是<。在更正的OP示例中，a将其包含在内，forall a. a -> a因为在该上下文 a中，该变量是非刚性类型的变量，并且可以将其与其他类型统一。因此，forall a. a -> a <= typeVar b被认为是正确的，同时也产生了约束typeVar b = forall a. a -> a（或者可能是不同的约束，取决于我们对类型推断系统的选择。实际步骤可能与我在下面的示例中概述的步骤明显不同）。

一个简单的分步示例：

-- goal 
(forall a. a -> Int) <= (Int -> Int)
-- instantiate variable on the left hand side with a fresh type variable.
(tvar a' -> Int) <= (Int -> Int)
-- check return type subsumption
Int <= Int -- OK
-- check argument type subsumption
Int <= tvar a' -- OK, add "tvar b = Int" to the set of constraints.
-- Done.

通常，如果我们有forall a. P <= Q一些P和Q，我们必须找到满足包含关系的某些特定实例a。这意味着我们a用一个灵活的类型变量实例化，然后从那里开始。在这种情况下，我们将搜索特定类型，然后继续进行类型变量的优化。

另一方面，如果我们有P <= forall a. Q，则对于所有可能的实例化，必须包含a在右侧。在这种情况下，我们通常将实例a化为刚性（或skolem）类型的变量。刚性类型变量并不是真正的“变量”。相反，它代表某种任意（未知）固定类型，我们无法对其进行优化。具有刚性变量的示例：

-- goal
(forall a. a -> Int) <= (forall b. b -> Int)
-- instantiate variable on the left
(tvar a' -> Int) <= (forall b. b -> Int)
-- instantiate variable on the right
(tvar a' -> Int) <= (skolem b' -> Int)
-- check return types
Int <= Int -- OK
-- check argument types
skolem b' <= tvar a' -- OK, record the "tvar a' = skolem b'" constraint 
-- Done. 

基本上，我们只能使用skolem变量做两件事：

1. 我们可以自由地得出结论skolem a <= skolem a，即他们可以自我包容。
2. 我们可以使用一个灵活的变量来统一它们，即我们可以拥有skolem a <= tvar b或tvar b <= skolem a。

旋转函数类型

我们已经在(a -> b) <= (a' -> b')iffb <= b'和a' <= a。的示例中看到了。将<=翻转参数类型。这是为什么？

假设我们的键入上下文期望type的某些功能a -> b。此函数（通常作为函数）会消耗type的a值并产生type的值b。从某种意义上说，上下文对-s有需求b，并且还可以为我们的函数提供 a-s。如果函数返回的类型比通用b，那就很好了，因为那样的话，它也可以满足上下文对的需求b。但是，如果函数期望的类型比通用a，则上下文会被阻塞。语境不佳的b库存只有-s，它可以使它们专门化，但不能对其进行概括。如果仅函数对它接受的类型不太挑剔！

按照行话来说，函数类型构造函数的实参类型是协变的（或为负），而返回类型则是协变的（或为正）。在Wikipedia上有一个关于方差的很好的讨论。它更关注与OOP类层次结构有关的子类型化，而不是多态子类型化，但是它也应该为后者提供有用的见解。

让我们看一个例子，其中包含翻转更显着：

-- goal 
((forall a. a -> a) -> Int) <= ((forall a. a -> Int) -> Int)
-- remember: the context can supply "forall a. a -> Int"-s and demands "Int"-s. 
-- check return types
Int <= Int -- OK
-- check argument types
(forall a. a -> Int) <= (forall a. a -> a)
-- instantiate on the left
(tvar a' -> Int) <= (forall a. a -> a)
-- instantiate on the right
(tvar a' -> Int) <= (skolem a'' -> skolem a'')
-- check return types
Int <= skolem a'' -- FAIL: this clearly does not hold.
-- Abort.

等级1与等级较高设置中的函数类型差异

我的前两个示例没有嵌套forall-s，即它们只有等级1类型。您可能已经注意到，翻转的推定没有任何区别！如果我们假设(a -> b) <= (a' -> b') iff b <= b' and a <= a'存在，那么这两个示例都将进行类型检查，因为我们只需要检查类型变量，skolem和单态类型的使用即可。

因此，协方差-协方差的区别仅与较高级别的类型相关（这在OP引用的论文的第3.3节中也有暗示）。尽管，如果我没记错的话，尽管HMF系统排名较高，但它也忽略了函数方差自旋。