Unifier should fully support eta/type-direction | Variable patterns should behave like lambdas

[UlfNorell]

From nils.anders.danielsson on June 21, 2011 13:43:53

I'm not sure if this bug is related to issue 376 .

module Bug where

---

-- Prelude

data ≡ {A : Set} (x : A) : A → Set where refl : x ≡ x

record Σ (A : Set) (B : A → Set) : Set where constructor , field proj₁ : A proj₂ : B proj₁

curry : {A C : Set} {B : A → Set} → (Σ A B → C) → ((x : A) → B x → C) curry f x y = f (x , y)

uncurry : {A C : Set} {B : A → Set} → ((x : A) → (y : B x) → C) → (Σ A B → C) uncurry f p = f (Σ.proj₁ p) (Σ.proj₂ p)

---

-- Preliminaries

postulate U : Set El : U → Set

mutual

data Ctxt : Set where ▻ : (Γ : Ctxt) (σ : Type Γ) → Ctxt

Type : Ctxt → Set Type Γ = Env Γ → U

Env : Ctxt → Set Env (Γ ▻ σ) = Σ (Env Γ) λ γ → El (σ γ)

postulate Γ : Ctxt σ : Type Γ

---

-- Problem

-- The following equality holds definitionally.

equal : (τ : (γ : Env Γ) → El (σ γ) → U) → curry (uncurry τ) ≡ τ equal τ = refl

-- However, the two sides behave differently.

works : (τ₁ τ₂ : (γ : Env Γ) → El (σ γ) → U) → τ₁ ≡ τ₂ → Set₁ works τ .τ refl = Set

works′ : (τ₁ τ₂ : (γ : Env Γ) → El (σ γ) → U) → curry (uncurry τ₁) ≡ τ₂ → Set₁ works′ τ .τ refl = Set

fails : (τ₁ τ₂ : (γ : Env Γ) → El (σ γ) → U) → τ₁ ≡ curry (uncurry τ₂) → Set₁ fails τ .τ refl = Set

fails′ : (τ₁ τ₂ : (γ : Env Γ) → El (σ γ) → U) → curry (uncurry τ₁) ≡ curry (uncurry τ₂) → Set₁ fails′ τ .τ refl = Set

-- I find it interesting that works′ works, whereas the symmetric -- variant fails fails.

Original issue: http://code.google.com/p/agda/issues/detail?id=423

[UlfNorell]

From andreas....@gmail.com on June 22, 2011 01:40:25

Well I guess you hit this piece of code in TypeChecking.Rules.LHS.Unify:

-- TODO: eta for records here
unify :: Type -> Term -> Term -> Unify ()
unify a u v = do

The unifier (in contrast to the meta solver) does not do eta yet. Actually, I never understood why these are two different engines...

[UlfNorell]

From andreas....@gmail.com on June 22, 2011 01:56:43

works' works because tau_2 is flexible (dot pattern) and can be instantiated to curry (uncurry tau) fails fails because tau is rigid and cannot be instantiated to curry (uncurry tau2) (with flexible tau2).

If the unifier worked modulo eta, I guess this difference would vanish.

[UlfNorell]

From andreas....@gmail.com on June 22, 2011 02:54:00

Partially fixed. More normalization helps, to get more eta-contraction. This bug disappears now if one defines curry/uncurry as lambda-abstractions. Then curry (uncurry \tau) reduces to \tau by beta and eta.

Summary: Unifier should fully support eta/type-direction | Variable patterns should behave like lambdas
Status: Started

[UlfNorell]

From ulf.nor...@gmail.com on June 22, 2011 04:44:22

Actually, I never understood why these are two different engines...

There are different requirements on the solutions they produce. In both cases you are dealing with open constraints involving free variables (actual variables, not metas). However, when solving metas you are looking for a unique solution that makes the open constraint true, and in the unifier you are looking for a solution that holds for all closed instances of the open constraint. An example:

Suppose we have a function f as follows

f : Bool -> A -> B f true y = ... f false y = ...

Now if in the meta solver we run into the constraint

f x _5 = f x t

for some variable x and arbitrary term t, it's safe to solve this by

_5 := t

Why? Because no other solution will satisfy the (open) constraint. If, on the other hand, we get the same constraint during unification, for instance from checking the function

g : (y : A) -> f x y == f x t -> B g .t refl = ...

we are in a different situation. We can only unify y with t if for any value of x, y = t is the only solution to f x y = f x t. This isn't true in general, and so unification fails.

[UlfNorell]

From andreas....@gmail.com on June 22, 2011 05:42:19

Sorry, no, we cannot solve _5 := t and we don't. This is only the unique solution if f is injective. But then we can also solve it this way during unification. [Take, for instance, f true y = true and f false y = false or anything independent of y]

[UlfNorell]

From ulf.nor...@gmail.com on June 23, 2011 00:10:58

Actually we do:

postulate A : Set a b : A T : A -> Set mkT : (a : A) -> T a

f : Bool -> A -> A f true y = a f false y = b

g : (x : Bool)(y : A) -> T (f x y) g x y = mkT (f x _)

Here the underscore is solved with y. The reason we can is that it's the unique solution that makes the program well-typed. That is the difference between solving metas and unification as I tried to explain. When solving metas a constraint a = b means that the open terms a and b should be definitionally equal, but in unification it means that all closed instances of a and b should be equal, which is a weaker statement.

[UlfNorell]

From ulf.nor...@gmail.com on September 10, 2011 23:09:49

Status: Duplicate
Mergedinto: 365