Idris中的等式证明和界面分辨率问题

Question

我正在尝试为Setoids建模Agda风格的等式推理证明(具有等价关系的类型).我的设置如下:

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

使用这样的接口,我可以模拟一些像Syntax.PreorderReasoning伊德里斯库那样的等式推理组合器 .

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

与Idris库的主要区别仅在于替代命题相等及其相关函数以使用来自VerifiedEquality接口的函数.

到现在为止还挺好.但是当我尝试使用这样的组合器时,我遇到了一些问题,我认为这些问题与接口解析有关.由于代码是我正在处理的矩阵库的一部分,我在下面的要点中发布了它的相关部分.

以下证明中发生错误

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  

返回以下错误消息:

 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)

至少在我看来,这个错误似乎与界面分辨率无关,而且与语法扩展没有良好的交互作用.

我的经验是,通过显式传递隐式参数可以解决这些奇怪的错误.问题是这种解决方案会破坏等式推理组合证明的"可读性".

有办法解决这个问题吗？重现此错误的相关部分可在先前链接的要点中找到.