GADT + Newtype deriving = Erroneous errors

[Lennart Augustsson]

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