I thank Jean-Jacques Lévy and James Leifer for their comments. I also thank Jacques Garrigue, whose work on the typing of polymorphic variant Garrigue [2004] makes use of exhaustiveness information. Jacques’ comments on my code and ideas encouraged me to write this paper.