The idea of needing a 1-5 compile-time constrained value is rare in any application I have worked with, because either you'd use an enum, or the "5" isn't reall

The idea of needing a 1-5 compile-time constrained value is rare in any application I have worked with, because either you'd use an enum, or the "5" isn't really known at compile time. (I thought about this when doing some basic Idris lesson.). It makes me wonder what the constrained type might be that I do need? A non-negative floating point number would be a common one I think, e.g. for a coordinate. I've not been keeping up with Haskell but can you guarantee this at compile time? I guess it would be hard to do so, because every assignment to this from a normal floating point would need to be checked, requiring you "prove" that the number is non-negative at compile time, so back to Idris I guess? E.g. x:Positive, x+5 -> this is now a normal float, or I need to prove x+5:Positive. I have only haskelled a little bit, but I would think most of the newtypes are mostly to trace the meaning of something. E.g. Latitude, Longitude, X, Y, WeightKg, and so on. These would be hard to constrain (and to what..?) they are just floating points.