Yellow irrelevant metas [Re: [Agda] Re: comlicated equivalence: need help to prove: errh, addres of repository]

[Andreas Abel]

The relevant issue is

   http://code.google.com/p/agda/issues/detail?id=351

If you have

   f : .A -> B

then the equation

   f a = f _1

does not lead to the solution _1 := a, because the equation holds for 
any _1 : A.  In fact, the constraint _1 = a is never generated because 
irrelevant arguments are ignored during equality checking.  Thus, in the 
absence of other constraints on _1, it will lead to yellow.

The problem could be overcome by searching for solutions for left-over 
irrelevant meta-variables.  However, I have not seen any published work 
on this.  Even Jason Reed, who studied unification in the presence of 
irrelevance did not attempt to solve this problem.

Cheers,
Andreas

On 2/24/11 4:33 PM, Nils Anders Danielsson wrote:
> On 2011-02-24 15:36, Daniel Peebles wrote:
>> If you're wondering why the name includes the underlying category, so
>> am I. It's very puzzling, but if I don't include the C parameter (by
>> making it implicit) even in the type of refl, it'll turn yellow. I
>> could understand it having trouble if C were an index to the type, but
>> as a parameter, the unsolved metas make no sense to me.
>
> If you make the irrelevant fields relevant, then the parameter can be
> inferred. Andreas may know more.
>

-- 
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/