# Strict Positivity of Indexed Datatype in Agda

Agda is ruling out definitions like

data Bad : Set where


Because "Non strictly-positive declarations are rejected because one can write a non-terminating function using them." (as one may read in Agda wiki). I know also that disabling strict positivity checking allows constructing inhabitant of empty type.

But Agda also complains about definition like this:

  data Bad? : ℕ → Set where


telling me that:

Bad? is not strictly positive, because it occurs
to the left of an arrow
in the type of the constructor badS


What i know is that i can create valid definition without inductive datatypes:

  Bad?′ : ℕ → Set



My question is:

Can "Bad?" datatype lead to similar inconsistencies, and this is the reason why it is rejected by Agda?

Or is it the case that positivity checking in Agda is too "cautious", and can't figure out that indexing is making it strict positive?

• Sorry, I did not see your Bad?' at first. I don't think that type leads to inconsistencies, after all Bad?' is accepted. I guess it can not be accepted since Agda does not know how to generate a proper induction principle for it. In Bad?' no induction principle is being introduced, on the type definition. The induction principle for ℕ seem to suffice to prove properties on Bad?'.
– chi
May 13, 2019 at 16:30
• @chi Could you elaborate more on your comment? I would be happy to accept it as good answer if you can provide some explanation about impossibility of generating proper induction principle.
– MJG
Aug 21, 2019 at 3:19
• I don't know much more to write a proper answer. Agda, like similar languages, generates the induction principle following a given algorithm, which only handles strictly positive types. While your Bad? type could be accepted without leading to an inconsistency, the algorithm can not generate an induction principle (and I'm unsure about what an induction principle for Bad? would be). In your case, the type is "stratified" using a natural index, so probably induction on naturals is already enough to prove properties on Bad? -- without a new induction principle.
– chi
Aug 21, 2019 at 7:33