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.