Agda unification failure

open import Agda.Builtin.Unit
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

record Add (A : Set) : Set where
  field
    add : A → A → A
open Add {{...}}

instance
  instAddNat : Add Nat
  instAddNat .add = _+_

instance
  instAddUnit : Add ⊤
  instAddUnit .add _ _ = _

test : (x y : Nat) → add x y ≡ add _ _
test x y = refl

{-
———— Errors ————————————————————————————————————————————————
Failed to solve the following constraints:
  _14 (x = x) (y = y) + _15 (x = x) (y = y) = x + y : Nat
    (blocked on _14)
-}