equality relations: user-facing pretty-printing question

[David Fox]

It is better, but you still might write ~~ and see an error message with ~,
right?

On Mon, Jan 18, 2016 at 9:55 AM, Richard Eisenberg <eir at cis.upenn.edu>
wrote:

> I like that idea. Do others?
>
> Yes, agreed about the difference between ~ and ~~.
>
> ~# is unlifted, and is now the type that the solver works on. ~~ is
> lifted. That's the only difference. But the fact that ~~ is lifted is what
> allows you to put it in a constraint, because all constraints are lifted.
> Users should never bother with ~#, but they might with ~~.
>
> Richard
>
> On Jan 18, 2016, at 12:52 PM, Iavor Diatchki <iavor.diatchki at gmail.com>
> wrote:
>
> Hello,
>
> What's the difference between `~~` and `~#` (I assume `~#` is
> heterogeneous)?
>
> As for the rest, as far as I understand, `~` is a strict subset of `~~` in
> the sense that:
>   1. if `a ~ b`, then `a ~~ b`
>   2. if `not (a ~ b)`, then `not (a ~~ b)`
>   3. if `a ~ b` is a kind error (i.e., the kind of `a` is known to be
> different from the kind of `b`), then `not (a ~~ b)`
>
> So, perhaps it makes sense to have a "smart" pretty printer for `a ~ b`:
>
>   if kindOf a == kindOf b then `a ~ b` else `a ~~ b`
>
> -Iavor
>
>
>
>
>
>
>
> On Mon, Jan 18, 2016 at 9:24 AM, Ryan Scott <ryan.gl.scott at gmail.com>
> wrote:
>
>> In my ideal world, GHC would remember as much as what the user wrote
>> as possible in printing error messages. So if the user writes:
>>
>>     f :: Int ~ Char => ...
>>
>> Then GHC would remember that the context was written with a single
>> tilde, and print out Int ~ Char in the error message explicitly
>> wherever the full type signature of f is printed.
>>
>> What it sounds like, though, is that deep in the guts of the type
>> inferencer, there's a chance that single-tilde equality might turn
>> into double-tilde or tilde-hash equality at some point. In those
>> cases, printing out the particular brand of tilde might get confusing.
>> In such cases, we might compromise and print out something neutral
>> like "is equal to". I suppose this would always be the case if you
>> didn't explicitly write a ~ b and had to infer it.
>>
>> I'm not sure about the technical details of this though, i.e., if GHC
>> actually remembers a ~ b all the way through the
>> typechecking/inferencing pipeline.
>>
>> Ryan S.
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
>
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160118/c0f5f247/attachment.html>