I am trying to model the Agda style argumentation Equation expressions for Setoids (types with equivalence relation). My setup is this:
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 equatorial rational combinators, such as Syntax.PreorderReasoning from the 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 the Idris library is simply the replacement of propositional equality and related functions with the use of VerifiedEquality interfaces.
So far so good. But when I try to use such combinators, I have problems that I think are related to the resolution of the interface. Since the code is part of the matrix library I'm working on, I posted the corresponding part in the next gist .
The error occurs in the following proof
zeroMatAddRight : ( VerifiedSemiring s , VerifiedEquality s ) => {r, c : Shape} -> (m : M src) -> (m :+: (zeroMat rc)) :=: m zeroMatAddRight {r = r}{c = c} m = m :+: (zeroMat rc) ={ addMatComm {r = r}{c = c} m (zeroMat rc) }= (zeroMat rc) :+: m ={ zeroMatAddLeft {r = r}{c = c} m }= m QED
which returns the following error message:
When checking right hand side of zeroMatAddRight with expected type m :+: (zeroMat rc) :=: 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 it seems to me that this error is related to the resolution of the interface, which interacts poorly with syntax extensions.
My experience is that such strange errors can be resolved by passing implicit parameters explicitly. The problem is that such a solution will kill the “readability” of evidence of combinatorial reasoning.
Is there any way to solve this? The corresponding part for reproducing this error is available in the previously linked gist .