Странное сообщение об ошибке с интерфейсами 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

Я считаю, что это может жаловаться, потому что я не знаю, что есть что-то, что ограничивает a в выражении Commutative (<**>) - так он не знает, что вы можете вызвать <**> по этому типу. Явное указание a, похоже, работает на меня - Commutative {a} (<**>) - Надеюсь, это означает, что a из сигнатуры интерфейса находится в области видимости и доступен для явного перехода к другим типам.