> you can define a function that only exists at runtime, so even in principle it wouldn’t be possible to type check that statically

Can you say more, maybe with with an example, about a function which can't be typed? Are you talking about generating bytecode at runtime, defining functions with lambda expressions, or something else?