How do you define operations on these liquid types? You can't even define subtraction or addition on this "non zero integer type". These types are not closed so how is it useful?
Liquid types are represented under the hood using ordinary data types, so e.g. the nonzero integer type will be stored as a value of ordinary Haskell integer type at runtime. Subtraction on the underlying type is defined as usual.
Now, the Liquid Haskell type checker knows a lot about integers: it can deduce whether your invocation of x-y could give a negative result or not.
If it cannot result in a negative value (e.g. because y has a particular liquid type), the type checker will accept your program, and you'll be able to use the subtraction function as you normally would.
However, if your invocation of x-y could potentially result in a negative value (e.g. because the values of x,y are not sufficiently constrained), the type checker will reject your program, and tell you to do something else (e.g. add runtime checks that rule out a negative result before invoking the subtraction).
Presumably it will reject it with a helpful message like "no"?
I think that's the main disadvantage of these types. It's now no longer a decidable system with (usually) easy to understand error messages. You're in the realm of formal verification and SMT solvers where the only error message is "didn't work; try something else".
Probably still good but I think it's important to be aware of the downsides.
As long as there's a good way to map from the real world into the liquid typed world, either by just telling the liquid typed world that this value can only be a positive integer, or by the liquid typed world having functions that ensure this at the boundary and return nice errors on runtime failure of this check, then it sounds really interesting.
Addition isn't a problem, any nonzero integer plus a nonzero integer is a nonzero integer.
For subtraction it becomes fallible. You get back an option, 5 - 4 = Some(1), 4 - 5 = None. (These are probably methods rather than infix operators, your language may vary.)
It is worth pointing out that the same problems apply to "normal" integer types like int32/uint32; you can trivially over/underflow the bounds with basic arithmetic. In that sense it doesn't really matter what the bounds are exactly.
