From 836771adedfbc73b7d8f5ad27c7a8fc3d457a1d5 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Thu, 28 Jun 2018 14:14:11 -0700
Subject: [PATCH] Tweak names and order of type variables on Cryptol prelude
 functions.

Also update test output for new type variable names.

See #517.
---
 lib/Cryptol.cry                      | 114 +++++++++++++--------------
 tests/issues/T146.icry.stdout        |  12 +--
 tests/issues/issue226.icry.stdout    |  81 +++++++++----------
 tests/issues/issue290v2.icry.stdout  |   2 +-
 tests/regression/AES.icry.stdout     |   8 +-
 tests/regression/check01.icry.stdout |   2 +-
 tests/regression/check02.icry.stdout |   2 +-
 tests/regression/check03.icry.stdout |   4 +-
 tests/regression/check04.icry.stdout |   4 +-
 tests/regression/check05.icry.stdout |   4 +-
 tests/regression/check06.icry.stdout |   4 +-
 tests/regression/check07.icry.stdout |  16 ++--
 tests/regression/check08.icry.stdout |   6 +-
 tests/regression/check09.icry.stdout |  10 +--
 tests/regression/check11.icry.stdout |   2 +-
 15 files changed, 133 insertions(+), 138 deletions(-)

diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry
index 076e6c0a9..d143f8cb1 100644
--- a/lib/Cryptol.cry
+++ b/lib/Cryptol.cry
@@ -143,13 +143,13 @@ primitive (!=) : {a} (Cmp a) => a -> a -> Bit
 /**
  * Compare the outputs of two functions for equality.
  */
-(===) : {a,b} (Cmp b) => (a -> b) -> (a -> b) -> (a -> Bit)
+(===) : {a, b} (Cmp b) => (a -> b) -> (a -> b) -> (a -> Bit)
 f === g = \ x -> f x == g x
 
 /**
  * Compare the outputs of two functions for inequality.
  */
-(!==) : {a,b} (Cmp b) => (a -> b) -> (a -> b) -> (a -> Bit)
+(!==) : {a, b} (Cmp b) => (a -> b) -> (a -> b) -> (a -> Bit)
 f !== g = \x -> f x != g x
 
 /**
@@ -280,7 +280,7 @@ primitive zero : {a} (Zero a) => a
 /**
  * Converts a bitvector to a non-negative integer in the range 0 to 2^^n-1.
  */
-primitive toInteger : {a} (fin a) => [a] -> Integer
+primitive toInteger : {bits} (fin bits) => [bits] -> Integer
 
 /**
  * Converts an unbounded integer to another arithmetic type. When converting
@@ -297,25 +297,25 @@ primitive fromZ : {n} (fin n, n >= 1) => Z n -> Integer
  * Left shift.  The first argument is the sequence to shift, the second is the
  * number of positions to shift by.
 */
-primitive (<<) : {a, b, c} (fin b, Zero c) => [a]c -> [b] -> [a]c
+primitive (<<) : {n, ix, a} (fin ix, Zero a) => [n]a -> [ix] -> [n]a
 
 /**
  * Right shift.  The first argument is the sequence to shift, the second is the
  * number of positions to shift by.
  */
-primitive (>>) : {a, b, c} (fin b, Zero c) => [a]c -> [b] -> [a]c
+primitive (>>) : {n, ix, a} (fin ix, Zero a) => [n]a -> [ix] -> [n]a
 
 /**
  * Left rotate.  The first argument is the sequence to rotate, the second is the
  * number of positions to rotate by.
  */
-primitive (<<<) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
+primitive (<<<) : {n, ix, a} (fin n, fin ix) => [n]a -> [ix] -> [n]a
 
 /**
  * Right rotate.  The first argument is the sequence to rotate, the second is
  * the number of positions to rotate by.
  */
-primitive (>>>) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
+primitive (>>>) : {n, ix, a} (fin n, fin ix) => [n]a -> [ix] -> [n]a
 
 /**
  * 2's complement signed (arithmetic) right shift.  The first argument
@@ -323,7 +323,7 @@ primitive (>>>) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
  * the second argument is the number of positions to shift
  * by (considered as an unsigned value).
  */
-primitive (>>$) : {n, k} (fin n, n >= 1, fin k) => [n] -> [k] -> [n]
+primitive (>>$) : {n, ix} (fin n, n >= 1, fin ix) => [n] -> [ix] -> [n]
 
 
 
@@ -358,24 +358,25 @@ primitive split : {parts, each, a} (fin each) => [parts * each]a
 /**
  * Reverses the elements in a sequence.
  */
-primitive reverse : {a, b} (fin a) => [a]b -> [a]b
+primitive reverse : {n, a} (fin n) => [n]a -> [n]a
 
 /**
- * Transposes an [a][b] matrix into a [b][a] matrix.
+ * Transposes a matrix.
+ * Satisfies the property 'transpose m @ i @ j == m @ j @ i'.
  */
-primitive transpose : {a, b, c} [a][b]c -> [b][a]c
+primitive transpose : {rows, cols, a} [rows][cols]a -> [cols][rows]a
 
 /**
  * Index operator.  The first argument is a sequence.  The second argument is
  * the zero-based index of the element to select from the sequence.
  */
-primitive (@) : {a, b, c} (fin c) => [a]b -> [c] -> b
+primitive (@) : {n, a, ix} (fin ix) => [n]a -> [ix] -> a
 
 /**
  * Bulk index operator.  The first argument is a sequence.  The second argument
  * is a sequence of the zero-based indices of the elements to select.
  */
-(@@) : {a, b, c, d} (fin d) => [a]b -> [c][d] -> [c]b
+(@@) : {n, k, ix, a} (fin ix) => [n]a -> [k][ix] -> [k]a
 xs @@ is = [ xs @ i | i <- is ]
 
 /**
@@ -383,14 +384,14 @@ xs @@ is = [ xs @ i | i <- is ]
  * argument is the zero-based index of the element to select, starting from the
  * end of the sequence.
  */
-primitive (!) : {a, b, c} (fin a, fin c) => [a]b -> [c] -> b
+primitive (!) : {n, a, ix} (fin n, fin ix) => [n]a -> [ix] -> a
 
 /**
  * Bulk reverse index operator.  The first argument is a finite sequence.  The
  * second argument is a sequence of the zero-based indices of the elements to
  * select, starting from the end of the sequence.
  */
-(!!) : {a, b, c, d} (fin a, fin d) => [a]b -> [c][d] -> [c]b
+(!!) : {n, k, ix, a} (fin n, fin ix) => [n]a -> [k][ix] -> [k]a
 xs !! is = [ xs ! i | i <- is ]
 
 /**
@@ -400,7 +401,7 @@ xs !! is = [ xs ! i | i <- is ]
  * The third argument is the new element.  The return value is the
  * initial sequence updated so that the indicated index has the given value.
  */
-primitive update : {a, b, c} (fin c) => [a]b -> [c] -> b -> [a]b
+primitive update : {n, a, ix} (fin ix) => [n]a -> [ix] -> a -> [n]a
 
 /**
  * Update the given sequence with new value at the given index position.
@@ -409,7 +410,7 @@ primitive update : {a, b, c} (fin c) => [a]b -> [c] -> b -> [a]b
  * The third argument is the new element.  The return value is the
  * initial sequence updated so that the indicated index has the given value.
  */
-primitive updateEnd : {a, b, c} (fin a, fin c) => [a]b -> [c] -> b -> [a]b
+primitive updateEnd : {n, a, ix} (fin n, fin ix) => [n]a -> [ix] -> a -> [n]a
 
 /**
  * Perform a series of updates to a sequence.  The first argument is
@@ -418,7 +419,7 @@ primitive updateEnd : {a, b, c} (fin a, fin c) => [a]b -> [c] -> b -> [a]b
  * This function applies the 'update' function in sequence with the
  * given update pairs.
  */
-updates : {a,b,c,d} (fin c, fin d) => [a]b -> [d][c] -> [d]b -> [a]b
+updates : {n, k, ix, a} (fin ix, fin k) => [n]a -> [k][ix] -> [k]a -> [n]a
 updates xs0 idxs vals = xss!0
  where
    xss = [ xs0 ] #
@@ -435,7 +436,7 @@ updates xs0 idxs vals = xss!0
  * This function applies the 'updateEnd' function in sequence with the
  * given update pairs.
  */
-updatesEnd : {a,b,c,d} (fin a, fin c, fin d) => [a]b -> [d][c] -> [d]b -> [a]b
+updatesEnd : {n, k, ix, a} (fin n, fin ix, fin k) => [n]a -> [k][ix] -> [k]a -> [n]a
 updatesEnd xs0 idxs vals = xss!0
  where
    xss = [ xs0 ] #
@@ -488,13 +489,13 @@ primitive infFrom : {a} (Arith a) => a -> [inf]a
  */
 primitive infFromThen : {a} (Arith a) => a -> a -> [inf]a
 
-primitive error : {at, len} (fin len) => [len][8] -> at
+primitive error : {a, len} (fin len) => [len][8] -> a
 
 
 /**
  * Performs multiplication of polynomials over GF(2).
  */
-pmult : {a, b} (fin a, fin b) => [1 + a] -> [1 + b] -> [1 + a + b]
+pmult : {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + u + v]
 pmult x y = last zs
   where
     zs = [0] # [ (z << 1) ^ (if yi then 0 # x else 0) | yi <- y | z <- zs ]
@@ -502,33 +503,33 @@ pmult x y = last zs
 /**
  * Performs division of polynomials over GF(2).
  */
-pdiv : {a, b} (fin a, fin b) => [a] -> [b] -> [a]
+pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u]
 pdiv x y = [ z ! degree | z <- zs ]
   where
-    degree : [width b]
-    degree = last (ds : [1 + b]_)
-      where ds = [0/0] # [if yi then i else d | yi <- reverse y | i <- [0..b] | d <- ds ]
+    degree : [width v]
+    degree = last (ds : [1 + v]_)
+      where ds = [0/0] # [if yi then i else d | yi <- reverse y | i <- [0..v] | d <- ds ]
 
-    reduce : [b] -> [b]
+    reduce : [v] -> [v]
     reduce u = if u ! degree then u ^ y else u
 
-    zs : [a][b]
+    zs : [u][v]
     zs = [ tail (reduce z # [xi]) | z <- [0] # zs | xi <- x ]
 
 /**
  * Performs modulus of polynomials over GF(2).
  */
-pmod : {a, b} (fin a, fin b) => [a] -> [1 + b] -> [b]
+pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v]
 pmod x y = if y == 0 then 0/0 else last zs
   where
-    degree : [width b]
-    degree = last (ds : [2 + b]_)
-      where ds = [0/0] # [if yi then i else d | yi <- reverse y | i <- [0..b] | d <- ds ]
+    degree : [width v]
+    degree = last (ds : [2 + v]_)
+      where ds = [0/0] # [if yi then i else d | yi <- reverse y | i <- [0..v] | d <- ds ]
 
-    reduce : [1 + b] -> [1 + b]
+    reduce : [1 + v] -> [1 + v]
     reduce u = if u ! degree then u ^ y else u
 
-    powers : [inf][1 + b]
+    powers : [inf][1 + v]
     powers = [reduce 1] # [ reduce (p << 1) | p <- powers ]
 
     zs = [0] # [ z ^ (if xi then tail p else 0) | xi <- reverse x | p <- powers | z <- zs ]
@@ -543,35 +544,34 @@ type String n = [n][8]
 type Word n = [n]
 type Char   = [8]
 
-take : {front,back,elem} (fin front) => [front + back] elem -> [front] elem
+take : {front, back, a} (fin front) => [front + back]a -> [front]a
 take (x # _) = x
 
-drop : {front,back,elem} (fin front) => [front + back] elem -> [back] elem
+drop : {front, back, a} (fin front) => [front + back]a -> [back]a
 drop ((_ : [front] _) # y) = y
 
-tail : {a, b} [1 + a]b -> [a]b
+tail : {n, a} [1 + n]a -> [n]a
 tail xs = drop`{1} xs
 
 /**
  * Return the left-most element of a sequence.
  */
-head : {a, b} [1 + a]b -> b
+head : {n, a} [1 + n]a -> a
 head xs = xs @ 0
 
 /**
  * Return the right-most element of a sequence.
  */
-last : {a, b} (fin a) => [1 + a]b -> b
+last : {n, a} (fin n) => [1 + n]a -> a
 last xs = xs ! 0
 
-width : {bits,len,elem} (fin len, fin bits, bits >= width len) => [len] elem -> [bits]
-width _ = `len
+width : {bits, n, a} (fin n, fin bits, bits >= width n) => [n]a -> [bits]
+width _ = `n
 
 undefined : {a} a
 undefined = error "undefined"
 
-groupBy : {each,parts,elem} (fin each) =>
-  [parts * each] elem -> [parts][each]elem
+groupBy : {each, parts, a} (fin each) => [parts * each]a -> [parts][each]a
 groupBy = split`{parts=parts}
 
 /**
@@ -623,19 +623,19 @@ or xs = zero != xs
 /**
  * Conjunction after applying a predicate to all elements.
  */
-all : {a,n} (fin n) => (a -> Bit) -> [n]a -> Bit
+all : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
 all f xs = and (map f xs)
 
 /**
  * Disjunction after applying a predicate to all elements.
  */
-any : {a,n} (fin n) => (a -> Bit) -> [n]a -> Bit
+any : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
 any f xs = or (map f xs)
 
 /**
  * Map a function over a sequence.
  */
-map : {a, b, n} (a -> b) -> [n]a -> [n]b
+map : {n, a, b} (a -> b) -> [n]a -> [n]b
 map f xs = [f x | x <- xs]
 
 /**
@@ -643,7 +643,7 @@ map f xs = [f x | x <- xs]
  *
  * foldl (+) 0 [1,2,3] = ((0 + 1) + 2) + 3
  */
-foldl : {a, b, n} (fin n) => (a -> b -> a) -> a -> [n]b -> a
+foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a
 foldl f acc xs = ys ! 0
   where ys = [acc] # [f a x | a <- ys | x <- xs]
 
@@ -652,27 +652,27 @@ foldl f acc xs = ys ! 0
  *
  * foldr (-) 0 [1,2,3] = 0 - (1 - (2 - 3))
  */
-foldr : {a,b,n} (fin n) => (a -> b -> b) -> b -> [n]a -> b
+foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b
 foldr f acc xs = ys ! 0
   where ys = [acc] # [f x a | a <- ys | x <- reverse xs]
 
 /**
  * Compute the sum of the values in the sequence.
  */
-sum : {a,n} (fin n, Zero a, Arith a) => [n]a -> a
-sum xs = foldl (+) zero xs
+sum : {n, a} (fin n, Arith a) => [n]a -> a
+sum xs = foldl (+) (fromInteger 0) xs
 
 /**
  * Scan left is like a foldl that also emits the intermediate values.
  */
-scanl : {b, a, n}  (b -> a -> b) -> b -> [n]a -> [n+1]b
+scanl : {n, b, a}  (b -> a -> b) -> b -> [n]a -> [n+1]b
 scanl f acc xs = ys
   where ys = [acc] # [f a x | a <- ys | x <- xs]
 
 /**
  * Scan right is like a foldr that also emits the intermediate values.
  */
-scanr : {a,b,n} (fin n) => (a -> b -> b) -> b -> [n]a -> [n+1]b
+scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [n+1]b
 scanr f acc xs = reverse ys
   where ys = [acc] # [f x a | a <- ys | x <- reverse xs]
 
@@ -685,36 +685,36 @@ repeat x = [ x | _ <- zero : [n] ]
 /**
  * `elem x xs` Returns true if x is equal to a value in xs.
  */
-elem : {n,a} (fin n, Cmp a) => a -> [n]a -> Bit
+elem : {n, a} (fin n, Cmp a) => a -> [n]a -> Bit
 elem a xs = any (\x -> x == a) xs
 
 /**
  * Create a list of tuples from two lists.
  */
-zip : {a,b,n} [n]a -> [n]b -> [n](a,b)
+zip : {n, a, b} [n]a -> [n]b -> [n](a, b)
 zip xs ys = [(x,y) | x <- xs | y <- ys]
 
 /**
  * Create a list by applying the function to each pair of elements in the input.
  */
-zipWith : {a,b,c,n} (a -> b -> c) -> [n]a -> [n]b -> [n]c
+zipWith : {n, a, b, c} (a -> b -> c) -> [n]a -> [n]b -> [n]c
 zipWith f xs ys = [f x y | x <- xs | y <- ys]
 
 /**
  * Transform a function into uncurried form.
  */
-uncurry : {a,b,c} (a -> b -> c) -> (a,b) -> c
+uncurry : {a, b, c} (a -> b -> c) -> (a, b) -> c
 uncurry f = \(a, b) -> f a b
 
 /**
  * Transform a function into curried form.
  */
-curry : {a,b,c} ((a, b) -> c) -> a -> b -> c
+curry : {a, b, c} ((a, b) -> c) -> a -> b -> c
 curry f = \a b -> f (a, b)
 
 /**
  * Map a function iteratively over a seed value, producing an infinite
  * list of successive function applications.
  */
-iterate : { a } (a -> a) -> a -> [inf]a
+iterate : {a} (a -> a) -> a -> [inf]a
 iterate f x = [x] # [ f v | v <- iterate f x ]
diff --git a/tests/issues/T146.icry.stdout b/tests/issues/T146.icry.stdout
index af568a412..2086ca48f 100644
--- a/tests/issues/T146.icry.stdout
+++ b/tests/issues/T146.icry.stdout
@@ -3,12 +3,12 @@ Loading module Cryptol
 Loading module Main
 
 [error] at ./T146.cry:1:18--6:10:
-  The type ?q33 is not sufficiently polymorphic.
-    It cannot depend on quantified variables: a`858
+  The type ?s33 is not sufficiently polymorphic.
+    It cannot depend on quantified variables: a`860
   where
-  ?q33 is type argument 'fv' of 'Main::ec_v1' at ./T146.cry:4:19--4:24
+  ?s33 is type argument 'fv' of 'Main::ec_v1' at ./T146.cry:4:19--4:24
 [error] at ./T146.cry:5:19--5:24:
-  The type ?s33 is not sufficiently polymorphic.
-    It cannot depend on quantified variables: a`858
+  The type ?u33 is not sufficiently polymorphic.
+    It cannot depend on quantified variables: a`860
   where
-  ?s33 is type argument 'fv' of 'Main::ec_v2' at ./T146.cry:5:19--5:24
+  ?u33 is type argument 'fv' of 'Main::ec_v2' at ./T146.cry:5:19--5:24
diff --git a/tests/issues/issue226.icry.stdout b/tests/issues/issue226.icry.stdout
index 4cbcf0f01..d2d0ef62e 100644
--- a/tests/issues/issue226.icry.stdout
+++ b/tests/issues/issue226.icry.stdout
@@ -33,11 +33,11 @@ Symbols
     (#) :
       {front, back, a} (fin front) =>
         [front]a -> [back]a -> [front + back]a
-    (<<) : {a, b, c} (fin b, Zero c) => [a]c -> [b] -> [a]c
-    (<<<) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
-    (>>) : {a, b, c} (fin b, Zero c) => [a]c -> [b] -> [a]c
-    (>>$) : {n, k} (fin n, n >= 1, fin k) => [n] -> [k] -> [n]
-    (>>>) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
+    (<<) : {n, ix, a} (fin ix, Zero a) => [n]a -> [ix] -> [n]a
+    (<<<) : {n, ix, a} (fin n, fin ix) => [n]a -> [ix] -> [n]a
+    (>>) : {n, ix, a} (fin ix, Zero a) => [n]a -> [ix] -> [n]a
+    (>>$) : {n, ix} (fin n, n >= 1, fin ix) => [n] -> [ix] -> [n]
+    (>>>) : {n, ix, a} (fin n, fin ix) => [n]a -> [ix] -> [n]a
     (+) : {a} (Arith a) => a -> a -> a
     (-) : {a} (Arith a) => a -> a -> a
     (%) : {a} (Arith a) => a -> a -> a
@@ -46,24 +46,23 @@ Symbols
     (/) : {a} (Arith a) => a -> a -> a
     (/$) : {a} (Arith a) => a -> a -> a
     (^^) : {a} (Arith a) => a -> a -> a
-    (!) : {a, b, c} (fin a, fin c) => [a]b -> [c] -> b
-    (!!) : {a, b, c, d} (fin a, fin d) => [a]b -> [c][d] -> [c]b
-    (@) : {a, b, c} (fin c) => [a]b -> [c] -> b
-    (@@) : {a, b, c, d} (fin d) => [a]b -> [c][d] -> [c]b
-    all : {a, n} (fin n) => (a -> Bit) -> [n]a -> Bit
+    (!) : {n, a, ix} (fin n, fin ix) => [n]a -> [ix] -> a
+    (!!) : {n, k, ix, a} (fin n, fin ix) => [n]a -> [k][ix] -> [k]a
+    (@) : {n, a, ix} (fin ix) => [n]a -> [ix] -> a
+    (@@) : {n, k, ix, a} (fin ix) => [n]a -> [k][ix] -> [k]a
+    all : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
     and : {n} (fin n) => [n] -> Bit
-    any : {a, n} (fin n) => (a -> Bit) -> [n]a -> Bit
+    any : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
     carry : {n} (fin n) => [n] -> [n] -> Bit
     complement : {a} (Logic a) => a -> a
     curry : {a, b, c} ((a, b) -> c) -> a -> b -> c
     demote : {val, rep} (Literal val rep) => rep
-    drop :
-      {front, back, elem} (fin front) => [front + back]elem -> [back]elem
+    drop : {front, back, a} (fin front) => [front + back]a -> [back]a
     elem : {n, a} (fin n, Cmp a) => a -> [n]a -> Bit
-    error : {at, len} (fin len) => [len][8] -> at
+    error : {a, len} (fin len) => [len][8] -> a
     False : Bit
-    foldl : {a, b, n} (fin n) => (a -> b -> a) -> a -> [n]b -> a
-    foldr : {a, b, n} (fin n) => (a -> b -> b) -> b -> [n]a -> b
+    foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a
+    foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b
     foo : {a} a -> a
     fromInteger : {a} (Arith a) => Integer -> a
     fromThen :
@@ -81,31 +80,30 @@ Symbols
         [1 + (last - first)]a
     fromZ : {n} (fin n, n >= 1) => Z n -> Integer
     groupBy :
-      {each, parts, elem} (fin each) =>
-        [each * parts]elem -> [parts][each]elem
-    head : {a, b} [1 + a]b -> b
+      {each, parts, a} (fin each) => [each * parts]a -> [parts][each]a
+    head : {n, a} [1 + n]a -> a
     infFrom : {a} (Arith a) => a -> [inf]a
     infFromThen : {a} (Arith a) => a -> a -> [inf]a
     iterate : {a} (a -> a) -> a -> [inf]a
     join :
       {parts, each, a} (fin each) => [parts][each]a -> [parts * each]a
-    last : {a, b} (fin a) => [1 + a]b -> b
+    last : {n, a} (fin n) => [1 + n]a -> a
     lg2 : {a} (Arith a) => a -> a
-    map : {a, b, n} (a -> b) -> [n]a -> [n]b
+    map : {n, a, b} (a -> b) -> [n]a -> [n]b
     max : {a} (Cmp a) => a -> a -> a
     min : {a} (Cmp a) => a -> a -> a
     negate : {a} (Arith a) => a -> a
     or : {n} (fin n) => [n] -> Bit
-    pdiv : {a, b} (fin a, fin b) => [a] -> [b] -> [a]
-    pmod : {a, b} (fin a, fin b) => [a] -> [1 + b] -> [b]
+    pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u]
+    pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v]
     pmult :
-      {a, b} (fin a, fin b) => [1 + a] -> [1 + b] -> [1 + (a + b)]
+      {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + (u + v)]
     random : {a} [256] -> a
     repeat : {n, a} a -> [n]a
-    reverse : {a, b} (fin a) => [a]b -> [a]b
+    reverse : {n, a} (fin n) => [n]a -> [n]a
     sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
-    scanl : {b, a, n} (b -> a -> b) -> b -> [n]a -> [1 + n]b
-    scanr : {a, b, n} (fin n) => (a -> b -> b) -> b -> [n]a -> [1 + n]b
+    scanl : {n, b, a} (b -> a -> b) -> b -> [n]a -> [1 + n]b
+    scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [1 + n]b
     scarry : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
     sext : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m]
     split :
@@ -113,30 +111,27 @@ Symbols
     splitAt :
       {front, back, a} (fin front) =>
         [front + back]a -> ([front]a, [back]a)
-    sum : {a, n} (fin n, Zero a, Arith a) => [n]a -> a
+    sum : {n, a} (fin n, Arith a) => [n]a -> a
     True : Bit
-    tail : {a, b} [1 + a]b -> [a]b
-    take :
-      {front, back, elem} (fin front) =>
-        [front + back]elem -> [front]elem
-    toInteger : {a} (fin a) => [a] -> Integer
+    tail : {n, a} [1 + n]a -> [n]a
+    take : {front, back, a} (fin front) => [front + back]a -> [front]a
+    toInteger : {bits} (fin bits) => [bits] -> Integer
     trace : {n, a, b} (fin n) => [n][8] -> a -> b -> b
     traceVal : {n, a} (fin n) => [n][8] -> a -> a
-    transpose : {a, b, c} [a][b]c -> [b][a]c
+    transpose : {rows, cols, a} [rows][cols]a -> [cols][rows]a
     uncurry : {a, b, c} (a -> b -> c) -> (a, b) -> c
     undefined : {a} a
-    update : {a, b, c} (fin c) => [a]b -> [c] -> b -> [a]b
-    updateEnd : {a, b, c} (fin a, fin c) => [a]b -> [c] -> b -> [a]b
+    update : {n, a, ix} (fin ix) => [n]a -> [ix] -> a -> [n]a
+    updateEnd : {n, a, ix} (fin n, fin ix) => [n]a -> [ix] -> a -> [n]a
     updates :
-      {a, b, c, d} (fin c, fin d) => [a]b -> [d][c] -> [d]b -> [a]b
+      {n, k, ix, a} (fin ix, fin k) => [n]a -> [k][ix] -> [k]a -> [n]a
     updatesEnd :
-      {a, b, c, d} (fin a, fin c, fin d) =>
-        [a]b -> [d][c] -> [d]b -> [a]b
+      {n, k, ix, a} (fin n, fin ix, fin k) =>
+        [n]a -> [k][ix] -> [k]a -> [n]a
     width :
-      {bits, len, elem} (fin len, fin bits, bits >= width len) =>
-        [len]elem -> [bits]
+      {bits, n, a} (fin n, fin bits, bits >= width n) => [n]a -> [bits]
     zero : {a} (Zero a) => a
     zext : {m, n} (fin m, m >= n) => [n] -> [m]
-    zip : {a, b, n} [n]a -> [n]b -> [n](a, b)
-    zipWith : {a, b, c, n} (a -> b -> c) -> [n]a -> [n]b -> [n]c
+    zip : {n, a, b} [n]a -> [n]b -> [n](a, b)
+    zipWith : {n, a, b, c} (a -> b -> c) -> [n]a -> [n]b -> [n]c
 
diff --git a/tests/issues/issue290v2.icry.stdout b/tests/issues/issue290v2.icry.stdout
index 8c8ac4ceb..0ba5e9c4e 100644
--- a/tests/issues/issue290v2.icry.stdout
+++ b/tests/issues/issue290v2.icry.stdout
@@ -4,7 +4,7 @@ Loading module Main
 
 [error] at ./issue290v2.cry:2:1--2:19:
   Unsolved constraints:
-    a`855 == 1
+    a`857 == 1
       arising from
       checking a pattern: type of 1st argument of Main::minMax
       at ./issue290v2.cry:2:8--2:11
diff --git a/tests/regression/AES.icry.stdout b/tests/regression/AES.icry.stdout
index cf89832f9..be0844fb8 100644
--- a/tests/regression/AES.icry.stdout
+++ b/tests/regression/AES.icry.stdout
@@ -2,13 +2,13 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module AES
 [warning] at ./AES.cry:86:21--86:40:
-  Defaulting type argument 'b' of '(<<<)' to 2
+  Defaulting type argument 'ix' of '(<<<)' to 2
 [warning] at ./AES.cry:91:24--91:43:
-  Defaulting type argument 'b' of '(>>>)' to 2
+  Defaulting type argument 'ix' of '(>>>)' to 2
 [warning] at ./AES.cry:147:28--147:51:
-  Defaulting type argument 'd' of '(@@)' to 4
+  Defaulting type argument 'ix' of '(@@)' to 4
 [warning] at ./AES.cry:147:53--147:63:
-  Defaulting type argument 'c' of '(@)' to 4
+  Defaulting type argument 'ix' of '(@)' to 4
 [warning] at ./AES.cry:127:32--127:33:
   Defaulting type argument 'rep' of 'demote' to [3]
 True
diff --git a/tests/regression/check01.icry.stdout b/tests/regression/check01.icry.stdout
index e7b4ff293..70bff27ff 100644
--- a/tests/regression/check01.icry.stdout
+++ b/tests/regression/check01.icry.stdout
@@ -2,6 +2,6 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module Main
 [warning] at ./check01.cry:2:5--2:27:
-  Defaulting type argument 'd' of '(@@)' to 5
+  Defaulting type argument 'ix' of '(@@)' to 5
 [0x00000007, 0x00000014]
 True
diff --git a/tests/regression/check02.icry.stdout b/tests/regression/check02.icry.stdout
index aa2986789..56e38338a 100644
--- a/tests/regression/check02.icry.stdout
+++ b/tests/regression/check02.icry.stdout
@@ -4,7 +4,7 @@ Loading module Main
 [warning] at ./check02.cry:3:24--3:25:
   Defaulting type argument 'rep' of 'demote' to [1]
 [warning] at <interactive>:1:1--1:18:
-  Defaulting type argument 'd' of '(@@)' to 4
+  Defaulting type argument 'ix' of '(@@)' to 4
 Showing a specific instance of polymorphic result:
   * Using 'Integer' for 1st type argument of 'Main::ones'
 [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
diff --git a/tests/regression/check03.icry.stdout b/tests/regression/check03.icry.stdout
index 47ba813e9..2468ab14b 100644
--- a/tests/regression/check03.icry.stdout
+++ b/tests/regression/check03.icry.stdout
@@ -2,12 +2,12 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module Main
 [warning] at <interactive>:1:1--1:22:
-  Defaulting type argument 'd' of '(@@)' to 4
+  Defaulting type argument 'ix' of '(@@)' to 4
 [0x00000000, 0x00000001, 0x00000002, 0x00000003, 0x00000004,
  0x00000005, 0x00000006, 0x00000007, 0x00000008, 0x00000009,
  0x0000000a]
 [warning] at <interactive>:1:1--1:23:
-  Defaulting type argument 'd' of '(@@)' to 4
+  Defaulting type argument 'ix' of '(@@)' to 4
 [0x0000000b, 0x0000000c, 0x0000000d, 0x0000000e, 0x0000000f,
  0x00000010, 0x00000011, 0x00000012, 0x00000013, 0x00000014,
  0x00000015]
diff --git a/tests/regression/check04.icry.stdout b/tests/regression/check04.icry.stdout
index 587af3034..5d22e3469 100644
--- a/tests/regression/check04.icry.stdout
+++ b/tests/regression/check04.icry.stdout
@@ -2,11 +2,11 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module Main
 [warning] at ./check04.cry:4:10--4:45:
-  Defaulting type argument 'd' of '(@@)' to 2
+  Defaulting type argument 'ix' of '(@@)' to 2
 [warning] at ./check04.cry:4:43--4:44:
   Defaulting type argument 'rep' of 'demote' to [2]
 [warning] at <interactive>:1:1--1:21:
-  Defaulting type argument 'd' of '(@@)' to 4
+  Defaulting type argument 'ix' of '(@@)' to 4
 Showing a specific instance of polymorphic result:
   * Using 'Integer' for 1st type argument of 'Main::onetwos'
 [1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1]
diff --git a/tests/regression/check05.icry.stdout b/tests/regression/check05.icry.stdout
index 9b0ad59ef..46bc58f1e 100644
--- a/tests/regression/check05.icry.stdout
+++ b/tests/regression/check05.icry.stdout
@@ -2,11 +2,11 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module Main
 [warning] at ./check05.cry:4:10--4:45:
-  Defaulting type argument 'd' of '(@@)' to 2
+  Defaulting type argument 'ix' of '(@@)' to 2
 [warning] at ./check05.cry:4:43--4:44:
   Defaulting type argument 'rep' of 'demote' to [2]
 [warning] at <interactive>:1:1--1:21:
-  Defaulting type argument 'd' of '(@@)' to 4
+  Defaulting type argument 'ix' of '(@@)' to 4
 Showing a specific instance of polymorphic result:
   * Using 'Integer' for 1st type argument of 'Main::twoones'
 [2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2]
diff --git a/tests/regression/check06.icry.stdout b/tests/regression/check06.icry.stdout
index 40c819d15..245937424 100644
--- a/tests/regression/check06.icry.stdout
+++ b/tests/regression/check06.icry.stdout
@@ -2,11 +2,11 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module Main
 [warning] at ./check06.cry:5:10--5:70:
-  Defaulting type argument 'd' of '(@@)' to 2
+  Defaulting type argument 'ix' of '(@@)' to 2
 [warning] at ./check06.cry:5:66--5:67:
   Defaulting type argument 'rep' of 'demote' to [2]
 [warning] at <interactive>:1:1--1:24:
-  Defaulting type argument 'd' of '(@@)' to 4
+  Defaulting type argument 'ix' of '(@@)' to 4
 Showing a specific instance of polymorphic result:
   * Using 'Integer' for 1st type argument of 'Main::onesytwosy'
 [[1, 2], [2, 1], [1, 2], [2, 1], [1, 2], [2, 1], [1, 2], [2, 1],
diff --git a/tests/regression/check07.icry.stdout b/tests/regression/check07.icry.stdout
index 2c801639f..6a1681d11 100644
--- a/tests/regression/check07.icry.stdout
+++ b/tests/regression/check07.icry.stdout
@@ -2,21 +2,21 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module Main
 [warning] at ./check07.cry:7:16--7:35:
-  Defaulting type argument 'b' of '(<<)' to 6
+  Defaulting type argument 'ix' of '(<<)' to 6
 [warning] at ./check07.cry:13:11--13:22:
-  Defaulting type argument 'a' of '(<<)' to 1
+  Defaulting type argument 'n' of '(<<)' to 1
 [warning] at ./check07.cry:11:11--11:51:
-  Defaulting type argument 'd' of '(@@)' to 4
+  Defaulting type argument 'ix' of '(@@)' to 4
 [warning] at ./check07.cry:5:14--5:29:
-  Defaulting type argument 'b' of '(>>)' to 7
+  Defaulting type argument 'ix' of '(>>)' to 7
 [warning] at ./check07.cry:4:14--4:29:
-  Defaulting type argument 'b' of '(>>)' to 6
+  Defaulting type argument 'ix' of '(>>)' to 6
 [warning] at ./check07.cry:3:14--3:29:
-  Defaulting type argument 'b' of '(<<)' to 32
+  Defaulting type argument 'ix' of '(<<)' to 32
 [warning] at ./check07.cry:2:14--2:29:
-  Defaulting type argument 'b' of '(<<)' to 7
+  Defaulting type argument 'ix' of '(<<)' to 7
 [warning] at ./check07.cry:1:14--1:29:
-  Defaulting type argument 'b' of '(<<)' to 6
+  Defaulting type argument 'ix' of '(<<)' to 6
 [0b00010010001101000101011001111000,
  0b00100100011010001010110011110000,
  0b01001000110100010101100111100000,
diff --git a/tests/regression/check08.icry.stdout b/tests/regression/check08.icry.stdout
index 1589d57d4..008360d8e 100644
--- a/tests/regression/check08.icry.stdout
+++ b/tests/regression/check08.icry.stdout
@@ -2,11 +2,11 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module Main
 [warning] at ./check08.cry:9:19--9:54:
-  Defaulting type argument 'd' of '(@@)' to 3
+  Defaulting type argument 'ix' of '(@@)' to 3
 [warning] at ./check08.cry:7:10--7:45:
-  Defaulting type argument 'd' of '(@@)' to 3
+  Defaulting type argument 'ix' of '(@@)' to 3
 [warning] at <interactive>:1:1--1:15:
-  Defaulting type argument 'd' of '(@@)' to 3
+  Defaulting type argument 'ix' of '(@@)' to 3
 [0x00000001, 0x00000002, 0x00000005, 0x0000000c, 0x0000001b]
 True
 Q.E.D.
diff --git a/tests/regression/check09.icry.stdout b/tests/regression/check09.icry.stdout
index 0f577a461..5ac6c91d1 100644
--- a/tests/regression/check09.icry.stdout
+++ b/tests/regression/check09.icry.stdout
@@ -14,16 +14,16 @@ Loading module Main
     This binding for ss shadows the existing binding from
     (at ./check09.cry:5:1--5:3, ss)
 [warning] at ./check09.cry:17:12--17:28:
-  Defaulting type argument 'd' of '(@@)' to 3
+  Defaulting type argument 'ix' of '(@@)' to 3
 [warning] at ./check09.cry:13:12--13:80:
-  Defaulting type argument 'd' of '(@@)' to 2
+  Defaulting type argument 'ix' of '(@@)' to 2
 [warning] at ./check09.cry:14:12--14:80:
-  Defaulting type argument 'd' of '(@@)' to 2
+  Defaulting type argument 'ix' of '(@@)' to 2
 [warning] at <interactive>:1:1--1:15:
-  Defaulting type argument 'd' of '(@@)' to 2
+  Defaulting type argument 'ix' of '(@@)' to 2
 [0x00000008, 0x00004080, 0x00068c00, 0x00a22800]
 [warning] at <interactive>:1:1--1:15:
-  Defaulting type argument 'd' of '(@@)' to 2
+  Defaulting type argument 'ix' of '(@@)' to 2
 [0x00000800, 0x00005080, 0x00072d00, 0x00b08200]
 [0x00000008, 0x131b638b, 0x4fdd24a2, 0xb9094711, 0xa9cc106f,
  0x52c445fb, 0xec66ea8b]
diff --git a/tests/regression/check11.icry.stdout b/tests/regression/check11.icry.stdout
index 91da1d250..3a1e510ff 100644
--- a/tests/regression/check11.icry.stdout
+++ b/tests/regression/check11.icry.stdout
@@ -2,7 +2,7 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module Main
 [warning] at ./check11.cry:5:10--5:25:
-  Defaulting type argument 'd' of '(@@)' to 7
+  Defaulting type argument 'ix' of '(@@)' to 7
 [warning] at ./check11.cry:3:10--3:19:
   Defaulting type argument 'a' of 'fromTo' to [7]
 True