<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
<p>Hey Tom,</p>
<p>there is a paper "Bidirectional type class instances" [1] about a
similar concept.</p>
<p>However, the approach is not implemented in GHC. At the moment,
the dictionary for 'C (a, b)' does not explicitly include a
dictionary for C a and C b. It is only implicitly referenced in
the implementation of C's class methods. <br>
For it to be explicitly available for further usage, the
dictionary data type for classes of C would have to be extended by
an argument. This is not trivial and is discussed in the mentioned
paper. <br>
<br>
The discussion at the GHC proposal show some alternative
approaches how something like this can be achieved with the
current GHC (e.g. [2]).</p>
<p>Best, <br>
Kai<br>
</p>
<p>[1] <a class="moz-txt-link-freetext" href="https://dl.acm.org/doi/abs/10.1145/3331545.3342596">https://dl.acm.org/doi/abs/10.1145/3331545.3342596</a><br>
[2]
<a class="moz-txt-link-freetext" href="https://github.com/ghc-proposals/ghc-proposals/pull/284#issuecomment-542322728">https://github.com/ghc-proposals/ghc-proposals/pull/284#issuecomment-542322728</a><br>
</p>
<div class="moz-cite-prefix">On 30.03.21 09:27, Tom Smeding wrote:<br>
</div>
<blockquote type="cite" cite="mid:tsPyxEBe3m6HcvGYtCT-JgQId3pKWu0v9Cpz2wjf5Kuav2nJZJGuuIIaApsfn0RJKgeIYdKp6JidzfBvu72dmBBzQYqZhmoBVKYDNN7xmww=@tomsmeding.com">
<div>Hi Cafe,<br>
</div>
<div><br>
</div>
<div>With this class definition with this instance:<br>
</div>
<div><br>
</div>
<div> class C a where<br>
</div>
<div> instance C b => C (a, b)<br>
</div>
<div><br>
</div>
<div>GHC can of course infer, given 'C b', that 'C (a, b)'. This
is nothing more<br>
</div>
<div>than the meaning of the instance declaration above.<br>
</div>
<div><br>
</div>
<div>However, GHC cannot infer the inverse:<br>
</div>
<div><br>
</div>
<div> {-# LANGUAGE FlexibleContexts #-}<br>
</div>
<div><br>
</div>
<div> foo :: C a => a -> Int<br>
</div>
<div> foo = undefined<br>
</div>
<div><br>
</div>
<div> bar1 :: C (a, b) => a -> b -> Int<br>
</div>
<div> bar1 _ = foo<br>
</div>
<div><br>
</div>
<div>This gives an error on the right-hand side of 'bar1': "Could
not deduce (C b)<br>
</div>
<div>arising from a use of ‘foo’; from the context: C (a, b)". The
same happens in<br>
</div>
<div>similar cases:<br>
</div>
<div><br>
</div>
<div> {-# LANGUAGE GADTs #-}<br>
</div>
<div><br>
</div>
<div> bar2 :: (C p, p ~ (a, b)) => a -> b -> Int<br>
</div>
<div> bar2 _ = foo<br>
</div>
<div><br>
</div>
<div> data Thing a where<br>
</div>
<div> Tup :: a -> b -> Thing (a, b)<br>
</div>
<div><br>
</div>
<div> bar3 :: C a => Thing a -> Int<br>
</div>
<div> bar3 (Tup x y) = foo y<br>
</div>
<div><br>
</div>
<div>Both these usages of 'foo' yield the same error.<br>
</div>
<div><br>
</div>
<div>My use-case is 'bar3', where I would like GHC to determine
that the call to<br>
</div>
<div>'foo' is valid. (I don't actually care directly about bar1
and bar2.)<br>
</div>
<div><br>
</div>
<div>Is there a way to make 'bar3' compile?<br>
</div>
<div><br>
</div>
<div>Note that:<br>
</div>
<div>- In my actual use case, 'C' is of course not empty.<br>
</div>
<div>- In my actual use case, my type class instances _are_ in
fact injective, even<br>
</div>
<div> though I do enable FlexibleInstances to be able to write
e.g.<br>
</div>
<div> 'instance C (T a Int)'.<br>
</div>
<div>- Above, the dictionary for 'C (a, b)' includes a dictionary
for 'C b', doesn't<br>
</div>
<div> it? So if inference can resolve 'C b', then the compilation
to Core can find<br>
</div>
<div> the right dictionary, I think? (Not sure about this part.)<br>
</div>
<div><br>
</div>
<div>Thanks a lot for your help.<br>
</div>
<div><br>
</div>
<div>Cheers,<br>
</div>
<div>Tom<br>
</div>
<div><br>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
<a class="moz-txt-link-freetext" href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a>
Only members subscribed via the mailman list are allowed to post.</pre>
</blockquote>
</body>
</html>