haskell - 使用 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 block 中，即只有 do 的最后一条语句。必须具有 do 的类型 block 的签名。其他语句只需在同一个 monad 中，即 IO a0而不是 IO () .

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

do getLine
   putStrLn "discarded input"

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

在那个特定的例子中，很明显 a0 ~ ()与 a1 ~ Int 完全无关从 GADT 匹配，但一般来说，只有当 GHC 跟踪它来自的所有类型信息时，才能证明这样的事实。我不知道这是否可能，它肯定会比 Haskell 的 Hindley-Milner 系统更复杂，后者严重依赖于统一类型信息，它基本上假设信息来自哪里并不重要。

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

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

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

或通过写作

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