Problems with equational proofs and interface resolution in Idris

Question

I'm trying to model Agda style equational reasoning proofs for Setoids (types with an equivalence relation). My setup is as follows:

infix 1 :=:

interface Equality a where
  (:=:)  : a -> a -> Type

interface Equality a => VerifiedEquality a where  
  eqRefl : {x : a} -> x :=: x
  eqSym  : {x, y : a} -> x :=: y -> y :=: x
  eqTran : {x, y, z : a} -> x :=: y -> y :=: z -> x :=: z

Using such interfaces I could model some equational reasoning combinators like Syntax.PreorderReasoning from Idris library.

syntax [expr] "QED" = qed expr 
syntax [from] "={" [prf] "}=" [to] = step from prf to

namespace EqReasoning
  using (a : Type, x : a, y : a, z : a)
    qed : VerifiedEquality a => (x : a) -> x :=: x
    qed x = eqRefl {x = x}

    step : VerifiedEquality a => (x : a) -> x :=: y -> (y :=: z) -> x :=: z
    step x prf prf1 = eqTran {x = x} prf prf1

The main difference from Idris library is just the replacement of propositional equality and their related functions to use the ones from VerifiedEquality interface.

So far, so good. But when I try to use such combinators, I run in problems that, I believe, are related to interface resolution. Since the code is part of a matrix library that I'm working on, I posted the relevant part of it in the following gist.

The error occurs in the following proof

zeroMatAddRight : ( VerifiedSemiring s
                  , VerifiedEquality s ) =>
                  {r, c : Shape} ->
                  (m : M s r c)  -> 
                  (m :+: (zeroMat r c)) :=: m
zeroMatAddRight {r = r}{c = c} m 
    = m :+: (zeroMat r c)
         ={ addMatComm {r = r}{c = c} m (zeroMat r c) }=
      (zeroMat r c) :+: m
         ={ zeroMatAddLeft {r = r}{c = c} m }=
      m
      QED  

that returns the following error message:

 When checking right hand side of zeroMatAddRight with expected type
         m :+: (zeroMat r c) :=: m

 Can't find implementation for Semiring a

 Possible cause:
         ./Data/Matrix/Operations/Addition.idr:112:11-118:1:When checking an application of function Algebra.Equality.EqReasoning.step:
                 Type mismatch between
                         m :=: m (Type of qed m)
                 and
                         y :=: z (Expected type)

At least to me, it appears that this error is related with interface resolution that isn't interacting well with syntax extensions.

My experience is that such strange errors can be solved by passing implicit parameters explicitly. The problem is that such solution will kill the "readability" of equational reasoning combinator proofs.

Is there a way to solve this? The relevant part for reproducing this error is available in previously linked gist.

Nipa