Why does GHC refuse to allow this existential type function?

Question

I have defined a general heterogenous, as I call it (I don't know if that's correct), type:

data Heterotype f = forall a. f a => Heterotype a

I then decided to make a function that allows you to create heterotypes from polymorphic values:

hset :: (forall a. f a => a) -> Heterotype f
hset x = Heterotype x

However, GHC complains with the following:

████████.hs:15:10: error:
    * Could not deduce: f a0 arising from a use of `Heterotype'
    * In the expression: Heterotype x
      In an equation for `hset': hset x = Heterotype x
    * Relevant bindings include
        x :: forall a. f a => a
          (bound at ████████.hs:15:6)
        hset :: (forall a. f a => a) -> Heterotype f
          (bound at ████████.hs:15:1)
   |
15 | hset x = Heterotype x
   |          ^^^^^^^^^^^^

EDIT: The following extensions are enabled:

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GADTs, ScopedTypeVariables #-}
{-# LANGUAGE NoStarIsType, ConstraintKinds #-}
{-# LANGUAGE AllowAmbiguousTypes, RankNTypes #-}
import Data.Kind

Answer 1

From a logical point of view, your code would correspond to a proof of a logical formula which can be read as follows (rouhgly):

• Let f be any property of types;
• Assume that, for any type a satisfying f, we can produce a value x of type a;
• Then, there exists a type a, satisfying f, and having a value x.

This is not logically sound. Indeed, it is possible that f a never holds, no matter what a is. In such case, the assumption above vacuously holds, hence it is true. Yet, the conclusion above contradicts the fact that f a is always false.

As a consequence of this, we can not define your hset with that type.

To make the argument sound, we must add, as an additional hypothesis, that there is some type b which makes the property f true. If we add that hypothesis, we can prove the statement:

-- (untested, but should work)
hset :: forall b . f b => (forall a. f a => a) -> Heterotype f
hset x = Heterotype (x :: b)

Answer 2

Your data definition hides a monotyped choice of a by packing up a value with the dictionary for f. It's important to recognize that the whole point of that is to throw away the information about the specific type while keeping the instance dictionary associated with that type.

This is incompatible with what you're trying to do in hset. There never is a concrete type to pack up the instance from. The pieces can't fit together that way, because they're both missing the same required thing. Heterotype f and (forall a. f a => a) both lack a concrete type to choose an instance for, but the Heterotype constructor needs a concrete instance to include. The information just doesn't exist. These pieces are incompatible.

Answer 3

You're over-specifying a bit :), the following works fine:

data Heterotype f = forall a. f a => Heterotype a

hset :: forall f a. f a => a -> Heterotype f
hset x = Heterotype x

The difference being that you've quantified your argument: (forall a. f a => a) which says that this function accepts an expression which must be ANY possible type all at once (the caller can't choose a specific 'a'), which doesn't really make sense. The new version (which consequently is identical to just using the Heterotype constructor on its own) says that the caller is allowed to pick the type of a, which can be anything, but must be exactly ONE type (per call).

It can take a bit of practice to get used to existentials; best way is trial and error :)