[Agda] irrelevant fields and EqReasoning

[Andreas Abel]

Hi Noam,

I agree with your analysis.

As I see it, you have already answered your question (from your second 
mail) in your first mail, which was:

On 16.07.12 4:59 PM, Noam Zeilberger wrote:
 > 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".

Here you write that if you omit repetitive hidden arguments, you get 
unsolved metas.  But EqReasoning does exactly this, omitting redundant 
args to trans.

   _∼⟨_⟩_ : ∀ x {y z} → x ∼ y → y IsRelatedTo z → x IsRelatedTo z
   _ ∼⟨ x∼y ⟩ relTo y∼z = relTo (trans x∼y y∼z)

Also, I think your observation is correct:  If Agda would propagate type 
information better, it would create less metas and hence, less unsolved 
metas.

Currently if you have

   f args : type

then the information from type is only pushed in if f is a constructor. 
  Otherwise, the type of f args is inferred from the type of f, creating 
metas for the hidden arguments, and then only is the inferred type 
unified with the given type.

Cheers,
Andreas

On 18.07.12 2:17 PM, Noam Zeilberger wrote:
> 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
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/