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:
forall a . C a => ameans that a user of a term of this type gets to pick which
athey want. Which is why
Any 3doesn’t make any sense: you “the implementer” can’t pick the
Intif 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?