[Agda] irrelevant fields and EqReasoning

[Noam Zeilberger]

I'm seeing some strange behavior while trying to use EqReasoning
(Relation.Binary.EqReasoning from the standard library) to build
proofs of equality of records containing irrelevant fields, and I was
wondering if someone has an idea of what could be going on.
(Apologies for a slightly vague question, but I'm having trouble
coming up with a small example of the behavior in question.)

So, following EqReasoning, the general shape of these proofs is

  Proof = begin x0 ≈⟨ e1 ⟩ x1 ≈⟨ e2 ⟩ x2 ... ≈⟨ en ⟩ xn ∎

where the xi are terms of a common type, and the ei are proofs of
equality ei : x(i-1) ≈ xi.  In my case, the xi are terms of a record
type Foo containing an irrelevant field "bar", and ≈ is a certain
equivalence relation on Foo (not defined as propositional equality).

The strange behavior is that type-checking Proof yields various
unsolved metas of type "bar".  If I rewrite Proof using explicit
application of transitivity

  Proof' = trans≈ {i = x0} {j = x1} {k = xn} e1 $
               trans≈ {i = x1} {j = x2} {k = xn} e2 $
               ...
               trans≈ {i = x(n-2)} {j = x(n-1)} {k = xn} e(n-1) $
               en

then the unsolved metas go away.  On the other hand, if I try to
remove some of the redundancy in Proof' (e.g., by leaving the j's or
the k's implicit) then again there are unsolved metas of type "bar".

Any ideas?

thanks,
Noam