我试图以这样一种方式证明类型级列表的关联性，这种方式将允许我在等效类型之间进行转换而无需携带任何约束。
假设串联的标准定义：
type family (++) (xs :: [k]) (ys :: [k]) :: [k] where
'[] ++ ys = ys
(x ': xs) ++ ys = x ': (xs ++ ys)
假设，我得到了一个函数：
given :: forall k (a :: [k]) (b :: [k]) (c :: [k]). Proxy ((a ++ b) ++ c)
given = Proxy -- Proxy is just an example
我想调用这个函数，然后使用关联性：
my :: forall k (a :: [k]) (b :: [k]) (c :: [k]). Proxy (a ++ (b ++ c))
my …