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