[Agda] Inference for invariant arguments question

[Andreas Abel]

Sorry, I somehow overlooked your message...

On 06.10.2013 00:34, Andrea Vezzosi wrote:
> In the following the _ in "yellow" is not resolved while the one in
> "inferred" is.
> Is it because g is not invariant in that argument and so it matters what
> we pass to it?

Exactly, yes!

The _ in inferred is resolved by instance search, since f does not 
depend on it.  However, g z might depend on z (we do not know since we 
do not know how g behaves...).

Cheers,
Andreas

> open import Relation.Binary.PropositionalEquality
>
> data X : Set where
>    x : X
>
> f : X -> X -> Set
> f _ x = X
>
> postulate
>    stuck : X
>    g : ∀ z -> f z stuck
>
> yellow : ∀ z -> f z stuck
> yellow z = g _
> inferred : ∀ z -> f _ ≡ f z
> inferred z = refl



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