<div dir="ltr"><a href="https://ghc.haskell.org/trac/ghc/ticket/11534">https://ghc.haskell.org/trac/ghc/ticket/11534</a> is somewhat relevant to this issue. Solving it would seem likely to fix this one as well.<br><div><br></div><div>-Edward</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Mar 1, 2016 at 1:47 PM, Iavor Diatchki <span dir="ltr"><<a href="mailto:iavor.diatchki@gmail.com" target="_blank">iavor.diatchki@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Hello Conal,<div><br></div><div>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.</div><div><br></div><div>Here is an example that shows the problem, just using type signatures:</div><div><font face="monospace, monospace"><br></font></div><div><div><font face="monospace, monospace">> class F a b | a -> b where</font></div><div><font face="monospace, monospace">> f :: a -> b -> ()</font></div><div><font face="monospace, monospace">></font></div><div><font face="monospace, monospace">> instance F Bool Char where</font></div><div><font face="monospace, monospace">> f _ _ = ()</font></div><div><font face="monospace, monospace">></font></div><div><font face="monospace, monospace">> test :: F Bool a => a -> Char</font></div><div><font face="monospace, monospace">> test a = a</font></div><div><br></div><div>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:<br></div></div><div><br></div><div><font face="monospace, monospace">forall x y z. (F x y, F x z) => (y ~ z)</font></div><div><br></div><div>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. </div><div><br></div><div>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.</div><div><br></div><div>I hope this helps!</div><div>-Iavor</div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Mar 1, 2016 at 9:38 AM, Conal Elliott <span dir="ltr"><<a href="mailto:conal@conal.net" target="_blank">conal@conal.net</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>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:<br><br><span style="font-family:monospace,monospace">> {-# OPTIONS_GHC -Wall #-}<br>> {-# LANGUAGE GADTs, KindSignatures, MultiParamTypeClasses, FunctionalDependencies #-}<br>> <br>> module FundepGadt where<br>> <br>> class C a b | a -> b<br>> <br>> data G :: * -> * where<br>> -- ...<br>> GC :: C a b => G b -> G a<br>> <br>> instance Eq (G a) where<br>> -- ...<br>> GC b == GC b' = b == b'</span><br><br>Error message:<br><br><span style="font-family:monospace,monospace"> FundepGadt.hs:14:25: error:<br> • Couldn't match type 'b1’ with 'b’<br> 'b1’ is a rigid type variable bound by<br> a pattern with constructor: GC :: forall a b. C a b => G b -> G a,<br> in an equation for '==’<br> at FundepGadt.hs:14:12<br> 'b’ is a rigid type variable bound by<br> a pattern with constructor: GC :: forall a b. C a b => G b -> G a,<br> in an equation for '==’<br> at FundepGadt.hs:14:3<br> Expected type: G b<br> Actual type: G b1<br> • In the second argument of '(==)’, namely 'b'’<br> In the expression: b == b'<br> In an equation for '==’: (GC b) == (GC b') = b == b'<br> • Relevant bindings include<br> b' :: G b1 (bound at FundepGadt.hs:14:15)<br> b :: G b (bound at FundepGadt.hs:14:6)</span><br><br>I think the functional dependency does ensure that "<span style="font-family:monospace,monospace">b == b</span>" is well-typed.<br><br>In contrast, the following type-family version does type-check:<br><br><span style="font-family:monospace,monospace">> {-# OPTIONS_GHC -Wall #-}<br>> {-# LANGUAGE GADTs, KindSignatures, TypeFamilies #-}<br>> <br>> module TyfamGadt where<br>> <br>> class C a where<br>> type B a<br>> <br>> data G :: * -> * where<br>> -- ...<br>> GC :: C a => G (B a) -> G a<br>> <br>> instance Eq (G a) where<br>> -- ...<br>> GC b == GC b' = b == b'</span><br><br></div>Thanks, - Conal<br></div>
<br>_______________________________________________<br>
ghc-tickets mailing list<br>
<a href="mailto:ghc-tickets@haskell.org" target="_blank">ghc-tickets@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets</a><br>
<br></blockquote></div><br></div>
<br>_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
<br></blockquote></div><br></div>