<div><br></div><div><div class="gmail_quote"><div dir="ltr">On Mon, 10 Dec 2018 at 6:12 PM, Anthony Clayden <<a href="mailto:anthony_clayden@clear.net.nz">anthony_clayden@clear.net.nz</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div>On Mon, 10 Dec 2018 at 9:36 PM, Tom Schrijvers wrote:<br></div><div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div dir="ltr"><div>Maybe our Haskell'17 paper about Elaboration on Functional Dependencies sheds some more light on your problem:</div><div><a href="https://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/haskell2017a.pdf" target="_blank">https://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/haskell2017a.pdf</a><br></div><div><br></div><div></div></div></div></blockquote><div dir="auto"><br></div><div dir="auto">Thank you Tom, looks interesting and very applicable. It'll be a few days before I can take a proper look.</div><div dir="auto"></div></div></div></blockquote><div dir="auto"><br></div><div dir="auto">So the paper's main motivation is wrt Trac #9670. I've added some comments there, including a link to your paper. In particular, both GHC and Hugs will infer the 'right' type -- i.e. as improved from the FunDep. But neither allows you to use that improvement to write the desired function `f`. It's a phasing of inference thing(?)</div><div dir="auto"><br></div><div dir="auto">I feel I'm not getting much light shed. No amount of adding `(~)` in GHC nor `TypeCast`+`typeCast` method in Hugs will get #9670 function `f` to compile. So my 'specific example' earlier in this thread shows `(~)` is moderately eager/more eager than FunDeps alone, but not eager enough for #9670.</div><div dir="auto"><br></div><div dir="auto">IOW from Adam's comment about "inferring where `typeCast` needs to be placed", it seems there's no such place. Perhaps because class `C` has no methods(?)</div><div dir="auto"><br></div><div dir="auto">Yes, as per your+Georgios' paper, replacing the FunDep with an Assoc Type and superclass `(~)` constraint is eager enough. That's not telling me why the FunDep+`(~)` constraint on the instances or function signatures isn't so eager.</div><div dir="auto"><br></div><div dir="auto">From the #9670 comment by spj: it's historically to do with an inability to represent evidence under System FC. It seems GHC is taking absence of evidence as evidence of absence, even though it's able to infer the 'right' type. </div><div dir="auto"><br></div><div dir="auto">AntC</div><div dir="auto"><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div>On Fri, 7 Dec 2018 at 10:57 PM, Adam Gundry wrote:<br></div><div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">...</blockquote><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
This is rather like automatically inferring where `typeCast` needs to be<br>
placed (indeed, at the Core level there is a construct for casting by an<br>
equality proof, which plays much the same role).<br>
<br></blockquote></div></div></blockquote></div></blockquote></div></div></blockquote></div></div>