[Agda] Bug?

[Benja Fallenstein]

Hi all,

The following code typechecks, but does not typecheck ("Type is not
strictly positive") if I remove the 'mutual' line:

data Cell : Set1 where
  cell : {X : Set} -> X -> Cell

module Foo (Var : Set) (type : Var -> Cell) where
 mutual
  data _==_ {X : Set₁} (x : X) : {Y : Set₁} → Y → Set where
      refl : x == x

  data Type : Set where
    pi : (x : Type) -> ((v : Var) -> type v == cell x -> Type) -> Type

Is this intentional?

Thanks,
- Benja