The proof is fine, only the compiler needs few more hints. Implicit arguements are filled in by unification and while it can do some cool stuff, sometimes you have to help it out and push it in the right direction.
Let's take a look at the definition of Preserves₂
:
_Preserves₂_⟶_⟶_ :
∀ {a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c} →
(A → B → C) → Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → Set _
_+_ Preserves₂ P ⟶ Q ⟶ R =
∀ {x y u v} → P x y → Q u v → R (x + u) (y + v)
If we specialize it to _+_ = _∪_
and P, Q, R = _≈_
, we get:
∀ {x y u v} → x ≈ y → u ≈ v → (x ∪ u) ≈ (y ∪ v)
There are four implicit arguments, let's fill in some of them and watch what happens:
bibble = ∙-cong
{x = x ∪ tree (Indexed.leaf l<u)}
(comm x (tree (Indexed.leaf l<u)))
refl
Nope, it's still yellow. Apparently, knowing only x
is not enough. Now y
:
bibble = ∙-cong
{x = x ∪ tree (Indexed.leaf l<u)}
{y = tree (Indexed.leaf l<u) ∪ x}
(comm x (tree (Indexed.leaf l<u)))
refl
And that's it! Giving x
and y
explicitly was enough for the compiler to figure out u
and v
.
Also, I wrote something about implicit arguments in this answer, you might want to check that out.
Anyways, the "unsolved meta" error messages are indeed a bit scary (and usually not very helpful), what I usually do is something like this:
bibble = ∙-cong
{?} {?} {?} {?}
(comm x (tree (Indexed.leaf l<u)))
refl
That is, I just prepare holes for all (or the most relevant) implicit arguments and fill them one by one until the compiler is happy.