请考虑：

(1) const :: forall a b. a -> b -> a

(2) const :: forall a. a -> a -> a

你不能从（1）推断出（2）;如果可以的话，这就意味着const * 总是 * 有一个适合forall a. a -> a -> a的类型（在（1）中并不明显，因为我们还没有应用足够的推理步骤），但是我显然可以在const True 'a'这样的情况下使用const，其中const有Bool -> Char -> Bool类型。
你能做的就是意识到（2）是的 * 示例化 *（1）. b与a一般不相同，但是，（正如你所说的）没有什么能阻止b在任何一个特定的用法中与a是同一个东西。因此，从使用const的上下文中，你可能能够推断那个特定的用法的类型为forall a. a -> a -> a。例如，这发生在：

silly :: forall a. a -> a
silly x = const x x

您还可以从const :: forall a b. a -> b -> a中得知，如果您选择将b示例化为与a相同，则会得到const :: forall a -> a -> a。其中我们总是为b选择与为a所做的相同的事情。
为此，我们只需将b替换为a即可（在我们正在示例化的量词的作用域中，但这里是整个表达式）。您表示怀疑您是否可以这样做，因为变量会冲突，但是示例化一个变量使其与另一个变量相同是我们在这里所做的重点。意外地 * 改变了表达式，给变量取了相同的名字，而这些名字本应该是不同的;在这里，我们是经过深思熟虑的选择来检验它们"不“不同的特殊情况。
但是，没有从const :: forall a -> b -> a（没有任何使用它的上下文）到const :: forall a. a -> a -> a的纯推理链，因为当你做出这种改变时，你正在削弱/专门化const;如果不添加额外的信息来限制b与a相同（用Haskelly的话来说，这是一个额外的a ~ b约束），推理规则就不会把你从（1）带到（2）。

以下内容以评论开头，已移至此处。
因为我不能在第二个量词上使用消去法，因为变量会冲突。
我认为你错了。事实上你可以使用消元法，而变量的冲突与普适消元法无关。[从我从下面的资料中了解到的情况来看，有时冲突是相关的，有时则不是。]
你能告诉我哪种自然演绎系统允许在普适消去推理中使用约束变量吗？
Chapter 8 of Stanford Introduction to Logic将 * 通用消除（UE）* 定义为

∀ν.φ[ν]
------------
φ[τ]
where τ is substitutable for ν in φ

和
我们说，项τ对于句子φ中的变量ν是自由的，当且仅当ν在τ中某个变量的量词的范围内没有自由出现。
有了这一点和 * 通用介绍（UI）*，我认为

∀a.∀b.a⇒(b⇒a)
-------------- UE, a is free for a in ∀b.a⇒(b⇒a).
∀b.a⇒(b⇒a)
-------------- UE, a is free for b in a⇒(b⇒a).
a⇒(a⇒a)
-------------- UI, a does not occur free in both a⇒(a⇒a) and
∀a.a⇒(a⇒a)       an active assumption. I am not sure about this.

这就剩下了声称a is free for a in ∀b.a⇒(b⇒a)等。

a is free for a in ∀b.a⇒(b⇒a) 
⇔
no free occurrence of a occurs within the scope of a quantifier of some variable in a

在∀b.a⇒(b⇒a)中不存在a的量词，因此a不会在∀b.a⇒(b⇒a)中a的（不存在的）量词的范围内自由出现。