Broadly, as others have highlighted, you appear to be mixing modes between internal algebra and external algebra. That's fine and in agreement with my argument: "nobody cares about using [categories] with [side effects], they merely want you to be explicit".
The only intensifying bit is that you need some kind of ambient category to build your notion of categories internally to and this one, by long tradition, is typically cartesian.
Differential equations are a great example, but I'm going to use them to again intensify my point instead of yours ;)
Differential equations clearly involve a vital component of state. However, it is benign in its usage. In particular, an enormous amount of work done in diffeq (from designing the models, to analyzing them, to solving them) is done statically either via algebraic manipulations of state free equations or via analyses such as, e.g., Laplace Transforms.
The point is that diffeq equations, by being explicit about state (e.g. external to it) enable many useful interpretations. If diffeq were truly about state alone then you would have no other choices---if I handed you a differential equation then the only thing you could do would be to observe it as it is now or press play and watch.
Clearly that's an important POV, but equally clearly it's not the only one.
So, if your argument boils down to the fact that there are many topics of study which have destructive internal algebras then, yes I agree wholeheartedly!
I just am emphasizing that you need a place to study them externally because it's damn powerful. This external place is, by mathematical convention and the seductive power of cartesian closure, usually side-effect free.
In particular, if you want to dive down into the internal algebra of a side-effective category then you have monads to do that with.
---
Complete inference in any interesting type system stronger than HM is probably undecidable. Personally I don't actually see that as such a big problem. Replacing complete inference is a compiler which will, in real time, tell you everything it knows about relevant names in scope which is pretty powerful. Not being able to ignore types entirely is actually a good thing.
---
And w.r.t. laws and the like, I disagree that TH is much of an answer, would rather suggest that "interpreters and compilers" are an ideal solution and essentially the best we can do while retaining constructivity, and suggest you look closer at the dependently typed languages if you want to learn more about law expression in that kind of tool.