How to define an existential type with a constraint

[Savelenko]

I am trying to define an existential type with a contract for the hidden type, using a type class. First attempt:

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 results in:

 No type class instance was found for

    AnyTest.C t0

  The instance head contains unknown type variables. Consider adding a type annotation.

while applying a function f
  of type C t0 => t0 -> Unit
  to argument a
while checking that expression f a
  has type Unit
in value declaration anyC

where t0 is an unknown type

I can't even create a value like u = Any 3, assuming there is an instance of C for Int. Am I doing something wrong?

However, things get more suspicious when I provide a type annotation at (1):

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

giving the following, at the very least confusing, error:

  Could not match constrained type

    C a0 => a0

  with type

    C a0 => a0


while trying to match type C a0 => a0
  with type C a0 => a0
while checking that expression case $1 of
                                 (Any a) -> f a
  has type Unit
in value declaration anyC

where a0 is a rigid type variable

[garyb]

You need to use Church encode it instead:

class C a where
  f :: a -> Unit

data Any = Any (forall r. (forall a. C a => a -> r) -> r)

instance anyC :: C Any where
  f (Any k) = k f

[Savelenko]

Thanks for the swift reply. This works, but I would very like to understand what's going on. Does this have to do with dictionary passing in the generated code (or rather, not having to store the dictionary in Any) or something else?

Still, the second compiler error above is unfortunate, as it seemingly states that types a and a cannot be unified, but they trivially can be.

[LiamGoodacre]

@Savelenko Your original type doesn't encode an existential; rather, a universal. I.e the difference between "forall x" and "exists x".

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.

With the existential, it's the other way around. You "the implementer" get to pick an a, but the caller must work "for all" possible choices of a. So the type: forall r . (forall b . C b => b -> r) -> r says that if the caller gives it a function that works for all choices of b, then it will be called with a specific b that has an instance of C.

With your:

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

I wouldn't expect this to work, because you aren't picking a type for the term a to be specialized to. I haven't checked, but if you did something like f (a :: Int) it may have worked.

[LiamGoodacre]

Closing as there's no issue here.
There's also a couple PureScript channels on the functionalprogramming slack and a discourse site if you have further questions.