这种类型的家庭是单独的吗？

Question

我有N-ary函数的类型族,从n类型的参数到类型t的值o:

type family NAry (n :: Nat) (t :: Type) (o :: Type) = (r :: Type) | r -> n t o where
    NAry 1 t o = t -> o
    NAry n t o = t -> (NAry (n - 1) t o)

我认为这个家庭应该是无形的,我无法向GHC证明:

error:
    * Type family equations violate injectivity annotation:
        NAry 1 t o = t -> o
        NAry n t o = t -> NAry (n - 1) t o
error:
    * Type family equation violates injectivity annotation.
      Type variable `n' cannot be inferred from the right-hand side.
      In the type family equation:
        NAry n t o = t -> NAry (n - 1) t o

Answer 1

它并不像你承诺的那样是单射的.拿类型

Int -> Int -> Bool

问:是这个NAry 2 Int Bool还是NAry 1 Int (Int -> Bool)？