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

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"

It does not seem to be the monomorphism restriction. This is what error do I get:

* 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

From the 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.

In other words, when we pattern match on a GADT type (either through multiple equations or with a case), providing an explicit type annotation is necessary.

As a thought experiment consider

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

f (C c) = c

What is the right typing?

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

The last one is more specific, the first two are strictly more general. However, none of the first two is more general than the other -- GHC can not pick the "best" one.

GADTs are not too special in this. Most advanced features require type annotations: GADTs, higher-rank types, type families at least do.