Является ли этот тип инъекционным?

Question

У меня есть тип семьи для N-арной функции от 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)?