Strict positivity constraints for inductive behave differently on a type alias

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

abbrev Alias (α : Type) := Option α

inductive I1 : Type where
| mk : Option I1 → I1

/-- error: (kernel) arg #1 of I2.mk' contains a non valid occurrence of the datatypes being declared -/
#guard_msgs in
inductive I2 : Type where
| mk : Alias I2 → I2

in this example Alias and Option should have identical effect when being used in inductive definition. But the second one failed.

The alias appears to omit the fact that X in Option X is in a positive position, and I haven't find a mechanism to make that property propagating to alias or other declarations

Context

N/A, example is self-contained

Steps to Reproduce

1. compile the code example without comment

Expected behavior: should compile cleanly

Actual behavior: (kernel) arg #1 of I2.mk' contains a non valid occurrence of the datatypes being declared

Versions

4.29.1

Additional Information

N/A

Impact

Start with the self-contained Alias, I1, and I2 reproduction in the issue and compile it against Lean nightly. Investigate how strict positivity is checked for inductive declarations through type aliases; done means the I2 declaration compiles with the same behavior as the direct Option case.