为什么 Eq (GADT) 案例给我一个类型错误？答案

【问题标题】：Why is the Eq (GADT) case giving me a type error?为什么 Eq (GADT) 案例给我一个类型错误？
【发布时间】：2017-01-17 14:43:03
【问题描述】：

{-# LANGUAGE GADTs #-}

module Main where

data CudaExpr x where
  C :: x -> CudaExpr x

  Add :: Num x => CudaExpr x -> CudaExpr x -> CudaExpr x
  Sub :: Num x => CudaExpr x -> CudaExpr x -> CudaExpr x
  Mul :: Num x => CudaExpr x -> CudaExpr x -> CudaExpr x
  Div :: (Num x, Fractional x) => CudaExpr x -> CudaExpr x -> CudaExpr x

  Eq :: (Eq x) => CudaExpr x -> CudaExpr x -> CudaExpr Bool
  -- LessThan :: CudaExpr x -> CudaExpr x -> CudaExpr Bool
  -- If :: CudaExpr Bool -> CudaExpr x -> CudaExpr x -> CudaExpr x

eval (C x) = x
eval (Add a b) = eval a + eval b
eval (Sub a b) = eval a - eval b
eval (Mul a b) = eval a * eval b
eval (Div a b) = eval a / eval b

eval (Eq a b) = eval a == eval b
-- eval (LessThan a b) = eval a < eval b
-- eval (If cond true false) = if eval cond then eval true else eval false


main :: IO ()
main = print "Hello"

似乎不是单态限制。这是我得到的错误：

* Could not deduce: x ~ Bool
  from the context: (t ~ Bool, Eq x)
    bound by a pattern with constructor:
               Eq :: forall x. Eq x => CudaExpr x -> CudaExpr x -> CudaExpr Bool,
             in an equation for `eval'
    at app\Main.hs:23:7-12
  `x' is a rigid type variable bound by
    a pattern with constructor:
      Eq :: forall x. Eq x => CudaExpr x -> CudaExpr x -> CudaExpr Bool,
    in an equation for `eval'
    at app\Main.hs:23:7
  Expected type: CudaExpr x -> Bool
    Actual type: CudaExpr t -> t
* In the first argument of `(==)', namely `eval a'
  In the expression: eval a == eval b
  In an equation for `eval': eval (Eq a b) = eval a == eval b
* Relevant bindings include
    b :: CudaExpr x (bound at app\Main.hs:23:12)
    a :: CudaExpr x (bound at app\Main.hs:23:10)

【问题讨论】：

eval 的返回类型是什么？不能是Num x => x，因为eval (Eq (C 3) (C 3))需要返回True :: Bool。不能是Bool，因为eval (Add (C 3) (C 3))需要返回6 :: Num x => x。
嗯，显然它应该取决于传递给函数的 CudaExpr 的结构。我不明白为什么它不应该是其中一个。我知道上面的示例可以使用幻像类型进行编码，那么我在这里设置问题的类型类约束是什么？ ...不，即使我注释掉所有案例但 Eq 它仍然不起作用。
好的，我明白了。毕竟有点像单态限制。一旦我添加了类型注释eval :: CudaExpr x -> x，错误就会消失。感谢您的提示。
GADT 和类型推断不能很好地混合：当您通过 GADT 进行模式匹配时，请始终添加显式类型注释

标签： haskell gadt

【解决方案1】：

来自GHC docs：

一般原则是：类型细化仅基于用户提供的类型注释进行。因此，如果没有为eval 提供类型签名，则不会发生类型细化，并且会出现许多晦涩的错误消息。

换句话说，当我们对 GADT 类型进行模式匹配时（通过多个方程式或使用 case），提供显式类型注释是必要的。

作为一个思想实验考虑

data T a where C :: Char -> T Char

f (C c) = c

什么是正确的打字方式？

f :: T a    -> a
f :: T a    -> Char
f :: T Char -> Char

最后一个更具体，前两个更笼统。但是，前两个中没有一个比另一个更通用——GHC 不能选择“最好”的那个。

GADT 在这方面并不太特别。大多数高级功能都需要类型注释：GADT、更高级别的类型、类型族至少需要。

【讨论】：