使用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以eg 结尾时会出现相同的错误putStrLn "done".

所以这个问题确实是在块的情况下,即在只的最后一条语句do必须具有类型的的do块的签名.其他陈述只需要在同一个monad中,IO a0而不是IO ().

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

do getLine
   putStrLn "discarded input"

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

在那个特定的例子中,似乎很明显a0 ~ ()与a1 ~ IntGADT匹配没有任何关系,但总的来说,这样的事实只有在GHC跟踪它来自的所有类型信息时才能被证明.我不知道这是否可能,它肯定会比Haskell的Hindley-Milner系统更复杂,后者严重依赖于统一类型信息,这基本上假设信息来自何处并不重要.

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

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

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

或通过写作

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