Unification gets stuck on obviously non-unifiable functions

[UlfNorell]

From adamgundry on October 26, 2012 15:50:20

-- I was trying to extend Conor's KIPLING technique (Outrageous but -- Meaningful Coincidences, WGP 2010) which depends on indexing a -- syntax by functions, when I hit this problem:

module Bug where

data U : Set where a : U b : U

data Foo : (U -> U) -> Set where mka : Foo (\ x -> a) mkb : Foo (\ x -> b)

foo : Foo (\ x -> a) -> Set foo mka = ?

-- This gives the error message:

-- -- Cannot decide whether there should be a case for the constructor -- -- mkb, since the unification gets stuck on unifying the inferred -- -- indices -- -- [λ x → b] -- -- with the expected indices -- -- [λ x → a] -- -- when checking the definition of foo

-- But these indices cannot be unified (a and b are constants) so it -- should be possible to exclude this case. Could we improve the -- unifier to notice this?

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

[UlfNorell]

From nils.anders.danielsson on October 26, 2012 08:41:16

Owner: andreas....@gmail.com

[UlfNorell]

From andreas....@gmail.com on October 28, 2012 10:37:20

Currently the unifier does not handle lambdas. It cannot disunify \ x -> a with \ x -> b. It could be improved, I guess, but maybe never anyone pressed for this...

Status: Accepted
Labels: Type-Enhancement Priority-Medium Unification

[UlfNorell]

From nils.anders.danielsson on October 29, 2012 03:01:55

Workaround:

bar : ∀ {f} → Foo f → (∀ x → f x ≡ a) → Set bar mka _ = ? bar mkb eq with eq a ... | ()

foo : Foo (λ x → a) → Set foo f = bar f (λ _ → refl)

[UlfNorell]

From adamgundry on October 29, 2012 03:37:41

Thanks for taking a look at this. This kind of workaround requires the domain of the indexing lambda to be inhabited, which may or may not be troublesome. I wonder if there are any other examples that need this; it seems unlikely that I am the first person to run into it!

[UlfNorell]

From guillaum...@gmail.com on October 29, 2012 05:20:35

This kind of workaround requires the domain of the indexing lambda to be inhabited

I think it would rather be troublesome not to require that the domain of the indexing lambda is inhabited. Assuming function extensionality the functions λ (x : empty) → a and λ (x : empty) → b are equal.

[UlfNorell]

From nils.anders.danielsson on October 29, 2012 09:29:16

Yes, we should be very careful if we try to make the unifier smarter: postulating extensional equality for functions should not make Agda inconsistent.

[UlfNorell]

From andreas....@gmail.com on October 29, 2012 11:45:25

Right, unification concerns extensional equality of closed things. This must be the reason why there is no rule for lambdas. So, no fix! Here is another workaround: Use parameters and explicit equality instead of indices.

data D (f : U → U) : Set where da : (f ≡ λ x → a) → D f db : (f ≡ λ x → b) → D f

app : ∀ {A B : Set}{f g : A → B} → f ≡ g → ∀ x → f x ≡ g x app refl x = refl

fu : D (λ x → a) → Set fu (da refl) = U fu (db p) with app p a ... | ()

Status: WontFix