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の型クラスのような作品をインタフェースすることを信じているコードは次のようです。ハスケルでは、うまくいくはずです。私は何か愚かなことをしていますか？

Answer 1

の式がCommutative (<**>)に制限されていることがわかっていないので、不平を言っている可能性があります。そのタイプの<**>を呼び出すことはできません。 - これは、インターフェイスシグネチャのaが有効範囲内にあり、明示的に他のタイプに渡すことができることを意味します。