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 <[email protected]> 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 <[email protected]> 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 >> [email protected] >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets >> >> >
_______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
