So what’s the alternative - shoving the entire SMT-solver framework inside a Haskell implementation just to have it available as primitive, but otherwise regular Haskell functions?
Certainly not! That’s the entire point of the thread - there has to be a better alternative than that? Merely to call a function that we know is “pure” but just inconveniently happens to live just outside our abstraction boundary. The point is, how we can be bring it inside safely, without this annoying abstraction-breaking burden of a monad.