Non-linear unification produces ill-typed term

[UlfNorell]

From jesper.c...@gmail.com on October 15, 2013 13:22:51

In the following program, a wildcard argument _ is accepted even though it cannot be replaced by a valid term. I'm using a recent darcs version of Agda on linux.

{-# OPTIONS --without-K #-}

module JohnMinor where

open import Level using () open import Data.Empty open import Relation.Nullary open import Data.Bool open import Relation.Binary.PropositionalEquality

-- Standard eliminator for ≡ J : ∀ {a b} {A : Set a} {x : A} {Φ : (y : A) → x ≡ y → Set b} → Φ x refl → {y : A} → (e : x ≡ y) → Φ y e J φ refl = φ

-- A kind of heterogeneous equality ≃ : {A : Set} (x : A) {A' : Set} → A' → Set ≃_ {A} x {A'} x' = (E : A ≡ A') → J x E ≡ x'

-- It shouldn't be possible to define this without K ≃refl : {A : Set} {x : A} → x ≃ x ≃refl {x = x} = λ E → J {Φ = λ A' E' → J x E' ≡ _} refl E

-- These can be given using univalence postulate Swap : Bool ≡ Bool postulate swap : true ≡ J {Φ = λ A _ → A} false Swap

-- Univalence and ≃refl don't play nice together right : ¬ (true ≡ false) right ()

wrong : true ≡ false wrong = trans swap (≃refl Swap)

madness : ⊥ madness = right wrong

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

[UlfNorell]

From jesper.c...@gmail.com on October 18, 2013 04:49:25

Just to be clear: I expect Agda to report an unsolved metavariable for this example, but it doesn't. Asking Agda to evaluate ≃refl to normal form with ShowImplicit gives the following:

λ {A} {x} → J {Level.suc Level.zero} {Level.zero} {Set} {A} {λ A' E' → ≡ {Level.zero} {A'} (J {Level.suc Level.zero} {Level.zero} {Set} {A} {λ v v₁ → v} x {A'} E') x} refl {A}

i.e. Agda fills in x for the underscore. However, filling in x for the underscore gives a type error because x has type A, while a term of type A' is expected.

I tried but failed to find a simpler example that exhibits the same problem.

[UlfNorell]

From nils.anders.danielsson on October 18, 2013 09:11:04

A cut-down example:

module Bug where

postulate Eq : (A : Set) (x : A) → A → Set cast : (A B : Set) → A → B magic : (P : Set → Set) (A : Set) → P A

bad : (A : Set) (x : A) → Eq A (cast A A x) x bad A x = magic (λ B → Eq B (cast A B x) _) A

Status: Accepted
Owner: andreas....@gmail.com
Labels: Priority-High Milestone-2.3.4 Type-Defect Unification

[UlfNorell]

From andreas....@gmail.com on October 18, 2013 10:32:46

Here, the hole has type

A : Set, x : A, B : Set |- _ : B

which Agda represents as

_ : (A : Set) (x : A) (B : Set) -> B

The rhs (magic (...) A) has type

A, x |- (\ B -> Eq B (cast A B x) (_ A x B)) A

which is

A, x |- Eq A (cast A A x) (_ A x A)

It is supposed to have type

A, x |- Eq A (cast A A x) x

Thus, we get the constraint

A, x |- _ A x A = x : A

which the unifier solves by

_ = \ A x B -> x

It is not strictly a Miller-pattern (non-linearity), but since the non-linear variable does not appear on the rhs, it does solve. And produces an ill-typed solution.

So there is a fundamental flaw in the current HO-unifier. Interesting and unexpected. It seems that non-linearity has to be treated with more care in the presence of dependent types...

Summary: Non-linear unification produces ill-typed term (was: Wildcard argument accepted where it shouldn't)

[UlfNorell]

From andreas....@gmail.com on October 18, 2013 21:31:12

One solution I see is: instead of solving a meta in a non-linear constraint, try to prune the non-linear variables from that meta. This may or may not lead to a linear equation which can then be solved.

In any case, I seems wise to type-check metavar solution candidates before accepting them. Upon this suggestion, Ulf uses to whine how expensive that would be. But maybe it is not that bad. After all, we also traverse the whole candidate solution during the occurs check, even twice sometimes, the second time normalizing it. Anyway, I will give double-checking a shot, now since I have a test case where it can actually fail.

[UlfNorell]

From andreas....@gmail.com on October 25, 2013 15:49:10

Double-checking does not work yet, but the original problem is fixed. Just had to remove some cleverness that did not regard non-linear variables as such if they did not appear on the rhs.

Thx for reporting.

Status: Fixed
Labels: Meta