[Agda] Why does this pass the positivity checker?

[Neel Krishnaswami]

Hello,

I wrote the following bit of code, to experiment with generic programming.
>
> data _×_ (A B : Set) : Set where
>    _,_ : A → B → A × B
>
>
> data _+_ (A B : Set) : Set where
>   inl : A → A + B
>   inr : B → A + B
>
>
> data Poly : Set₁ where
>   K : Set → Poly
>   _⊗_ : Poly → Poly → Poly
>   _⊕_ : Poly → Poly → Poly
>   Id : Poly
>
> [_] : Poly → Set → Set
> [ K X ] A = X
> [ p ⊗ q ] A = [ p ] A × [ q ] A
> [ p ⊕ q ] A = [ p ] A + [ q ] A
> [ Id ] A = A
>
> data μ (F : Poly) : Set where
>   into : [ F ] (μ F) → μ F
and Agda accepted the declaration of μ. I was surprised by this -- did 
Agda look at the body of the definition of [_] to decide that every  
recursive occurrence was  positive? If so, how deeply does it look?

-- 
Neel Krishnaswami
nk480 at cl.cam.ac.uk