Re: kind of type equalities (was: equality relations: user-facing pretty-printing question)

And lifted ones can exist at runtime, via deferred type errors. With deferred type errors, a lifted equality might be a thunk that evaluates to a type error. I also think that "because Core needs it" is a satisfying answer. That's why we have coercions. If we didn't care about type-checking Core, we could just omit very large swathes of GHC. But then we'd have a non-working compiler. :) Richard On Jan 18, 2016, at 1:12 PM, Eric Seidel wrote:

This is a bit tangential, but I find it odd that we care about whether a type equality has kind Lifted or Unlifted.

As I understand, the Lifted/Unlifted distinction exists so that we know whether we have a thunk (and by extension a pointer of a constant size) or the thing itself (the size depends on the type). So Lifted/Unlifted is primarily important for code-gen and runtime purposes. Type equalities, on the other hand, shouldn't exist at runtime as the types are erased.

So why do we care whether a type equality is a thunk? My guess is that we only care because type equalities *do* exist in Core as proof terms, so they need to be well-kinded, but this isn't a very satisfying answer.

On Mon, Jan 18, 2016, at 09:55, Richard Eisenberg wrote:

...

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

_______________________________________________ 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