[Agda] Why does Agda think this is not strictly positive?

[Roman]

Hi. Here is the code:

    open import Level

    data Coerce β : ∀ {α} -> Set α -> Set β where
      coerce : ∀ {A} -> A -> Coerce β A

    data D : Set where
      C : Coerce zero D -> D

Agda reports

    D is not strictly positive, because it occurs
    in the third argument to Coerce
    in the type of the constructor C
    in the definition of D.

Is Agda correct that D is not strictly positive? Is there something I
can do to make positivity check pass?