Re: equality relations: user-facing pretty-printing question

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 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 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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs