如何从Haskell const的原始类型签名合法推导const :: a->a->a类型

你之前卡壳在全称消去的变量冲突，核心是漏掉了类型论里最基础的alpha等价转换规则，整个推导完全符合System F（Haskell多态的理论基础）的规则，没有任何跳步：

• 首先明确初始前提：const的最通用类型是

  const :: forall a b. a -> b -> a
  

  这个签名的含义是：对任意类型a、任意类型b，const都能接受一个a类型的值、一个b类型的值，返回第一个a类型的值。
• 先做alpha重命名，规避变量捕获
  类型系统里的绑定变量名只是占位符，只要不改变变量的绑定关系，重命名绑定变量不会改变类型的语义，这就是alpha等价规则：比如forall b. b -> Int和forall x. x -> Int是完全同一个类型。
  你之前想直接把b替换成a会触发变量捕获问题：b是内层量词绑定的变量，如果直接替换成外层已经被forall a绑定的a，会把原本独立的b错误绑定到外层的量词上，违反替换规则。所以我们先把内层的绑定变量b重命名为全新的、和外层变量不冲突的名字c，得到和原类型完全等价的签名：

  const :: forall a c. a -> c -> a
  

• 应用全称消去（全称实例化）规则
  System F里的全称消去规则明确：如果一个项的类型是forall t. T，那么你可以把类型里所有自由出现的t替换成任意合法类型S，只要替换过程不会出现变量捕获，就能得到一个合法的特化类型。
  现在我们对上面重命名后的类型，消去内层的forall c量词，把c替换为类型a——这时候没有任何捕获问题：重命名后的c是独立的绑定变量，替换成a之后，两个参数的类型都对应外层forall a绑定的同一个类型，最终得到：

  const :: forall a. a -> a -> a
  

补充说明 #

很多初学者会误以为不同的类型变量必须代表不同类型，这是完全错误的认知。类型变量的本质是“这个位置可以放任意类型”，没有任何规则要求两个不同的类型变量必须实例化为不同的类型。从逻辑角度看，既然const对“任意a、任意b”都成立，那当b取和a相同的类型时自然也成立——这就像数学里如果对任意实数x、任意实数y都有f(x,y)=x，那对任意实数x，f(x,x)=x自然是成立的，你之前遇到的推导障碍本质只是一阶逻辑/类型论里替换操作的“无捕获”前置要求，只要提前做alpha重命名绕开名字冲突，整个推导完全合规。
你可以在GHCi里实际验证这个特化是合法的：

Prelude> :set -XTypeApplications
Prelude> :t const @Bool @Bool
const @Bool @Bool :: Bool -> Bool -> Bool

这里就是把a和b都实例化为Bool，正好对应我们推导出来的forall a. a -> a -> a的特化形式。

内容的提问来源于stack exchange，提问作者F. Zer