Error on equational reasoning proofs and interface resolution

[rodrigogribeiro]

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.

[ahmadsalim]

@rodrigogribeiro Thanks for reporting the issue

Syntax expressions should have no effect after they parse. It does seem that there is some issues w.r.t. the way inference and implementation resolution is performed. I am unsure whether this could be completely solved by better heurestics, but I think your issue might be useful to try and fine tune them.

[rodrigogribeiro]

@ahmadsalim : Thanks for taking a look at this. Since syntax expressions have no effect after parsing, the problem is interface resolution. It appears that is not aware that VerifiedSemiring is subinterface of Semiring that is mentioned on error message.

[edwinb]

Have you found a way to resolve this with implicits? It would really help to debug the issue if you could find an explicit term that does type check. If there isn't a way to resolve it by making some more things explicit, it might be that the issue is something else...

[edwinb]

So I reduced the definition and added some holes (this is always a really helpful step to see what might be going on):

zeroMatAddRight : ( VerifiedSemiring s
                , VerifiedEquality s ) =>
                {r, c : Shape} ->
                (m : M s r c)  ->
                (m :+: (zeroMat r c)) :=: m
zeroMatAddRight {r = r}{c = c} m
  = let step1 = m :+: (zeroMat r c)
        prf = addMatComm {r} {c} m (zeroMat r c)
        in ?foo

Idris tells me the type of ?foo is:

  r : Shape
  c : Shape
  s : Type
  m : M s r c
  constraint : VerifiedSemiring s
  constraint1 : VerifiedEquality s
  step1 : M s r c
  prf : meq (addM m (zeroMat r c)) (addM (zeroMat r c) m)
--------------------------------------
foo : meq (addM m (zeroMat r c)) m

All of the interfaces are resolved at this stage. However, these are normalised, and it looks like the evaluator is stuck on reducing 'prf' any further, because it needs to be able to pattern match on r and c to make progress in zeroMat, for a start.

If you try applying preorder reasoning in the hole, you won't make any progress, because 'prf' isn't necessarily an equality proof.

If you write more, Idris will certainly blunder on in the hope of finding more information that means the type of prf can reduce, but in this case it can't. It reports that it can't find Semiring a which actually means that there's some variable a it hasn't been able to resolve - it's nothing to do with the implementations given in the signature, but rather than there's some other information it couldn't figure out.

So, unless I'm missing something (I haven't spent a huge amount of time looking at this after all, and certainly haven't thought much about the meaning of the proof...) it seems that this shouldn't type check as it stands.

It should certainly report the error differently - if it can't resolve a type class because it doesn't know what it's resolving yet, then there's something more helpful it can say, surely. I will think about that.