On Tue, Jan 15, 2013 at 3:15 AM, Iavor Diatchki
In general, I was never comfortable with GHC's choice to add an axiom equating a newtype and its representation type, because it looks unsound to me (without any type-functions or newtype deriving). For example, consider:
newtype T a = MkT Int
Now, if this generates an axiom asserting that `froall a. T a ~ Int`, then we can derive a contradiction:
T Int ~ Int ~ T Char, and hence `Int ~ Char`.
It looks like what we need is a different concept: one that talks about the equality of the representations of types, rather then equality of the types themselves.
-Iavor
This is what Simon's paper[1] referenced from the wiki is about, except he uses the terminology "the representations of types" -> "types", "the types themselves" -> "codes". (IMHO talking about "representations" and "types", respectively, would be more accessible.) [1] http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/ "Generative Type Abstraction and Type-level Computation" -- Your ship was destroyed in a monadic eruption.