GADT + Newtype deriving = Erroneous errors

Chris Kuklewicz haskell at list.mightyreason.com
Tue Mar 27 06:32:29 EDT 2007


Stefan O'Rear wrote:
> This code causes GHC to incorrectly fail - the case *is* reachable.
> (I invented this technique in an attempt to directly access the
> internal System FC newtype coercion; it promised until a few minutes
> ago to solve all the EnumMap performance concerns.)
> 
> stefan at stefans:/tmp$ cat A.lhs
>> {-# OPTIONS_GHC -fglasgow-exts #-}
>>
>> data IsIntT x where IsIntT :: IsIntT Int
>>
>> class IsIntC a where isInt :: IsIntT a
>> instance IsIntC Int where isInt = IsIntT
>>
>> newtype Foo = Foo Int deriving(IsIntC)
>>
>> x :: IsIntT Foo -> Int
>> x IsIntT = (Foo 2) + 2

IsIntT Foo is a concrete type.
IsIntT has concrete type IsInt Int.
These types cannot possibly match.

This may be what you want:

> {-# OPTIONS_GHC -fglasgow-exts #-}
> data IsIntT :: * -> * where IsIntT :: IsIntT Int
> 
> class IsIntC a where isInt :: IsIntT a
> instance IsIntC Int where isInt = IsIntT
> 
> newtype Foo = Foo Int deriving(IsIntC)
> 
> x :: IsIntT free -> Int
> x IsIntT = 2
> 
> y = x (isInt :: IsIntT Foo)

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.


More information about the Glasgow-haskell-users mailing list