GHC不能结合多态性功能而不对其进行单态化

Question

在原始代码中，人们可以看到我只是将表达式提取到绑定中，这是Haskell声称应该始终可能的基本内容之一。

最小大小写(在自由节点上的@dminuoso的帮助下创建)

我希望g保持多态性(以便我可以将其提供给其他期望它的函数)：

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
main = do
let a :: forall t. Functor t => t () = undefined
let g :: forall u. Functor u => u () = a
pure ()

错误：

source_file.hs:6:44:
Couldn't match expected type ‘forall (u :: * -> *).
Functor u =>
u ()’
with actual type ‘t0 ()’
When checking that: t0 ()
is more polymorphic than: forall (u :: * -> *). Functor u => u ()
In the expression: a

原始问题(动机)发布在 #haskell IRC上：

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

class Monad m => Monad' m where
instance Monad' IO where
f1 :: (forall m . Monad' m => m Int) -> IO Int
f1 g = do
let a :: forall n . Monad' n => n Int = g
a
-- this works
--f1 :: (forall m . Monad' m => m Int) -> IO Int
--f1 g = do
--    g
main = print $ "Hello, world!"

但我得到：

source_file.hs:12:45:
Couldn't match expected type ‘forall (n :: * -> *).
Monad' n =>
n Int’
with actual type ‘m0 Int’
When checking that: m0 Int
is more polymorphic than: forall (n :: * -> *). Monad' n => n Int
In the expression: g

基于 https://ghc.haskell.org/trac/ghc/ticket/12587 我尝试显式应用类型来帮助类型检查器：

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
class Monad m => Monad' m where
instance Monad' IO where
f1 :: (forall m . Monad' m => m Int) -> IO Int
f1 g = do
let a :: forall n . Monad' n => n Int = g @n
a
main = print $ "Hello, world!"

但后来我得到：

main.hs:13:48: error: Not in scope: type variable ‘n’

Answer 1

第

1 部分

善

写作时会发生什么

a :: forall f. Functor f => f ()
a = _

？具体来说，GHC正在寻找什么类型的表达来填补漏洞(_)？你可能认为它在寻找一个forall f. Functor f => f ()，但这并不完全正确。相反，a实际上更像是一个函数，GHC 隐式插入了两个参数：一个名为f的类型参数，种类为* -> *，以及约束Functor f的一个实例(与所有实例一样，它是未命名的)。

a :: forall f. Functor f => f ()
a @f {Functor f} = _
-- @-syntax is a currently proposed extension, {}-syntax is fake

在type f :: * -> *; instance Functor f的背景下，GHC正在寻找一个f ()。这与在f :: A -> B; c :: C的上下文中寻找(A -> B) -> C -> D和寻找D之间的区别相同。如果我直接有solution :: (A -> B) -> C -> D，在第一种情况下我只能写solution，但是，在第二种情况下，我必须写出solution f c。

坏人

这不是你写作时发生的事情

a :: forall f. Functor f => f () = _

由于您使用的是模式类型签名，而不是普通签名，因此 GHC 不再为您隐式绑定类型变量和实例。GHC 现在，诚实而真实地希望您用forall f. Functor f => f ()来填充该_。这很难，我们很快就会看到...

(我真的不认为丹尼尔·瓦格纳引用的话在这里是相关的。我相信这只是指5 :: Num a => a隐含表示5 :: forall a. Num a => a的方式与g :: a -> a = id并不意味着g :: forall a. a -> a = id的方式之间的差异(当ScopedTypeVariables打开而type a不在范围内时)。

第 2 部分

写作时会发生什么

undefined

？具体来说，它的类型是什么？你可能认为这是forall a. a，但这并不完全正确。是的，确实，undefined本身具有forall a. a类型，但 GHC 不允许你自己编写undefined。相反，表达式中每次出现的undefined始终应用于类型参数。以上内容隐式重写为

undefined @_a0

并创建一个新的统一变量(实际上没有名称)_a0。此表达式的类型为_a0。如果我在需要Int的上下文中使用这个表达式，那么_a0必须等于Int，并且GHC设置_a0 := Int，将表达式重写为

：

undefined @Int

(因为_a0可以设置为某些东西，所以它被称为统一变量。它受"我们的"内部控制。上面，f无法设置为任何内容。这是一个给定的，并且在"他们的"(用户的)外部控制下，这使它成为一个skolem变量。

第 3 部分

善

通常，类型变量的自动绑定和统一变量的自动应用效果很好。 例如，这两种方法都很好：

undefined :: forall a. a

bot :: forall a. a
bot = undefined

因为它们分别扩展为

(@a -> undefined @a) :: forall a. a

bot :: forall a. a
bot @a = undefined @a

媒介

当你这样做时

a :: forall f. Functor f => f () = undefined

，你让一些非常奇怪的事情发生了。正如我之前所说，带有forall的模式类型签名不会引入任何东西。RHS上的undefined实际上需要是一个forall f. Functor f => f ().统一变量的隐式应用仍然发生：

a :: forall f. Functor f => f () = undefined @_a0

undefined @_a0 :: _a0，所以_a0 ~ (forall f. Functor f => f ())必须坚持。因此，GHC必须设定_a0 := (forall f. Functor f => f ())。通常，这是一个禁忌，因为这是非谓词多态性：将类型变量设置为包含foralls 的类型。然而，在足够过时的GHC中，某些功能是允许的。也就是说，undefined不是用类型forall (a :: *). a来定义的，而是用forall (a :: OpenKind). a来定义的，其中OpenKind允许这种不真实性。这意味着您的代码将作为

a :: forall f. Functor f => f () = undefined @(forall f. Functor f => f ())

如果你写

a :: forall f. Functor f => f () = bot

，这是行不通的，因为bot没有undefined拥有的那种神奇的酱汁。此外，这在最近的GHC中不起作用，这些GHC已经消除了这种奇怪的非指示性多态性。(我说这是一件非常好的事情)。

坏人

您对a的定义，即使带有模式签名，也确实出现了所需的类型forall f. Functor f => f ()。该问题现在g：

g :: forall f. Functor f => f () = a

g再次不绑定type f :: * -> *或instance Functor f。同时，a被应用于一些隐式的东西：

g :: forall f. Functor f => f () = a @_f0 {_}

但。。。RHS现在有_f0 ()型，LHS希望它有forall f. Functor f => f ()型。这些看起来不一样。因此，键入错误。

由于您无法停止对类型变量的隐式应用a而只写入g = a，因此您必须在g中允许类型变量的隐式绑定：

g :: forall f. Functor f => f ()
g = a

这行得通。

Answer 2

正如Freenode上的@Lears所指出的那样，将类型声明放在声明上方可以修复它，因此它可能是GHC中的某种错误。

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
main = do
let a :: forall t. Functor t => t () = undefined
let g :: forall u. Functor u => u () = a
putStrLn "success"

失败

但

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
main = do
let a :: forall t. Functor t => t () = undefined
let g :: forall u. Functor u => u ()
g = a
putStrLn "success"

成功。

Answer 3

关于模式类型签名的文档的相关部分是这样的：

与表达式和声明类型签名不同，模式类型签名不是隐式概括的。

所以模式签名，就像你写的一样，是一种特殊情况，其中泛化(即将提到超出范围的类型变量a的单态类型t转换为多态类型forall a. t的过程)没有完成。可以使用任何其他形式的类型签名来恢复泛化过程;例如，代替

let foo :: forall a. a = undefined

尝试：

let foo :: forall a. a
foo = undefined

Answer 4

如果我放一个打字的洞，GHC给了我这个：

foo.hs:11:45: error:
• Cannot instantiate unification variable ‘t0’
with a type involving foralls:
forall (b :: * -> *). Monad' b => b Int
GHC doesn't yet support impredicative polymorphism
• In the expression: _
In a pattern binding:
a :: forall (b :: * -> *). Monad' b => b Int = _
In the expression:
do let a :: forall b. Monad' b => b Int = _
a
|
11 |     let a :: forall b . Monad' b => b Int = _
|          

鉴于评论GHC doesn't yet support impredicative polymorphism也许您正在尝试的内容还是不可能的。