On Mon, 10 Dec 2018 at 9:36 PM, Tom Schrijvers wrote:
Maybe our Haskell'17 paper about Elaboration on Functional Dependencies sheds some more light on your problem:
Thank you Tom, looks interesting and very applicable. It'll be a few days before I can take a proper look.
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(?)
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.
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(?)
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.
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.
AntC
On Fri, 7 Dec 2018 at 10:57 PM, Adam Gundry wrote:
...
This is rather like automatically inferring where `typeCast` needs to be
placed (indeed, at the Core level there is a construct for casting by an
equality proof, which plays much the same role).