與Idris接口的奇怪的錯誤消息

Question

我想實現一個簡單的代數結構層次結構使用Idris接口。代碼如下：

module AlgebraicStructures 

-- definition of some algebraic structures in terms of type classes 

%access public export 

Associative : {a : Type} -> (a -> a -> a) -> Type 
Associative {a} op = (x : a) -> 
        (y : a) -> 
        (z : a) -> 
        (op x (op y z)) = (op (op x y) z) 

Identity : {a : Type} -> (a -> a -> a) -> a -> Type 
Identity op v = ((x : a) -> (op x v) = x, 
       (x : a) -> (op v x) = x)     


Commutative : {a : Type} -> (a -> a -> a) -> Type 
Commutative {a} op = (x : a) -> 
        (y : a) -> 
        (op x y) = (op y x) 


infixl 4 <**> 

interface IsMonoid a where 
    empty : a 
    (<**>) : a -> a -> a 
    assoc : Associative (<**>) 
    ident : Identity (<**>) empty 


interface IsMonoid a => IsCommutativeMonoid a where 
    comm : Commutative (<**>) 

但是，伊德里斯是給這個奇怪的錯誤消息：

When checking type of constructor of AlgebraicStructures.IsCommutativeMonoid: 
Can't find implementation for IsMonoid a 

我相信，伊德里斯接口，如Haskell的類型類作品。在Haskell中，它應該起作用。我在做一些愚蠢的事情嗎？

Answer 1

我認爲它可能會抱怨，因爲我不知道有任何約束的表達Commutative (<**>)的a做 - 所以它不知道，你可以在該類型調用<**>。 明確指定a似乎對我很有用 - Commutative {a} (<**>) - 我希望這意味着來自接口簽名的a在範圍內並可用於顯式傳遞給其他類型。