[Agda] A question on Setoid in the standard library

[David Leduc]

I do not understand why the following code results in a parsing error.
Please someone, help me.

{-# OPTIONS --universe-polymorphism #-}

module test where

open import Level
open import Relation.Binary
open import Data.Bool

f : (c l : Level)(A : DecSetoid c l) ->
    DecSetoid.Carrier A -> DecSetoid.Carrier A -> Bool
f c l A X Y with DecSetoid._≟_ A X Y
... | yes _ = true
... | no _ = true