[Agda] Guardedness-preserving type constructors

[Nils Anders Danielsson]

Hi,

One of the new features implemented during AIM XI was
"guardedness-preserving type constructors". Thorsten wanted to be able
to write ΠΣ code in Agda; in particular, he wanted to be able to define
types recursively. Now he can.

If the new flag --guardedness-preserving-type-constructors is used, then
type constructors are treated as inductive constructors when we check
productivity (but only in parameter positions, and only if the
parameters are used strictly positively or not at all). This makes
examples such as the following possible:

  data Rec (A : ∞ Set) : Set where
    fold : ♭ A → Rec A

  ℕ : Set
  ℕ = ⊤ ⊎ Rec (♯ ℕ)

  zero : ℕ
  zero = inj₁ _

  suc : ℕ → ℕ
  suc n = inj₂ (fold n)

  ℕ-rec : (P : ℕ → Set) →
          P zero →
          (∀ n → P n → P (suc n)) →
          ∀ n → P n
  ℕ-rec P z s (inj₁ _)        = z
  ℕ-rec P z s (inj₂ (fold n)) = s n (ℕ-rec P z s n)

Note that this feature is experimental. We do not know if it leads to
inconsistencies. Furthermore it seems to be rather strong. We can for
instance encode the following universe without using
induction-recursion:

  data Label : Set where
    ′0 ′1 ′2 ′σ ′π ′w : Label

  mutual

    U : Set
    U = ∃ U′

    U′ : Label → Set
    U′ ′0 = ⊤
    U′ ′1 = ⊤
    U′ ′2 = ⊤
    U′ ′σ = Rec (♯ ∃ λ (a : U) → El a → U)
    U′ ′π = Rec (♯ ∃ λ (a : U) → El a → U)
    U′ ′w = Rec (♯ ∃ λ (a : U) → El a → U)

    El : U → Set
    El (′0 , _)            = ⊥
    El (′1 , _)            = ⊤
    El (′2 , _)            = Bool
    El (′σ , fold (a , b)) = ∃ λ (x : El a) → El (b x)
    El (′π , fold (a , b)) = (x : El a) → El (b x)
    El (′w , fold (a , b)) = W (El a) (λ (x : El a) → El (b x))

--
/NAD