I agree with the premise - type-level logic is still just logic, so why not unify the syntax? There's a specification / model checking system called TLA+. This is exactly how you specify types - just as predicates in the same logic as the behavior is defined in. The issue is, it's not statically checkable.

I think the issue is that the vast minority of logic is statically checkable, so your type-level logic would have so many weird restrictions that you couldn't use the full syntax anyway. So it's actually beneficial to keep them separate.