Do not delay processing equivalence class merges in datatypes (#4952)

Do not delay processing equivalence class merges in datatypes (#4952)

Currently, the theory of datatypes buffers its processing of when equivalence class merges are processed. This was an earlier design to avoid using the equality engine while it was doing internal operations. Now, equivalence class merge callbacks are called at a time when it is safe to use the equality engine and thus this level of indirection is unnecessary.

This will simplify further work on datatypes towards having a standard inference manager.