<div dir="ltr"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span style="font-size:12.8px">  alpha y = P y   (from 1)<br></span><span style="font-size:12.8px">  alpha x = P x   (from 2)</span></blockquote><div><br></div><div>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.</div></div><div class="gmail_extra"><br><div class="gmail_quote">2017-07-19 18:24 GMT+02:00 Andreas Abel <span dir="ltr"><<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi András,<span class=""><br>
On 19.07.2017 16:12, András Kovács wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I don't understand why type inference is able to fill the "_" in the example below:<br>
<br>
{-# OPTIONS --type-in-type #-}<br>
<br>
Eq : ∀ {A} → A → A → Set<br>
Eq {A} x y = (P : A → Set) → P x → P y<br>
<br>
trans : ∀ A x y z → Eq {A} x y → Eq y z → Eq x z<br>
trans A x y z p q P px = q P (p _ px)<br>
<br>
My understanding is that first we get a new "α [A, x, y, z, p, q, P, px]" meta for the underscore, <br>
</blockquote>
<br></span>
That's correct.<span class=""><br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
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<br>
doesn't actually fail in Agda 2.5.2.<br>
</blockquote>
<br></span>
Mmh, let's see.  We have<br>
<br>
  q P (p alpha px) : P z<br>
<br>
thus, we get the ascribed type<br>
<br>
  p alpha px : P y    (1)<br>
<br>
at the same time, we get the inferred types<br>
<br>
 p alpha : alpha x -> alpha y<br>
 px      : P x  (2)<br>
<br>
This will give us two constraints<br>
<br>
  alpha y = P y   (from 1)<br>
  alpha x = P x   (from 2)<br>
<br>
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).<span class=""><br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Also, there is a similar situation in Agda which has similar non-linearity but doesn't get inferred, as I would expect.<br>
<br>
foo : (A : Set) (x : A) → ((P : A → Set) → P x) → (P : A → Set) → P x<br>
foo A x f P = f _<br>
</blockquote>
<br></span>
Here, we only get the non-linear constraint, thus, Agda is stuck.<br>
<br>
Best,<br>
Andreas<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
Andreas Abel  <><      Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www.cse.chalmers.se/~abela/" rel="noreferrer" target="_blank">http://www.cse.chalmers.se/~ab<wbr>ela/</a><br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</font></span></blockquote></div><br></div>