Debugging inside the typechecker knot