The breakpointJump functions never show up in the code that the typechecker sees, as they are inserted by the desugarer later.