为什么ghc无法在此类别产品上匹配这些类型？

admin

我对一个类别有一个非常典型的定义：

class Category (cat :: k -> k -> Type) where
  id :: cat a a
  (.) :: cat a b -> cat c a -> cat c b

现在我想做Product Category，所以我做了这个

data ProductCategory
  (cat1 :: a -> a -> Type)
  (cat2 :: b -> b -> Type)
  (x :: (a, b))
  (y :: (a, b))
  where
MorphismProduct :: cat1 x x -> cat2 y y -> ProductCategory cat1 cat2 '(x, y) '(x, y)

现在这段代码编译得很好，当我试图使它成为Category的一个实例时，我的问题就来了。这里的数学真的很简单，似乎这应该是一个简单的例子。所以这就是我的想法：

instance
  ( Category cat1
  , Category cat2
  )
    => Category (ProductCategory cat1 cat2)
  where
    id = MorphismProduct id id
    (MorphismProduct f1 f2) . (MorphismProduct g1 g2) = MorphismProduct (f1 . g1) (f2 . g2)

但这会带来一个错误：

    ? Couldn't match type ‘a2’ with ‘'(x0, y0)’
      ‘a2’ is a rigid type variable bound by
        the type signature for:
          id :: forall (a2 :: (a1, b1)). ProductCategory cat1 cat2 a2 a2
        at src/Galaxy/Brain/Prelude.hs:175:5-6
      Expected type: ProductCategory cat1 cat2 a2 a2
        Actual type: ProductCategory cat1 cat2 '(x0, y0) '(x0, y0)
    ? In the expression: MorphismProduct id id
      In an equation for ‘id’: id = MorphismProduct id id
      In the instance declaration for
        ‘Category (ProductCategory cat1 cat2)’
    ? Relevant bindings include
        id :: ProductCategory cat1 cat2 a2 a2
          (bound at src/Galaxy/Brain/Prelude.hs:175:5)
    |
175 |     id = MorphismProduct id id
    |          ^^^^^^^^^^^^^^^^^^^^^

我在这个错误上花了很长时间，我只是不知道它试图向我传达什么。它声称它不能将a与'(x0, y0)匹配，但我不知道为什么，似乎它真的应该能够匹配。

这里遇到的问题是什么？如何解决它将是很好的，但我真的想知道如何阅读这条消息。

转载请注明出处:http://www.tstxxqczl.com/article/20230526/2087236.html