我可以静态拒绝存在类型的不同实例吗？

Question

第一次尝试

这个问题很难简洁，但提供一个最小的例子，假设我有这种类型：

{-# LANGUAGE GADTs #-}
data Val where
  Val :: Eq a => a -> Val

这种类型让我很高兴地构建了以下异类列表：

l = [Val 5, Val True, Val "Hello!"]

但是，唉，当我写下 Eq 实例时，事情就出错了：

instance Eq Val where
  (Val x) == (Val y) = x == y -- type error

啊，所以我们Could not deduce (a1 ~ a)。完全正确;定义中没有说x 和y 必须是同一类型。事实上，重点是允许它们不同的可能性。

第二次尝试

让我们将Data.Typeable 加入其中，仅在它们恰好是同一类型时尝试比较两者：

data Val2 where
  Val2 :: (Eq a, Typeable a) => a -> Val2

instance Eq Val2 where
  (Val2 x) == (Val2 y) = fromMaybe False $ (==) x <$> cast y

这很不错。如果x 和y 是同一类型，则它使用底层Eq 实例。如果它们不同，它只返回False。然而，这个检查会延迟到运行时，让nonsense = Val2 True == Val2 "Hello" 可以毫无怨言地进行类型检查。

问题

我意识到我在这里与依赖类型调情，但是 Haskell 类型系统是否有可能静态拒绝类似上述 nonsense 的内容，同时允许类似 sensible = Val2 True == Val2 False 的内容在运行时交回 False？

我处理这个问题的次数越多，我似乎就越需要采用HList 的一些技术来实现我需要作为类型级函数的操作。但是，我对使用存在主义和 GADT 比较陌生，我很想知道是否可以找到解决方案。所以，如果答案是否定的，我非常感谢讨论这个问题究竟在哪里达到了这些功能的极限，以及推动适当的技术、HList 或其他方式。

Answer 1

为了根据包含的类型做出类型检查决定，我们需要通过将包含的类型公开为类型参数来“记住”它。

data Val a where
  Val :: Eq a => a -> Val a

现在Val Int 和Val Bool 是不同的类型，因此我们可以轻松强制只允许进行相同类型的比较。

instance Eq (Val a) where
  (Val x) == (Val y) = x == y

但是，由于 Val Int 和 Val Bool 是不同的类型，如果没有一个额外的层再次“忘记”包含的类型，我们不能将它们混合在一个列表中。

data AnyVal where
  AnyVal :: Val a -> AnyVal

-- For convenience
val :: Eq a => a -> AnyVal
val = AnyVal . Val

现在，我们可以写了

[val 5, val True, val "Hello!"] :: [AnyVal]

现在应该很清楚了，你不能用一种数据类型同时满足这两个要求，因为这样做需要同时“忘记”和“记住”包含的类型。

Answer 2

因此，您需要一个允许您使用异构类型的构造函数，但您希望拒绝在编译时可知的异构类型之间的比较。如：

Val True == Val "bar"  --> type error

allSame [] = True
allSame (x:xs) = all (== x) xs

allSame [Val True, Val "bar"]  --> False

当然：

(x == y) = allSame [x,y]

所以我很确定满足这些约束的函数会违反类型系统的某些理想属性。在你看来不是这样吗？我强烈猜测“不，你不能那样做”。