[Haskell-cafe] Type system trickery

[Ross Mellgren]

This works for me:

{-# LANGUAGE EmptyDataDecls, GADTs #-}
module Main where

data NoZoo
data Zoo

newtype X = X Int deriving (Show)
newtype Y = Y Char deriving (Show)

data Foobar a where
     Foo :: X -> Y -> Foobar NoZoo
     Bar :: X -> Y -> Foobar NoZoo
     Zoo :: Foobar NoZoo -> Foobar Zoo

foobar :: Foobar a -> X
foobar f = case f of
              Foo x _ -> x
              Zoo g   -> foobar g

main :: IO ()
main = putStrLn . show $ foobar (Zoo $ Foo (X 1) (Y 'a'))


Could you post a test case?


On Jun 22, 2009, at 3:34 PM, Andrew Coppin wrote:

> Niklas Broberg wrote:
>>> Not nearly as annoying as this:
>>>
>>> data Foobar a where
>>>  Foo :: X -> Y -> Foobar NoZoo
>>>  Bar :: X -> Y -> Foobar NoZoo
>>>  Zoo :: Foobar NoZoo -> Foobar Zoo
>>>
>>> For some reason, if I do this I get endless type check errors. I  
>>> have to
>>> change the top two back to Foobar a before it will work. *sigh*
>>>
>>
>> Well, that means something very different obviously. It means Zoo
>> constructors can never take Zoo arguments.
>
> ...which would be precisely what I want, yes. :-)
>
>> Why would that give you type check errors? If it
>> does, you're doing something else wrong.
>>
>
> I think (I'm not sure) it's because of stuff like this:
>
> foobar :: Foobar a -> X
> foobar f = case f of
>   Foo x y -> ...
>   Zoo g -> foobar g
>
> The first case implies that f :: Foobar NoZoo, while the second  
> implies that f :: Foobar Zoo. Apparently this seemingly reasonable  
> construct does not type-check...
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe