<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div class="">> Is there a way to somehow convince GHC of that fact so that g typechecks?</div><div class=""><br class=""></div>No.<div class=""><br class=""></div><div class="">First, it would actually be unsound to do so, because of the possibility of exotic types, built with pathological combinations of type and data families: <a href="https://gitlab.haskell.org/ghc/ghc/-/issues/14420" class="">https://gitlab.haskell.org/ghc/ghc/-/issues/14420</a></div><div class=""><br class=""></div><div class="">But, actually, the bigger problem is that we need a class constraint in order to allow a function to compute at runtime. The function f actually takes two arguments at runtime: a representation of the instance which carries f's implementation (this is sometimes called a dictionary), and the normal argument of type a. `g`, on the other hand, has no access to the dictionary needed at runtime, and so it's unclear how it should compute.</div><div class=""><br class=""></div><div class="">Put another way: a value of type Foo carries no information (beyond the fact that it terminates), because Foo has only one data constructor. So there's no way that g :: Foo a -> Int could be anything but a constant function. You need the class constraint to change this fact.</div><div class=""><br class=""></div><div class="">Hope this helps!</div><div class="">Richard</div><div class=""><div class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Mar 2, 2021, at 9:16 AM, Paul Brauner <<a href="mailto:polux2001@gmail.com" class="">polux2001@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class="">Hello,<div class=""><br class=""></div><div class="">the following program doesn't typecheck in GHC 9:</div><div class=""><br class=""></div><div class=""><font face="monospace" class="">data Tag = A | B<br class="">data Foo (a :: Tag) = Foo<br class=""><br class="">class C a where<br class=""> f :: a -> Int<br class=""><br class="">instance C (Foo A) where<br class=""> f x = 1<br class=""><br class="">instance C (Foo B) where<br class=""> f x = 2<br class=""><br class="">g :: Foo a -> Int<br class="">g = f</font><br class=""></div><div class=""><font face="monospace" class=""><br class=""></font></div><div class="">Yet one could argue that for all a :: Tag, C (Foo a) holds because a :: Tag can only take two values: A or B, and C (Foo A) and C (Foo B) hold. Is there a way to somehow convince GHC of that fact so that g typechecks?</div><div class=""><br class=""></div><div class="">Cheers,</div><div class="">Paul</div></div>
_______________________________________________<br class="">Haskell-Cafe mailing list<br class="">To (un)subscribe, modify options or view archives go to:<br class=""><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br class="">Only members subscribed via the mailman list are allowed to post.</div></blockquote></div><br class=""></div></div></body></html>