是这种类型的内射？

Question

我有型家族N元函数从t型n参数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)？