[Agda] Why does unification work here?

[Andreas Abel]

Hi András,
On 19.07.2017 16:12, András Kovács wrote:
> 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, 

That's correct.

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

Mmh, let's see.  We have

   q P (p alpha px) : P z

thus, we get the ascribed type

   p alpha px : P y    (1)

at the same time, we get the inferred types

  p alpha : alpha x -> alpha y
  px      : P x  (2)

This will give us two constraints

   alpha y = P y   (from 1)
   alpha x = P x   (from 2)

As you observe correctly, the second constraint does not allow us to 
solve for alpha, because of non-linearity, but the first does 
(validating the second constraint).

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

Here, we only get the non-linear constraint, thus, Agda is stuck.

Best,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/