<div>Hi Kai,<br></div><div><br></div><div>Thanks for the links! Your [2] is a workaround that works perfectly for my purposes. I had already considered using an associated type, but that puts the GHC type checker into an infinite loop... Using a separate type family fixes my issue.<br></div><div><br></div><div>Cheers,<br></div><div>Tom<br></div><div class="protonmail_signature_block protonmail_signature_block-empty"><div class="protonmail_signature_block-user protonmail_signature_block-empty"><div><br></div></div><div class="protonmail_signature_block-proton protonmail_signature_block-empty"><br></div></div><div><br></div><div>‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐<br></div><div> On Tuesday, March 30, 2021 10:01 AM, Kai-Oliver Prott <kai.prott@hotmail.de> wrote:<br></div><div> <br></div><blockquote class="protonmail_quote" type="cite"><p>Hey Tom,<br></p><p>there is a paper "Bidirectional type class instances" [1] about a
similar concept.<br></p><p></p><div>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></div><div> 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></div><div> <br></div><div> The discussion at the GHC proposal show some alternative
approaches how something like this can be achieved with the
current GHC (e.g. [2]).<br></div><p></p><p></p><div>Best, <br></div><div> Kai<br></div><p></p><p></p><div>[1] <a href="https://dl.acm.org/doi/abs/10.1145/3331545.3342596">https://dl.acm.org/doi/abs/10.1145/3331545.3342596</a><br></div><div> [2] <a 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></div><p></p><div class="moz-cite-prefix">On 30.03.21 09:27, Tom Smeding wrote:<br></div><blockquote type="cite"><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><div><br></div><pre wrap>_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
<a 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.<br></pre></blockquote></blockquote><div><br></div>