GHC 无法在不单态化的情况下绑定多态函数
GHC fails to bind polymorphic function without monomorphising it
在原始代码中，可以看到我只是将表达式提取到绑定中，这是 haskell 声称应该始终可行的基本内容之一。
最小案例（在@dminuoso 的帮助下在 freenode 上创建）
我希望 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’
正如 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"
成功。
如果我输入一个打字孔，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 可能您正在尝试的还不可能。
documentation on pattern type signatures 的相关位是这样的：
Unlike expression and declaration type signatures, pattern type signatures are not implicitly generalised.
所以模式签名，就像你写的那样，是一种特殊情况，其中泛化（这是将单态类型t转换为提到范围外类型变量a的过程进入多态类型 forall a. t) 还没有完成。您可以使用任何其他形式的类型签名来恢复泛化过程；例如而不是
let foo :: forall a. a = undefined
尝试：
let foo :: forall a. a
foo = undefined
第 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
GHC 正在寻找，在 type f :: * -> *; instance Functor f 的上下文中，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 () 填充 _。这很难，我们很快就会看到...
（我真的不认为 Daniel Wagner 引用的内容在这里是相关的。我相信它只是指差异（当 ScopedTypeVariables 开启且 type a 不在范围内时）在 5 :: Num a => a 隐式表示 5 :: forall a. Num a => a 和 g :: a -> a = id 不 表示 g :: forall a. a -> a = id 的方式之间。）
第 2 部分
当你写的时候会发生什么
undefined
？具体来说，它的类型是什么？您可能认为它是 forall a. a，但这并不完全正确。是的，确实 all by itself，undefined 的类型是 forall a. a，但是 GHC 不允许你写 undefined all by itself .相反，表达式中每次出现的 undefined 总是应用于类型参数。上面被隐式重写为
undefined @_a0
并创建了一个新的统一变量（实际上没有名称）_a0。此表达式的类型为 _a0。如果我在需要 Int 的上下文中使用此表达式，则 _a0 必须等于 Int，并且 GHC 设置 _a0 := Int，将表达式重写为
undefined @Int
(因为_a0可以设置为某种东西，所以叫统一变量。在"our"下，内部控制。上面，f 不能设置为任何值。它是给定的，并且在"their"（用户的）外部控制下，这使它成为一个 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 ())。通常，这是一个禁忌，因为这是谓语多态性：将类型变量设置为包含 forall 的类型。但是，在足够过时的 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
这行得通。
在原始代码中，可以看到我只是将表达式提取到绑定中，这是 haskell 声称应该始终可行的基本内容之一。
最小案例（在@dminuoso 的帮助下在 freenode 上创建）
我希望 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’
正如 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"
成功。
如果我输入一个打字孔，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 可能您正在尝试的还不可能。
documentation on pattern type signatures 的相关位是这样的：
Unlike expression and declaration type signatures, pattern type signatures are not implicitly generalised.
所以模式签名，就像你写的那样，是一种特殊情况，其中泛化（这是将单态类型t转换为提到范围外类型变量a的过程进入多态类型 forall a. t) 还没有完成。您可以使用任何其他形式的类型签名来恢复泛化过程；例如而不是
let foo :: forall a. a = undefined
尝试：
let foo :: forall a. a
foo = undefined
第 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
GHC 正在寻找，在 type f :: * -> *; instance Functor f 的上下文中，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 () 填充 _。这很难，我们很快就会看到...
（我真的不认为 Daniel Wagner 引用的内容在这里是相关的。我相信它只是指差异（当 ScopedTypeVariables 开启且 type a 不在范围内时）在 5 :: Num a => a 隐式表示 5 :: forall a. Num a => a 和 g :: a -> a = id 不 表示 g :: forall a. a -> a = id 的方式之间。）
第 2 部分
当你写的时候会发生什么
undefined
？具体来说，它的类型是什么？您可能认为它是 forall a. a，但这并不完全正确。是的，确实 all by itself，undefined 的类型是 forall a. a，但是 GHC 不允许你写 undefined all by itself .相反，表达式中每次出现的 undefined 总是应用于类型参数。上面被隐式重写为
undefined @_a0
并创建了一个新的统一变量（实际上没有名称）_a0。此表达式的类型为 _a0。如果我在需要 Int 的上下文中使用此表达式，则 _a0 必须等于 Int，并且 GHC 设置 _a0 := Int，将表达式重写为
undefined @Int
(因为_a0可以设置为某种东西，所以叫统一变量。在"our"下，内部控制。上面，f 不能设置为任何值。它是给定的，并且在"their"（用户的）外部控制下，这使它成为一个 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 ())。通常，这是一个禁忌，因为这是谓语多态性：将类型变量设置为包含 forall 的类型。但是，在足够过时的 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
这行得通。