[Agda] irrelevant fields and EqReasoning

[Noam Zeilberger]

On Mon, Jul 16, 2012 at 5:17 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
>
> irrelevant fields may produce more unsolved metas, since from
>
>   record { irr = a } == record { irr = b }
>
> you cannot conclude that a is equal to b.  In case a is a meta, no
> constraints are generated for a.

That makes sense.  What isn't at all obvious to me though is why this
example should be generating metas in the first place, since
intuitively all of the information needed for typechecking is explicit
in the term Proof, and Proof should be interchangeable with Proof'.

Maybe that's the wrong intuition...but on the other hand it does seem
that there is a potentially devious source of nondeterminism in
typechecking records containing irrelevant fields (RCIFs), given that
Agda is not completely explicit about bidirectionality.  That is,
there is a difference between *inferring* a RCIF versus introducing a
meta for the RCIF together with an equality constraint (with the
latter generally leading to unsolved metas because of proof
irrelevance, as you described).  Is that what is going on here in
Proof versus Proof'?

Noam