GADTs and functional dependencies?

[Iavor Diatchki]

The method `f` of the class is not important---I simplified the example I'd
written before and forgot to delete it.  Apologies for the noise!

On Tue, Mar 1, 2016 at 10:47 AM, Iavor Diatchki <iavor.diatchki at gmail.com>
wrote:

> 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 at 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 at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160301/7feab548/attachment-0001.html>