来自泛型-sop 的 All 的超类

Question

我正在尝试使用来自 generics-sop 的All来限制类型列表。使用简单的类（如 ）All Typeable xs，一切都按预期工作，但我希望能够执行以下操作：

class (Typeable a) => TestClass (a :: k)
instance (Typeable a) => TestClass a

foo :: (All Typeable xs) => NP f xs -> z
foo = undefined

bar :: (All TestClass xs) => NP f xs -> z
bar = foo 

这给出了错误

Could not deduce: Generics.SOP.Constraint.AllF Typeable xs
  arising from a use of ‘foo’
  from the context: All TestClass xs

generics-sop 文档指出

"所有 Eq '[ Int, Bool, Char ] 等价于约束 (Eq Int, Eq Bool, Eq Char)

但在这种情况下似乎并非如此，因为

foo2 :: (Typeable a, Typeable b) => NP f '[a,b] -> z
foo2 = undefined

bar2 :: (TestClass a, TestClass b) => NP f '[a,b] -> z
bar2 = foo2

编译正常。

我的问题

1）这是预期的行为吗？2）如果是这样，有什么解决方法吗？

我的使用情况。这就是我想通过周围的下一个类名（如由一群不同类别的约束类型类型级别列表class (Typeable a, Eq a, Show a) => MyClass a），而且还能够调用不太专业的功能，只有需要这些类的某个子集.

不考虑搜索答案出现超类，但我认为这不是这里的问题 - 我认为这与All约束在generics-sop. 就好像编译器只是简单地比较两个All约束，而不是扩展它们然后进行类型检查。

Answer 1

All f xs实际上相当于(AllF f xs, SListI xs). AllF是一个类型族：

type family AllF (c :: k -> Constraint) (xs :: [k]) :: Constraint where
  AllF _ '[] = ()
  AllF c (x:xs) = (c x, All c xs)

您会看到除非xs在 WHNF 中，否则它无法减少，因此它会卡在您的案例中。您可以使用mapAll：

import Generics.SOP.Dict

mapAll :: forall c d xs.
          (forall a. Dict c a -> Dict d a) ->
          Dict (All c) xs -> Dict (All d) xs
-- ::ish forall f g xs. (forall a. f a -> g a) -> All f xs -> All g xs

-- stores a constraint in a manipulatable way
data Dict (f :: k -> Constraint) (a :: k) where
     Dict :: f a => Dict f a

bar :: forall xs f z. (All TestClass xs) => NP f xs -> z
bar = case mapAll @TestClass @Typeable @xs (\Dict -> Dict) Dict of
           Dict -> foo

-- TestClass a -> Typeable a pretty trivially:
--   match Dict to reveal TestClass a
--   put the Typeable part of the TestClass instance into another Dict
-- We already know All TestClass xs; place that into a Dict
-- mapAll magic makes a Dict (All Typeable) xs
-- match on it to reveal
-- foo's constraint is satisfied