How many times does a type function run, can you prove?

Question

People say a dependent type language is slow in type checking so I think it is slow in running type functions.

Use the classic example on https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html

isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat

mkSingle : (x : Bool) -> isSingleton x
mkSingle True = 0
mkSingle False = []

and run

mkSingle True

How many times does isSingleton run?

In a traditional language, I can print to console. But Idris doesn't appear to execute the IO machinery when type checking. I can increase a global counter or set a breakpoint at the beginning of isSingleton and count how many times the breakpoint is hit.

Can I do something in idris 2 to easily convince people, "hey, during the time isSingleton has been called x times"?

Update

f : (x : Bool) -> isSingleton x -> Nat
f True n = 0
f False ls = 1

I set the multiplicity of isSingleton to 0, add the above code to my file and run

Main> f True []
Error: When unifying:
    List ?a
and:
    isSingleton True
Mismatch between: List ?a and Nat.

(Interactive):1:8--1:10
 1 | f True []
            ^^

idris knows the second argument should be Nat, which is provided by isSingleton, right? But isSingleton is erased at runtime, how is isSingleton called?

Answer 1

Erase isSingleton

0 isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat

then you know it doesn't exist at runtime and is never called. I imagine it's also never called (in this example) if you don't erase it, but by erasing it you can be sure.