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

Question

{-# 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)

Answer 1

来自GHC docs：

The general principle is this: type refinement is only carried out based on user-supplied type annotations. So if no type signature is supplied for eval, no type refinement happens, and lots of obscure error messages will occur.

换句话说，当我们在 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

最后一个更具体，前两个更笼统。但是，前两个的 none 比另一个更通用——GHC 不能选择 "best" 一个。

GADTs在这方面并不算特别。大多数高级功能都需要类型注释：GADT，higher-rank 类型，类型族至少需要。

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

Why is the Eq (GADT) case giving me a type error?

haskell

gadt