[Haskell-cafe] Type system trickery

[Thomas DuBuisson]

Andrew Coppin said:
>  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*

That code snippet works for me, so I think you're doing something else
wrong or I transcribed wrong

My code in full:
-------------------------
{-# LANGUAGE GADTs, EmptyDataDecls #-}

data NoZoo
data Zoo

data Place a where
        Office :: String -> Int -> Place NoZoo
        Home   :: String -> Int -> Place NoZoo
        Zoo    :: Place NoZoo -> Place Zoo
---------------------------------

It works fine (but I absolutely agree the lack of deriving is frustrating):
---------------------
*Main> let x = Zoo (Office "9th street" 3342)
*Main> let y = Home "Friends House" 4422
*Main> :t x
x :: Place Zoo
*Main> :t y
y :: Place NoZoo
*Main>
------------


And if you want to change it wrt Niklas's comments:
-------------------
{-# LANGUAGE GADTs, EmptyDataDecls #-}

data NoZoo
data Zoo

data Place a where
        Office :: String -> Int -> Place NoZoo
        Home   :: String -> Int -> Place NoZoo
        Zoo    :: Place a -> Place Zoo
-------------------

Which works:
---------------
*Main> let x = Zoo (Zoo (Office "9th street" 3342))
*Main> let y = Home "Friends House" 4422
*Main> :t x
x :: Place Zoo
*Main> :t y
y :: Place NoZoo
-----------------