[Agda] swap in record ambiguity

[Sergei Meshveliani]

Can anybody tell, please, 
how to resolve the following code:

------------------------------------------------------------------
record GCD (a b : ℕ) : Set
    where
    constructor gcd′
    field  proper   : ℕ         -- proper gcd          
           divides₁ : proper ∣ a
           divides₂ : proper ∣ b
           greatest : ∀ {d} → (d ∣ a) → (d ∣ b) → (d ∣ proper)

swapGCD :  (a b : ℕ) → GCD a b → GCD b a
swapGCD a b (gcd′ g g∣a g∣b maxg) =  gcd′ g g∣b g∣a maxg'  
                        where
                        maxg' : {d : ℕ} → (d ∣ b) → (d ∣ a) → (d ∣ g)
                        maxg' {d} d∣b d∣a =  maxg {d} d∣a d∣b
------------------------------------------------------------------


Agada 2.6.0-207bde6  reports

-------------------
Failed to solve the following constraints:
  _974 := (λ a b g g∣a g∣b maxg {.d} → maxg')
    [blocked on problem 2107]
  [2107, 2129, 2132] (_d_973 a b g g∣a g∣b maxg * x) = (.d * x) : ℕ
  [2107, 2117, 2121, 2124] (.d * x) = (_d_973 a b g g∣a g∣b maxg * x)
                             : ℕ
  [2107, 2108, 2112, 2115] (.d * x) = (_d_973 a b g g∣a g∣b maxg * x)
                             : ℕ
Unsolved metas at the following locations:
  /home/mechvel/doconA/2.00/source/Int/Nat1.agda:481,53-58
-----------------

where  481  is the line of  
                        swapGCD ... = gcd′ g g∣b g∣a maxg'


Thanks,

------
Sergei