Dlaczego GHC generuje błąd ograniczenia równości, a nie błąd dopasowania typu?

Question

Kontynuując od this question, nie jestem pewien, dlaczego te dwa fragmenty kodu produkować zupełnie różne błędy:

f :: a -> b 
f x = x 
-- Couldn't match expected type `b' with actual type `a' 
-- In the expression: x 

g :: Monad m => a -> m b 
g x = return x 
-- Could not deduce (a ~ b) from the context (Monad m) 
-- In the first argument of `return', namely `x'. 

Jaka jest zasada powodujące tego zachowania?

Nie jest czytelny, nawet dla kogoś, kto zna standardowy Haskell; ograniczenie równości (a ~ b) wymaga rozszerzenia języka.

zauważyć, że jako chi wskazał, sama obecność ograniczenie powoduje błąd wiązania:

class C a 

h :: C a => a -> b 
h x = x 
-- Could not deduce... 

(Pusty ograniczeń, () => a -> b, daje nie odpowiadać błąd wiązania.)

Answer 1

Nie sądzę, że odpowiedź jest krótsza niż wgłębienie w GHC, aby zrozumieć dlaczego.

Jeśli używasz GHC z przełącznikiem -ddump-tc-trace, możesz uzyskać dość długą historię procesu sprawdzania poprawności. W szczególności, jeśli uruchomić go na ten kod:

f :: a -> b 
f x = x 

class C a 

h :: C c => c -> d 
h x = x 

Widać, że typechecking a vs b i typechecking c vs d postępuje dokładnie tak samo w obu przypadkach, zakończone w dwóch następujących nierozwiązanych ograniczeń (wyjście wynosi od GHC 7.8.2):

tryReporters { [[W] cobox_aJH :: c ~ d (CNonCanonical)] 
... 
tryReporters { [[W] cobox_aJK :: a ~ b (CNonCanonical)] 

Postępując zgodnie z króliczej nory nieco więcej w TcErrors, można zobaczyć, że dla równości na skolems, tryReporters ostatecznie dostaje się do tworzenia się komunikat o błędzie poprzez misMatchOrCND, WH Ich ma wyraźny specjalny przypadek dla pustych kontekstów:

misMatchOrCND :: ReportErrCtxt -> Ct -> Maybe SwapFlag -> TcType -> TcType -> SDoc 
-- If oriented then ty1 is actual, ty2 is expected 
misMatchOrCND ctxt ct oriented ty1 ty2 
    | null givens || 
    (isRigid ty1 && isRigid ty2) || 
    isGivenCt ct 
     -- If the equality is unconditionally insoluble 
     -- or there is no context, don't report the context 
    = misMatchMsg oriented ty1 ty2 
    | otherwise 
    = couldNotDeduce givens ([mkTcEqPred ty1 ty2], orig)