[Agda] problem with proj1

[Michel Levy]

I have a problem with the two lines below in the context
open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)

test0 : 1 ≡ proj₁ ⟨ 1 , 2 ⟩
test0 = refl

———— Errors ————————————————————————————————————————————————
Failed to solve the following constraints:
  _50 := 2 [blocked on problem 99]
  [99] ℕ =< _B_49 1 : Set

The term proj₁ ⟨ 1 , 2 ⟩ appears in _yellow_ and its value calculated by
C-c C-n is 1


Still more strange, when I rename proj₁ in proj1 with

proj1 : {A B : Set} -> A × B -> A
proj1 ⟨ x , y ⟩ = x

I have without error

test0' : 1 ≡ proj1 ⟨ 1 , 2 ⟩
test0' = refl

-- 
courriel : michel.levy.imag at free.fr
mobile : 06 59 13 42 53
web : michel.levy.imag.free.fr
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200418/0e597847/attachment.html>