Hello Conal, the implementation of fun-deps in GHC is quite limited, and they don't do what you'd expect with existential types (like in your example), type-signatures, or GADTs. Basically, GHC only uses fun-deps to fill-in types for unification variables, but it won't use them to reason about quantified variables. Here is an example that shows the problem, just using type signatures:

class F a b | a -> b where f :: a -> b -> ()

instance F Bool Char where f _ _ = ()

test :: F Bool a => a -> Char test a = a

GHC rejects the declaration for `test` because there it needs to prove that `a ~ Char`. Using the theory of fun-deps, the equality follows because from the fun-dep we know that: forall x y z. (F x y, F x z) => (y ~ z) Now, if we instantiate this axiom with `Bool`, `Char`, and `a`, we can prove that `Char ~ a` by combining the instance and the local assumption from the signature. Unfortunately, this is exactly the kind of reasoning GHC does not do. I am not 100% sure on why not, but at present GHC will basically do all the work to ensure that the fun-dep axiom for each class is valid (that's all the checking that instances are consistent with their fun-deps), but then it won't use that invariant when solving equalities. I hope this helps! -Iavor On Tue, Mar 1, 2016 at 9:38 AM, Conal Elliott wrote:

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

_______________________________________________ ghc-tickets mailing list ghc-tickets@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets