The Size-Change Principle (SCP) is a simple algorithm giving a partial termination test for recursive definitions. It is particularly well suited for functional languages with inductive types where recursive functions are given by pattern matching (Caml / Coq) or equations (Haskell / Agda).

If term constructors are lazy, the SCP also gives (by duality) a partial productivity test for recursive functions involving coinductive types. This is what is used in Agda.

Unfortunately, when inductive and coinductive types are nested, this test is unsound: there are "well typed" and terminating recursive definitions producing terms in empty types. Such definitions make Agda inconsistant.

By using ideas from L. Santocanale about circular proof and parity games, I'll show how the SCP can be used to check "totality" of recursive definitions to make sure the definition denote actual objects in their type.