Issue3989.agda:6,11-38
Shadowing in telescope, repeated variable names: a
when scope checking the declaration
  data _~_ {a a : Level}{A : Set a}(a : A) : A → Set
Issue3989.agda:16,24-40
Shadowing in telescope, repeated variable names: A
when scope checking ∀ {A : Set a} A ~ A → Set → Set
Issue3989.agda:40,12-15
Shadowing in telescope, repeated variable names: x
when scope checking λ x x → x
Issue3989.agda:43,13-16
Shadowing in telescope, repeated variable names: A
when scope checking (A A : Set) → Set
Issue3989.agda:44,13-24
Shadowing in telescope, repeated variable names: A
when scope checking (A : Set) (A : A) → Set

———— All done; warnings encountered ————————————————————————

Issue3989.agda:6,11-38
Shadowing in telescope, repeated variable names: a
when scope checking the declaration
  data _~_ {a a : Level}{A : Set a}(a : A) : A → Set

Issue3989.agda:16,24-40
Shadowing in telescope, repeated variable names: A
when scope checking ∀ {A : Set a} A ~ A → Set → Set

Issue3989.agda:40,12-15
Shadowing in telescope, repeated variable names: x
when scope checking λ x x → x

Issue3989.agda:43,13-16
Shadowing in telescope, repeated variable names: A
when scope checking (A A : Set) → Set

Issue3989.agda:44,13-24
Shadowing in telescope, repeated variable names: A
when scope checking (A : Set) (A : A) → Set
