Equality constraints (~): type-theory behind them

[Anthony Clayden]

On Sat, 22 Dec 2018 at 7:08 PM, Anthony Clayden <
anthony_clayden at clear.net.nz> wrote:

>
> 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
>>>
>>>
>>
> 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.
>


Can anybody explain @yav's comment here
https://github.com/ghc-proposals/ghc-proposals/pull/158#issuecomment-449590613
"currently equality constraints have no run-time evidence associated with
them".

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?

Does this mean `(~)` constraints don't produce evidence at compile time?
Which is also the difficulty for type improvement under FunDeps.

(I tried a type family to achieve the same effect as `(~)` with an
injective TF. No improvement in improvement.)


AntC

>

>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20181223/8a12353b/attachment.html>