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无关：在以[.0]结尾的情况下，您会遇到相同的错误。 main。

所以问题确实存在于case块中，即仅putStrLn "done"的最后一个语句必须具有类型 do块的签名。其他语句只需在同一单子中即可，即do而不是IO a0。

现在，通常IO ()是从语句本身推断出来的，因此例如您可以编写

a0

尽管

do getLine
   putStrLn "discarded input"

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

在该特定示例中，很明显case与GADT匹配中的a0 ~ ()毫无关系，但总的来说，只有GHC跟踪针对所有类型信息来源。我不知道这是否可能，它肯定会比Haskell的Hindley-Milner系统复杂得多，后者严重依赖unifying类型的信息，该系统基本上假设信息的来源无关紧要。

因此，GADT匹配项仅充当刚性的“类型信息二极管”：里面的东西永远不能用来确定外部的类型，就像a1 ~ Int块整体上应该是case。

但是，您可以通过相当丑陋的方式手动断言

IO ()

或通过书写

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

Answer 2

@@ aroundabout：我必须使用

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

进行输入。有趣的是，这是在unsafeCoerce所调用的函数中，我显然忽略了mapM_输出。这对我来说没有意义。