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