[Agda] How safe is Type:Type?

[Stefan Monnier]

> Indeed in Coq we statically compute the possible recursive calls at the
> definition of the inductive type, independently of its use. In this case
> Agda is "fooled" because it thinks that [f] is a valid subterm (of type
> [D]) of [x : D], while Coq simply doesn't categorize [f] as a subterm when
> checking the guardedness/structural recursion criterion.

I think Agda's termination checker is based on the notion of size
(where a function's size is taken extensionally, so any output of the
function is of course smaller than the function itself) rather
than the notion of induction.

In the case of impredicativity this breaks down, since now our
impredicative identity function can take itself as argument and return
itself as value, so its extensional representation is not just infinite
(as is common) but circular.


        Stefan