Apparently, there is some feature in Agda called positivity checking which can apparently keep the system sound even if type-in-type is enabled.
I am curious to know what this is about, but the Agda Manual fails to answer the question, and only explains how to turn it off.
At a lunch table I overheard that this is about polarity in type theory, but that is about all I know. I am failing to find anything online which explains this concept and why it is useful in maintaining soundness. Any intelligible explanation would be appreciated.
First, I have to clear up a misconception: positivity checking does not guarantee soundness when type-in-type is enabled. Data types must thus satisfy both the positivity check and universe check to preserve soundness.
Now, to explain positivity checking, let's first look at a counterexample when we wouldn't have positivity checking:
-- the empty type
data ⊥ : Set where
-- a non-positive type
data Bad : Set where
bad : (Bad → ⊥) → Bad
Suppose this datatype was allowed, then you could easily prove ⊥:
bad-is-false : Bad → ⊥
bad-is-false (bad f) = f (bad f)
bad-is-true : Bad
bad-is-true = bad bad-is-false
boom : ⊥
boom = bad-is-false bad-is-true
Under the Curry-Howard correspondence, the definition of Bad says: Bad is true if and only if Bad is false. So it is not surprising that it leads to inconsistencies.
Positivity checking rules out datatypes such as Bad. In general, the (strict) positivity criterion says that each constructor c of a datatype D should have a type of the form
c : (x1 : A1)(x2 : A2) ... (xn : An) → D xs
where the type Ai of each argument is either non-recursive (i.e. it doesn't refer to D) or of the form (y1 : B1)(y2 : B2) ... (ym : Bm) → D ys where each Bj doesn't refer to D.
Bad doesn't satisfy this criterion because the argument of the constructor bad has type Bad → ⊥, which is neither of the two allowed forms.
The name 'positivity checking' comes (as many things in type theory do) from category theory, specifically the notion of a positive endofunctor. Each definition of a datatype that satisfies the positivity criterion is such a positive endofunctor on the category of types. This means we can construct the initial algebra of that endofunctor, which can be used to model the datatype when constructing a model of type theory (which is used to prove soundness).