Do GADTs and functional dependencies get along? I'm wondering why the following code doesn't type-check under GHC 7.10.3 and 8.1.20160224:
{-# OPTIONS_GHC -Wall #-} {-# LANGUAGE GADTs, KindSignatures, MultiParamTypeClasses, FunctionalDependencies #-}
module FundepGadt where
class C a b | a -> b
data G :: * -> * where -- ... GC :: C a b => G b -> G a
instance Eq (G a) where -- ... GC b == GC b' = b == b'
Error message: FundepGadt.hs:14:25: error: • Couldn't match type 'b1’ with 'b’ 'b1’ is a rigid type variable bound by a pattern with constructor: GC :: forall a b. C a b => G b -> G a, in an equation for '==’ at FundepGadt.hs:14:12 'b’ is a rigid type variable bound by a pattern with constructor: GC :: forall a b. C a b => G b -> G a, in an equation for '==’ at FundepGadt.hs:14:3 Expected type: G b Actual type: G b1 • In the second argument of '(==)’, namely 'b'’ In the expression: b == b' In an equation for '==’: (GC b) == (GC b') = b == b' • Relevant bindings include b' :: G b1 (bound at FundepGadt.hs:14:15) b :: G b (bound at FundepGadt.hs:14:6) I think the functional dependency does ensure that "b == b" is well-typed. In contrast, the following type-family version does type-check:
{-# OPTIONS_GHC -Wall #-} {-# LANGUAGE GADTs, KindSignatures, TypeFamilies #-}
module TyfamGadt where
class C a where type B a
data G :: * -> * where -- ... GC :: C a => G (B a) -> G a
instance Eq (G a) where -- ... GC b == GC b' = b == b'
Thanks, - Conal