Newtype wrappers

Gábor Lehel illissius at
Tue Jan 15 09:48:54 CET 2013

On Tue, Jan 15, 2013 at 3:15 AM, Iavor Diatchki
<iavor.diatchki at> wrote:
> 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

"Generative Type Abstraction and Type-level Computation"

Your ship was destroyed in a monadic eruption.

More information about the Glasgow-haskell-users mailing list