[Agda] How safe is Type:Type?

[Stefan Monnier]

>   data D : Set where
>     c : (f : (A : Set) → A → A) → D
>   -- Structural recursion with  f args < c f  is no longer valid.
>   -- We should not be able to demonstrated that D is empty.

Coq lets us define this datatype (in Prop).

>   empty : D → ⊥
>   empty (c f) = empty (f D (c f))

But rejects this definition:

    Error:
    Recursive definition of empty is ill-formed.
    In environment
    empty : D -> False
    x : D
    f : forall A : Prop, A -> A
    Recursive call to empty has principal argument equal to 
    "f D (c f)" instead of a subterm of "x".
    Recursive definition is:
    "fun x : D => match x with
                  | c f => empty (f D (c f))
                  end".

Not sure exactly what is the rule they use to decide whether a recursive
call is considered as valid structural recursion.  I suspect it depends
on the notion of a "large inductive type" or something along these lines.


        Stefan