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(a)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(a)haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
>
>
tl;dr. Stabilizing the ghc-8.0 is taking a bit longer than was anticipated.
The release schedule is being pushed back a bit.
Hello everyone,
As you likely know we are currently in the depths of the 8.0 release. In
fact, under more ideal circumstances I would probably be cutting another
release candidate right now instead of writing this email, in
preparation for a final release next week or so.
However, our world is far from ideal as evidenced by the number
[1] of significant bugs present on the 8.0 branch. This isn't altogether
unexpected; we knew we were taking a bit of a risk in merging so many
high-impact patches in one release. However, we thought that given a
longer-than-usual period between first-candidate and the final release,
we'd have enough time to smooth out the wrinkles. Sadly, this has taken
a bit longer than we anticipated.
Of course, the last thing we want is to push a known buggy release out
the door. Consequently, we won't be delivering the 8.0.1 release next
week as originally planned. Instead, we'll be pushing the release back
by about three weeks. This will give developers a bit more breathing
room in which to work out the remaining issues. Hopefully in a few weeks
the tree will be in such a state that we can push out yet another
candidate which, with luck, will be the last before the release.
If you'd like to expedite the process (and have fun in the process), you
could do worse than to having a look at Trac [1], choosing a bug of your
liking, and trying your hand at solving it.
Thanks to everyone who has contributed to this effort thusfar.
If you have any questions about the release process or how you can help,
don't hesistate to ask.
Cheers,
- Ben
[1] https://ghc.haskell.org/trac/ghc/wiki/Status/GHC-8.0.1
