A critical property tying together a type system with the operational semantics for a programming language is type preservation. It expresses that if we start in a well-typed state, during the execution of a program all intermediate states will be well-typed. This is an absolutely fundamental property without which a type system does not make much sense. Either the type system or the operational semantics needs to be revised in such a case so that they match at least to this extent.
An algebraic perspective on type preservation is that semantics coalesces the free term algebra by equating predicates and their definitions.
One way to ensure type preservation is to generate inferred annotations for all unannotated term constructors that are defined as predicates, and make sure that explicit annotations are at least as specific as inferred annotations. This would have the not-necessarily-undesirable effect of constraining even non-goal occurrences.
Type checking a program, rather than a mere term, should respect the language's semantics.
Frank Pfenning is adamant about this in his lecture on types in LP:
An algebraic perspective on type preservation is that semantics coalesces the free term algebra by equating predicates and their definitions.
One way to ensure type preservation is to generate inferred annotations for all unannotated term constructors that are defined as predicates, and make sure that explicit annotations are at least as specific as inferred annotations. This would have the not-necessarily-undesirable effect of constraining even non-goal occurrences.