我有以下类表示类别，其中对象类由一种表示，并且每个 hom 类由由上述种类的类型索引的类型表示。
{-# LANGUAGE GADTs, DataKinds, KindSignatures, PolyKinds #-}
type Hom o = o -> o -> *
class GCategory (p :: Hom o)
where
gid :: p a a
gcompose :: p b c -> p a b -> p a c
一个简单的实例示例是：
instance GCategory (->)
where
gid = id
gcompose = (.)
现在我想为产品类别建模。作为一个简单的起点，这里有一个类型，它对对应于->with 自身乘积的类别的态射进行建模：
data Bifunction ab cd
where
Bifunction :: (a -> c) -> (b -> d) -> Bifunction '(a, b) '(c, d)
下面是相应的操作：
bifunction_id :: Bifunction '(a, a') '(a, a')
bifunction_id = Bifunction id id
bifunction_compose :: Bifunction '(b, b') '(c, c') -> Bifunction '(a, a') '(b, b') -> Bifunction '(a, a') '(c, c')
bifunction_compose (Bifunction f1 g1) (Bifunction f2 g2) = Bifunction (f1 . f2) (g1 . g2)
但是当我尝试将操作粘贴到类的实例中时：
instance GCategory Bifunction
where
gid = bifunction_id
gcompose = bifunction_compose
我遇到以下问题：
• Couldn't match type ‘a’ with ‘'(a0, a'0)’
‘a’ is a rigid type variable bound by
the type signature for:
gid :: forall (a :: (*, *)). Bifunction a a
at /tmp/ghc-mod29677/Bifunction29676-49.hs:28:3-5
Expected type: Bifunction a a
Actual type: Bifunction '(a0, a'0) '(a0, a'0)
• In the expression: bifunction_id
In an equation for ‘gid’: gid = bifunction_id
In the instance declaration for ‘GCategory Bifunction’
• Relevant bindings include
gid :: Bifunction a a
(bound at /tmp/ghc-mod29677/Bifunction29676-49.hs:28:3)
我相信消息的重要部分如下：
Expected type: Bifunction a a
Actual type: Bifunction '(a0, a'0) '(a0, a'0)
特别是它不能将 typeforall x y. Bifunction '(x, y) '(x, y)与 type统一起来forall (a :: (*, *)). Bifunction a a。
剥离大部分领域特定的东西，我们只剩下以下问题的最小重现：
{-# LANGUAGE GADTs, DataKinds, KindSignatures, PolyKinds, RankNTypes #-}
module Repro where
data Bifunction ab cd
where
Bifunction :: (a -> c) -> (b -> d) -> Bifunction '(a, b) '(c, d)
bifunction_id :: Bifunction '(a, a') '(a, a')
bifunction_id = Bifunction id id
bifunction_id' :: Bifunction a a
bifunction_id' = bifunction_id
有没有办法可以bifunction_id与bifunction_id'上面统一？
我尝试过的另一种方法是使用类型族，但这仍然不能完全解决问题：
{-# LANGUAGE GADTs, DataKinds, KindSignatures, PolyKinds, RankNTypes, TypeFamilies #-}
module Repro where
type family Fst (ab :: (x, y)) :: x
where
Fst '(x, y) = x
type family Snd (ab :: (x, y)) :: y
where
Fst '(x, y) = y
data Bifunction ab cd = Bifunction (Fst ab -> Fst cd) (Snd cd -> Snd cd)
bifunction_id :: Bifunction '(a, a') '(a, a')
bifunction_id = Bifunction id id
-- This still doesn't work
-- bifunction_id' :: Bifunction a a
-- bifunction_id' = bifunction_id
-- But now I can do this successfully
bifunction_id' :: Bifunction a a
bifunction_id' = Bifunction id id
但是我真的不明白为什么这个相同的表达式有效，并且宁愿不必在代码的其余部分中管理像这样的有点不明显的区别。