I'm no expert, but it seems like those constructors should return Foobar NoZoo, unless you're nesting so there could be a Zoo, in which case the type variable a should transit, for example: data Foobar a where Foo :: X -> Y -> Foobar NoZoo Bar :: X -> Y -> Foobar NoZoo Baz :: Foobar a -> Foobar a Zoo :: Foobar NoZoo -> Foobar Zoo value = Zoo $ Foo (X 1) (Y 'a') value2 = Zoo $ Baz $ Foo (X 1) (Y 'a') -- value3 = Zoo $ Baz $ Zoo $ Foo (X 1) (Y 'a') -- Couldn't match expected type `NoZoo' against inferred type `Zoo' -- Expected type: Foobar NoZoo -- Inferred type: Foobar Zoo -- In the second argument of `($)', namely -- `Baz $ Zoo $ Foo (X 1) (Y 'a')' -- In the expression: Zoo $ Baz $ Zoo $ Foo (X 1) (Y 'a') That is, if you construct a Baz with something else that doesn't have a Zoo (e.g. NoZoo) then the resultant type is also NoZoo. The converse is true. Why would you want it to generate a polymorphic Foobar when it definitely is NoZoo? -Ross (p.s. the example names in this thread are a bit ridiculous ;-) ) On Jun 23, 2009, at 4:01 PM, Andrew Coppin wrote:
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
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe