GADT + Newtype deriving = Erroneous errors

[Stefan O'Rear]

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