<html><head><meta http-equiv="Content-Type" content="text/html charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div>I like that idea. Do others?</div><div><br></div><div>Yes, agreed about the difference between ~ and ~~.</div><div><br></div><div>~# 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 ~~.</div><div><br></div><div>Richard</div><br><div><div>On Jan 18, 2016, at 12:52 PM, Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com">iavor.diatchki@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div dir="ltr">Hello,<div><br></div><div>What's the difference between `~~` and `~#` (I assume `~#` is heterogeneous)? <br></div><div><br></div><div>As for the rest, as far as I understand, `~` is a strict subset of `~~` in the sense that:</div><div> 1. if `a ~ b`, then `a ~~ b`</div><div> 2. if `not (a ~ b)`, then `not (a ~~ b)`</div><div> 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)`</div><div><br></div><div>So, perhaps it makes sense to have a "smart" pretty printer for `a ~ b`:</div><div><br></div><div> if kindOf a == kindOf b then `a ~ b` else `a ~~ b`</div><div><br></div><div>-Iavor</div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Jan 18, 2016 at 9:24 AM, Ryan Scott <span dir="ltr"><<a href="mailto:ryan.gl.scott@gmail.com" target="_blank">ryan.gl.scott@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">In my ideal world, GHC would remember as much as what the user wrote<br>
as possible in printing error messages. So if the user writes:<br>
<br>
f :: Int ~ Char => ...<br>
<br>
Then GHC would remember that the context was written with a single<br>
tilde, and print out Int ~ Char in the error message explicitly<br>
wherever the full type signature of f is printed.<br>
<br>
What it sounds like, though, is that deep in the guts of the type<br>
inferencer, there's a chance that single-tilde equality might turn<br>
into double-tilde or tilde-hash equality at some point. In those<br>
cases, printing out the particular brand of tilde might get confusing.<br>
In such cases, we might compromise and print out something neutral<br>
like "is equal to". I suppose this would always be the case if you<br>
didn't explicitly write a ~ b and had to infer it.<br>
<br>
I'm not sure about the technical details of this though, i.e., if GHC<br>
actually remembers a ~ b all the way through the<br>
typechecking/inferencing pipeline.<br>
<br>
Ryan S.<br>
<div class="HOEnZb"><div class="h5">_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</div></div></blockquote></div><br></div>
_______________________________________________<br>ghc-devs mailing list<br><a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs<br></blockquote></div><br></body></html>