Inconsistent integer argument handling

[maurobringolf]

Motivated by #66 which used Integer int for all integer arguments, I looked into the matter. Our current types for integer API arguments are inconsistent and even allow some invalid Z3 API calls (admittedly edge cases though). In the C world it is common to use unsigned integers when appropriate and so does the Z3 C API. In the Haskell world it seems much less common and Int is everywhere. So we have a choice:

1. Use unsigned integer types ( Word, Word64 ) for unsigned int and unsigned long arguments. This means that API users have to do fromIntegral and think about under- and overflows themselves if they are using Int in their application.

2. Accept Int or Integral int and handle under- and overflows by

   1. Silently wrapping them around by just using fromIntegral.
   2. Adding runtime boundary checks and error-ing out if arguments fall outside of the target type range.

Our current choice is (2.i) in 95% of the cases and either (1) or (2.ii) in the rest.

Since this library is most useful in verification and similar fields where correctness is crucial, I think (2.i) is not good enough. Moving from (2) to (1) is a massive breaking change, so I propose we do (2.ii) using Integral int such that all types stay backwards compatible. Technically this is also a breaking change since we add new runtime errors, but these are proper edge cases where users most likely already get Z3 errors or crashes anyway, e.g. Z3.algebraicRoot ctx _ (-1) results in Z3 error: Overflow encountered when expanding vector. I think it would be much more helpful to error out in the HS API already. The cost is of course the runtime checks.

@IagoAbal I would like to hear your opinion before working on anything here.

---

Status quo

Cases of integer arguments into Z3 API functions

HS API type	C API type	Example	Range consistency
Integral int	CInt	mkIntSymbol	custom runtime error if outside range
Word64	CULLong	mkFiniteDomainSort	type system
Integral int	CUInt	mkBvSort	with function specific range check, but not full type range check
Int	CUInt	algebraicRoot	without range check
Word	CUInt	paramsSetUInt	type system
Int	CInt	mkReal	type system
Int64	CLLong	mkInt64	type system
Word64	CULLong	mkUnsignedInt64	type system

[IagoAbal]

Thanks a lot for looking into this @maurobringolf! Yeah I agree that (2.ii) is probably the way to go.