"Compile-time" patterns

Question

If I define a function like

f[x : {_, _Integer}] := (* function body *)

then, as I understand it, every time f[expr] is encountered during the evaluation, expr will be matched against {_, _Integer} to determine which definition for f (if any) should be used.

Has anyone tried to implement "compile-time" patterns in mathematica, which would select definitions before evaluation? For example, if I had some code like

(* ... *)
a = {"ok", 24};
(* ... *)
f[a];

and I had certain extra constraints on how a was used in that code, determined what could "touch" its definition and how it got modified at those times, etc., I might be able to determine that I should always use the f[x : {_, _Integer}] definition of f before I even started evaluating.

If it turns out patterns per se are too flexible for this, I wonder if one could define explicit "type declarations" to implement the same behavior; for example, the definition for f might look like

f[x ::: {_, _Integer}] := (* body *)

and all declarations and modifications of a that I expect to use in my calls to f might come with some type declaration, like

a = {"ok", 24} ::: {_, _Integer}

I'm using the pattern {_, _Integer} just as before here, but maybe only some restricted subset of patterns would be feasible to use here to ensure termination (or such)—for example, perhaps a complicated pattern like {_, _?f} where f is an arbitrary predicate would be disallowed for these kinds of declarations.

Then, for an expression that involved these kinds of type declarations to evaluate, we would need to be able to check the times any definition was modified, and be able to see by way of these declarations that the declaration was preserved. For example, if I had the syntax a = {"ok", b} ::: {_, _Integer}; in my expression, I would also need to be able to prove that I could infer b ::: _Integer from this expression or from the context.

Certain "dangerous" operations, like ToExpression["a = 2"], spring to mind as potential obstructions. These might also need to be weeded out, and if safety is our goal, perhaps only a subset of the Wolfram language would be usable in the evaluation of expressions containing type declarations. (Otherwise, perhaps a warning message could simply be printed whenever a type-dangerous operation was performed in a way that might interfere with the type declarations.)

When I have some time, I'd maybe like to try to build this; but in the meantime, I was wondering if anyone had seen anything like it done for the Wolfram language already, or if they could see any big potential problems that I might be missing—or if I'm misunderstanding the way evaluation proceeds in a way that makes this unnecessary! (For all I know, maybe Mathematica already does this to the extent it can.)