이 제품군은 주사기입니까? 나는이 가족은 내가 GHC 그것을 증명할 수에 의해 단사이되어야한다고 생각</p> <pre><code>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) </code></pre> <p>:

Question

I 형 t의 n 인수에서 유형 o의 값으로 N 진 기능 형 가족이

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)입니까?