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

[Richard Eisenberg]

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 <eric at seidel.io> 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 <iavor.diatchki at gmail.com>
>> 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 <ryan.gl.scott at 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 at haskell.org
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>> 
>>> _______________________________________________
>>> ghc-devs mailing list
>>> ghc-devs at haskell.org
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>> 
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs