[Agda] Positivity check

[Andrew Cave]

Hi all,

The following fails the positivity check, but it seems to me that it could
be allowed to pass without introducing inconsistency. Thoughts?

Regards,
Andrew

open import Data.Nat
open import Data.Fin

data functor (n : ℕ) : Set where
 ▹ : (X : Fin n) -> functor n
 μ : (F : functor (suc n)) -> functor n
 _⇒_ : (A : functor zero) (F : functor n) -> functor n

env : ℕ -> Set₁
env n = ∀ (X : Fin n) -> Set

extend : ∀ {n} -> env n -> Set -> env (suc n)
extend ρ A zero = A
extend ρ A (suc i) = ρ i

mutual
 data μ' {n} (F : functor (suc n)) (ρ : env n) : Set where
  ⟨_⟩ : ⟦ F ⟧ (extend ρ (μ' F ρ)) -> μ' F ρ

 ⟦_⟧ : ∀ {n} -> functor n -> (ρ : env n) -> Set
 ⟦ ▹ X ⟧ ρ = ρ X
 ⟦ μ F ⟧ ρ = μ' F ρ
 ⟦ A ⇒ F ⟧ ρ = ⟦ A ⟧ (λ ()) → ⟦ F ⟧ ρ
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121113/cd7024c5/attachment.html