equality relations: user-facing pretty-printing question

[Richard Eisenberg]

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160118/c55a6bd1/attachment.html>