A good bit of philosophical advice is to design your architecture around what the type system can express, instead of trying to go the other way around.
There will always exist “reasonable” patterns that a static type checker cannot “prove”, pretty much because of the halting problem.