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

[Eric Seidel]

On Mon, Jan 18, 2016, at 10:26, Richard Eisenberg wrote:
> 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.

Ah, fair point. 

> 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. :)

I should have elaborated on why I find it unsatisfying :) 

My point was not that type-checking Core is not desirable enough to
warrant tracking the kind of a type equality, rather that perhaps
there's a simpler way that doesn't include runtime concerns. For
example, perhaps type equalities could have their own kind. But it
sounds like we can't actually separate equalities from code-gen/runtime.