Agda is ruling out definitions like
data Bad : Set where
bad : (Bad → Bad) → Bad
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
badZ : Bad? zero
badS : ∀ {n} → (Bad? n → Bad? n) → Bad? (suc n)
telling me that:
Bad? is not strictly positive, because it occurs
to the left of an arrow
in the type of the constructor badS
in the definition of Bad?.
What i know is that i can create valid definition without inductive datatypes:
Bad?′ : ℕ → Set
Bad?′ zero = Unit
Bad?′ (suc n) = (Bad?′ n) → (Bad?′ n)
badZ′ : Bad?′ zero
badZ′ = tt
badS′ : ∀ {n} → (Bad?′ n → Bad?′ n) → Bad?′ (suc n)
badS′ x = x
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?
Bad?'
at first. I don't think that type leads to inconsistencies, after allBad?'
is accepted. I guess it can not be accepted since Agda does not know how to generate a proper induction principle for it. InBad?'
no induction principle is being introduced, on the type definition. The induction principle forℕ
seem to suffice to prove properties onBad?'
. $\endgroup$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 forBad?
would be). In your case, the type is "stratified" using a natural index, so probably induction on naturals is already enough to prove properties onBad?
-- without a new induction principle. $\endgroup$