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. A variant of this principle is for example used in Agda.

Unfortunately, when inductive and coinductive types are nested, productivity is insufficient. 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.

A prototype has been implemented, and experiments tend to show this principle is quite strong in practice.