GADT + Newtype deriving = Erroneous errors

[Simon Peyton-Jones]

Right.  There are two things going on in this thread.  First, when you say
        newtype T = MkT Int
then T and Int are distinct types.  Adding a deriving( whatever ) doesn't change that fact.  Earlier messages make this point.

The second is that GHC's current "newtype deriving" mechanism is plain wrong.  It's one of those feature-interaction things.  Something that used to work fine (newtype deriving) breaks when you elaborate an apparently unrelated feature (GADTs).

Stefan has helpfully boiled out a bug report http://hackage.haskell.org/trac/ghc/ticket/1251.  Thank you Stefan.  I'm nose-down in ICFP mode at the moment, but I'll look at it after that deadline.

Meanwhile, it's clear that the rules for "newtype deriving" need to be refined.  Would anyone like to have a go at refining them?
http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#newtype-deriving

Simon

| -----Original Message-----
| From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-users-bounces at haskell.org] On
| Behalf Of Lennart Augustsson
| Sent: 29 March 2007 00:29
| To: Stefan O'Rear
| Cc: glasgow-haskell-users at haskell.org
| Subject: Re: GADT + Newtype deriving = Erroneous errors
|
| We don't have to wait for the type checkers to rule.  The semantics
| of GADTs is pretty clear (if it's implemented correctly is another
| matter).  If you write
|     data IsIntT x where
|       IsIntT :: IsIntT Int
| then there is only one (non-bottom) value in the IsIntT families of
| types and that is IsIntT::IsInt Int
|
| And since Haskell uses nominal type equality there is no type equal
| to Int that is not Int.
|
| The fact that you can derive IsIntC looks like a good ole' bug to me.
|
|         -- Lennart
|
|
| On Mar 28, 2007, at 23:22 , Stefan O'Rear wrote:
|
| > On Wed, Mar 28, 2007 at 12:03:41PM +0100, Chris Kuklewicz wrote:
| >> Stefan O'Rear wrote:
| >>> On Tue, Mar 27, 2007 at 11:32:29AM +0100, Chris Kuklewicz wrote:
| >>>> Stefan O'Rear wrote:
| >>
| >>>>>> newtype Foo = Foo Int deriving(IsIntC)
| >>>>>>
| >>
| >>>
| >>>> Note that (Foo 2) + 2 is an attempt to add a Foo and an Int,
| >>>> which cannot
| >>>> possibly compile.  So I replaced it with just a 2.
| >>>
| >>> Why not?  They are the same type, and I have Curry-Howard proof
| >>> of this fact.
| >>>
| >>> Stefan
| >>
| >> Foo is isomorphic to Int in structure.  But it is not the same
| >> type.  Foo is a
| >> new type that is distinct from Int.  That means I get type safety
| >> -- you cannot
| >> pass an Int to a function that expects a Foo and vice versa.
| >> Since (+) is
| >> defined as (Num a => a->a->a) it cannot add type different types
| >> and thus you
| >> *cannot* add a Foo and an Int.
| >
| > Well, I thought I had a non-bottom value of type IsIntT Foo, but when
| > I tried to seq it ghc crashed: http://hackage.haskell.org/trac/ghc/
| > ticket/1251
| >
| > Let's postpone this discussion until the people who maintain the
| > typechecker have a chance to rule :)
| >
| > Stefan
| > _______________________________________________
| > Glasgow-haskell-users mailing list
| > Glasgow-haskell-users at haskell.org
| > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
|
| _______________________________________________
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users at haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users