kind of type equalities (was: equality relations: user-facing pretty-printing question)
eric at seidel.io
Mon Jan 18 18:45:35 UTC 2016
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.
More information about the ghc-devs