[Haskell-cafe] Type system trickery

Andrew Coppin andrewcoppin at btinternet.com
Mon Jun 22 15:34:35 EDT 2009

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...

More information about the Haskell-Cafe mailing list