equality relations: user-facing pretty-printing question

[David Kraeutmann]

If ~# is hidden from the user, I think it's reasonable to hide it as an implementation detail.
The idea Iavor had sounds good, but we can get (potentially) confusing error messages when writing `Int ~~ Char => ...` -- the smart pretty printer would print `Int ~ Char`. Might get a bit messy.
On 1/18/2016 6:55 PM, Richard Eisenberg 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 --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4291 bytes
Desc: S/MIME Cryptographic Signature
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160118/8ba91451/attachment.bin>