Various changes:

* Improve type inference for numeric if statements (if_infer test)

* Correctly handle constraints for existentially quantified constructors (constraint_ctor test)

* Canonicalise all numeric types in function arguments, which
  triggers some weird edge cases between parametric polymorphism and
  subtyping of numeric arguments

* Because of this eq_int, eq_range, and eq_atom etc become identical

* Avoid duplicating destruct_exist in Env

* Handle some odd subtyping cases better

1 files changed, 2 insertions, 2 deletions

diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index 8cd18fac..505ca7b6 100755
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -143,12 +143,12 @@ val UInt = {
   interpreter: "uint",
   c: "sail_unsigned",
   coq: "uint"
-} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
+} : forall 'n. bits('n) -> {'m, 0 <= 'm <= 2 ^ 'n - 1. int('m)}
 
 val SInt = {
   c: "sail_signed",
   _: "sint"
-} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
+} : forall 'n. bits('n) -> {'m, (- (2 ^ ('n - 1))) <= 'm <= 2 ^ ('n - 1) - 1. int('m)}
 
 val hex_slice = "hex_slice" : forall 'n 'm. (string, atom('n), atom('m)) -> bits('n - 'm) effect {escape}