haskell - 带有 RankNTypes 扩展的奇怪类型推断

Question

我正在尝试在 Haskell 中尝试 System-F 类型，并通过 type 实现自然数的 Church 编码。

加载此代码时

{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE RankNTypes #-}

type CNat = forall t . (t -> t) -> (t -> t)

c0 :: CNat
c0 _ x = x

type CPair a b = forall t . (a -> b -> t) -> t

cpair :: a -> b -> CPair a b
cpair a b f = f a b

-- pair3 :: CPair CNat String
pair3 = cpair c0 "hello"

进入 ghci 7.8.2 我收到警告:

λ: :l test.hs 
[1 of 1] Compiling Main             ( test.hs, interpreted )

test.hs:29:1: Warning:
    Top-level binding with no type signature:
      pair3 :: forall t t1.
               (((t1 -> t1) -> t1 -> t1) -> [Char] -> t) -> t
Ok, modules loaded: Main.
λ: 

问题是，类型不应该是

pair3 :: forall t.
      ((forall t1. (t1 -> t1) -> t1 -> t1) -> [Char] -> t) -> t

？

UPD:提供了一个更简单的示例

Answer 1

这是一个非常好的类型……但这不是 Hindley-Milner 给出的类型。 HM总是推断出 1 级类型。我相信，推断 2 级类型实际上是可判定的，但 GHC 甚至没有尝试。