Strange error message with Idris interfaces

Question

I'm trying to implement a simple algebraic structures hierarchy using Idris interfaces. The code is as follows:

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 (<**>)

But, Idris is giving this strange error message:

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

I believe that Idris interfaces works like Haskell's type classes. In Haskell, it should work. Am I doing something silly?

Answer 1

I believe it may be complaining because I don't know that there's anything that constrains the a in the expression Commutative (<**>) - so it doesn't know that you can invoke <**> on that type. Explicitly specifying the a seems to work for me - Commutative {a} (<**>) - I hope that that means that the a from the interface signature is in scope and available for explicitly passing to other types.