是這種類型的內射？

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)？