Dependent constructor reproted as not strictly positive when in mutual block

[uzytkownik]

Steps to Reproduce

module repro

-- Warning goes away without mutual
mutual
  data Foo : Type -> Type where
    Foo1    : Foo v

  data Bar : {v : Type} -> Nat -> Foo v -> Type where
    Bar1 : Bar n Foo1
    -- This works:
    -- Bar1 : Bar n v

Expected Behavior

Bar should be strictly positive

Observed Behavior

Bar is reported as possibly not strictly positive when mutual keyword is present.

[uzytkownik]

Even simpler:

module repro

-- Warning goes away without mutual
mutual
  data Foo : Type where
    Foo1    : Foo

  data Bar : Nat -> Foo -> Type where
    Bar1 : Bar n Foo1