为什么列举所有情况时通配符匹配不起作用？

Question

考虑此代码：

{-# LANGUAGE GADTs #-}

data P t where
 PA :: P Int
 PB :: P Double
 PC :: P Char

isA PA = True
isA _ = False

它可以编译并正常工作。现在考虑以下代码：

{-# LANGUAGE GADTs #-}

data P t where
 PA :: P Int
 PB :: P Double
 PC :: P Char

isA PA = True
isA PB = False
isA PC = False

无法编译：

Main.hs:8:10: error:
    • Couldn't match expected type ‘p’ with actual type ‘Bool’
        ‘p’ is untouchable
          inside the constraints: t ~ Int
          bound by a pattern with constructor: PA :: P Int,
                   in an equation for ‘isA’
          at Main.hs:8:5-6
      ‘p’ is a rigid type variable bound by
        the inferred type of isA :: P t -> p
        at Main.hs:(8,1)-(10,14)
      Possible fix: add a type signature for ‘isA’
    • In the expression: True
      In an equation for ‘isA’: isA PA = True
    • Relevant bindings include isA :: P t -> p (bound at Main.hs:8:1)
  |
8 | isA PA = True
  |          ^^^^

Main.hs:9:10: error:
    • Couldn't match expected type ‘p’ with actual type ‘Bool’
        ‘p’ is untouchable
          inside the constraints: t ~ Double
          bound by a pattern with constructor: PB :: P Double,
                   in an equation for ‘isA’
          at Main.hs:9:5-6
      ‘p’ is a rigid type variable bound by
        the inferred type of isA :: P t -> p
        at Main.hs:(8,1)-(10,14)
      Possible fix: add a type signature for ‘isA’
    • In the expression: False
      In an equation for ‘isA’: isA PB = False
    • Relevant bindings include isA :: P t -> p (bound at Main.hs:8:1)
  |
9 | isA PB = False
  |          ^^^^^

Main.hs:10:10: error:
    • Couldn't match expected type ‘p’ with actual type ‘Bool’
        ‘p’ is untouchable
          inside the constraints: t ~ Char
          bound by a pattern with constructor: PC :: P Char,
                   in an equation for ‘isA’
          at Main.hs:10:5-6
      ‘p’ is a rigid type variable bound by
        the inferred type of isA :: P t -> p
        at Main.hs:(8,1)-(10,14)
      Possible fix: add a type signature for ‘isA’
    • In the expression: False
      In an equation for ‘isA’: isA PC = False
    • Relevant bindings include isA :: P t -> p (bound at Main.hs:8:1)
   |
10 | isA PC = False
   |          ^^^^^

为什么？这是怎么回事？

编辑：添加类型签名isA :: P t -> Bool使它起作用，所以现在我的问题变成了：为什么在第二种情况下键入推断不起作用，因为在第一种情况下起作用？

Answer 1

Disclaimer：之所以将其写为答案，是因为它不适合注释。但我可能错了

GADTs上的模式匹配时，此行为是预期的。最多GHC的User manual：

类型细化仅根据用户提供的类型进行注释。因此，如果没有为eval提供类型签名，则没有类型进行细化，并且会出现很多模糊的错误消息

也来自用户手册：

与从GADT提取的数据构造函数进行模式匹配时，案例表达式中的示例，适用以下规则：

检查的类型必须是刚性的。整个case表达式的类型必须是固定的。在任何一种情况下，任何提及的自由变量的类型都必须是刚性的。

注意：类型变量是刚性的[[iff，它由用户指定。

至此，当与GADT进行模式匹配时，您

必须提供了类型签名（原因是GADTs上的类型推断很困难）。因此，显然isA的第一个定义应该无法编译，但是在paper中解释了GADTs的类型推断（第6.4节）：

我们在第4.3节中指出，在PCON-R中使用它是不合理的除最一般的统一以外的任何统一。但必须细化一个统一者吗？例如，即使case表达式可以做细化，

无需细化就可以检查此功能：

f :: Term a -> Int
f (Lit i) = i
f _       = 0 

以上示例正是您的情况！。在本文中，这称为
pre-unifier

，并对此进行了非常技术性的解释，但据我所知，编写时：

data P t where
 PA :: P Int
 PB :: P Double
 PC :: P Char

isA PA = True
isA PB = False
isA PC = False

编译器通过推导isA :: P t -> p开始并拒绝继续，因为类型变量不是严格的（即不是用户指定的）
而写时：
data P t where
 PA :: P Int
 PB :: P Double
 PC :: P Char

isA PA = True
isA _  = False

编译器可以推断出任何类型推论都不会比将Bool推论为返回类型那么普遍，因此它可以安全地推导isA :: P t -> Bool。
[对您而言，这对我来说似乎很晦涩，但是可以肯定，您所要求的两种情况都已记录在案，所以这可能是GHC开发人员所希望的行为，而不是奇怪的错误。