[Agda] swap in record ambiguity

[Sergei Meshveliani]

I am sorry, I recall the way out:
to set
      \{d} -> maxg'
instead of
      maxg' 



On Fri, 2017-06-30 at 23:25 +0300, Sergei Meshveliani wrote:
> 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'
>