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