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 <[email protected]> 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 <[email protected]> >> 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 <[email protected]> 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 >>> [email protected] >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >>> >>> _______________________________________________ >>> ghc-devs mailing list >>> [email protected] >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >> >> _______________________________________________ >> ghc-devs mailing list >> [email protected] >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > _______________________________________________ > ghc-devs mailing list > [email protected] > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs _______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
