Le ``size-change principle'' (SCP) est un algorithme simple donnant un test partiel de terminaison qui s'adapte très bien aux langages fonctionnels où les fonctions sont définies de manière récursive par pattern-matching. En présence de constructeurs paresseux, le SCP donne également un test (partiel) de productivité : c'est sur ce principe que les tests (terminaison + productivité) de PML et Agda reposent. Malheureusement, en présence de type coinductifs, certaines définitions récursives bien typées terminent (i.e. sont productives) mais sont incorrectes et rendent Agda/PML inconsistants. En utilisant les travaux de L. Santocanale sur les preuves circulaires et les jeux de parité, je montrerais comment utiliser le SCP pour implanter un test partiel de totalité des définitions récursives qui généralise le test de terminaison/productivité, et garantie qu'une définition est correcte vis à vis de son type.