I hope you can reproduce it with this self-contained code:
open import Data.Nat using (ℕ; zero; suc)
infixr 5 _∷_
data Vec (X : Set) : ℕ → Set where
[] : Vec X zero
_∷_ : ∀ {n} (x : X) (xs : Vec X n) → Vec X (suc n)
vapp : ∀ {n S T} → Vec (S → T) n → Vec S n → Vec T n
vapp [] [] = []
vapp (f ∷ fs) (x ∷ xs) = f x ∷ vapp fs xs
open import Data.String
fun : ℕ → String
fun 1 = "a"
fun 2 = "b"
fun 3 = "c"
fun _ = "not a, b or c"
ex₁ : Vec String 3
ex₁ = "c" ∷ "b" ∷ "a" ∷ []
ex₂ : Vec (ℕ → String) 3
ex₂ = fun ∷ fun ∷ fun ∷ []
open import Agda.Builtin.Sigma using (_,_)
open import Data.Product using (_×_)
ex₃ : Vec (ℕ → String → ℕ × String) 3
ex₃ = _,_ ∷ _,_ ∷ _,_ ∷ []
open import Agda.Builtin.Equality
_ : vapp ex₃ ex₀ ex₁ ≡ ex₀ , ex₁
_ = refl
Agda throws an error because of the same mixfix priority of the operators, and the problem is that when clicking on the links, they show empty files. The URL is built somehow with parentheses and relative to the current path instead of absolute:
Could not parse the application vapp ex₃ ex₀ ex₁ ≡ ex₀ , ex₁
Operators used in the grammar:
, (infixr operator, level 4) [_,_ 🔗 (.../Agda-2.6.1/lib/prim/Agda/Builtin/Sigma.agda:9,15-18)]
≡ (infix operator, level 4) [_≡_ 🔗 (.../Agda-2.6.1/lib/prim/Agda/Builtin/Equality.agda:7,6-9)]
I hope you can reproduce it with this self-contained code:
Agda throws an error because of the same mixfix priority of the operators, and the problem is that when clicking on the links, they show empty files. The URL is built somehow with parentheses and relative to the current path instead of absolute: