[Agda] not strictly positive?! I don't believe it!

[David Leduc]

--According to the type checker, the T below is not strictly positive.
--But I don't believe it.
--Is it a bug?
--If not, can I force Agda to accept this definition anyway?

module test where

open import Coinduction

data unit : Set where
  * : unit

mutual
  data T : Set1 where
    intro : (t : ∞ T) -> [ ♭ t ] -> T

  [_] : T -> Set
  [ intro _ _ ] = unit