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" 

단조 제한이라고 보이지 않습니다. GHC docs에서

* 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

: 형 정제에만 사용자가 제공 한 유형 약어에 따라 수행된다

일반적인 원칙이 인이 내가받을 수 있나요 어떤 오류입니다. 따라서 형식 서명이 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, 상위 순위 유형, 유형 계열이 적어도 있습니다.