I think we’re reaching an understanding. I agree strict-wrapper still has a big advantage due to easy integration with the existing ecosystem and that it is already a worked-out approach.
The main weakness that I can see now is that I don’t think it is obvious for everybody which functions to use and which to avoid and people can still make mistakes, for example this recent case:
I guess Stan could be used to give warnings about this, or does it already do that?
Unlifted types are still very much a work in progress and it is not clear if it can make true on all the potential that I see in it. And even if it does, there is still the question if it causes too much friction with the rest of the ecosystem. But it still seems worth investigating.