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

Question

假设我有一个通过 Writer 发出软故障的 monad。简化版本如下(为了记录，我使用的是 GHC 9.0.2):

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE FlexibleContexts #-}
-- {-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Lib where

import Control.Monad.Writer.CPS
import Data.Maybe

verify :: MonadWriter [String] m => some -> args -> m ()
verify _ _ = fix \(_ :: m ()) ->
  do
    let warn = tell . (: [])
        a = Just 1 :: Maybe Int
        b = Just [1, 23] :: Maybe [Int]
        c = Just (id :: forall a. a -> a)
        -- isJust' :: String -> Maybe a -> m ()
        isJust' tag v = unless (isJust v) do
          warn $ tag <> " is Nothing"
    isJust' "a" a
    isJust' "b" b
    isJust' "c" c

一切正常，直到我添加 GADTs 扩展，然后 GHC 无法为 isJust' 找到最通用的类​​型:

    • Couldn't match type ‘[Int]’ with ‘Int’
      Expected: Maybe Int
        Actual: Maybe [Int]
    • In the second argument of ‘isJust'’, namely ‘b’
      In a stmt of a 'do' block: isJust' "b" b
      In the expression:
        do let warn = tell . (: [])
               a = ...
               ....
           isJust' "a" a
           isJust' "b" b
           isJust' "c" c
   |
22 |     isJust' "b" b
   |                 ^

/var/tmp/demo/src/Lib.hs:23:17: error:
    • Couldn't match type ‘a0 -> a0’ with ‘Int’
      Expected: Maybe Int
        Actual: Maybe (a0 -> a0)
    • In the second argument of ‘isJust'’, namely ‘c’
      In a stmt of a 'do' block: isJust' "c" c
      In the expression:
        do let warn = tell . (: [])
               a = ...
               ....
           isJust' "a" a
           isJust' "b" b
           isJust' "c" c
   |
23 |     isJust' "c" c
   |                 ^

此时我必须取消注释 isJust' 的类型注释才能进行类型检查 - 我想知道这里发生了什么，我认为我没有使用任何 GADT特点？

旁注 1:我通常只是猛击 NoMonomorphismRestriction 看看它是否有帮助，但没有。

旁注 2:fix 的使用只是为了在存在 ScopedTypeVariables 的情况下保留 m - 一个附带问题是否有更好的方法来做到这一点而不依赖于具有显式类型签名的verify(假设这个函数是在一个实例中定义的)。

Answer 1

问题不在于GADTs，而在于MonoLocalBinds，它由GADTs 自动启用。问题是 isJust'::String -> Maybe a -> m () 有一个多态类型签名，这意味着你每次调用时都可以选择 a 是什么它。至少，如果 MonoLocalBinds 未启用，它将是多态的。每the documentation :

With MonoLocalBinds, a binding group will be generalised if and only if

• It is a top-level binding group, or
• Each of its free variables (excluding the variables bound by the group itself) is closed (see next bullet), or
• Any of its binders has a partial type signature (see Partial Type Signatures).

如果一个变量不满足三个要点之一，它的类型就不是泛化的，即它不是多态的。

对于什么是“闭变量”，有一个严格的定义，但重要的是:

if a variable is closed, then its type definitely has no free type variables.

isJust' 的第二个参数的类型是Maybe a，代表一些未知的a，这意味着它不是关闭(编辑:请参阅夏丽瑶在评论中的更正)。因此，项目符号 1 不满足，因为 isJust' 是在 verify 中定义的，项目符号 2 不满足，因为 isJust' 的第二个参数不是关闭，项目符号 3 不满足，因为 isJust' 类型没有漏洞。因此，isJust' 毕竟不是多态的。

这意味着 String -> Maybe a -> m () 中的 a 实际上是 GHC 必须推断的固定类型。它看到你调用 isJust' "a"(a::Maybe Int) 并假定 a ~ Int，但随后它看到 isJust' "b"(b::Maybe [Int]) 并假定 a ~ [Int]。显然这是一个问题，所以 GHC 提示。添加类型签名所做的唯一事情就是告诉 GHC 使 isJust' 多态。

请注意，您可以同时拥有 GADTs 和 NoMonoLocalBinds，但是因为 GADTs 的类型推断很棘手，这可能只会导致当您实际使用 GADT 时会遇到更多问题。