Contexts in datatypes

[Koen Claessen <koen@cs.chalmers.se>]

Hello,

Consider the following datatype declaration:

  data Eq a => Foo a = Foo a

It introduces a new constructor function with the type:

  Foo :: Eq a => a -> Foo a

So far so good. This is what we expect.

It also introduces a new pattern, which will result in the following
typing:

  unFoo :: Eq a => Foo a -> a
  unFoo (Foo a) = a

Why?? I require the context at _construction_ time, not at _destruction_
time! Actually, when I unpack (Foo a), I _know_ there must be a dictionary
(Eq a) somewhere! Because I required that at construction time!

Consider the following function:

  eqFoo :: Eq a => Foo a -> Bool
  eqFoo (Foo a) = a == a

I think the typing of this function should be:

  eqFoo :: Foo a -> Bool
  eqFoo (Foo a) = a == a

Because at the moment we unpack (Foo a), we also get a dictionary (Eq a),
which was there at construction time!

Why doesn't it work like this in Haskell? Do contexts in datatypes make
sense if it doesn't work like this? I couldn't find a description of how
patterns of datatypes with contexts work in the Haskell report.

Regards,
Koen.

--
Koen Claessen,
koen@cs.chalmers.se,
http://www.cs.chalmers.se/~koen,
Chalmers University of Technology.