GADT + Newtype deriving = Erroneous errors

[Chris Kuklewicz]

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.

This (+) is allowed, since "type" is just shorthand:

> type Bar = Int
> 
> x :: Bar
> x = 2
> y :: Int
> y = 3
> z = x+y

This (+) is not allowed, since "data" declares a new type:

> data Bar = Bar Int deriving (Num)
>
> x :: Bar
> x = Bar 2
> y :: Int
> y = 3
> z = x+y

This (+) is not allowed, since "newtype" declares a new type:

> newtype Bar = Bar Int deriving (Num)
>
> x :: Bar
> x = Bar 2
> y :: Int
> y = 3
> z = x+y