Non-total functions are treated as constants at the type level?

In Type-Driven Development with Idris, ch 6, he says

Type-level functions exist at compile time only ...

Only functions that are total will be evaluated at the type level. A function that isn't total may not terminate, or may not cover all possible inputs. Therefore, to ensure that type-checking itself terminates, functions that are not total are treated as constants at the type level, and don't evaluate further.

I'm having difficulty understanding what the second bullet point means.

How could the type checker claim the code type checks if there's a function that isn't total in its signature? Wouldn't there by definition be some inputs for which the type isn't defined?
When he says constant, does he mean in the same sense as in the docs, like
```
one: Nat
one = 1
```
is a constant? If so, how could that enable the type checker to complete its job?
If a type-level function exists at compile time only, does it ever get evaluated if it's not total? If not, what purpose does it serve?

Solution

Partial type-level functions are treated as constants in the Skolem sense: invocations of a partial function f remain f with no further meaning.

Let's see an example. Here f is a partial predecessor function:

f : Nat -> Nat
f (S x) = x

If we then try to use it in a type, it will not reduce, even though f 3 would reduce to 2:

bad : f 3 = 2
bad = Refl

When checking right hand side of bad with expected type f 3 = 2

Type mismatch between 2 = 2 (Type of Refl) and f 3 = 2 (Expected type)

So f is an atomic constant here, standing only for itself. Of course, because it does stand for itself, the following still typechecks:

good : f 3 = f 3
good = Refl