Почему случай 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:

Общий принцип таков: типа уточнение осуществляется только на основе введенных пользователем аннотаций типа. Поэтому, если сигнатура типа не указана для 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, типы более высокого ранга, семейства типов, по крайней мере, делают.