[Agda] Problem with coinduction and positivity checker

[Darin Morrison]

Hi All,

I'm working on a constructive domain theory module where I need a
formalization of chains and ωchains but I'm having some problems with
the positivity checker.

Here is a snippet of the code I am using:

-- Chains

mutual
  data Chain : ℕ → Set where
    []    : Chain 0
    _∷_,_ : ∀ {n} (x : carrier) (xs : Chain n) (p : x ≼ xs) → Chain (suc n)

  _≼_ : ∀ {n} → carrier → Chain n → Set
  _ ≼ []           = ⊤
  x ≼ (x′ ∷ _ , _) = x ≤ x′

head : ∀ {n} → Chain (suc n) → carrier
head (x ∷ _ , _) = x

-- ωChains

mutual
  data ωChain : Set where
    _∷_,_ : ∀ (x : carrier) (xω : ∞ ωChain) (p : x ≼ xω) → ωChain

  head : ωChain → carrier
  head (x ∷ _ , _) = x

  _≼_ : carrier → ∞ ωChain → Set
  x ≼ xω = x ≤ head (♭ xω)

The above encoding of Chains works great.  However, Agda complains
that ωChain is not strictly positive because of (xω : ∞ ωChain).  Note
that I am using the Coinduction module described by Nils in a previous
post.

If I change the definition of ωChain to the following, the positivity
checker no longer complains:

mutual
  codata ωChain : Set where
    _∷_,_ : ∀ (x : carrier) (xω : ωChain) (p : x ≼ xω) → ωChain

  head : ωChain → carrier
  head (x ∷ _ , _) = x

  _≼_ : carrier → ωChain → Set
  x ≼ xω = x ≤ head xω

But this formulation is harder to work with for reasons discussed in
several recent posts on codata.

I'd rather not have to turn off the positivity checker.  Is there any
way to get around this?  Perhaps the positivity checker should be
modified not to complain in cases like this?

-- 
Darin