Heterogeneous type equality not really heterogeneous

Summary

While answering a question on discourse, I ran into an unexpected situation.

I was thinking of examples where ~~ and ~ are different. I came up with the type: forall (a :: *). a ~~ Eq => a. I feel like that should be a valid type that is only inhabited by undefined. GHCi gives me the kind without errors:

> :set -XTypeOperators
> :set -XTypeFamilies
> :set -XKindSignatures
> :set -XExplicitForAll
> import GHC.Types
> :k forall (a :: *). a ~ Eq => a
forall (a :: *). a ~~ Eq => a :: *

But putting it in a file:

{-# LANGUAGE TypeOperators, TypeFamilies, ExplicitForAll, KindSignatures #-}

import GHC.Types

x :: forall (a :: *). a ~~ Eq => a
x = undefined

Gives errors:

[1 of 1] Compiling Main             ( Test.hs, interpreted )

Test.hs:5:6: error:
    • Couldn't match kind ‘* -> Constraint’ with ‘*’
      When matching types
        a :: *
        Eq :: * -> Constraint
    • In the ambiguity check for ‘x’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature: x :: forall (a :: *). a ~~ Eq => a
  |
5 | x :: forall (a :: *). a ~~ Eq => a
  |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

I feel like that error should not occur. I have already tried enabeling AllowAmbiguousTypes; it doesn't help.

Environment

• GHC version used: 8.10.4

Optional:

• Operating System: Debian buster
• System Architecture: x86_64