Проблемы с эквивалентными доказательствами и разрешением интерфейса в Idris

Question

Я пытаюсь смоделировать доказательства эквациональных рассуждений в стиле Агды для сетоидов (типов с отношением эквивалентности). Моя установка выглядит следующим образом:

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)

По крайней мере, мне кажется, что эта ошибка связана с разрешением интерфейса, которое плохо взаимодействует с расширениями синтаксиса.

Мой опыт показывает, что такие странные ошибки могут быть решены путем явной передачи неявных параметров. Проблема в том, что такое решение убьет "читабельность" доказательств комбинатора эквационального мышления.

Есть ли способ решить это? Соответствующая часть для воспроизведения этой ошибки доступна в ранее связанной суть.