<div dir="ltr"><div>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:<br><br><span style="font-family:monospace,monospace">> {-# OPTIONS_GHC -Wall #-}<br>> {-# LANGUAGE GADTs, KindSignatures, MultiParamTypeClasses, FunctionalDependencies #-}<br>> <br>> module FundepGadt where<br>> <br>> class C a b | a -> b<br>> <br>> data G :: * -> * where<br>>   -- ...<br>>   GC :: C a b => G b -> G a<br>> <br>> instance Eq (G a) where<br>>   -- ...<br>>   GC b  == GC b' = b == b'</span><br><br>Error message:<br><br><span style="font-family:monospace,monospace">    FundepGadt.hs:14:25: error:<br>        • Couldn't match type 'b1’ with 'b’<br>          'b1’ is a rigid type variable bound by<br>            a pattern with constructor: GC :: forall a b. C a b => G b -> G a,<br>            in an equation for '==’<br>            at FundepGadt.hs:14:12<br>          'b’ is a rigid type variable bound by<br>            a pattern with constructor: GC :: forall a b. C a b => G b -> G a,<br>            in an equation for '==’<br>            at FundepGadt.hs:14:3<br>          Expected type: G b<br>            Actual type: G b1<br>        • In the second argument of '(==)’, namely 'b'’<br>          In the expression: b == b'<br>          In an equation for '==’: (GC b) == (GC b') = b == b'<br>        • Relevant bindings include<br>            b' :: G b1 (bound at FundepGadt.hs:14:15)<br>            b :: G b (bound at FundepGadt.hs:14:6)</span><br><br>I think the functional dependency does ensure that "<span style="font-family:monospace,monospace">b == b</span>" is well-typed.<br><br>In contrast, the following type-family version does type-check:<br><br><span style="font-family:monospace,monospace">>     {-# OPTIONS_GHC -Wall #-}<br>>     {-# LANGUAGE GADTs, KindSignatures, TypeFamilies #-}<br>> <br>>     module TyfamGadt where<br>> <br>>     class C a where<br>>       type B a<br>> <br>>     data G :: * -> * where<br>>       -- ...<br>>       GC :: C a => G (B a) -> G a<br>> <br>>     instance Eq (G a) where<br>>       -- ...<br>>       GC b  == GC b' = b == b'</span><br><br></div>Thanks, - Conal<br></div>