Fundeps and quantified constructors

[Tom Pledger]

nubie nubie writes:
 | So I want to have a polymorphic Collection type, just because.
 | 
 | > class Collection c e | c -> e where
 | >   empty :: c
 | >   put   :: c -> e -> c
 | 
 | > data SomeCollection e = forall c . Collection c e => MakeSomeCollection c
 | 
 | Hugs (February 2000) doesn't like it. It says
 |   Variable "e" in constraint is not locally bound
 | 
 | I feel that e *is* bound, sort of, because c is bound and there's a
 | fundep c->e.

That line of reasoning establishes that e is constrained on the right
hand side of the "=".  However, it's still bound (by an implicit
"forall e") on the left hand side of the "=".  The problem is that e
can leak details about c to parts of the program outside the "forall
c".  It's still a problem if you remove the "| c -> e" fundep.

A more common use of a "Collection c e | c -> e" class is:

    data SomeCollection e = --some data structure involving e

    instance SomeContext e => Collection (SomeCollection e) e where
        --implementations of empty and put, for the aforementioned
        --data structure, and entitled to assume SomeContext

Is that collection type polymorphic enough for your purposes?

 :
 | The following things work as expected:
 | 
 | > data IntCollection = forall c . Collection c Int => MakeIntCollection c
 | > data AnyCollection = forall c e . Collection c e => MakeAnyCollection c

Neither of them has a type variable tunnelling through the local
quantifier.

HTH.
Tom