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