Your idea to use heuristics and tactics to solve problems in type theory is good, and is massively used, not just for equality checking but also for all sorts of other things.
But you are trying to put it in the wrong place. It does not belong to the underlying theoretical formalism (type theory), but to the operational part of a proof assistant (tactics, vernacular, meta-language, etc.)
The job of type theory is to be the mathematical bedrock on top of which we build a proof assistant. It is not there to help solve problems, but as a standard of mathematical correctness, guaranteeing objective and verifiable expression of mathematical statements, constructions and proofs.
Imagine a situation in which we implemented a proof assistant by inserting in its kernel (the core that everyone trusts to do its job correctly and reliably) some external tool $T$, such as a SAT solver or an automated theorem prover, and declared that whatever the tool $T$ says is the holy mathematical truth (inference rules are precisely that). Suddenly all of our formalized mathematics is subject to bugs in $T$, which is presumably a much much larger piece of software than the kernel of a proof assistant. If someone fixes a bug in $T$, or upgrades $T$ so that it works better, does that mean mathematics changed and there are now new mathematical truths, while the old ones are possibly false? What if $T$ works differently on your computer than mine (because it runs concurrently on many cores and I have more core than you), do we live in different worlds of mathematics? This situation is untenable.