GADT + Newtype deriving = Erroneous errors

Lennart Augustsson lennart at augustsson.net
Wed Mar 28 19:29:02 EDT 2007


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



More information about the Glasgow-haskell-users mailing list