[Haskell-cafe] Type system trickery

[Andrew Coppin]

Ross Mellgren wrote:
> 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?

Thinking about this more carefully, I started out with

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

which is no good, because Zoo can be nested arbitrarily deep. So I tried 
to change it to

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

But *actually*, changing the second type signature only is sufficient. 
Indeed, it turns out I don't *want* to change the first one. I want to 
use the type system to track whether Zoo "may" or "may not" be present, 
not whether it "is" or "is not" present. In other words, I want Foobar 
Zoo to mean that there *might* be a Zoo in there, but there isn't 
guaranteed to be one. But I want Foobar NoZoo to be guaranteed not to 
contain Zoo.

So anyway... my program now uses GADTs, I've spent ages chasing down all 
the typechecker errors (and, inevitably, in some places clarifying what 
the code is actually supposed to do), and my program now typechecks and 
does what it did before, except with slightly more type safety. (In 
particular, I've deleted several calls to "error" now, because those 
case alternatives can never occur).

Thanks to all the people for your help! :-D