使用 GADT 进行类型推断 - a0 是不可触及的

Question

假设我有这个程序

{-# LANGUAGE GADTs #-}

data My a where
  A :: Int  -> My Int
  B :: Char -> My Char


main :: IO ()
main = do
  let x = undefined :: My a

  case x of
    A v -> print v

  -- print x

编译正常。

但是当我在 print x 中发表评论时，我得到：

gadt.hs: line 13, column 12:
  Couldn't match type ‘a0’ with ‘()’
    ‘a0’ is untouchable
      inside the constraints (a1 ~ GHC.Types.Int)
      bound by a pattern with constructor
                 Main.A :: GHC.Types.Int -> Main.My GHC.Types.Int,
               in a case alternative
      at /home/niklas/src/hs/gadt-binary.hs:13:5-7
  Expected type: GHC.Types.IO a0
    Actual type: GHC.Types.IO ()
  In the expression: System.IO.print v
  In a case alternative: Main.A v -> System.IO.print v

为什么我在第 13 行 (A v -> print v) 而不是仅在 print x 行收到此错误？

我认为第一次出现应该确定类型。

请赐教:)

Answer 1

嗯，首先请注意，这与特定的 print x 无关：当 main 以例如结尾时，您会遇到相同的错误。 putStrLn "done".

所以问题确实出在 case 块中，即 只有 do 的最后一条语句需要具有 [=16] 的类型 =] 区块的签名。其他语句只需要在同一个 monad 中，即 IO a0 而不是 IO ().

现在，通常这个 a0 是从语句本身推断出来的，所以例如你可以写

do getLine
   putStrLn "discarded input"

虽然 getLine :: IO String 而不是 IO ()。但是，在您的示例中，信息 print :: ... -> IO () 来自 case 块内部， 来自 GADT 匹配 。这种 GADT 匹配的行为与其他 Haskell 语句不同：基本上，它们不会让任何类型信息超出其范围，因为如果信息来自 GADT 构造函数，那么它在 case 之外是不正确的.

在那个特定的例子中，很明显 a0 ~ () 与 GADT 比赛中的 a1 ~ Int 完全无关，但一般来说，只有在以下情况下才能证明这一事实GHC 追踪了所有类型信息 的来源。我不知道这是否可能，它肯定会比 Haskell 的 Hindley-Milner 系统更复杂，后者严重依赖 unifying 类型信息，这基本上假设信息来自何处并不重要。

因此，GADT 匹配只是作为一个刚性的“类型信息二极管”：里面的东西永远不能用来确定外部的类型，就像 case 块作为一个整体应该是 IO ().

但是，您可以手动断言，相当丑陋

  (case x of
     A v -> print v
    ) :: IO ()

或写

  () <- case x of
          A v -> print v

使用 GADT 进行类型推断 - a0 是不可触及的

Type inference with GADTs - a0 is untouchable

haskell

gadt