This is a more research-oriented question on TVM. But to the community, is there any value in having type-preserving (or something stronger like semantic-preserving) transformations in TVM? For context, in PL literature, type preservation typically means that you have a strongly typed AST (or IR), and when you apply a transformation like operator fusion, the types are preserved in the transformed program. There exist quite formal definitions of type preservation, but I am refraining from introducing PL jargon in this post.
An advantage of type preservation is that you can rule out bugs introduced by unsound compiler passes that might compromise things like tensor types, shapes, etc. There are stronger things like semantic preservation, but that would typically involve using full-fledged proof assistants. I work on programming language theory and implementation, and if the topic is of value to the community, do let me know, as I believe something lightweight like type preservation can already improve the robustness of a tensor compiler.