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

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