Hi everyone,

In 3474 I was having trouble defining an existential type as follows:

```
class C a where
f :: a -> Unit
data Any = Any (forall a. C a => a)
instance anyC :: C Any where
f (Any a) = f a -- (1)
```

This gives a compiler error. Then, Liam remarked the following:

The type

`forall a . C a => a`

means that a user of a term of this type gets to pick which`a`

they want. Which is why`Any 3`

doesn’t make any sense: you “the implementer” can’t pick the`a`

to be`Int`

if the caller must pick it.

However, I have doubts about this, because with existentials the notion of “user” is a bit more nuanced. Namely, I would expect that a concrete `a`

*can* be picked when introducing `Any`

and cannot when eliminating. That is, `Any 3`

should be OK (given an instance `C Int`

) and `f`

above should only know that there is an instance `C a`

and no more. The above program is perfectly fine in Haskell, modulo syntax, so I suspect that `forall`

inside constructors works differently in PureScript?