From 8f02c093349acc506257d5f18f31e67d8b5bc68f Mon Sep 17 00:00:00 2001
From: Iavor Diatchki <iavor.diatchki@gmail.com>
Date: Sat, 1 Jun 2024 01:57:28 -0700
Subject: [PATCH 1/6] Fixes #1490

---
 lib/Cryptol.cry | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry
index f514bbd6b..d777bb209 100644
--- a/lib/Cryptol.cry
+++ b/lib/Cryptol.cry
@@ -725,16 +725,16 @@ scarry : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
 scarry x y = (sx == sy) && (sx != sz)
   where
     z  = x + y
-    sx = x@0
-    sy = y@0
-    sz = z@0
+    sx = head x
+    sy = head y
+    sz = head z
 
 /**
  * Signed borrow.  Returns true if the 2's complement signed subtraction of the
  * given bitvector arguments would result in a signed overflow.
  */
 sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
-sborrow x y = ( x <$ (x-y) ) ^ y@0
+sborrow x y = ( x <$ (x-y) ) ^ head y
 
 /**
  * Zero extension of a bitvector.
@@ -747,7 +747,7 @@ zext x = zero # x
  */
 sext : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m]
 sext x = newbits # x
-  where newbits = if x@0 then ~zero else zero
+  where newbits = if head x then ~zero else zero
 
 /**
  * 2's complement signed (arithmetic) right shift.  The first argument
@@ -850,13 +850,13 @@ tail xs = drop`{1} xs
  * Return the first (left-most) element of a sequence.
  */
 head : {n, a} [1 + n]a -> a
-head xs = xs @ 0
+head xs = xs @ (0 : [64])
 
 /**
  * Return the right-most element of a sequence.
  */
 last : {n, a} (fin n) => [1 + n]a -> a
-last xs = xs ! 0
+last xs = xs ! (0 : [64])
 
 /**
  * Same as 'split', but with a different type argument order.
@@ -985,13 +985,13 @@ sort = sortBy (<=)
 sortBy : {a, n} (fin n) => (a -> a -> Bit) -> [n]a -> [n]a
 sortBy le ((xs : [n/2]a) # (ys : [n/^2]a)) = take zs.0
   where
-    xs' = if `(n/2)  == 1 then xs else sortBy le xs
-    ys' = if `(n/^2) == 1 then ys else sortBy le ys
+    xs' = if `(n/2)  == (1 : Integer) then xs else sortBy le xs
+    ys' = if `(n/^2) == (1 : Integer) then ys else sortBy le ys
     zs  = [ if i == `(n/2)        then (ys'@j, i  , j+1)
              | j == `(n/^2)       then (xs'@i, i+1, j  )
              | le (xs'@i) (ys'@j) then (xs'@i, i+1, j  )
             else                       (ys'@j, i  , j+1)
-          | (_, i, j) <- [ (undefined, 0, 0) ] # zs
+          | (_, i , j) <- [ (undefined, 0 : Integer, 0 : Integer) ] # zs
           ]
 
 // GF_2^n polynomial computations -------------------------------------------

From d599934038bd93aafcb5c57ac32891d92ba71032 Mon Sep 17 00:00:00 2001
From: Iavor Diatchki <iavor.diatchki@gmail.com>
Date: Sat, 1 Jun 2024 03:04:15 -0700
Subject: [PATCH 2/6] Fix tests

---
 tests/ffi/ffi-runtime-errors.icry.stdout |  2 +-
 tests/ffi/ffi-type-errors.icry.stdout    | 10 +++++-----
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/tests/ffi/ffi-runtime-errors.icry.stdout b/tests/ffi/ffi-runtime-errors.icry.stdout
index 4ca90de0a..0ee2f7bf3 100644
--- a/tests/ffi/ffi-runtime-errors.icry.stdout
+++ b/tests/ffi/ffi-runtime-errors.icry.stdout
@@ -4,7 +4,7 @@ Loading module Main
 Loading dynamic library ffi-runtime-errors.so
 
 numeric type argument to foreign function is too large: 18446744073709551616
-in type parameter n`902 of function Main::f
+in type parameter n`892 of function Main::f
 type arguments must fit in a C `size_t`
 -- Backtrace --
 Main::f called at ffi-runtime-errors.icry:4:1--4:2
diff --git a/tests/ffi/ffi-type-errors.icry.stdout b/tests/ffi/ffi-type-errors.icry.stdout
index 1763d2c0f..f808f915e 100644
--- a/tests/ffi/ffi-type-errors.icry.stdout
+++ b/tests/ffi/ffi-type-errors.icry.stdout
@@ -35,23 +35,23 @@ Loading module Main
   When checking the type of 'Main::badFloatSizes'
 [error] at ffi-type-errors.cry:5:9--6:59:
   Type unsupported for FFI:
-    [n`972] -> [n`972]([16], [16]) -> [n`972][4][8]{a : [n`972],
+    [n`962] -> [n`962]([16], [16]) -> [n`962][4][8]{a : [n`962],
      b : [2]}
     Due to:
       Type unsupported for FFI:
-        [n`972]
+        [n`962]
         Due to:
         Unsupported sequence element type
         Only words or floats are supported as the element type of
         (possibly multidimensional) sequences
       Type unsupported for FFI:
-        [n`972]([16], [16])
+        [n`962]([16], [16])
         Due to:
         Unsupported sequence element type
         Only words or floats are supported as the element type of
         (possibly multidimensional) sequences
       Type unsupported for FFI:
-        [n`972][4][8]{a : [n`972], b : [2]}
+        [n`962][4][8]{a : [n`962], b : [2]}
         Due to:
         Unsupported sequence element type
         Only words or floats are supported as the element type of
@@ -65,7 +65,7 @@ Loading module Main
   When checking the type of 'Main::notFunction'
 [error] at ffi-type-errors.cry:8:9--8:32:
   Kind of type variable unsupported for FFI: 
-    t`973 : *
+    t`963 : *
     Only type variables of kind # are supported
     When checking the type of 'Main::badKind'
 [error] at ffi-type-errors.cry:9:9--9:43:

From 4f2cf7d5fa6f0262552c43b7e6e20db28458ab49 Mon Sep 17 00:00:00 2001
From: Iavor Diatchki <iavor.diatchki@gmail.com>
Date: Sun, 2 Jun 2024 00:04:53 -0700
Subject: [PATCH 3/6] Use `Integer` in `head` and `last`.

This is a bit of an overkill, as clearly 0 doesn't need it,
but it ensures maximum compatibility with the old behavior.
---
 lib/Cryptol.cry | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry
index d777bb209..4151d959c 100644
--- a/lib/Cryptol.cry
+++ b/lib/Cryptol.cry
@@ -850,13 +850,13 @@ tail xs = drop`{1} xs
  * Return the first (left-most) element of a sequence.
  */
 head : {n, a} [1 + n]a -> a
-head xs = xs @ (0 : [64])
+head xs = xs @ (0 : Integer)
 
 /**
  * Return the right-most element of a sequence.
  */
 last : {n, a} (fin n) => [1 + n]a -> a
-last xs = xs ! (0 : [64])
+last xs = xs ! (0 : Integer)
 
 /**
  * Same as 'split', but with a different type argument order.

From a9f962a5e75f0924e1846ea7db9aba5dac31d255 Mon Sep 17 00:00:00 2001
From: Iavor Diatchki <iavor.diatchki@gmail.com>
Date: Sun, 2 Jun 2024 04:16:37 -0700
Subject: [PATCH 4/6] Fix darwin test

---
 tests/ffi/ffi-runtime-errors.icry.stdout.darwin | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/ffi/ffi-runtime-errors.icry.stdout.darwin b/tests/ffi/ffi-runtime-errors.icry.stdout.darwin
index 1b089a5b8..23ff0286e 100644
--- a/tests/ffi/ffi-runtime-errors.icry.stdout.darwin
+++ b/tests/ffi/ffi-runtime-errors.icry.stdout.darwin
@@ -4,7 +4,7 @@ Loading module Main
 Loading dynamic library ffi-runtime-errors.dylib
 
 numeric type argument to foreign function is too large: 18446744073709551616
-in type parameter n`902 of function Main::f
+in type parameter n`892 of function Main::f
 type arguments must fit in a C `size_t`
 -- Backtrace --
 Main::f called at ffi-runtime-errors.icry:4:1--4:2

From c77db36a252d846ae79bce5dbd4a0c82326141e4 Mon Sep 17 00:00:00 2001
From: Iavor Diatchki <iavor.diatchki@gmail.com>
Date: Sun, 2 Jun 2024 04:20:31 -0700
Subject: [PATCH 5/6] Update mingw test

---
 tests/ffi/ffi-runtime-errors.icry.stdout.mingw32 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/ffi/ffi-runtime-errors.icry.stdout.mingw32 b/tests/ffi/ffi-runtime-errors.icry.stdout.mingw32
index 674f6f226..aab021f1b 100644
--- a/tests/ffi/ffi-runtime-errors.icry.stdout.mingw32
+++ b/tests/ffi/ffi-runtime-errors.icry.stdout.mingw32
@@ -4,7 +4,7 @@ Loading module Main
 Loading dynamic library ffi-runtime-errors.dll
 
 numeric type argument to foreign function is too large: 18446744073709551616
-in type parameter n`902 of function Main::f
+in type parameter n`892 of function Main::f
 type arguments must fit in a C `size_t`
 -- Backtrace --
 Main::f called at ffi-runtime-errors.icry:4:1--4:2

From d6eed17be58e9907b826f246a4936d836303c3e8 Mon Sep 17 00:00:00 2001
From: Iavor Diatchki <iavor.diatchki@gmail.com>
Date: Sun, 2 Jun 2024 07:13:27 -0700
Subject: [PATCH 6/6] More test fixes

---
 tests/issues/T146.icry.stdout          |  8 ++++----
 tests/issues/issue1024.icry.stdout     | 12 ++++++------
 tests/issues/issue290v2.icry.stdout    |  4 ++--
 tests/issues/issue723.icry.stdout      |  4 ++--
 tests/regression/tc-errors.icry.stdout |  8 ++++----
 5 files changed, 18 insertions(+), 18 deletions(-)

diff --git a/tests/issues/T146.icry.stdout b/tests/issues/T146.icry.stdout
index 17da0aa64..3b264dba3 100644
--- a/tests/issues/T146.icry.stdout
+++ b/tests/issues/T146.icry.stdout
@@ -4,15 +4,15 @@ Loading module Main
 
 [error] at T146.cry:11:10--11:12:
   The type ?b is not sufficiently polymorphic.
-    It cannot depend on quantified variables: fv`905
+    It cannot depend on quantified variables: fv`895
     When checking signature variable 'fv'
   where
   ?b is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24
-  fv`905 is signature variable 'fv' at T146.cry:11:10--11:12
+  fv`895 is signature variable 'fv' at T146.cry:11:10--11:12
 [error] at T146.cry:12:11--12:21:
   The type ?a is not sufficiently polymorphic.
-    It cannot depend on quantified variables: fv`905
+    It cannot depend on quantified variables: fv`895
     When checking type of field 'v0'
   where
   ?a is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24
-  fv`905 is signature variable 'fv' at T146.cry:11:10--11:12
+  fv`895 is signature variable 'fv' at T146.cry:11:10--11:12
diff --git a/tests/issues/issue1024.icry.stdout b/tests/issues/issue1024.icry.stdout
index 8c1df7baa..491e08fcc 100644
--- a/tests/issues/issue1024.icry.stdout
+++ b/tests/issues/issue1024.icry.stdout
@@ -13,20 +13,20 @@ Loading module Main
     Unused name: g
 
 [error] at issue1024a.cry:1:6--1:24:
-  Illegal kind assigned to type variable: f`902
+  Illegal kind assigned to type variable: f`892
   Unexpected: # -> *
   where
-  f`902 is signature variable 'f' at issue1024a.cry:1:13--1:14
+  f`892 is signature variable 'f' at issue1024a.cry:1:13--1:14
 [error] at issue1024a.cry:2:6--2:24:
-  Illegal kind assigned to type variable: f`903
+  Illegal kind assigned to type variable: f`893
   Unexpected: Prop
   where
-  f`903 is signature variable 'f' at issue1024a.cry:2:15--2:16
+  f`893 is signature variable 'f' at issue1024a.cry:2:15--2:16
 [error] at issue1024a.cry:4:13--4:49:
-  Illegal kind assigned to type variable: f`905
+  Illegal kind assigned to type variable: f`895
   Unexpected: # -> *
   where
-  f`905 is signature variable 'f' at issue1024a.cry:4:22--4:32
+  f`895 is signature variable 'f' at issue1024a.cry:4:22--4:32
 Loading module Cryptol
 Loading module Main
 0xffff
diff --git a/tests/issues/issue290v2.icry.stdout b/tests/issues/issue290v2.icry.stdout
index 05378ca34..831325262 100644
--- a/tests/issues/issue290v2.icry.stdout
+++ b/tests/issues/issue290v2.icry.stdout
@@ -17,9 +17,9 @@ Loading module Main
             at issue290v2.cry:2:1--2:19
 [error] at issue290v2.cry:2:8--2:11:
   Unsolved constraints:
-    • n`902 == 1
+    • n`892 == 1
         arising from
         checking a pattern: type of 1st argument of Main::minMax
         at issue290v2.cry:2:8--2:11
   where
-  n`902 is signature variable 'n' at issue290v2.cry:1:11--1:12
+  n`892 is signature variable 'n' at issue290v2.cry:1:11--1:12
diff --git a/tests/issues/issue723.icry.stdout b/tests/issues/issue723.icry.stdout
index 42b8254de..86b922758 100644
--- a/tests/issues/issue723.icry.stdout
+++ b/tests/issues/issue723.icry.stdout
@@ -10,9 +10,9 @@ Loading module Main
       assuming
         • fin k
       the following constraints hold:
-        • k == n`902
+        • k == n`892
             arising from
             matching types
             at issue723.cry:7:17--7:19
   where
-  n`902 is signature variable 'n' at issue723.cry:1:6--1:7
+  n`892 is signature variable 'n' at issue723.cry:1:6--1:7
diff --git a/tests/regression/tc-errors.icry.stdout b/tests/regression/tc-errors.icry.stdout
index b74ed4984..0eee36930 100644
--- a/tests/regression/tc-errors.icry.stdout
+++ b/tests/regression/tc-errors.icry.stdout
@@ -84,19 +84,19 @@ Loading module Main
 
 [error] at tc-errors-5.cry:2:1--2:7:
   Inferred type is not sufficiently polymorphic.
-    Quantified variable: a`902
+    Quantified variable: a`892
     cannot match type: [0]?a
     When checking the type of 'Main::f'
   where
   ?a is type of sequence member at tc-errors-5.cry:2:5--2:7
-  a`902 is signature variable 'a' at tc-errors-5.cry:1:6--1:7
+  a`892 is signature variable 'a' at tc-errors-5.cry:1:6--1:7
 Loading module Cryptol
 Loading module Main
 
 [error] at tc-errors-6.cry:4:3--4:8:
   The type ?a is not sufficiently polymorphic.
-    It cannot depend on quantified variables: b`906
+    It cannot depend on quantified variables: b`896
     When checking the type of 'g'
   where
   ?a is the type of 'x' at tc-errors-6.cry:1:3--1:4
-  b`906 is signature variable 'b' at tc-errors-6.cry:3:8--3:9
+  b`896 is signature variable 'b' at tc-errors-6.cry:3:8--3:9