How to define an existential type with a constraint

[borar]

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?

[borar]

Furthermore, providing a type annotation at (1) like this

instance anyC :: C Any where
  f (Any (a :: forall a. C a => a)) = f a

results in a compiler error which makes me wonder whether there is a bug somewhere:

Could not match constrained type

C a0 => a0

with type

C a0 => a0
…

Is this error OK?

[monoidmusician]

Two quick comments:

• Does the Haskell code you’re referring to look like data Any = forall a. C a => Any a? (with the forall before the type constructor?) If so, that’s something different – it really is an existential type, but it’s special syntax for that. PS doesn’t support that syntax … Would you agree that forall a. C a => a is an universal type by itself? Then it will operate the same inside a datatype.
• The “could not match constrained type with constrainted type” issue is well known. Basically, the compiler can’t decide higher-order polymorphism (aka nested foralls), so it doesn’t even try, which is unfortunate, as even a few simple cases (like this) would be helpful. Most of the time it can be worked around via eta-expansion: (\a -> f a) :: forall a. C a => a (because then the compiler introduces the a variable as a skolem, and then it can choose the inner one to unify with that “chosen” a).

[borar]

Yes, I am indeed referring to ExistentialQuantification. Thanks for confirming my suspicion that that extension is a bit different than this case. Also, thanks for the explanation about type checking. The error message remains unfortunate though, because “symbolically” it shows a trivial situation…