[Agda] Why does unification work here?

[András Kovács]

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


Aren't these both non-linear, respectively in "y" and "x"? I think it works
because we prune the left side of one equation and postpone it, which makes
the second equation linear, and then solve the postponed one.

2017-07-19 18:24 GMT+02:00 Andreas Abel <abela at chalmers.se>:

> 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/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170719/4cc64326/attachment.html>