fix: missing check at kernel inductive declaration

This PR fixes a kernel bug where a nested inductive datatype
whose parametric arguments are ill typed could be accepted.

When eliminating a nested occurrence `I Ds is`, the parametric
arguments `Ds` are dropped from the generated auxiliary types,
so they used to escape type checking. We now type check them
once the inductive types being declared are available.

Closes #14576