<div><br></div><div><br><div class="gmail_quote"><div dir="ltr">On Sat, 22 Dec 2018 at 7:08 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><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" target="_blank">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></div></blockquote><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 #9627 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 #9627.</div></div></div></blockquote><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="gmail_quote"><div dir="auto"></div></div></div></blockquote><div dir="auto"><br></div><div dir="auto"><br></div><div dir="auto">Can anybody explain @yav's comment here <div><a href="https://github.com/ghc-proposals/ghc-proposals/pull/158#issuecomment-449590613">https://github.com/ghc-proposals/ghc-proposals/pull/158#issuecomment-449590613</a> "currently equality constraints have no run-time evidence associated with them".</div><div dir="auto"><br></div><div dir="auto">Haskell has type-erasure semantics. Why would I need any _run-time_ evidence for anything to do with type improvement? What impact would the lack of evidence have at run-time?</div><div dir="auto"><br></div><div dir="auto">Does this mean `(~)` constraints don't produce evidence at compile time? Which is also the difficulty for type improvement under FunDeps.</div><div dir="auto"><br></div><div dir="auto">(I tried a type family to achieve the same effect as `(~)` with an injective TF. No improvement in improvement.)</div></div><div dir="auto"><br></div><div dir="auto"><br></div><div dir="auto">AntC</div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="gmail_quote"><div dir="auto"></div></div></div></blockquote><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"><div dir="auto"><br></div></div></div></blockquote></div></div>