[Agda] Inference for invariant arguments question

[Andrea Vezzosi]

Hi,

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?

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


-- Andrea
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131006/0845247e/attachment.html