在这种情况下，GADT 如何影响类型推断？

Question

假设我有一个通过 Writer 发出软故障的 monad。简化版本如下（郑重声明，我使用的是 GHC 9.0.2）：

\n

{-# LANGUAGE BlockArguments #-}\n{-# LANGUAGE FlexibleContexts #-}\n-- {-# LANGUAGE GADTs #-}\n{-# LANGUAGE ScopedTypeVariables #-}\n\nmodule Lib where\n\nimport Control.Monad.Writer.CPS\nimport Data.Maybe\n\nverify :: MonadWriter [String] m => some -> args -> m ()\nverify _ _ = fix \\(_ :: m ()) ->\n  do\n    let warn = tell . (: [])\n        a = Just 1 :: Maybe Int\n        b = Just [1, 23] :: Maybe [Int]\n        c = Just (id :: forall a. a -> a)\n        -- isJust\' :: String -> Maybe a -> m ()\n        isJust\' tag v = unless (isJust v) do\n          warn $ tag <> " is Nothing"\n    isJust\' "a" a\n    isJust\' "b" b\n    isJust\' "c" c\n

\n

一切都很顺利，直到我添加GADTs扩展名，然后 GHC 无法找到最通用的类​​型isJust\'：

\n

    \xe2\x80\xa2 Couldn\'t match type \xe2\x80\x98[Int]\xe2\x80\x99 with \xe2\x80\x98Int\xe2\x80\x99\n      Expected: Maybe Int\n        Actual: Maybe [Int]\n    \xe2\x80\xa2 In the second argument of \xe2\x80\x98isJust\'\xe2\x80\x99, namely \xe2\x80\x98b\xe2\x80\x99\n      In a stmt of a \'do\' block: isJust\' "b" b\n      In the expression:\n        do let warn = tell . (: [])\n               a = ...\n               ....\n           isJust\' "a" a\n           isJust\' "b" b\n           isJust\' "c" c\n   |\n22 |     isJust\' "b" b\n   |                 ^\n\n/var/tmp/demo/src/Lib.hs:23:17: error:\n    \xe2\x80\xa2 Couldn\'t match type \xe2\x80\x98a0 -> a0\xe2\x80\x99 with \xe2\x80\x98Int\xe2\x80\x99\n      Expected: Maybe Int\n        Actual: Maybe (a0 -> a0)\n    \xe2\x80\xa2 In the second argument of \xe2\x80\x98isJust\'\xe2\x80\x99, namely \xe2\x80\x98c\xe2\x80\x99\n      In a stmt of a \'do\' block: isJust\' "c" c\n      In the expression:\n        do let warn = tell . (: [])\n               a = ...\n               ....\n           isJust\' "a" a\n           isJust\' "b" b\n           isJust\' "c" c\n   |\n23 |     isJust\' "c" c\n   |                 ^\n

\n

此时我必须取消注释类型注释才能isJust\'进行类型检查 - 我想知道这里发生了什么，我不认为我正在使用任何 GADT 功能？

\n

旁注 1：我通常只是按 aNoMonomorphismRestriction看看是否有帮助，但没有。

\n

旁注 2：使用 的目的只是为了在存在的情况下fix掌握这一点- 一个附带问题是是否有更好的方法来做到这一点而不依赖于显式类型签名（假设该函数是在实例内定义的） 。mScopedTypeVariablesverify

\n

Answer 1

问题不是GADTs但是MonoLocalBinds，它是由自动启用的GADTs。问题是它具有多态类型签名，这意味着您每次调用它时都isJust' :: String -> Maybe a -> m ()可以选择什么。a至少，如果 MonoLocalBinds不启用它将会是多态的。根据文档：

使用 MonoLocalBinds，绑定组将被泛化当且仅当

• 它是一个顶级绑定组，或者
• 它的每个自由变量（不包括组本身绑定的变量）都是封闭的（参见下一个项目符号），或者
• 它的任何绑定器都有部分类型签名（请参阅部分类型签名）。

如果变量不满足三个要点之一，则其类型不会被泛化，即它不会成为多态。

什么是“封闭变量”有严格的定义，但重要的部分是：

如果一个变量是封闭的，那么它的类型肯定没有自由类型变量。

的第二个参数具有某些未知的isJust'类型，这意味着它不是封闭的（编辑：请参阅评论中 Li-yao Xia 的更正）。因此，项目符号 1 不满足，因为是在 中定义的，项目符号 2 不满足，因为 的第二个参数未封闭，项目符号 3 不满足，因为 的类型中没有漏洞。因此，它毕竟不是多态的。Maybe aaisJust'verifyisJust'isJust'isJust'

所有这些意味着ainString -> Maybe a -> m ()实际上是 GHC 必须推断的固定类型。它看到你调用isJust' "a" (a::Maybe Int)并假设a ~ Int，但随后它也看到isJust' "b" (b::Maybe [Int])并假设a ~ [Int]。显然这是一个问题，因此 GHC 抱怨道。添加类型签名的唯一作用是告诉 GHC 进行isJust'多态。

请注意，您可以同时使用GADTs和，但由于 GADT 的类型推断很棘手，因此当您实际使用 GADT 时，这可能会导致更多问题。NoMonoLocalBinds