agda/agda — pull request #19 by fredrikNordvallForsberg (2014-10-21 13:48:28+00:00)
Title: make instance search work on the reduced type

This small change fixes an internal error caused by the following code (simplified from code found in the HoTT-Agda repository), since n ≠ zero is not reduced to n == zero -> ⊥ before instance search:

data _==_ {A : Set} (a : A) : A -> Set where
refl : a == a

data ⊥ : Set where

data ℕ : Set where
zero : ℕ
suc : ℕ -> ℕ

¬ : (A : Set) → Set
¬ A = A → ⊥

_≠_ : {A : Set} → (A → A → Set)
x ≠ y = ¬ (x == y)

f : (n : ℕ) ⦃ _ : n ≠ zero ⦄ -> ℕ
f n = n

g : ℕ
g = f (suc zero)

I haven't added a test case, because it is not clear to me how instance search should ideally work for higher-order types, especially with performance issues in mind. (In particular, as the new error message informs us, the search currently looks for a solution of the form \ _ -> x, where x : ⊥, which seems a little bit too optimistic...)