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 <conal@conal.net> 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

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