[Agda] irrelevant fields and EqReasoning

[Noam Zeilberger]

For anyone interested, here is an alternate implementation of
PreorderReasoning that pushes the types through explicitly, rather
than relying on constraint solving (which as Andreas explained will
fail when there are irrelevant fields).  This gets rid of the unsolved
metas in my original example.  It is not quite patch-worthy, though,
since as per Jean-Philippe's suggestion I'm using "syntax" to deal
with the fact that the mixfix operators now have non-left-to-right
dependency order, and I'm not sure what's the best way of dealing with
the fact that a bunch of other library modules want to rename these
now unrenameable operators.

Also, I wanted to clarify a bit what I wrote here...

On Wed, Jul 18, 2012 at 2:17 PM, Noam Zeilberger
<noam.zeilberger at gmail.com> wrote:
> [...] 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.

This is a bit sloppy.  What I was trying to say is that initially this
was very confusing to me -- that these unsolved metas should be
appearing in an apparently completely explicit proof term -- and that
from what Andreas explained, potentially this kind of thing could
sneak in whenever you are dealing with proof irrelevance.  So it seems
to me that this is a concrete argument for eventually taking a more
Epigram-like approach in Agda, trying to make it more explicit to the
programmer in which direction the types are flowing.

Just something to keep in mind.

Noam
-------------- next part --------------
A non-text attachment was scrubbed...
Name: PreorderReasoning.agda
Type: application/octet-stream
Size: 2470 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20120720/9d8143f8/PreorderReasoning.obj