haskell - 为什么 GHCi 在此错误消息中不显示多态类型？

Question

我将 Num a => a -> a 类型的变量的类型归因于 Int，这会按照预期抛出错误。然而，错误并不完全符合我的预期。

GHCi

λ> let x = typeInference 1
λ> :t x
x :: Num a => a -> a
λ> x :: Int

<interactive>:141:1: error:
    • Couldn't match expected type 'Int'
                  with actual type 'Integer -> Integer'
    • Probable cause: 'x' is applied to too few arguments
      In the expression: x :: Int
      In an equation for 'it': it = x :: Int
λ>

类型推断定义

typeInference :: Num a => a -> a -> a
typeInference x y = x + y + 1

我期望错误消息显示实际类型为“Num a => a -> a”，这是多态类型，为什么不呢？这与 GHCi 的类型默认有关吗？

Answer 1

这确实是因为GHCi's type defaulting .

section 4.3.4 of the Haskell 2010 Report 中描述了此规则。这部分特别相关:

Each defaultable variable is replaced by the first type in the default list that is an instance of all the ambiguous variable’s classes. It is a static error if no such type is found.

每个可默认的变量都会被其默认值替换，这是在生成错误消息之前发生的操作。

当存在不明确的类型时，类型默认必须在类型检查之前发生。特别是，如果保留类型类约束而不是默认值，则表达式 x::Int 中将具有不明确的类型，如

中所定义。

We say that an expression e has an ambiguous type if, in its type ∀ u'. cx ⇒ t, there is a type variable u in u' that occurs in cx but not in t. Such types are invalid.

(摘自 Haskell 2010 报告，将 u 替换为带有 u' 的上划线)。

因为，如果类型有效，则整个表达式将具有一个类型变量(受 Num 约束的变量)，该变量不会出现在结果类型 (Int )(并且类型变量不能被统一掉)，这里的默认必须在类型检查之前发生。

通过意识到我们正在进行类型检查，这可以变得更加明确

(x :: forall a. Num a => a -> a) :: Int

看起来，在统一期间，如果最外层的类型构造函数与左侧的 ((->) 和右侧的 Int 不匹配侧)，它必须默认，因为它不能自动深入到统一(如果右侧最外层的类型构造函数也是 (->) 的话，就可以了)。

以下是我测试过的几个遵循此行为的示例:

ghci> :set -XExplicitForAll
ghci> (x :: forall a. Num a => a -> a) :: Char -> Char  -- Outermost constructor matches, so 'a' can get unified with Char and the 'a' type variable disappears

<interactive>:5:2: error:
    • No instance for (Num Char)
        arising from an expression type signature
    • In the expression:
          (x :: forall a. Num a => a -> a) :: Char -> Char
      In an equation for ‘it’:
          it = (x :: forall a. Num a => a -> a) :: Char -> Char
ghci> (x :: forall a. Num a => a -> a) :: Maybe Char

<interactive>:8:2: error:
    • Couldn't match expected type ‘Maybe Char’
                  with actual type ‘Integer -> Integer’
    • In the expression: (x :: forall a. Num a => a -> a) :: Maybe Char
      In an equation for ‘it’:
          it = (x :: forall a. Num a => a -> a) :: Maybe Char
ghci> (x :: forall a. Num a => a -> a) :: Either Char Bool

<interactive>:10:2: error:
    • Couldn't match expected type ‘Either Char Bool’
                  with actual type ‘Integer -> Integer’
    • In the expression:
          (x :: forall a. Num a => a -> a) :: Either Char Bool
      In an equation for ‘it’:
          it = (x :: forall a. Num a => a -> a) :: Either Char Bool
ghci> (x :: forall a. Num a => (,) a a) :: Either Char Bool

<interactive>:11:2: error:
    • Couldn't match expected type ‘Either Char Bool’
                  with actual type ‘(Integer, Integer)’
    • In the expression:
          (x :: forall a. Num a => (,) a a) :: Either Char Bool
      In an equation for ‘it’:
          it = (x :: forall a. Num a => (,) a a) :: Either Char Bool
ghci> (x :: forall a. Num a => (,) a a) :: Char

<interactive>:12:2: error:
    • Couldn't match expected type ‘Char’
                  with actual type ‘(Integer, Integer)’
    • In the expression: (x :: forall a. Num a => (,) a a) :: Char
      In an equation for ‘it’:
          it = (x :: forall a. Num a => (,) a a) :: Char