Positivity Checking

Note

This is a stub.

Occurrence analysis

By default Agda analyses how functions use their arguments. For instance, Agda can tell that D in the following code is strictly positive, because Vec uses its Type argument in a strictly positive way:

data _×_ (A B : Type) : Type where
  _,_ : A → B → A × B

Vec : Type → Nat → Type
Vec A zero    = ⊤
Vec A (suc n) = A × Vec A n

data D : Type where
  c : ∀ n → Vec D n → D

However, this analysis can be slow, especially for big mutual blocks. It can be turned off with the --no-occurrence-analysis flag.

The analysis is also used to detect unused function arguments. For instance, Agda by default notices that the last argument of F in the following code is unused, and accepts the use of reflexivity:

F : Bool → Type → Type
F true  _ = Bool
F false _ = ⊤

_ : {b : Bool} → F b Bool ≡ F b ⊤
_ = refl

The NO_POSITIVITY_CHECK pragma

The pragma switches off the positivity checker for data/record definitions and mutual blocks. This pragma was added in Agda 2.5.1

The pragma must precede a data/record definition or a mutual block. The pragma cannot be used in --safe mode.

Examples:

  • Skipping a single data definition:

    {-# NO_POSITIVITY_CHECK #-}
data D : Type where
  lam : (D → D) → D

  • Skipping a single record definition:

    {-# NO_POSITIVITY_CHECK #-}
record U : Type where
  inductive
  field ap : U → U

  • Skipping an old-style mutual block. Somewhere within a mutual block before a data/record definition:

    mutual
  data D : Type where
    lam : (D → D) → D

  {-# NO_POSITIVITY_CHECK #-}
  record U : Type where
    inductive
    field ap : U → U

  • Skipping an old-style mutual block. Before the mutual keyword:

    {-# NO_POSITIVITY_CHECK #-}
mutual
  data D : Type where
    lam : (D → D) → D

  record U : Type where
    inductive
    field ap : U → U

  • Skipping a new-style mutual block. Anywhere before the declaration or the definition of a data/record in the block:

    record U : Type
data D   : Type

record U where
  inductive
  field ap : U → U

{-# NO_POSITIVITY_CHECK #-}
data D where
  lam : (D → D) → D

POLARITY pragmas

Polarity pragmas can be attached to postulates. The polarities express how the postulate’s arguments are used. The following polarities are available:

  • _: Unused.

  • ++: Strictly positive.

  • +: Positive.

  • -: Negative.

  • *: Unknown/mixed.

Polarity pragmas have the form {-# POLARITY name <zero or more polarities> #-}, and can be given wherever fixity declarations can be given. The listed polarities apply to the given postulate’s arguments (explicit/implicit/instance), from left to right. Polarities currently cannot be given for module parameters. If the postulate takes n arguments (excluding module parameters), then the number of polarities given must be between 0 and n (inclusive).

Polarity pragmas make it possible to use postulated type formers in recursive types in the following way:

postulate
  ∥_∥ : Type → Type

{-# POLARITY ∥_∥ ++ #-}

data D : Type where
  c : ∥ D ∥ → D

Note that one can use postulates that may seem benign, together with polarity pragmas, to prove that the empty type is inhabited:

postulate
  _⇒_    : Type → Type → Type
  lambda : {A B : Type} → (A → B) → A ⇒ B
  apply  : {A B : Type} → A ⇒ B → A → B

{-# POLARITY _⇒_ ++ #-}

data ⊥ : Type where

data D : Type where
  c : D ⇒ ⊥ → D

not-inhabited : D → ⊥
not-inhabited (c f) = apply f (c f)

d : D
d = c (lambda not-inhabited)

bad : ⊥
bad = not-inhabited d

Polarity pragmas are not allowed in safe mode.