For me, I use "type error" or "typing error". I would avoid "type disagreement" because it suggests that you actually have types that disagree. But that's not correct; any expression is only meaningful only when it does not have any type error! If there is a type error, it would be more accurate to say that the expression is meaningless!
As for how to make sure students do not make this mistake, in my experience typing errors clearly indicate that the students were not taught proper logical reasoning. I have written before about what I think needs to be taught for students to actually be capable of logical reasoning, and I also think that trying to find a shortcut will be terrible for most students in the long run. 1% of them will somehow figure out how to do logical reasoning on their own, but 99% of them will never be 100% sure of their own reasoning in the absence of a proper deductive system.
Once you have taught a proper deductive system, all typing errors will completely and permanently vanish. Also see below for some remarks about the teaching process specific to definitions.
I also want to elaborate on some of my comments. I said:
Predicates are not objects and actually cannot be objects in some foundational systems. They are meta-objects. To truly understand what defining a predicate means, you need to have a solid grasp of basic FOL (e.g. using a Fitch-style system such as this one), and you need to know the distinction between ∃elim and definitorial expansion for new predicate/function-symbols. If you follow the definitorial expansion rule in that linked system, an example would be "Let Q(k) ≡ ¬∃x∈ℤ ( 2^k+5 = 17·x ), for each k∈ℕ.". This is a complete definition of a (fresh) predicate-symbol "Q" (where ℕ,ℤ,+,·,^ are inbuilt or have been defined). You can also see that if you fastidiously follow the rules in that system, you are forced to think about what every object type is, and will never write the kind of nonsense listed in this question.
I know from experience that the only way to truly impart understanding is to be 100% precise. You must clearly distinguish between predicates and predicate-symbols. Taking my earlier example, "¬∃x∈ℤ ( 2^[1]+5 = 17·x )" (where the "[1]" is a place-holder for the 1st input parameter) is a predicate, whereas the symbol "Q" in "Let Q(k) ≡ ¬∃x∈ℤ ( 2^k+5 = 17·x ), for each k∈ℕ." is a predicate-symbol. Under "Definitorial expansion" in that linked post you can find the deductive rules supporting definitions, plus a link to an explanation of why we want definitions. This motivation tells us that we want to be able to express predicates without having to write it again and again. To support this, we allow defining new predicate-symbols. Make very clear to students this motivation as well as the fact that "Q(E)" can be substituted for the definition of Q with every "[1]" replaced by "E". This is the true meaning of definitions.
Regarding the first point, make sure you never call predicates or predicate-symbols "objects"; neither of them are objects. And avoid talking about their "type", because that would be a meta-type. For your own reference (don't tell beginning students about it), Russel's paradox concerns the fact that we can define R(x) ≡ x∉x, for each set x, but in ordinary set theories we cannot have an object that captures this predicate R. That is, we cannot have a set S such that ∀x∈set ( x∈S ⇔ R(x) ), otherwise we would get a contradiction.
Regarding the second point, notice that if students truly understand the meaning of definitions (i.e. using symbols to denote a longer expression), then automatically they will not write nonsense such as "If P(k) = 2^k+5" when "P" has been declared to denote a predicate. Technically, this problem should never even occur in the first place, because students ought to be taught to correctly use a deductive system before even using definitions! In my experience, none of my students who learnt my deductive system ever made typing errors...
But if students had been taught in the wrong order, then you can help to get rid of the problem quickly by simply asking them to substitute the "P(k)" for its exact definition to show the 'meaning' of what they wrote. They should get something like "If f(k) = 2^k+5 = 2^k+5", and realize why their original is not sensible.
If you really want to comment on types, as per my explanation above, make sure you do not say "The type of P is ...". But you can say the following:
Whenever you want to reason about a conditional scenario, you would say "If something, then ...". What can that something be? It can be anything with a boolean value (true/false). You cannot say "If elephant, then ...". You can say "If elephants are cute, then ...". You cannot say "If elephants are cute are cute, then ...".
And if we write "Let P(k) ≡ ( f(k) = 2^k+5 ), for each k∈ℕ.", from then on "P" is a predicate-symbol we can use, and "P(E)" is boolean for any expression "E" that is natural. Keep in mind that "P" cannot be used by itself; it is simply ungrammatical (i.e. syntax error).
So if we want to reason about the scenario in which "P(k)" is true, then we would say "If P(k), then ...". We cannot say "If P(k) = 2^k+5, then ...". We also cannot say "If 2^k+5, then ...". They are simply ungrammatical.