<div dir="ltr">Hi,<div><br></div><div>I don't understand why type inference is able to fill the "_" in the example below:</div><div><br></div><div><div>{-# OPTIONS --type-in-type #-}</div><div><br></div><div>Eq : ∀ {A} → A → A → Set</div><div>Eq {A} x y = (P : A → Set) → P x → P y</div><div><br></div><div>trans : ∀ A x y z → Eq {A} x y → Eq y z → Eq x z</div><div>trans A x y z p q P px = q P (p _ px)</div></div><div><br></div><div>My understanding is that first we get a new "α [A, x, y, z, p, q, P, px]" meta for the underscore, then attempt to solve "α [A, x, y, z, p, q, P, px] x = P x", which is non-linear in "x", so it should fail. It doesn't actually fail in Agda 2.5.2.</div><div><br></div><div>It works in Coq, but there is a reference to "tail removal" of equations in page 8 of <a href="https://people.mpi-sws.org/~beta/papers/unicoq.pdf">here</a> which justifies it.</div><div><br></div><div>Also, there is a similar situation in Agda which has similar non-linearity but doesn't get inferred, as I would expect.</div><div><br></div><div><div>foo : (A : Set) (x : A) → ((P : A → Set) → P x) → (P : A → Set) → P x</div><div>foo A x f P = f _</div></div><div><br></div><div>Thanks,</div><div>András Kovács</div><div><br></div><div><br></div><div><br></div><div><br></div></div>