positive vs strictly positive occurrence

Stream: lean4

[Asei Inoue]

Please take a look at the following error message:

/-
error: (kernel) arg #1 of 'Bar.mk' has a non positive occurrence of the datatypes being declared
-/
inductive Bar where
  | mk (f : (Bar → Nat) → Nat)

In the constructor of the inductive type Bar, Bar appears in a negative position within a negative position, so I believe it is actually in a positive position. However, the error message states that there is a "non positive occurrence."

I think this error message is not appropriate.

Wouldn't it be better to say that Bar occurs in a way that is not strictly positive instead?

[Mario Carneiro]

note that positivity is not a concept that occurs in CIC or MLTT based systems at all. I think it might appear in system F? The terminology comes from this earlier notion of co-/contra-variance based on looking at whether you are left of an arrow, but in MLTT it's not really about variance at all, there are just very limited ways that the type can appear in the constructor's type which bear some surface resemblance to positivity

[Arthur Adjedj]

While I'm not aware of any particular papers that prove this result, Coquand & Paulin did believe in their first presentations of inductive types that (not only strictly) positive inductive types would be compatible with predicative type theories such as MLTT.