为什么 GHC 拒绝允许这种存在类型函数？

Question

我定义了一个通用的heterogenous，我称之为（我不知道这是否正确），输入：

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

然后我决定创建一个函数，允许您从多态值创建异型：

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

但是，GHC 抱怨以下内容：

????????.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
   |          ^^^^^^^^^^^^

编辑：启用以下扩展：

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

Answer 1

从逻辑的角度来看，您的代码将对应于逻辑公式的证明，可以如下（粗略地）阅读：

• 让f是任何类型的属性；
• 假设，对于任何a满足 的类型f，我们都可以产生一个x类型的值a；
• 那么，存在一个类型a，满足f，并且有一个值x。

这在逻辑上是不合理的。事实上，f a无论是什么，都可能永远不会成立a。在这种情况下，上面的假设空洞地成立，因此它是正确的。然而，上述结论与f a总是错误的事实相矛盾。

因此，我们无法hset使用该类型定义您。

为了使论证合理，我们必须添加一个额外的假设，即存在某种类型b使该属性为f真。如果我们加上这个假设，我们可以证明这个陈述：

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