"Scott J." wrote:

Well I don't feel alone anymore.

Here follows how I think runST :: (forall s. ST s a) -> a works:

if a is represented by e.g. MutVar s a . Then the compiler complains because it did find an s in the "data" represented by a. This s must first be eliminated by some other combinators(?).

Right. The `s' is appearing outside the area it is defined in.

I agree that something must be written for the argument of runST to warn programmers about the possible "representations" of a. But I still have problems that one has chosen forall.

`forall' and `Pi' are the basic names for this sort of thing in type theory. See the discussion of the Howard-Curry isomorphism for `forall'. You probably don't want to know about `Pi'.

Scott

Jon Cast