`check_positivity` throws for `EStateM`, `IO`, etc though should not

Prerequisites

It doesnt throw for expanded version of IO or EStateM
But it does throw for non-expanded version of IO or EStateM

-- `check_positivity` throws for `EStateM` and `IO`, etc though should not

namespace UsingFunction

inductive Wrapper (a : Type 0) : Type 0
  | mk : (IO.RealWorld → EStateM.Result PEmpty IO.RealWorld a) → Wrapper a

inductive Proxy (r : Type 0) : Type 0 -- This is ok
  | M       : Wrapper (Proxy r) -> Proxy r
  | Pure    : r → Proxy r

inductive ProxyNoWrapper (r : Type 0) : Type 0 -- This is ok
  | M2       : (IO.RealWorld → EStateM.Result PEmpty IO.RealWorld (ProxyNoWrapper r)) -> ProxyNoWrapper r
  | Pure2    : r → ProxyNoWrapper r

end UsingFunction

namespace UsingEStateM

inductive Wrapper (a : Type 0) : Type 0
  | mk : (EStateM Empty IO.RealWorld a) → Wrapper a
-- structure Wrapper (a : Type 0) : Type 0 where -- throws for this too
--   myfield : EStateM Empty IO.RealWorld a 
-- def Wrapper (a : Type 0) : Type 0 := EStateM Empty IO.RealWorld a -- or this
-- abbrev Wrapper (a : Type 0) : Type 0 := EStateM Empty IO.RealWorld a -- or this

-- Actual: throws with
--    (kernel) arg #2 of '_nested.UsingEStateM.Wrapper_1.mk' contains a non valid occurrence of the datatypes being declared
-- Expected: should not throw since `a` is in positive position
inductive Proxy (r : Type 0) : Type 0
  | M       : Wrapper (Proxy r) -> Proxy r
  | Pure    : r → Proxy r

-- Actual: throws with
--    (kernel) arg #2 of 'UsingEStateM.ProxyNoWrapper.M2' contains a non valid occurrence of the datatypes being declared
-- Expected: should not throw since `a` is in positive position
inductive ProxyNoWrapper (r : Type 0) : Type 0
  | M2       : (EStateM Empty IO.RealWorld (ProxyNoWrapper r)) -> ProxyNoWrapper r
  | Pure2    : r → ProxyNoWrapper r

end UsingEStateM

namespace UsingBaseIO

inductive Wrapper (a : Type 0) : Type 0
  | mk : (BaseIO a) → Wrapper a

-- Actual: throws with
--    (kernel) arg #2 of '_nested.UsingBaseIO.Wrapper_1.mk' contains a non valid occurrence of the datatypes being declared
-- Expected: should not throw since `a` is in positive position
inductive Proxy (r : Type 0) : Type 0
  | M       : Wrapper (Proxy r) -> Proxy r
  | Pure    : r → Proxy r

-- Actual: throws with
--    (kernel) arg #2 of 'UsingBaseIO.ProxyNoWrapper.M2' contains a non valid occurrence of the datatypes being declared
-- Expected: should not throw since `a` is in positive position
inductive ProxyNoWrapper (r : Type 0) : Type 0
  | M2       : (BaseIO (ProxyNoWrapper r)) -> ProxyNoWrapper r
  | Pure2    : r → ProxyNoWrapper r

end UsingBaseIO

namespace UsingEIO

inductive Wrapper (a : Type 0) : Type 0
  | mk : (EIO Unit a) → Wrapper a

-- Actual: throws with
--    (kernel) arg #2 of '_nested.UsingEIO.Wrapper_1.mk' contains a non valid occurrence of the datatypes being declared
-- Expected: should not throw since `a` is in positive position
inductive Proxy (r : Type 0) : Type 0
  | M       : Wrapper (Proxy r) -> Proxy r
  | Pure    : r → Proxy r

-- Actual: throws with
--    (kernel) arg #2 of 'UsingEIO.ProxyNoWrapper.M2' contains a non valid occurrence of the datatypes being declared
-- Expected: should not throw since `a` is in positive position
inductive ProxyNoWrapper (r : Type 0) : Type 0
  | M2       : (EIO Unit (ProxyNoWrapper r)) -> ProxyNoWrapper r
  | Pure2    : r → ProxyNoWrapper r

end UsingEIO

namespace UsingIO

inductive Wrapper (a : Type 0) : Type 0
  | mk : (IO a) → Wrapper a

-- Actual: throws with
--    (kernel) arg #2 of '_nested.UsingIO.Wrapper_1.mk' contains a non valid occurrence of the datatypes being declared
-- Expected: should not throw since `a` is in positive position
inductive Proxy (r : Type 0) : Type 0
  | M       : Wrapper (Proxy r) -> Proxy r
  | Pure    : r → Proxy r

-- Actual: throws with
--    (kernel) arg #2 of 'UsingIO.ProxyNoWrapper.M2' contains a non valid occurrence of the datatypes being declared
-- Expected: should not throw since `a` is in positive position
inductive ProxyNoWrapper (r : Type 0) : Type 0
  | M2       : (IO (ProxyNoWrapper r)) -> ProxyNoWrapper r
  | Pure2    : r → ProxyNoWrapper r

end UsingIO

Reproduce the check_positivity failures using the UsingEStateM, UsingBaseIO, UsingEIO, and UsingIO examples in the issue, comparing them with the expanded forms that succeed. Trace the positivity and inductive-occurrence handling for these types; done means the shown non-expanded declarations are accepted without the reported kernel errors.