Secondarily, perhaps totality isn't the right term; maybe we need a
word for "good enough to satisfy the checker", where the checker is
generous in letting us be sloppy regarding silly values.
In searching for names for "total enough to satisfy the type checker",
it briefly occurred to me to make an appeal to the notion from real
analysis of "almost everwhere" (often written a.e., or Remi might have
seen this as p.p.):
https://en.wikipedia.org/wiki/Almost_everywhere
Though, the analogy isn't quite right because a.e. is not picky about
what measure-zero set the property does not hold. Here, we want to
outline a _specific_ set on which the property is allowed to not hold.
We toyed with "optimistically total", which is appealing because the
cases that are covered are the ones we hope will never show up (hence
the optimism.)
Another variant of totality is "effectively total". We've used the
phrase "effectively final" to mean "you didn't say final, but I figured
it out anyway." The same could apply to things like covering all the
subtypes of a sealed type. It is a more friendly name than o.t., but it
may not be as obvious that there's a strange-shaped remainder.
There might also be phrases that don't include the t-word, but I think a
modifier on the t-word is probably better. What I like about a modifier
is that true totality is a degenerate case of {almost, effectively,
optimistically}-total.
