[Agda] Why does unification work here?

[Andreas Abel]

On 19.07.2017 19:47, András Kovács wrote:
>        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.

Indeed, you are right.  We can prune away all the context dependencies 
from alpha, and end up with *literally* these two equations, which are 
trivial.

You can watch Agda pruning with

   {-# OPTIONS -v tc.meta.kill:100 #-}

attempting kills
   m'    = _1
   xs    = [P, x]
   vs    = [A, x, y, z, p, q, P, px, x]
   kills = [True,False,True,True,True,True,False,True,False]
after kill analysis
   metavar = _P_1
   kills   = [True,False,True,True,True,True,False,True,False]
   kills'  = 
[ru(False),ru(False),ru(True),ru(True),ru(True),ru(True),ru(False),ru(True),ru(False)]
   oldType = ((A₁ : Set) (x₁ y₁ z₁ : A₁) (p₁ : Eq A₁ x₁ y₁)
              (q₁ : Eq A₁ y₁ z₁) (P₁ : A₁ → Set) (px₁ : P₁ x₁) →
              A₁ → Set)
   newType = ((A₁ : Set) → A₁ → (A₁ → Set) → A₁ → Set)
actual killing
   new meta: _2
   kills   : 
[ru(False),ru(False),ru(True),ru(True),ru(True),ru(True),ru(False),ru(True),ru(False)]
   inst    : _1 := (_P_2 @8 A q px)

That prunes away "y" amongst other context dependencies, making the 
constraint alpha[...] y = P y linear.

I implemented this "if-you-cannot-solve-at-least-try-to-prune" sometimes 
in 2011, it goes beyond what is described in

   Andreas Abel, Brigitte Pientka:
   Higher-Order Dynamic Pattern Unification for Dependent Types and 
Records.
   TLCA 2011: 10-26

Thanks for bringing up a nice application for this technique.

Best,
Andreas

> 2017-07-19 18:24 GMT+02:00 Andreas Abel <abela at chalmers.se 
> <mailto: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 <mailto:andreas.abel at gu.se>
>     http://www.cse.chalmers.se/~abela/ <http://www.cse.chalmers.se/~abela/>
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>
> 
> 

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