Decide-ability here means "Can we come to an answer in a known amount of steps". If you have an algorithm for type checking; then that answer is yes! You're _always_ able to come up with an answer that is yes or no.
For example the following algorithm is for typechecking is decideable:
typechecks :: Program -> Bool
typechecks _ = false
We always come to decision. There is no "semi" here. Just a clear yes/no answer.
The algorithm is even sound. It rejects all incorrect programs.
However it is not complete. It might also reject correct programs (In this case it rejects all correct programs).
Of course you want a as little conservative typechecker without getting into trouble. But it's always conservative to some extent. Preferably you would both be sound _and_ complete. But the problem is that any reasonable logic system can't proof its own consistency.
Hence we can't have both. However we can get "as close as we possibly can".
I believe you're explaining what a computable function is. A decidable set S of a type T is defined to be one for which there is a computable function f : T -> Bool such that the set of values x with f x = true is equal to S. A semidecidable set S of a type T is defined to be one for which there is a partial computable function f : T -> Bool such that whenever x is in S, then f x is computable and equals true.
Given a definition for a well-typed program, you get a set W of Program of the well-typed programs. You can ask whether W is decidable or semidecidable -- i.e., whether there is some (partial) computable function f : Program -> Bool with the above properties.
The example you give is certainly computable, but it has nothing to do with the set W, so it says nothing about (semi)decidability of the typechecking decision problem.
However, it is a valid trying to find the largest subset of W that is (semi)decidable. Or trying to redefine what it means to be well-typed so that it is (semi)decidable!
One interesting case of a programming language without a semidecidable typechecking problem is Lean. The typechecker they've implemented will both reject or time out on valid programs (so the typechecker is at least a computable function in a sense), but in practice these cases don't really occur.
> We always come to decision. There is no "semi" here.
That's not really how I understand the "semi" in the terminology. For a decidable question, you can recognize when the answer is yes, and you can recognize when the answer is no. For a semidecidable question, you can recognize when the answer is yes.
It doesn't take much of a stretch to describe that as cutting your capabilities in "half".
The way I usually think about this is that with full decidability, you can rule something in or out. With semidecidability, you can rule something in, but you can't rule things out.
That framework extends well to the situation described above, where if the compiler chooses to compile a program, then the typing in that program was valid, and if the compiler chooses to complain about the typing, we can't draw any conclusions. It doesn't match your example; you can't rule anything in or out.
For example the following algorithm is for typechecking is decideable:
We always come to decision. There is no "semi" here. Just a clear yes/no answer.The algorithm is even sound. It rejects all incorrect programs.
However it is not complete. It might also reject correct programs (In this case it rejects all correct programs).
Of course you want a as little conservative typechecker without getting into trouble. But it's always conservative to some extent. Preferably you would both be sound _and_ complete. But the problem is that any reasonable logic system can't proof its own consistency. Hence we can't have both. However we can get "as close as we possibly can".