I think all of the complications with your proposal can be eliminated if you change "float y;" to "float<positive> y;". If you tell the compiler what type you actually want to use, it will check all of the constraint propagation for you. This is exactly what Haskell, ML, Idris and friends will do. In fact, in Haskell and ML you would be better off leaving out the declarations altogether; the compiler would spot that you've used "fabs", so it will infer "float<positive>", and unify this with the "float<positive>" argument of "sqrt". In Idris, you could declare that the fabs function converts "float" to "float<positive>" and it would automatically insert calls to fabs when you try passing floats to sqrt.

No need for runtime checks/errors, no need to solve the halting problem, etc.