I have a dependant type that consists of a value plus some proofs about its properties. Naturally I would like my notion of equality over this type to be equivalent to equality over the value component. This is all fine except that I run into problems when proving properties of lifted notions of this equality (for example equality over lists of this type).
For example:
open import Data.Nat
open import Data.Product
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.List.Pointwise renaming (Rel to ListRel) hiding (refl)
module Test where
_≈_ : Rel (ℕ × ℕ) _
(a₁ , _) ≈ (a₂ , _) = a₁ ≡ a₂
≈-sym : Symmetric _≈_
≈-sym refl = refl
≋-sym : Symmetric (ListRel _≈_)
≋-sym = symmetric ≈-sym
In the last line Agda complains that it can't solve for the second projections out of the pairs. Interestingly changing the last line to the following eta-equivalent expression means that it can solve them:
≋-sym = symmetric (λ {x} {y} → ≈-sym {x} {y})
Now naturally I know that sometimes Agda can't solve for all the implicit arguments and needs a bit of extra help but I don't understand what new information I'm providing it by doing this...
I'm doing a lot of lifting of equality and I'd rather avoid adding these ugly eta expansions everywhere in my code. I was wondering if anyone has any suggestions to allow something similar to the original code to pass?
I have looked into irrelevance but the second projection is used elsewhere, even if it is computationally irrelevant for equality.
I'm guessing, but I think the problem is that the order of implicit arguments doesn't matter for (a part of) unification. Consider
flipped : (({n m : ℕ} -> n ≡ m) -> ℕ) -> ({m n : ℕ} -> n ≡ m) -> ℕ
flipped k f = k f
Here k receives something of type {n m : ℕ} -> n ≡ m and f is of type {m n : ℕ} -> n ≡ m (m comes before n), but Agda happily unifies these two expressions, since each implicit argument becomes a metavariable during elaboration and metas are not ordered by when they was introduced — they are ordered by how they was instantiated (e.g. you can't instantiate α to β -> β and then β to α as it would result in α ≡ α -> α and handling such loops (called equirecursive types) is an unsound nightmare). So when you write
≋-sym = symmetric ≈-sym
Agda is confused, because it could mean any of
≋-sym = symmetric (λ {x} {y} → ≈-sym {x} {y})
≋-sym = symmetric (λ {x} {y} → ≈-sym {y} {x})
(well, not quite, because the second expression is ill-typed, but Agda doesn't backtrack and can't solve such problems therefore)
This is different from the flipped example, because flipped explicitly specifies how n and m are used, so unification of
{n1 m1 : ℕ} -> n1 ≡ m1
{m2 n2 : ℕ} -> n2 ≡ m2
results in n1 ≡ n2 and m1 ≡ m2 and hence the problem is solved. If you drop this specification
unsolved : (({n m : ℕ} -> ℕ) -> ℕ) -> ({m n : ℕ} -> ℕ) -> ℕ
unsolved k f = k f
you'll get unsolved metas back.
The exact problem with your definition is that only the first projections of pairs are mentioned in the RHS of _≈_, so Agda doesn't know how to unify the second projections. Here is a workaround:
record Sing {α} {A : Set α} (x : A) : Set where
module Test where
_≈_ : Rel (ℕ × ℕ) _
(a₁ , b₁) ≈ (a₂ , b₂) = a₁ ≡ a₂ × Sing (b₁ , b₂)
≈-sym : Symmetric _≈_
≈-sym (refl , _) = (refl , _)
≋-sym : Symmetric (ListRel _≈_)
≋-sym = symmetric ≈-sym
Sing is a dummy record that have only one inhabitant that can be inferred automatically. But Sing allows to mention b₁ and b₂ in the RHS of _≈_ in an inference-friendly way, which makes those metas in ≋-sym solvable.
Though, it seems that (a₁ , b₁) ≈ (a₂ , b₂) = a₁ ≡ a₂ × Sing b₁ already gives Agda enough hints how to solve metas in ≋-sym.
You can also define a pattern synonym to make the code slightly nicer:
pattern refl₁ = (refl , _)
≈-sym : Symmetric _≈_
≈-sym refl₁ = refl₁