使用GADTs - 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的最后一条语句才能具有do块的签名类型。其他语句只需位于同一个单子中，即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的辛德雷-米尔纳系统更复杂，该系统严重依赖于统一类型的信息，该系统本质上假设信息从哪里来并不重要。

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

但是，您可以手动断言，使用相当难看的

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

或通过写作

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