Haskell - 具有类约束的 GADT 模式匹配

Question

考虑以下示例

{-# LANGUAGE DataKinds, GADTs #-}
data Phantom = A | B
data Foo (a :: Phantom) where
  FooA :: Foo 'A
  FooB :: Foo 'B
class PhantomConstraint (a :: Phantom)
instance PhantomConstraint 'A -- Note: No instance for 'B
someFunc :: PhantomConstraint a => Foo a -> ()
someFunc FooA = ()

如果我做这样的事情，GHC 会提示 someFunc 的模式匹配是不详尽的，但是，如果我尝试包含 FooB 的情况(我不想为域做这件事)具体原因)它提示无法推断出 Foo 'B

的 PhantomConstraint 实例

是否有任何方法可以使 GADT 模式匹配了解类型类约束，从而消除模式匹配所需的部分？

编辑:有关我想做的事情的更多详细信息。我有一桶类型，它们都有些相关但具有不同的属性。在面向对象的世界中，这就是人们使用子类型和继承的目的。然而，在 FP 社区中，共识似乎是没有真正好的方法来进行子类型化，所以在这种情况下我需要绕过它。因此，我有一个统一所有类型的 GADT，但该类型具有不同的参数。然后，我继续在类型参数上编写不同的类型类和类型类实例(由数据类型启用，无术语表示)。我希望能够表达数据类型中的某些类型具有其他类型所没有的属性，但它们确实共享某些公共(public)属性，因此我真的不想分解该类型。我可以预见的唯一其他选择是在类型部分上创建分类法，但随后 DataKinds 类型会变得困惑。

Answer 1

我无法重现该问题。在 GHCi 8.4.3 中加载时不会出现警告或错误。

{-# LANGUAGE GADTs, DataKinds, KindSignatures #-}
{-# OPTIONS -Wall #-}
module GADTwarning2 where

data Phantom = A | B

data Foo (a :: Phantom) where
  FooA :: Foo 'A
  FooB :: Foo 'B

class PhantomConstraint (a :: Phantom)

instance PhantomConstraint 'A -- Note: No instance for 'B

someFunc :: PhantomConstraint a => Foo a -> ()
someFunc FooA = ()
someFunc FooB = ()

正如 luqui 在评论中解释的那样，我们无法避免 FooB 情况，因为类型类是开放的，并且稍后可以由另一个模块添加另一个实例，从而使模式匹配不详尽.

如果您绝对确定除了 A 之外不需要任何其他实例，您可以尝试使用

class a ~ 'A => PhantomConstraint (a :: Phantom)

或者，如果索引 a 可以是 'A 或 'B，但不能是第三个构造函数 'C，那么我们可以尝试具体化这个事实:

class PhantomConstraint (a :: Phantom) where
   aIsAOrB :: Either (a :~: 'A) (a :~: 'B)

然后稍后利用该成员。