Tracking this as part of follow up work for the diagnostics. The current wellformedness check only looks at a single function, does not report descriptive errors and has some challenges when running on a whole module at once.
We should consider refactoring it more aggressively now that the diagnostic changes are landing in TVM.
cc @altanh