[Agda] Guardedness-preserving type constructors

[Thorsten Altenkirch]

On 5 Apr 2010, at 13:48, Nils Anders Danielsson wrote:
> 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

The example which motivated my suggestion was a Universe of concrete  
datatypes with decidable equality:

mutual

data Data : Set where
  empty : Data
  maybe : ∞ Data -> Data
  sigma : (A : Data) → (El A → Data) -> Data

El : Data → Set
El empty = ⊥
El (maybe A) = Rec (♯ Maybe (El (♭ A)))
El (sigma A B) = Σ (El A) (λ a → El (B a))

Previously, I believe, it was impossible to define this universe due  
to the presence of infinite types guarded by maybe.

I also have defined

eq : ∀ {A} → El A → El A → Bool

together with

rfl : ∀ {A} → (a : El A) → T (eq a a)
sbst : ∀ {A}(B : El A → Set) → (a a' : El A) → T (eq a a') →  
B a → B a'

but alas the $%^$@! termination checker isn't happy about my code (I  
know how to fix this but I think it is rather the checker which needs  
fixing).

Cheers,
Thorsten