Equality constraints (~): type-theory behind them

[Anthony Clayden]

On Mon, 10 Dec 2018 at 6:12 PM, Anthony Clayden <
anthony_clayden at clear.net.nz> wrote:

> 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:
>>
>> https://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/haskell2017a.pdf
>>
>>
> 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).
>>>>
>>>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20181222/0ad240d7/attachment.html>