[Agda] Why does unification work here?

[András Kovács]

Hi,

I don't understand why type inference is able to fill the "_" in the
example below:

{-# OPTIONS --type-in-type #-}

Eq : ∀ {A} → A → A → Set
Eq {A} x y = (P : A → Set) → P x → P y

trans : ∀ A x y z → Eq {A} x y → Eq y z → Eq x z
trans A x y z p q P px = q P (p _ px)

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.

It works in Coq, but there is a reference to "tail removal" of equations in
page 8 of here <https://people.mpi-sws.org/~beta/papers/unicoq.pdf> which
justifies it.

Also, there is a similar situation in Agda which has similar non-linearity
but doesn't get inferred, as I would expect.

foo : (A : Set) (x : A) → ((P : A → Set) → P x) → (P : A → Set) → P x
foo A x f P = f _

Thanks,
András Kovács
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170719/f6506084/attachment-0001.html>