diff --git a/docs/conf.py b/docs/conf.py
--- a/docs/conf.py
+++ b/docs/conf.py
@@ -162,7 +162,7 @@
 # Add any paths that contain custom static files (such as style sheets) here,
 # relative to this directory. They are copied after the builtin static files,
 # so a file named "default.css" will overwrite the builtin "default.css".
-html_static_path = ['_static']
+# html_static_path = ['_static']
 
 # Add any extra paths that contain custom files (such as robots.txt or
 # .htaccess) here, relative to this directory. These files are copied
diff --git a/docs/man/futhark-bench.rst b/docs/man/futhark-bench.rst
--- a/docs/man/futhark-bench.rst
+++ b/docs/man/futhark-bench.rst
@@ -35,6 +35,14 @@
   The backend used when compiling Futhark programs (without leading
   ``futhark``, e.g. just ``opencl``).
 
+--concurrency=NUM
+
+  The number of benchmark programs to prepare concurrently.  Defaults
+  to the number of cores available.  *Prepare* means to compile the
+  benchmark, as well as generate any needed datasets.  In some cases,
+  this generation can take too much memory, in which case lowering
+  ``--concurrency`` may help.
+
 --entry-point=name
 
   Only run entry points with this name.
@@ -103,6 +111,13 @@
   example, given ``--tuning=tuning`` (the default), the program
   ``foo.fut`` will be passed the tuning file ``foo.fut.tuning`` if it
   exists.
+
+WHAT FUTHARK BENCH MEASURES
+===========================
+
+``futhark bench`` measures the time it takes to run the given Futhark
+program by passing the ``-t FILE`` option to the generated program. See
+the man page for the specific compiler to see exactly what is measured.
 
 EXAMPLES
 ========
diff --git a/docs/man/futhark-c.rst b/docs/man/futhark-c.rst
--- a/docs/man/futhark-c.rst
+++ b/docs/man/futhark-c.rst
@@ -54,6 +54,43 @@
 --Werror
   Treat warnings as errors.
 
+EXECUTABLE OPTIONS
+==================
+
+The following options are accepted by executables generated by ``futhark c``.
+
+-b, --binary-output
+
+  Print the program result in the binary output format.  The default
+  is human-readable text, which is very slow.
+
+-D, --debugging
+
+  Perform possibly expensive internal correctness checks and verbose
+  logging.  Implies ``-L``.
+
+-e, --entry-point=FUN
+
+  The entry point to run.  Defaults to ``main``.
+
+-L, --log
+
+  Print various low-overhead logging information to stderr while
+  running.
+
+-r, --runs=NUM
+
+  Perform NUM runs of the program.  With ``-t``, the runtime for each
+  individual run will be printed.  Additionally, a single leading
+  warmup run will be performed (not counted).  Only the final run will
+  have its result written to stdout.
+
+-t, --write-runtime-to=FILE
+
+  Print the time taken to execute the program to the indicated file, an
+  integral number of microseconds.
+
+
 SEE ALSO
 ========
 
diff --git a/docs/man/futhark-cuda.rst b/docs/man/futhark-cuda.rst
--- a/docs/man/futhark-cuda.rst
+++ b/docs/man/futhark-cuda.rst
@@ -23,8 +23,9 @@
 resulting program will otherwise behave exactly as one compiled with
 ``futhark c``.
 
-The generated programs use the NVRTC API for run-time compilation,
-which must consequently be available.
+``futhark cuda`` uses ``-lcuda -lnvrtc`` to link.  If using
+``--library``, you will need to do the same when linking the final
+binary.
 
 OPTIONS
 =======
@@ -54,6 +55,89 @@
 
 --Werror
   Treat warnings as errors.
+
+EXECUTABLE OPTIONS
+==================
+
+Generated executables accept the same options as those generated by
+:ref:`futhark-c(1)`.  The ``-t`` option behaves as with
+:ref:`futhark-opencl(1)`.  For commonality, the options use OpenCL
+nomenclature ("group" instead of "thread block").
+
+The following additional options are accepted.
+
+--default-group-size=INT
+
+  The default size of thread blocks that are launched.  Capped to the
+  hardware limit if necessary.
+
+--default-num-groups=INT
+
+  The default number of thread blocks that are launched.
+
+--default-threshold=INT
+
+  The default parallelism threshold used for comparisons when
+  selecting between code versions generated by incremental flattening.
+  Intuitively, the amount of parallelism needed to saturate the GPU.
+
+--default-tile-size=INT
+
+  The default tile size used when performing two-dimensional tiling
+  (the workgroup size will be the square of the tile size).
+
+--dump-cuda=FILE
+
+  Don't run the program, but instead dump the embedded CUDA kernels to
+  the indicated file.  Useful if you want to see what is actually
+  being executed.
+
+--dump-ptx=FILE
+
+  Don't run the program, but instead dump the PTX-compiled version of
+  the embedded kernels to the indicated file.
+
+--load-cuda=FILE
+
+  Instead of using the embedded CUDA kernels, load them from the
+  indicated file.
+
+--load-ptx=FILE
+
+  Load PTX code from the indicated file.
+
+--nvrtc-option=OPT
+
+  Add an additional build option to the string passed to NVRTC.  Refer
+  to the CUDA documentation for which options are supported.  Be
+  careful - some options can easily result in invalid results.
+
+--print-sizes
+
+  Print all sizes that can be set with ``-size`` or ``--tuning``.
+
+--size=NAME=INT
+
+  Set a configurable run-time parameter to the given value.  Use
+  ``--print-sizes`` to see which are available.
+
+--tuning=FILE
+
+  Read size=value assignments from the given file.
+
+ENVIRONMENT
+===========
+
+If run without ``--library``, ``futhark cuda`` will invoke ``gcc(1)``
+to compile the generated C program into a binary.  This only works if
+``gcc`` can find the necessary CUDA libraries.  On most systems, CUDA
+is installed in ``/usr/local/cuda``, which is not part of the default
+``gcc`` search path.  You may need to set the following environment
+variables before running ``futhark cuda``::
+
+  LIBRARY_PATH=/usr/local/cuda/lib64
+  LD_LIBRARY_PATH=/usr/local/cuda/lib64/
+  CPATH=/usr/local/cuda/include
 
 SEE ALSO
 ========
diff --git a/docs/man/futhark-opencl.rst b/docs/man/futhark-opencl.rst
--- a/docs/man/futhark-opencl.rst
+++ b/docs/man/futhark-opencl.rst
@@ -23,6 +23,10 @@
 ``-std=c99``. The resulting program will otherwise behave exactly as
 one compiled with ``futhark c``.
 
+``futhark opencl`` uses ``-lOpenCL`` to link (``-framework OpenCL`` on
+macOS).  If using ``--library``, you will need to do the same when
+linking the final binary.
+
 OPTIONS
 =======
 
@@ -51,6 +55,101 @@
 
 --Werror
   Treat warnings as errors.
+
+EXECUTABLE OPTIONS
+==================
+
+Generated executables accept the same options as those generated by
+:ref:`futhark-c(1)`.  For the ``-t`` option, The time taken to perform
+device setup or teardown, including writing the input or reading the
+result, is not included in the measurement. In particular, this means
+that timing starts after all kernels have been compiled and data has
+been copied to the device buffers but before setting any kernel
+arguments. Timing stops after the kernels are done running, but before
+data has been read from the buffers or the buffers have been released.
+
+The following additional options are accepted.
+
+--build-option=OPT
+
+  Add an additional build option to the string passed to
+  ``clBuildProgram()``.  Refer to the OpenCL documentation for which
+  options are supported.  Be careful - some options can easily
+  result in invalid results.
+
+--default-group-size=INT
+
+  The default size of OpenCL workgroups that are launched.  Capped
+  to the hardware limit if necessary.
+
+--default-num-groups=INT
+
+  The default number of OpenCL workgroups that are launched.
+
+--default-threshold=INT
+
+  The default parallelism threshold used for comparisons when
+  selecting between code versions generated by incremental flattening.
+  Intuitively, the amount of parallelism needed to saturate the GPU.
+
+--default-tile-size=INT
+
+  The default tile size used when performing two-dimensional tiling
+  (the workgroup size will be the square of the tile size).
+
+-d, --device=NAME
+
+  Use the first OpenCL device whose name contains the given string.
+  The special string ``#k``, where ``k`` is an integer, can be used to
+  pick the *k*-th device, numbered from zero.  If used in conjunction
+  with ``-p``, only the devices from matching platforms are
+  considered.
+
+--dump-opencl=FILE
+
+  Don't run the program, but instead dump the embedded OpenCL program
+  to the indicated file.  Useful if you want to see what is actually
+  being executed.
+
+--dump-opencl-binary=FILE
+
+  Don't run the program, but instead dump the compiled version of
+  the embedded OpenCL program to the indicated file.  On NVIDIA
+  platforms, this will be PTX code.
+
+--load-opencl=FILE
+
+  Instead of using the embedded OpenCL program, load it from the
+  indicated file.
+
+--load-opencl-binary=FILE
+
+  Load an OpenCL binary from the indicated file.
+
+-p, --platform=NAME
+
+  Use the first OpenCL platform whose name contains the given string.
+  The special string ``#k``, where ``k`` is an integer, can be used to
+  pick the *k*-th platform, numbered from zero.
+
+--print-sizes
+
+  Print all sizes that can be set with ``-size`` or ``--tuning``.
+
+-P, --profile
+
+  Gather profiling data while executing and print out a summary at the
+  end.  When ``-r`` is used, only the last run will be profiled.
+  Implied by ``-D``.
+
+--size=NAME=INT
+
+  Set a configurable run-time parameter to the given value.  Use
+  ``--print-sizes`` to see which are available.
+
+--tuning=FILE
+
+  Read size=value assignments from the given file.
 
 SEE ALSO
 ========
diff --git a/docs/man/futhark-test.rst b/docs/man/futhark-test.rst
--- a/docs/man/futhark-test.rst
+++ b/docs/man/futhark-test.rst
@@ -50,8 +50,8 @@
 the case of arrays.  When ``futhark test`` is run, a file located in a
 ``data/`` subdirectory, containing values of the indicated types and
 shapes is, automatically constructed with ``futhark-dataset``.  Apart
-from sizes, integer constants (without any type suffix) are also
-permitted.  These become ``i32`` values.
+from sizes, integer constants (with or without type suffix) are also
+permitted.
 
 If ``input`` is followed by an ``@`` and a file name (which must not
 contain any whitespace) instead of curly braces, values will be read
@@ -125,6 +125,12 @@
 
 -C
   Compile the programs, but do not run them.
+
+
+--concurrency=NUM
+
+  The number of tests to run concurrently.  Defaults to the number of
+  (hyper-)cores available.
 
 --exclude=tag
 
diff --git a/futhark.cabal b/futhark.cabal
--- a/futhark.cabal
+++ b/futhark.cabal
@@ -4,10 +4,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: b3f4de758564b29b93d0b51ac0628666279014b6a327dfe8d83b743ad959b249
+-- hash: f4cfd9b833eff0672980c67287441d068079b0a227279aa3a06a58262a3833c6
 
 name:           futhark
-version:        0.13.2
+version:        0.14.1
 synopsis:       An optimising compiler for a functional, array-oriented language.
 description:    Futhark is a small programming language designed to be compiled to
                 efficient parallel code. It is a statically typed, data-parallel,
@@ -311,7 +311,7 @@
     , language-c-quote >=0.12
     , mainland-pretty >=0.6.1
     , markdown >=0.1.16
-    , megaparsec >=7.0.1
+    , megaparsec >=8.0.0
     , mtl >=2.2.1
     , neat-interpolation >=0.3
     , parallel >=3.2.1.0
diff --git a/futlib/math.fut b/futlib/math.fut
--- a/futlib/math.fut
+++ b/futlib/math.fut
@@ -61,15 +61,15 @@
   val lowest: t
 
   -- | Returns zero on empty input.
-  val sum: []t -> t
+  val sum [n]: [n]t -> t
 
   -- | Returns one on empty input.
-  val product: []t -> t
+  val product [n]: [n]t -> t
 
   -- | Returns `lowest` on empty input.
-  val maximum: []t -> t
+  val maximum [n]: [n]t -> t
   -- | Returns `highest` on empty input.
-  val minimum: []t -> t
+  val minimum [n]: [n]t -> t
 }
 
 -- | An extension of `numeric`@mtype that provides facilities that are
diff --git a/package.yaml b/package.yaml
--- a/package.yaml
+++ b/package.yaml
@@ -1,5 +1,5 @@
 name: futhark
-version: "0.13.2"
+version: "0.14.1"
 synopsis: An optimising compiler for a functional, array-oriented language.
 description: |
   Futhark is a small programming language designed to be compiled to
@@ -46,7 +46,7 @@
     - srcloc >= 0.4
     - language-c-quote >= 0.12
     - mainland-pretty >= 0.6.1
-    - megaparsec >= 7.0.1
+    - megaparsec >= 8.0.0
     - parser-combinators >= 1.0.0
     - regex-tdfa >= 1.2
     - filepath >= 1.4.1.1
diff --git a/rts/c/opencl.h b/rts/c/opencl.h
--- a/rts/c/opencl.h
+++ b/rts/c/opencl.h
@@ -504,6 +504,7 @@
                                                   const char *extra_build_opts[]) {
   int error;
 
+  free_list_init(&ctx->free_list);
   ctx->queue = queue;
 
   OPENCL_SUCCEED_FATAL(clGetCommandQueueInfo(ctx->queue, CL_QUEUE_CONTEXT, sizeof(cl_context), &ctx->ctx, NULL));
@@ -727,8 +728,6 @@
                                const char *extra_build_opts[]) {
 
   ctx->lockstep_width = 0; // Real value set later.
-
-  free_list_init(&ctx->free_list);
 
   struct opencl_device_option device_option = get_preferred_device(&ctx->cfg);
 
diff --git a/rts/c/panic.h b/rts/c/panic.h
--- a/rts/c/panic.h
+++ b/rts/c/panic.h
@@ -20,7 +20,7 @@
 static char* msgprintf(const char *s, ...) {
   va_list vl;
   va_start(vl, s);
-  size_t needed = 1 + vsnprintf(NULL, 0, s, vl);
+  size_t needed = 1 + (size_t)vsnprintf(NULL, 0, s, vl);
   char *buffer = (char*) malloc(needed);
   va_start(vl, s); /* Must re-init. */
   vsnprintf(buffer, needed, s, vl);
diff --git a/rts/c/values.h b/rts/c/values.h
--- a/rts/c/values.h
+++ b/rts/c/values.h
@@ -38,7 +38,7 @@
   int i = 0;
   while (i < bufsize) {
     int c = getchar();
-    buf[i] = c;
+    buf[i] = (char)c;
 
     if (c == EOF) {
       buf[i] = 0;
@@ -47,7 +47,7 @@
       // Line comment, so skip to end of line and start over.
       for (; c != '\n' && c != EOF; c = getchar());
       goto start;
-    } else if (!constituent(c)) {
+    } else if (!constituent((char)c)) {
       if (i == 0) {
         // We permit single-character tokens that are not
         // constituents; this lets things like ']' and ',' be
@@ -89,7 +89,7 @@
   if (reader->n_elems_used == reader->n_elems_space) {
     reader->n_elems_space *= 2;
     reader->elems = (char*) realloc(reader->elems,
-                                    reader->n_elems_space * reader->elem_size);
+                                    (size_t)(reader->n_elems_space * reader->elem_size));
   }
 
   ret = reader->elem_reader(buf, reader->elems + reader->n_elems_used * reader->elem_size);
@@ -102,12 +102,12 @@
 }
 
 static int read_str_array_elems(char *buf, int bufsize,
-                                struct array_reader *reader, int dims) {
+                                struct array_reader *reader, int64_t dims) {
   int ret;
   int first = 1;
-  char *knows_dimsize = (char*) calloc(dims,sizeof(char));
+  char *knows_dimsize = (char*) calloc((size_t)dims, sizeof(char));
   int cur_dim = dims-1;
-  int64_t *elems_read_in_dim = (int64_t*) calloc(dims,sizeof(int64_t));
+  int64_t *elems_read_in_dim = (int64_t*) calloc((size_t)dims, sizeof(int64_t));
 
   while (1) {
     next_token(buf, bufsize);
@@ -202,7 +202,7 @@
 
     next_token(buf, bufsize);
 
-    if (sscanf(buf, "%"SCNi64, &shape[i]) != 1) {
+    if (sscanf(buf, "%"SCNu64, &shape[i]) != 1) {
       return 1;
     }
 
@@ -257,7 +257,7 @@
   reader.n_elems_used = 0;
   reader.elem_size = elem_size;
   reader.n_elems_space = 16;
-  reader.elems = (char*) realloc(*data, elem_size*reader.n_elems_space);
+  reader.elems = (char*) realloc(*data, (size_t)(elem_size*reader.n_elems_space));
   reader.elem_reader = elem_reader;
 
   ret = read_str_array_elems(buf, sizeof(buf), &reader, dims);
@@ -285,7 +285,7 @@
   remove_underscores(buf);
   int j, x;
   if (sscanf(buf, "%i%n", &x, &j) == 1) {
-    *(int8_t*)dest = x;
+    *(int8_t*)dest = (int8_t)x;
     return !(strcmp(buf+j, "") == 0 || strcmp(buf+j, "i8") == 0);
   } else {
     return 1;
@@ -301,7 +301,7 @@
   remove_underscores(buf);
   int j, x;
   if (sscanf(buf, "%i%n", &x, &j) == 1) {
-    *(uint8_t*)dest = x;
+    *(uint8_t*)dest = (uint8_t)x;
     return !(strcmp(buf+j, "") == 0 || strcmp(buf+j, "u8") == 0);
   } else {
     return 1;
@@ -479,7 +479,7 @@
 struct primtype_info_t {
   const char binname[4]; // Used for parsing binary data.
   const char* type_name; // Same name as in Futhark.
-  const int size; // in bytes
+  const int64_t size; // in bytes
   const writer write_str; // Write in text format.
   const str_reader read_str; // Read in text format.
 };
@@ -606,9 +606,9 @@
           dims, expected_type->type_name, dims, bin_primtype->type_name);
   }
 
-  uint64_t elem_count = 1;
+  int64_t elem_count = 1;
   for (int i=0; i<dims; i++) {
-    uint64_t bin_shape;
+    int64_t bin_shape;
     ret = fread(&bin_shape, sizeof(bin_shape), 1, stdin);
     if (ret != 1) {
       panic(1, "binary-input: Couldn't read size for dimension %i of array.\n", i);
@@ -617,18 +617,18 @@
       flip_bytes(sizeof(bin_shape), (unsigned char*) &bin_shape);
     }
     elem_count *= bin_shape;
-    shape[i] = (int64_t) bin_shape;
+    shape[i] = bin_shape;
   }
 
-  size_t elem_size = expected_type->size;
-  void* tmp = realloc(*data, elem_count * elem_size);
+  int64_t elem_size = expected_type->size;
+  void* tmp = realloc(*data, (size_t)(elem_count * elem_size));
   if (tmp == NULL) {
     panic(1, "binary-input: Failed to allocate array of size %i.\n",
           elem_count * elem_size);
   }
   *data = tmp;
 
-  size_t num_elems_read = fread(*data, elem_size, elem_count, stdin);
+  int64_t num_elems_read = (int64_t)fread(*data, (size_t)elem_size, (size_t)elem_count, stdin);
   if (num_elems_read != elem_count) {
     panic(1, "binary-input: tried to read %i elements of an array, but only got %i elements.\n",
           elem_count, num_elems_read);
@@ -655,11 +655,11 @@
   if (rank==0) {
     elem_type->write_str(out, (void*)data);
   } else {
-    int64_t len = shape[0];
+    int64_t len = (int64_t)shape[0];
     int64_t slice_size = 1;
 
     int64_t elem_size = elem_type->size;
-    for (int64_t i = 1; i < rank; i++) {
+    for (int8_t i = 1; i < rank; i++) {
       slice_size *= shape[i];
     }
 
@@ -704,7 +704,7 @@
   fwrite(&rank, sizeof(int8_t), 1, out);
   fputs(elem_type->binname, out);
   if (shape != NULL) {
-    fwrite(shape, sizeof(int64_t), rank, out);
+    fwrite(shape, sizeof(int64_t), (size_t)rank, out);
   }
 
   if (IS_BIG_ENDIAN) {
@@ -715,7 +715,7 @@
       }
     }
   } else {
-    fwrite(data, elem_type->size, num_elems, out);
+    fwrite(data, (size_t)elem_type->size, (size_t)num_elems, out);
   }
 
   return 0;
@@ -737,8 +737,8 @@
     return expected_type->read_str(buf, dest);
   } else {
     read_bin_ensure_scalar(expected_type);
-    size_t elem_size = expected_type->size;
-    int num_elems_read = fread(dest, elem_size, 1, stdin);
+    int64_t elem_size = expected_type->size;
+    int num_elems_read = fread(dest, (size_t)elem_size, 1, stdin);
     if (IS_BIG_ENDIAN) {
       flip_bytes(elem_size, (unsigned char*) dest);
     }
diff --git a/rts/python/values.py b/rts/python/values.py
--- a/rts/python/values.py
+++ b/rts/python/values.py
@@ -299,17 +299,17 @@
 def read_str_empty_array(f, type_name, rank):
     parse_specific_string(f, 'empty')
     parse_specific_char(f, b'(')
-    smallest = 1
+    dims = []
     for i in range(rank):
         parse_specific_string(f, '[')
-        smallest = min(smallest, int(parse_int(f)))
+        dims += [int(parse_int(f))]
         parse_specific_string(f, ']')
-    if smallest != 0:
+    if np.product(dims) != 0:
         raise ValueError
     parse_specific_string(f, type_name)
     parse_specific_char(f, b')')
 
-    return None
+    return tuple(dims)
 
 def read_str_array_elems(f, elem_reader, type_name, rank):
     skip_spaces(f)
@@ -352,9 +352,9 @@
 
 def read_str_array(f, elem_reader, type_name, rank, bt):
     elems = read_str_array_helper(f, elem_reader, type_name, rank)
-    if elems == None:
+    if type(elems) == tuple:
         # Empty array
-        return np.empty([0]*rank, dtype=bt)
+        return np.empty(elems, dtype=bt)
     else:
         dims = expected_array_dims(elems, rank)
         verify_array_dims(elems, dims)
diff --git a/src/Futhark/Analysis/Alias.hs b/src/Futhark/Analysis/Alias.hs
--- a/src/Futhark/Analysis/Alias.hs
+++ b/src/Futhark/Analysis/Alias.hs
@@ -4,10 +4,13 @@
 -- module does not implement the aliasing logic itself, and derives
 -- its information from definitions in
 -- "Futhark.Representation.AST.Attributes.Aliases" and
--- "Futhark.Representation.Aliases".
+-- "Futhark.Representation.Aliases".  The alias information computed
+-- here will include transitive aliases (note that this is not what
+-- the building blocks do).
 module Futhark.Analysis.Alias
        ( aliasAnalysis
          -- * Ad-hoc utilities
+       , AliasTable
        , analyseFun
        , analyseStm
        , analyseExp
@@ -16,6 +19,9 @@
        )
        where
 
+import Data.List (foldl')
+import qualified Data.Map as M
+
 import Futhark.Representation.AST.Syntax
 import Futhark.Representation.Aliases
 
@@ -28,30 +34,61 @@
               FunDef lore -> FunDef (Aliases lore)
 analyseFun (FunDef entry fname restype params body) =
   FunDef entry fname restype params body'
-  where body' = analyseBody body
+  where body' = analyseBody mempty body
 
+-- | Pre-existing aliases for variables.  Used to add transitive
+-- aliases.
+type AliasTable = M.Map VName Names
+
 analyseBody :: (Attributes lore,
                 CanBeAliased (Op lore)) =>
-               Body lore -> Body (Aliases lore)
-analyseBody (Body lore origbnds result) =
-  let bnds' = fmap analyseStm origbnds
-  in mkAliasedBody lore bnds' result
+               AliasTable -> Body lore -> Body (Aliases lore)
+analyseBody atable (Body lore stms result) =
+  let (stms', _atable') = analyseStms atable stms
+  in mkAliasedBody lore stms' result
 
+analyseStms :: (Attributes lore, CanBeAliased (Op lore)) =>
+               AliasTable -> Stms lore -> (Stms (Aliases lore), AliasesAndConsumed)
+analyseStms orig_aliases =
+  foldl' f (mempty, (orig_aliases, mempty)) . stmsToList
+  where f (stms, aliases) stm =
+          let stm' = analyseStm (fst aliases) stm
+              atable' = trackAliases aliases stm'
+          in (stms<>oneStm stm', atable')
+
 analyseStm :: (Attributes lore, CanBeAliased (Op lore)) =>
-              Stm lore -> Stm (Aliases lore)
-analyseStm (Let pat (StmAux cs attr) e) =
-  let e' = analyseExp e
+              AliasTable -> Stm lore -> Stm (Aliases lore)
+analyseStm aliases (Let pat (StmAux cs attr) e) =
+  let e' = analyseExp aliases e
       pat' = addAliasesToPattern pat e'
       lore' = (Names' $ consumedInExp e', attr)
   in Let pat' (StmAux cs lore') e'
 
 analyseExp :: (Attributes lore, CanBeAliased (Op lore)) =>
-              Exp lore -> Exp (Aliases lore)
-analyseExp = mapExp analyse
+              AliasTable -> Exp lore -> Exp (Aliases lore)
+
+-- Would be better to put this in a BranchType annotation, but that
+-- requires a lot of other work.
+analyseExp aliases (If cond tb fb attr) =
+  let Body ((tb_als, tb_cons), tb_attr) tb_stms tb_res = analyseBody aliases tb
+      Body ((fb_als, fb_cons), fb_attr) fb_stms fb_res = analyseBody aliases fb
+      cons = tb_cons <> fb_cons
+      isConsumed v = any (`nameIn` unNames cons) $
+                     v : namesToList (M.findWithDefault mempty v aliases)
+      notConsumed = Names' . namesFromList .
+                    filter (not . isConsumed) .
+                    namesToList . unNames
+      tb_als' = map notConsumed tb_als
+      fb_als' = map notConsumed fb_als
+      tb' = Body ((tb_als', tb_cons), tb_attr) tb_stms tb_res
+      fb' = Body ((fb_als', fb_cons), fb_attr) fb_stms fb_res
+  in If cond tb' fb' attr
+
+analyseExp aliases e = mapExp analyse e
   where analyse =
           Mapper { mapOnSubExp = return
                  , mapOnVName = return
-                 , mapOnBody = const $ return . analyseBody
+                 , mapOnBody = const $ return . analyseBody aliases
                  , mapOnRetType = return
                  , mapOnBranchType = return
                  , mapOnFParam = return
@@ -62,7 +99,10 @@
 analyseLambda :: (Attributes lore, CanBeAliased (Op lore)) =>
                  Lambda lore -> Lambda (Aliases lore)
 analyseLambda lam =
-  let body = analyseBody $ lambdaBody lam
+  -- XXX: it may cause trouble that we pass mempty to analyseBody
+  -- here.  However, fixing this generally involves adding an
+  -- AliasTable argument to addOpAliases.
+  let body = analyseBody mempty $ lambdaBody lam
   in lam { lambdaBody = body
          , lambdaParams = lambdaParams lam
          }
diff --git a/src/Futhark/Analysis/SymbolTable.hs b/src/Futhark/Analysis/SymbolTable.hs
--- a/src/Futhark/Analysis/SymbolTable.hs
+++ b/src/Futhark/Analysis/SymbolTable.hs
@@ -35,6 +35,8 @@
   , consume
   , index
   , index'
+  , Indexed(..)
+  , indexedAddCerts
   , IndexOp(..)
     -- * Insertion
   , insertStm
@@ -56,7 +58,7 @@
   )
   where
 
-import Control.Arrow (second, (&&&))
+import Control.Arrow ((&&&))
 import Control.Monad
 import Control.Monad.Reader
 import Data.Ord
@@ -164,8 +166,24 @@
                          availableAtClosestLoop = namesFromList $ M.keys $ bindings vtable
                        }
 
+-- | The result of indexing a delayed array.
+data Indexed = Indexed Certificates (PrimExp VName)
+               -- ^ A PrimExp based on the indexes (that is, without
+               -- accessing any actual array).
+             | IndexedArray Certificates VName [PrimExp VName]
+               -- ^ The indexing corresponds to another (perhaps more
+               -- advantageous) array.
+
+indexedAddCerts :: Certificates -> Indexed -> Indexed
+indexedAddCerts cs1 (Indexed cs2 v) = Indexed (cs1<>cs2) v
+indexedAddCerts cs1 (IndexedArray cs2 arr v) = IndexedArray (cs1<>cs2) arr v
+
+instance FreeIn Indexed where
+  freeIn' (Indexed cs v) = freeIn' cs <> freeIn' v
+  freeIn' (IndexedArray cs arr v) = freeIn' cs <> freeIn' arr <> freeIn' v
+
 -- | Indexing a delayed array if possible.
-type IndexArray = [PrimExp VName] -> Maybe (PrimExp VName, Certificates)
+type IndexArray = [PrimExp VName] -> Maybe Indexed
 
 data Entry lore = LoopVar (LoopVarEntry lore)
                 | LetBound (LetBoundEntry lore)
@@ -364,7 +382,7 @@
 available name = maybe False (not . consumed) . M.lookup name . bindings
 
 index :: Attributes lore => VName -> [SubExp] -> SymbolTable lore
-      -> Maybe (PrimExp VName, Certificates)
+      -> Maybe Indexed
 index name is table = do
   is' <- mapM asPrimExp is
   index' name is' table
@@ -373,7 +391,7 @@
           return $ primExpFromSubExp t i
 
 index' :: VName -> [PrimExp VName] -> SymbolTable lore
-       -> Maybe (PrimExp VName, Certificates)
+       -> Maybe Indexed
 index' name is vtable = do
   entry <- lookup name vtable
   case entry of
@@ -407,7 +425,7 @@
 class IndexOp op where
   indexOp :: (Attributes lore, IndexOp (Op lore)) =>
              SymbolTable lore -> Int -> op
-          -> [PrimExp VName] -> Maybe (PrimExp VName, Certificates)
+          -> [PrimExp VName] -> Maybe Indexed
   indexOp _ _ _ _ = Nothing
 
 instance IndexOp () where
@@ -420,15 +438,15 @@
 
 indexExp _ (BasicOp (Iota _ x s to_it)) _ [i]
   | IntType from_it <- primExpType i =
-      Just ( ConvOpExp (SExt from_it to_it) i
-             * primExpFromSubExp (IntType to_it) s
-             + primExpFromSubExp (IntType to_it) x
-           , mempty)
+      Just $ Indexed mempty $
+       ConvOpExp (SExt from_it to_it) i
+       * primExpFromSubExp (IntType to_it) s
+       + primExpFromSubExp (IntType to_it) x
 
 indexExp table (BasicOp (Replicate (Shape ds) v)) _ is
   | length ds == length is,
     Just (Prim t) <- lookupSubExpType v table =
-      Just (primExpFromSubExp t v, mempty)
+      Just $ Indexed mempty $ primExpFromSubExp t v
 
 indexExp table (BasicOp (Replicate (Shape [_]) (Var v))) _ (_:is) =
   index' v is table
@@ -477,7 +495,7 @@
     , letBoundScalExp =
       runReader (toScalExp (`lookupScalExp` vtable) (stmExp bnd)) types
     , letBoundStmDepth = 0
-    , letBoundIndex = \k -> fmap (second (<>(stmAuxCerts $ stmAux bnd))) .
+    , letBoundIndex = \k -> fmap (indexedAddCerts (stmAuxCerts $ stmAux bnd)) .
                             indexExp vtable (stmExp bnd) k
     , letBoundConsumed = False
     }
diff --git a/src/Futhark/Bench.hs b/src/Futhark/Bench.hs
--- a/src/Futhark/Bench.hs
+++ b/src/Futhark/Bench.hs
@@ -222,14 +222,15 @@
 
 -- | Compile and produce reference datasets.
 prepareBenchmarkProgram :: MonadIO m =>
-                           CompileOptions
+                           Maybe Int
+                        -> CompileOptions
                         -> FilePath
                         -> [InputOutputs]
                         -> m (Either (String, Maybe SBS.ByteString) ())
-prepareBenchmarkProgram opts program cases = do
+prepareBenchmarkProgram concurrency opts program cases = do
   let futhark = compFuthark opts
 
-  ref_res <- runExceptT $ ensureReferenceOutput futhark "c" program cases
+  ref_res <- runExceptT $ ensureReferenceOutput concurrency futhark "c" program cases
   case ref_res of
     Left err ->
       return $ Left ("Reference output generation for " ++ program ++ " failed:\n" ++
diff --git a/src/Futhark/CLI/Autotune.hs b/src/Futhark/CLI/Autotune.hs
--- a/src/Futhark/CLI/Autotune.hs
+++ b/src/Futhark/CLI/Autotune.hs
@@ -73,53 +73,58 @@
 
 type DatasetName = String
 
-prepare :: AutotuneOptions -> FilePath -> IO [(DatasetName, RunDataset)]
+prepare :: AutotuneOptions -> FilePath -> IO [(DatasetName, RunDataset, T.Text)]
 prepare opts prog = do
   spec <- testSpecFromFileOrDie prog
   copts <- compileOptions opts
 
   truns <-
     case testAction spec of
-      RunCases ios _ _
-        | Just runs <-
-            iosTestRuns <$> find ((=="main") . iosEntryPoint) ios -> do
-            res <- prepareBenchmarkProgram copts prog ios
+      RunCases ios _ _ | not $ null ios -> do
+            when (optVerbose opts > 1) $
+               putStrLn $
+                 unwords ("Entry points:" : map (T.unpack . iosEntryPoint) ios)
+
+            res <- prepareBenchmarkProgram Nothing copts prog ios
             case res of
               Left (err, errstr) -> do
                 putStrLn err
                 maybe (return ()) SBS.putStrLn errstr
                 exitFailure
               Right () ->
-                return runs
+                return ios
       _ ->
-        fail "Program does not have a 'main' entry point with datasets."
+        fail "Unsupported test spec."
 
-  let runnableDataset trun =
+  let runnableDataset entry_point trun =
         case runExpectedResult trun of
           Succeeds expected
             | null (runTags trun `intersect` ["notune", "disable"]) ->
-                Just (runDescription trun, run trun expected)
+                Just (runDescription trun, run entry_point trun expected)
 
           _ -> Nothing
 
   -- We wish to let datasets run for the untuned time + 20% + 1 second.
   let timeout elapsed = ceiling (elapsed * 1.2) + 1
 
-  forM (mapMaybe runnableDataset truns) $ \(dataset, do_run) -> do
-    bef <- toRational <$> getPOSIXTime
-    res <- do_run 60000 [] RunBenchmark
-    aft <- toRational <$> getPOSIXTime
-    case res of Left err -> do
-                  putStrLn $ "Error when running " ++ prog ++ ":"
-                  putStrLn err
-                  exitFailure
-                Right _ -> do
-                  let t = timeout $ aft - bef
-                  putStrLn $ "Calculated timeout for " ++ dataset ++
-                    " : " ++ show t ++ "s"
-                  return (dataset, do_run t)
+  fmap concat $ forM truns $ \ios ->
+    forM (mapMaybe (runnableDataset $ iosEntryPoint ios)
+                   (iosTestRuns ios)) $
+      \(dataset, do_run) -> do
+      bef <- toRational <$> getPOSIXTime
+      res <- do_run 60000 [] RunBenchmark
+      aft <- toRational <$> getPOSIXTime
+      case res of Left err -> do
+                    putStrLn $ "Error when running " ++ prog ++ ":"
+                    putStrLn err
+                    exitFailure
+                  Right _ -> do
+                    let t = timeout $ aft - bef
+                    putStrLn $ "Calculated timeout for " ++ dataset ++
+                      " : " ++ show t ++ "s"
+                    return (dataset, do_run t, iosEntryPoint ios)
 
-  where run trun expected timeout path purpose = do
+  where run entry_point trun expected timeout path purpose = do
           let opts' = case purpose of RunSample -> opts { optRuns = 1 }
                                       RunBenchmark -> opts
 
@@ -131,13 +136,12 @@
               ropts = runOptions path timeout opts'
 
           when (optVerbose opts > 1) $
-            putStrLn $ "Running with options: " ++
-            unwords (runExtraOptions ropts)
+            putStrLn $ "Running with options: " ++ unwords (runExtraOptions ropts)
 
           either (Left . T.unpack) (Right . averageRuntime) <$>
-            benchmarkDataset ropts prog "main"
+            benchmarkDataset ropts prog entry_point
             (runInput trun) expected
-            (testRunReferenceOutput prog "main" trun)
+            (testRunReferenceOutput prog entry_point trun)
 
 --- Benchmarking a program
 
@@ -209,57 +213,65 @@
            xmax `min` ymax)
 
 tuneThreshold :: AutotuneOptions
-              -> [(DatasetName, RunDataset)]
+              -> [(DatasetName, RunDataset, T.Text)]
               -> Path -> (String, Path)
               -> IO Path
 tuneThreshold opts datasets already_tuned (v, v_path) = do
   ranges <-
-    forM datasets $ \(dataset_name, run) -> do
+    forM datasets $ \(dataset_name, run, entry_point) ->
 
-    putStrLn $ unwords ["Tuning", v, "on dataset", dataset_name]
+    if not $ isPrefixOf (T.unpack entry_point ++ ".") v then do
+        when (optVerbose opts > 0) $
+          putStrLn $ unwords [v, "is irrelevant for", T.unpack entry_point]
+        return (thresholdMin, thresholdMax)
+    else do
 
-    sample_run <- run path RunSample
+      putStrLn $ unwords ["Tuning", v, "on entry point", T.unpack entry_point,
+                          "and dataset", dataset_name]
 
-    case sample_run of
-      Left err -> do
-        -- If the sampling run fails, we treat it as zero information.
-        -- One of our ancestor thresholds will have be set such that
-        -- this path is never taken.
-        when (optVerbose opts > 0) $ putStrLn $ "Sampling run failed:\n" ++ err
-        return (thresholdMin, thresholdMax)
-      Right (cmps, _) ->
-        case lookup v cmps of
-          Nothing -> do
-            -- A missing comparison is not necessarily a bug - it may
-            -- simply mean that this comparison is inside a loop or
-            -- branch that is never reached for this dataset.  In such
-            -- cases, the optimal range is universal.
-            when (optVerbose opts > 0) $ putStrLn "Irrelevant for dataset.\n"
-            return (thresholdMin, thresholdMax)
-          Just e_par -> do
-            t_run <- run path_t RunBenchmark
-            f_run <- run path_f RunBenchmark
+      sample_run <- run path RunSample
 
-            let prefer_t = (thresholdMin, e_par)
-                prefer_f = (e_par+1, thresholdMax)
+      case sample_run of
+        Left err -> do
+          -- If the sampling run fails, we treat it as zero information.
+          -- One of our ancestor thresholds will have be set such that
+          -- this path is never taken.
+          when (optVerbose opts > 0) $ putStrLn $
+            "Sampling run failed:\n" ++ err
+          return (thresholdMin, thresholdMax)
+        Right (cmps, _) ->
+          case lookup v cmps of
+            Nothing -> do
+              -- A missing comparison is not necessarily a bug - it may
+              -- simply mean that this comparison is inside a loop or
+              -- branch that is never reached for this dataset.  In such
+              -- cases, the optimal range is universal.
+              when (optVerbose opts > 0) $ putStrLn "Irrelevant for dataset.\n"
+              return (thresholdMin, thresholdMax)
+            Just e_par -> do
+              t_run <- run path_t RunBenchmark
+              f_run <- run path_f RunBenchmark
 
-            case (t_run, f_run) of
-              (Left err, _) -> do
-                when (optVerbose opts > 0) $
-                  putStrLn $ "True comparison run failed:\n" ++ err
-                return prefer_f
-              (_, Left err) -> do
-                when (optVerbose opts > 0) $
-                  putStrLn $ "False comparison run failed:\n" ++ err
-                return prefer_t
-              (Right (_, runtime_t), Right (_, runtime_f)) ->
-                if runtime_t < runtime_f
-                then do when (optVerbose opts > 0) $
-                          putStrLn "True branch is fastest."
-                        return prefer_t
-                else do when (optVerbose opts > 0) $
-                          putStrLn "False branch is fastest."
-                        return prefer_f
+              let prefer_t = (thresholdMin, e_par)
+                  prefer_f = (e_par+1, thresholdMax)
+
+              case (t_run, f_run) of
+                (Left err, _) -> do
+                  when (optVerbose opts > 0) $
+                    putStrLn $ "True comparison run failed:\n" ++ err
+                  return prefer_f
+                (_, Left err) -> do
+                  when (optVerbose opts > 0) $
+                    putStrLn $ "False comparison run failed:\n" ++ err
+                  return prefer_t
+                (Right (_, runtime_t), Right (_, runtime_f)) ->
+                  if runtime_t < runtime_f
+                  then do when (optVerbose opts > 0) $
+                            putStrLn "True branch is fastest."
+                          return prefer_t
+                  else do when (optVerbose opts > 0) $
+                            putStrLn "False branch is fastest."
+                          return prefer_f
 
   let (_lower, upper) = intersectRanges ranges
   return $ (v,upper) : already_tuned
diff --git a/src/Futhark/CLI/Bench.hs b/src/Futhark/CLI/Bench.hs
--- a/src/Futhark/CLI/Bench.hs
+++ b/src/Futhark/CLI/Bench.hs
@@ -39,11 +39,12 @@
                    , optIgnoreFiles :: [Regex]
                    , optEntryPoint :: Maybe String
                    , optTuning :: Maybe String
+                   , optConcurrency :: Maybe Int
                    }
 
 initialBenchOptions :: BenchOptions
 initialBenchOptions = BenchOptions "c" Nothing "" 10 [] Nothing (-1) False
-                      ["nobench", "disable"] [] Nothing (Just "tuning")
+                      ["nobench", "disable"] [] Nothing (Just "tuning") Nothing
 
 runBenchmarks :: BenchOptions -> [FilePath] -> IO ()
 runBenchmarks opts paths = do
@@ -53,8 +54,12 @@
   hSetBuffering stdout LineBuffering
 
   benchmarks <- filter (not . ignored . fst) <$> testSpecsFromPathsOrDie paths
+  -- Try to avoid concurrency at both program and data set level.
+  let opts' = if length paths /= 1
+              then opts { optConcurrency = Just 1}
+              else opts
   (skipped_benchmarks, compiled_benchmarks) <-
-    partitionEithers <$> pmapIO (compileBenchmark opts) benchmarks
+    partitionEithers <$> pmapIO (optConcurrency opts) (compileBenchmark opts') benchmarks
 
   when (anyFailedToCompile skipped_benchmarks) exitFailure
 
@@ -105,7 +110,7 @@
 
         compile_opts <- compileOptions opts
 
-        res <- prepareBenchmarkProgram compile_opts program cases
+        res <- prepareBenchmarkProgram (optConcurrency opts) compile_opts program cases
 
         case res of
           Left (err, errstr) -> do
@@ -249,6 +254,16 @@
   , Option [] ["no-tuning"]
     (NoArg $ Right $ \config -> config { optTuning = Nothing })
     "Do not load tuning files."
+  , Option [] ["concurrency"]
+    (ReqArg (\n ->
+               case reads n of
+                 [(n', "")]
+                   | n' > 0 ->
+                   Right $ \config -> config { optConcurrency = Just n' }
+                 _ ->
+                   Left $ error $ "'" ++ n ++ "' is not a positive integer.")
+    "NUM")
+    "Number of benchmarks to prepare (not run) concurrently."
   ]
   where max_timeout :: Int
         max_timeout = maxBound `div` 1000000
diff --git a/src/Futhark/CLI/REPL.hs b/src/Futhark/CLI/REPL.hs
--- a/src/Futhark/CLI/REPL.hs
+++ b/src/Futhark/CLI/REPL.hs
@@ -16,6 +16,7 @@
 import Control.Monad.IO.Class
 import Control.Monad.State
 import Control.Monad.Except
+import qualified Data.List.NonEmpty as NE
 import qualified Data.Text as T
 import qualified Data.Text.IO as T
 import NeatInterpolation (text)
@@ -23,6 +24,7 @@
 import System.FilePath
 import System.Console.GetOpt
 import System.IO
+import Text.Read (readMaybe)
 import qualified System.Console.Haskeline as Haskeline
 
 import Language.Futhark
@@ -34,7 +36,7 @@
 import Futhark.Compiler
 import Futhark.Pipeline
 import Futhark.Util.Options
-import Futhark.Util (toPOSIX, maybeHead)
+import Futhark.Util (toPOSIX)
 
 import qualified Language.Futhark.Interpreter as I
 
@@ -111,12 +113,20 @@
             "The entry point to execute."
           ]
 
+-- | Representation of breaking at a breakpoint, to allow for
+-- navigating through the stack frames and such.
+data Breaking = Breaking { breakingStack :: NE.NonEmpty I.StackFrame
+                         , breakingAt :: Int
+                           -- ^ Index of the current breakpoint (with
+                           -- 0 being the outermost).
+                         }
+
 data FutharkiState =
   FutharkiState { futharkiImports :: Imports
                 , futharkiNameSource :: VNameSource
                 , futharkiCount :: Int
                 , futharkiEnv :: (T.Env, I.Ctx)
-                , futharkiBreaking :: Maybe Loc
+                , futharkiBreaking :: Maybe Breaking
                   -- ^ Are we currently stopped at a breakpoint?
                 , futharkiSkipBreaks :: [Loc]
                 -- ^ Skip breakpoints at these locations.
@@ -272,24 +282,32 @@
     where showErr :: Show a => Either a b -> Either String b
           showErr = either (Left . show) Right
 
+prettyBreaking :: Breaking -> String
+prettyBreaking b =
+  prettyStacktrace (breakingAt b) $ map locStr $ NE.toList $ breakingStack b
+
 runInterpreter :: F I.ExtOp a -> FutharkiM (Either I.InterpreterError a)
 runInterpreter m = runF m (return . Right) intOp
   where
     intOp (I.ExtOpError err) =
       return $ Left err
     intOp (I.ExtOpTrace w v c) = do
-      liftIO $ putStrLn $ "Trace at " ++ locStr w ++ ": " ++ v
+      liftIO $ putStrLn $ "Trace at " ++ locStr (srclocOf w) ++ ": " ++ v
       c
-    intOp (I.ExtOpBreak w ctx tenv c) = do
+    intOp (I.ExtOpBreak callstack c) = do
       s <- get
 
-      -- Are we supposed to skip this breakpoint?
-      let loc = maybe noLoc locOf $ maybeHead w
+      let top = NE.head callstack
+          ctx = I.stackFrameCtx top
+          tenv = I.typeEnv $ I.ctxEnv ctx
+          breaking = Breaking callstack 0
 
-      -- We do not want recursive breakpoints.  It could work fine
-      -- technically, but is probably too confusing to be useful.
-      unless (isJust (futharkiBreaking s) || loc `elem` futharkiSkipBreaks s) $ do
-        liftIO $ putStrLn $ "Breaking at " ++ intercalate " -> " (map locStr w) ++ "."
+      -- Are we supposed to skip this breakpoint?  Also, We do not
+      -- want recursive breakpoints.  It could work fine technically,
+      -- but is probably too confusing to be useful.
+      unless (isJust (futharkiBreaking s) || locOf top `elem` futharkiSkipBreaks s) $ do
+        liftIO $ putStrLn $ "Breakpoint at " ++ locStr top
+        liftIO $ putStrLn $ prettyBreaking breaking
         liftIO $ putStrLn "<Enter> to continue."
 
         -- Note the cleverness to preserve the Haskeline session (for
@@ -299,7 +317,8 @@
           runStateT (runExceptT $ runFutharkiM $ forever readEvalPrint)
           s { futharkiEnv = (tenv, ctx)
             , futharkiCount = futharkiCount s + 1
-            , futharkiBreaking = Just loc }
+            , futharkiBreaking = Just breaking
+            }
 
         case stop of
           Left (Load file) -> throwError $ Load file
@@ -315,7 +334,7 @@
         intOp (I.ExtOpTrace w v c) = do
           liftIO $ putStrLn $ "Trace at " ++ locStr w ++ ": " ++ v
           c
-        intOp (I.ExtOpBreak _ _ _ c) = c
+        intOp (I.ExtOpBreak _ c) = c
 
 type Command = T.Text -> FutharkiM ()
 
@@ -354,12 +373,30 @@
 
 unbreakCommand :: Command
 unbreakCommand _ = do
-  breaking <- gets futharkiBreaking
-  case breaking of
+  top <- fmap (NE.head . breakingStack) <$> gets futharkiBreaking
+  case top of
     Nothing -> liftIO $ putStrLn "Not currently stopped at a breakpoint."
-    Just loc -> do modify $ \s -> s { futharkiSkipBreaks = loc : futharkiSkipBreaks s }
-                   throwError Stop
+    Just top' -> do modify $ \s -> s { futharkiSkipBreaks = locOf top' : futharkiSkipBreaks s }
+                    throwError Stop
 
+frameCommand :: Command
+frameCommand which = do
+  maybe_stack <- fmap breakingStack <$> gets futharkiBreaking
+  case (maybe_stack, readMaybe $ T.unpack which) of
+    (Just stack, Just i)
+      | frame:_ <- NE.drop i stack -> do
+          let breaking = Breaking stack i
+              ctx = I.stackFrameCtx frame
+              tenv = I.typeEnv $ I.ctxEnv ctx
+          modify $ \s -> s { futharkiEnv = (tenv, ctx)
+                           , futharkiBreaking = Just breaking
+                           }
+          liftIO $ putStrLn $ prettyBreaking breaking
+    (Just _, _) ->
+      liftIO $ putStrLn $ "Invalid stack index: " ++ T.unpack which
+    (Nothing, _) ->
+      liftIO $ putStrLn "Not stopped at a breakpoint."
+
 pwdCommand :: Command
 pwdCommand _ = liftIO $ putStrLn =<< getCurrentDirectory
 
@@ -387,9 +424,8 @@
 
   > :load foo.fut
 
-If the loading succeeds, any subsequentialy entered expressions entered
-subsequently will have access to the definition (such as function definitions)
-in the source file.
+If the loading succeeds, any expressions entered subsequently can use the
+declarations in the source file.
 
 Only one source file can be loaded at a time.  Using the :load command a
 second time will replace the previously loaded file.  It will also replace
@@ -405,6 +441,11 @@
             ("unbreak", (unbreakCommand, [text|
 Skip all future occurences of the current breakpoint.
 |])),
+            ("frame", (frameCommand, [text|
+While at a break point, jump to another stack frame, whose variables can then
+be inspected.  Resuming from the breakpoint will jump back to the innermost
+stack frame.
+|])),
             ("pwd", (pwdCommand, [text|
 Print the current working directory.
 |])),
@@ -415,5 +456,5 @@
 Print a list of commands and a description of their behaviour.
 |])),
             ("quit", (quitCommand, [text|
-Quit futharki.
+Exit REPL.
 |]))]
diff --git a/src/Futhark/CLI/Run.hs b/src/Futhark/CLI/Run.hs
--- a/src/Futhark/CLI/Run.hs
+++ b/src/Futhark/CLI/Run.hs
@@ -137,4 +137,4 @@
         intOp (I.ExtOpTrace w v c) = do
           liftIO $ putStrLn $ "Trace at " ++ locStr w ++ ": " ++ v
           c
-        intOp (I.ExtOpBreak _ _ _ c) = c
+        intOp (I.ExtOpBreak _ c) = c
diff --git a/src/Futhark/CLI/Test.hs b/src/Futhark/CLI/Test.hs
--- a/src/Futhark/CLI/Test.hs
+++ b/src/Futhark/CLI/Test.hs
@@ -168,7 +168,9 @@
           extra_options = configExtraCompilerOptions progs
       unless (mode == Compile) $
         context "Generating reference outputs" $
-        ensureReferenceOutput futhark "c" program ios
+        -- We probably get the concurrency at the test program level,
+        -- so force just one data set at a time here.
+        ensureReferenceOutput (Just 1) futhark "c" program ios
       unless (mode == Interpreted) $
         context ("Compiling with --backend=" <> T.pack backend) $ do
           compileTestProgram extra_options futhark backend program warnings
@@ -395,7 +397,7 @@
                testSpecsFromPathsOrDie paths
   testmvar <- newEmptyMVar
   reportmvar <- newEmptyMVar
-  concurrency <- getNumCapabilities
+  concurrency <- maybe getNumCapabilities pure $ configConcurrency config
   replicateM_ concurrency $ forkIO $ runTest testmvar reportmvar
 
   let (excluded, included) = partition (excludedTest config) all_tests
@@ -484,6 +486,7 @@
                   , configPrograms :: ProgConfig
                   , configExclude :: [T.Text]
                   , configLineOutput :: Bool
+                  , configConcurrency :: Maybe Int
                   }
 
 defaultConfig :: TestConfig
@@ -499,6 +502,7 @@
                              , configTuning = Just "tuning"
                              }
                            , configLineOutput = False
+                           , configConcurrency = Nothing
                            }
 
 data ProgConfig = ProgConfig
@@ -583,6 +587,16 @@
   , Option [] ["no-tuning"]
     (NoArg $ Right $ changeProgConfig $ \config -> config { configTuning = Nothing })
     "Do not load tuning files."
+  , Option [] ["concurrency"]
+    (ReqArg (\n ->
+               case reads n of
+                 [(n', "")]
+                   | n' > 0 ->
+                   Right $ \config -> config { configConcurrency = Just n' }
+                 _ ->
+                   Left $ error $ "'" ++ n ++ "' is not a positive integer.")
+    "NUM")
+    "Number of tests to run concurrently."
   ]
 
 main :: String -> [String] -> IO ()
diff --git a/src/Futhark/CodeGen/Backends/CCUDA.hs b/src/Futhark/CodeGen/Backends/CCUDA.hs
--- a/src/Futhark/CodeGen/Backends/CCUDA.hs
+++ b/src/Futhark/CodeGen/Backends/CCUDA.hs
@@ -16,6 +16,7 @@
 import Futhark.Representation.ExplicitMemory hiding (GetSize, CmpSizeLe, GetSizeMax)
 import Futhark.MonadFreshNames
 import Futhark.CodeGen.ImpCode.OpenCL
+import Futhark.CodeGen.Backends.COpenCL.Boilerplate (commonOptions)
 import Futhark.CodeGen.Backends.CCUDA.Boilerplate
 import Futhark.CodeGen.Backends.GenericC.Options
 
@@ -49,77 +50,36 @@
                             ]
 
 cliOptions :: [Option]
-cliOptions = [ Option { optionLongName = "dump-cuda"
-                      , optionShortName = Nothing
-                      , optionArgument = RequiredArgument "FILE"
-                      , optionAction = [C.cstm|{futhark_context_config_dump_program_to(cfg, optarg);
-                                                entry_point = NULL;}|]
-                      }
-             , Option { optionLongName = "load-cuda"
-                      , optionShortName = Nothing
-                      , optionArgument = RequiredArgument "FILE"
-                      , optionAction = [C.cstm|futhark_context_config_load_program_from(cfg, optarg);|]
-                      }
-             , Option { optionLongName = "dump-ptx"
-                      , optionShortName = Nothing
-                      , optionArgument = RequiredArgument "FILE"
-                      , optionAction = [C.cstm|{futhark_context_config_dump_ptx_to(cfg, optarg);
-                                                entry_point = NULL;}|]
-                      }
-             , Option { optionLongName = "load-ptx"
-                      , optionShortName = Nothing
-                      , optionArgument = RequiredArgument "FILE"
-                      , optionAction = [C.cstm|futhark_context_config_load_ptx_from(cfg, optarg);|]
-                      }
-             , Option { optionLongName = "nvrtc-option"
-                      , optionShortName = Nothing
-                      , optionArgument = RequiredArgument "OPT"
-                      , optionAction = [C.cstm|futhark_context_config_add_nvrtc_option(cfg, optarg);|]
-                      }
-             , Option { optionLongName = "print-sizes"
-                      , optionShortName = Nothing
-                      , optionArgument = NoArgument
-                      , optionAction = [C.cstm|{
-                          int n = futhark_get_num_sizes();
-                          for (int i = 0; i < n; i++) {
-                            printf("%s (%s)\n", futhark_get_size_name(i),
-                                                futhark_get_size_class(i));
-                          }
-                          exit(0);
-                        }|]
-                      }
-             , Option { optionLongName = "default-group-size"
-                      , optionShortName = Nothing
-                      , optionArgument = RequiredArgument "INT"
-                      , optionAction = [C.cstm|futhark_context_config_set_default_group_size(cfg, atoi(optarg));|]
-                      }
-             , Option { optionLongName = "default-num-groups"
-                      , optionShortName = Nothing
-                      , optionArgument = RequiredArgument "INT"
-                      , optionAction = [C.cstm|futhark_context_config_set_default_num_groups(cfg, atoi(optarg));|]
-                      }
-             , Option { optionLongName = "default-tile-size"
-                      , optionShortName = Nothing
-                      , optionArgument = RequiredArgument "INT"
-                      , optionAction = [C.cstm|futhark_context_config_set_default_tile_size(cfg, atoi(optarg));|]
-                      }
-             , Option { optionLongName = "default-threshold"
-                      , optionShortName = Nothing
-                      , optionArgument = RequiredArgument "INT"
-                      , optionAction = [C.cstm|futhark_context_config_set_default_threshold(cfg, atoi(optarg));|]
-                      }
-             , Option { optionLongName = "tuning"
-                 , optionShortName = Nothing
-                 , optionArgument = RequiredArgument "FILE"
-                 , optionAction = [C.cstm|{
-                     char *fname = optarg;
-                     char *ret = load_tuning_file(optarg, cfg, (int(*)(void*, const char*, size_t))
-                                                               futhark_context_config_set_size);
-                     if (ret != NULL) {
-                       panic(1, "When loading tuning from '%s': %s\n", optarg, ret);
-                     }}|]
-                 }
-             ]
+cliOptions =
+  commonOptions ++
+  [ Option { optionLongName = "dump-cuda"
+           , optionShortName = Nothing
+           , optionArgument = RequiredArgument "FILE"
+           , optionAction = [C.cstm|{futhark_context_config_dump_program_to(cfg, optarg);
+                                     entry_point = NULL;}|]
+           }
+  , Option { optionLongName = "load-cuda"
+           , optionShortName = Nothing
+           , optionArgument = RequiredArgument "FILE"
+           , optionAction = [C.cstm|futhark_context_config_load_program_from(cfg, optarg);|]
+           }
+  , Option { optionLongName = "dump-ptx"
+           , optionShortName = Nothing
+           , optionArgument = RequiredArgument "FILE"
+           , optionAction = [C.cstm|{futhark_context_config_dump_ptx_to(cfg, optarg);
+                                     entry_point = NULL;}|]
+           }
+  , Option { optionLongName = "load-ptx"
+           , optionShortName = Nothing
+           , optionArgument = RequiredArgument "FILE"
+           , optionAction = [C.cstm|futhark_context_config_load_ptx_from(cfg, optarg);|]
+           }
+  , Option { optionLongName = "nvrtc-option"
+           , optionShortName = Nothing
+           , optionArgument = RequiredArgument "OPT"
+           , optionAction = [C.cstm|futhark_context_config_add_nvrtc_option(cfg, optarg);|]
+           }
+  ]
 
 writeCUDAScalar :: GC.WriteScalar OpenCL ()
 writeCUDAScalar mem idx t "device" _ val = do
diff --git a/src/Futhark/CodeGen/Backends/COpenCL.hs b/src/Futhark/CodeGen/Backends/COpenCL.hs
--- a/src/Futhark/CodeGen/Backends/COpenCL.hs
+++ b/src/Futhark/CodeGen/Backends/COpenCL.hs
@@ -71,108 +71,52 @@
                              &ctx->$id:(kernelRuntime name))|]
 
 cliOptions :: [Option]
-cliOptions = [ Option { optionLongName = "platform"
-                      , optionShortName = Just 'p'
-                      , optionArgument = RequiredArgument "NAME"
-                      , optionAction = [C.cstm|futhark_context_config_set_platform(cfg, optarg);|]
-                      }
-             , Option { optionLongName = "device"
-                      , optionShortName = Just 'd'
-                      , optionArgument = RequiredArgument "NAME"
-                      , optionAction = [C.cstm|futhark_context_config_set_device(cfg, optarg);|]
-                      }
-             , Option { optionLongName = "default-group-size"
-                      , optionShortName = Nothing
-                      , optionArgument = RequiredArgument "INT"
-                      , optionAction = [C.cstm|futhark_context_config_set_default_group_size(cfg, atoi(optarg));|]
-                      }
-             , Option { optionLongName = "default-num-groups"
-                      , optionShortName = Nothing
-                      , optionArgument = RequiredArgument "INT"
-                      , optionAction = [C.cstm|futhark_context_config_set_default_num_groups(cfg, atoi(optarg));|]
-                      }
-             , Option { optionLongName = "default-tile-size"
-                      , optionShortName = Nothing
-                      , optionArgument = RequiredArgument "INT"
-                      , optionAction = [C.cstm|futhark_context_config_set_default_tile_size(cfg, atoi(optarg));|]
-                      }
-             , Option { optionLongName = "default-threshold"
-                      , optionShortName = Nothing
-                      , optionArgument = RequiredArgument "INT"
-                      , optionAction = [C.cstm|futhark_context_config_set_default_threshold(cfg, atoi(optarg));|]
-                      }
-             , Option { optionLongName = "dump-opencl"
-                      , optionShortName = Nothing
-                      , optionArgument = RequiredArgument "FILE"
-                      , optionAction = [C.cstm|{futhark_context_config_dump_program_to(cfg, optarg);
-                                                entry_point = NULL;}|]
-                      }
-             , Option { optionLongName = "load-opencl"
-                      , optionShortName = Nothing
-                      , optionArgument = RequiredArgument "FILE"
-                      , optionAction = [C.cstm|futhark_context_config_load_program_from(cfg, optarg);|]
-                      }
-             , Option { optionLongName = "dump-opencl-binary"
-                      , optionShortName = Nothing
-                      , optionArgument = RequiredArgument "FILE"
-                      , optionAction = [C.cstm|{futhark_context_config_dump_binary_to(cfg, optarg);
-                                                entry_point = NULL;}|]
-                      }
-             , Option { optionLongName = "load-opencl-binary"
-                      , optionShortName = Nothing
-                      , optionArgument = RequiredArgument "FILE"
-                      , optionAction = [C.cstm|futhark_context_config_load_binary_from(cfg, optarg);|]
-                      }
-             , Option { optionLongName = "build-option"
-                      , optionShortName = Nothing
-                      , optionArgument = RequiredArgument "OPT"
-                      , optionAction = [C.cstm|futhark_context_config_add_build_option(cfg, optarg);|]
-                      }
-             , Option { optionLongName = "print-sizes"
-                      , optionShortName = Nothing
-                      , optionArgument = NoArgument
-                      , optionAction = [C.cstm|{
-                          int n = futhark_get_num_sizes();
-                          for (int i = 0; i < n; i++) {
-                            printf("%s (%s)\n", futhark_get_size_name(i),
-                                                futhark_get_size_class(i));
-                          }
-                          exit(0);
-                        }|]
-                      }
-             , Option { optionLongName = "size"
-                      , optionShortName = Nothing
-                      , optionArgument = RequiredArgument "NAME=INT"
-                      , optionAction = [C.cstm|{
-                          char *name = optarg;
-                          char *equals = strstr(optarg, "=");
-                          char *value_str = equals != NULL ? equals+1 : optarg;
-                          int value = atoi(value_str);
-                          if (equals != NULL) {
-                            *equals = 0;
-                            if (futhark_context_config_set_size(cfg, name, value) != 0) {
-                              panic(1, "Unknown size: %s\n", name);
-                            }
-                          } else {
-                            panic(1, "Invalid argument for size option: %s\n", optarg);
-                          }}|]
-                      }
-             , Option { optionLongName = "tuning"
-                      , optionShortName = Nothing
-                      , optionArgument = RequiredArgument "FILE"
-                      , optionAction = [C.cstm|{
-                          char *ret = load_tuning_file(optarg, cfg, (int(*)(void*, const char*, size_t))
-                                                                    futhark_context_config_set_size);
-                          if (ret != NULL) {
-                            panic(1, "When loading tuning from '%s': %s\n", optarg, ret);
-                          }}|]
-                      }
-            , Option { optionLongName = "profile"
-                     , optionShortName = Just 'P'
-                     , optionArgument = NoArgument
-                     , optionAction = [C.cstm|futhark_context_config_set_profiling(cfg, 1);|]
-                     }
-             ]
+cliOptions =
+  commonOptions ++
+  [ Option { optionLongName = "platform"
+           , optionShortName = Just 'p'
+           , optionArgument = RequiredArgument "NAME"
+           , optionAction = [C.cstm|futhark_context_config_set_platform(cfg, optarg);|]
+           }
+  , Option { optionLongName = "device"
+           , optionShortName = Just 'd'
+           , optionArgument = RequiredArgument "NAME"
+           , optionAction = [C.cstm|futhark_context_config_set_device(cfg, optarg);|]
+           }
+  , Option { optionLongName = "dump-opencl"
+           , optionShortName = Nothing
+           , optionArgument = RequiredArgument "FILE"
+           , optionAction = [C.cstm|{futhark_context_config_dump_program_to(cfg, optarg);
+                                     entry_point = NULL;}|]
+           }
+  , Option { optionLongName = "load-opencl"
+           , optionShortName = Nothing
+           , optionArgument = RequiredArgument "FILE"
+           , optionAction = [C.cstm|futhark_context_config_load_program_from(cfg, optarg);|]
+           }
+  , Option { optionLongName = "dump-opencl-binary"
+           , optionShortName = Nothing
+           , optionArgument = RequiredArgument "FILE"
+           , optionAction = [C.cstm|{futhark_context_config_dump_binary_to(cfg, optarg);
+                                     entry_point = NULL;}|]
+           }
+  , Option { optionLongName = "load-opencl-binary"
+           , optionShortName = Nothing
+           , optionArgument = RequiredArgument "FILE"
+           , optionAction = [C.cstm|futhark_context_config_load_binary_from(cfg, optarg);|]
+           }
+  , Option { optionLongName = "build-option"
+           , optionShortName = Nothing
+           , optionArgument = RequiredArgument "OPT"
+           , optionAction = [C.cstm|futhark_context_config_add_build_option(cfg, optarg);|]
+           }
+
+  , Option { optionLongName = "profile"
+           , optionShortName = Just 'P'
+           , optionArgument = NoArgument
+           , optionAction = [C.cstm|futhark_context_config_set_profiling(cfg, 1);|]
+           }
+  ]
 
 -- We detect the special case of writing a constant and turn it into a
 -- non-blocking write.  This may be slightly faster, as it prevents
diff --git a/src/Futhark/CodeGen/Backends/COpenCL/Boilerplate.hs b/src/Futhark/CodeGen/Backends/COpenCL/Boilerplate.hs
--- a/src/Futhark/CodeGen/Backends/COpenCL/Boilerplate.hs
+++ b/src/Futhark/CodeGen/Backends/COpenCL/Boilerplate.hs
@@ -5,6 +5,8 @@
 
   , kernelRuntime
   , kernelRuns
+
+  , commonOptions
   ) where
 
 import Data.FileEmbed
@@ -14,6 +16,7 @@
 
 import Futhark.CodeGen.ImpCode.OpenCL
 import qualified Futhark.CodeGen.Backends.GenericC as GC
+import Futhark.CodeGen.Backends.GenericC.Options
 import Futhark.CodeGen.OpenCL.Heuristics
 import Futhark.Util (chunk, zEncodeString)
 
@@ -490,3 +493,67 @@
                                                   sizeof($exp:which'),
                                                   &$exp:which',
                                                   NULL);|]
+
+-- Options that are common to multiple GPU-like backends.
+commonOptions :: [Option]
+commonOptions =
+   [ Option { optionLongName = "default-group-size"
+            , optionShortName = Nothing
+            , optionArgument = RequiredArgument "INT"
+            , optionAction = [C.cstm|futhark_context_config_set_default_group_size(cfg, atoi(optarg));|]
+            }
+   , Option { optionLongName = "default-num-groups"
+            , optionShortName = Nothing
+            , optionArgument = RequiredArgument "INT"
+            , optionAction = [C.cstm|futhark_context_config_set_default_num_groups(cfg, atoi(optarg));|]
+            }
+   , Option { optionLongName = "default-tile-size"
+            , optionShortName = Nothing
+            , optionArgument = RequiredArgument "INT"
+            , optionAction = [C.cstm|futhark_context_config_set_default_tile_size(cfg, atoi(optarg));|]
+            }
+   , Option { optionLongName = "default-threshold"
+            , optionShortName = Nothing
+            , optionArgument = RequiredArgument "INT"
+            , optionAction = [C.cstm|futhark_context_config_set_default_threshold(cfg, atoi(optarg));|]
+            }
+   , Option { optionLongName = "print-sizes"
+            , optionShortName = Nothing
+            , optionArgument = NoArgument
+            , optionAction = [C.cstm|{
+                int n = futhark_get_num_sizes();
+                for (int i = 0; i < n; i++) {
+                  printf("%s (%s)\n", futhark_get_size_name(i),
+                                      futhark_get_size_class(i));
+                }
+                exit(0);
+              }|]
+            }
+   , Option { optionLongName = "size"
+            , optionShortName = Nothing
+            , optionArgument = RequiredArgument "NAME=INT"
+            , optionAction = [C.cstm|{
+                char *name = optarg;
+                char *equals = strstr(optarg, "=");
+                char *value_str = equals != NULL ? equals+1 : optarg;
+                int value = atoi(value_str);
+                if (equals != NULL) {
+                  *equals = 0;
+                  if (futhark_context_config_set_size(cfg, name, value) != 0) {
+                    panic(1, "Unknown size: %s\n", name);
+                  }
+                } else {
+                  panic(1, "Invalid argument for size option: %s\n", optarg);
+                }}|]
+            }
+   , Option { optionLongName = "tuning"
+            , optionShortName = Nothing
+            , optionArgument = RequiredArgument "FILE"
+            , optionAction = [C.cstm|{
+                char *ret = load_tuning_file(optarg, cfg, (int(*)(void*, const char*, size_t))
+                                                          futhark_context_config_set_size);
+                if (ret != NULL) {
+                  panic(1, "When loading tuning from '%s': %s\n", optarg, ret);
+                }}|]
+            }
+   ]
diff --git a/src/Futhark/CodeGen/Backends/GenericC.hs b/src/Futhark/CodeGen/Backends/GenericC.hs
--- a/src/Futhark/CodeGen/Backends/GenericC.hs
+++ b/src/Futhark/CodeGen/Backends/GenericC.hs
@@ -716,7 +716,7 @@
 
   let prepare_new = do
         resetMem [C.cexp|arr->mem|]
-        allocMem [C.cexp|arr->mem|] [C.cexp|$exp:arr_size * sizeof($ty:pt')|] space
+        allocMem [C.cexp|arr->mem|] [C.cexp|((size_t)$exp:arr_size) * sizeof($ty:pt')|] space
                  [C.cstm|return NULL;|]
         forM_ [0..rank-1] $ \i ->
           let dim_s = "dim"++show i
@@ -726,20 +726,20 @@
     prepare_new
     copy arr_raw_mem [C.cexp|0|] space
          [C.cexp|data|] [C.cexp|0|] DefaultSpace
-         [C.cexp|$exp:arr_size * sizeof($ty:pt')|]
+         [C.cexp|((size_t)$exp:arr_size) * sizeof($ty:pt')|]
 
   new_raw_body <- collect $ do
     prepare_new
     copy arr_raw_mem [C.cexp|0|] space
          [C.cexp|data|] [C.cexp|offset|] space
-         [C.cexp|$exp:arr_size * sizeof($ty:pt')|]
+         [C.cexp|((size_t)$exp:arr_size) * sizeof($ty:pt')|]
 
   free_body <- collect $ unRefMem [C.cexp|arr->mem|] space
 
   values_body <- collect $
     copy [C.cexp|data|] [C.cexp|0|] DefaultSpace
          arr_raw_mem [C.cexp|0|] space
-         [C.cexp|$exp:arr_size_array * sizeof($ty:pt')|]
+         [C.cexp|((size_t)$exp:arr_size_array) * sizeof($ty:pt')|]
 
   ctx_ty <- contextType
 
@@ -1583,11 +1583,14 @@
 derefPointer ptr i res_t =
   [C.cexp|(($ty:res_t)$exp:ptr)[$exp:i]|]
 
+volQuals :: Volatility -> [C.TypeQual]
+volQuals Volatile = [C.ctyquals|volatile|]
+volQuals Nonvolatile = []
+
 writeScalarPointerWithQuals :: PointerQuals op s -> WriteScalar op s
 writeScalarPointerWithQuals quals_f dest i elemtype space vol v = do
   quals <- quals_f space
-  let quals' = case vol of Volatile -> [C.ctyquals|volatile|] ++ quals
-                           Nonvolatile -> quals
+  let quals' = volQuals vol ++ quals
       deref = derefPointer dest i
               [C.cty|$tyquals:quals' $ty:elemtype*|]
   stm [C.cstm|$exp:deref = $exp:v;|]
@@ -1595,8 +1598,7 @@
 readScalarPointerWithQuals :: PointerQuals op s -> ReadScalar op s
 readScalarPointerWithQuals quals_f dest i elemtype space vol = do
   quals <- quals_f space
-  let quals' = case vol of Volatile -> [C.ctyquals|volatile|] ++ quals
-                           Nonvolatile -> quals
+  let quals' = volQuals vol ++ quals
   return $ derefPointer dest i [C.cty|$tyquals:quals' $ty:elemtype*|]
 
 compileExpToName :: String -> PrimType -> Exp -> CompilerM op s VName
@@ -1618,9 +1620,7 @@
           src' <- rawMem src
           derefPointer src'
             <$> compileExp iexp
-            <*> pure [C.cty|$tyquals:vol' $ty:(primTypeToCType restype)*|]
-            where vol' = case vol of Volatile -> [C.ctyquals|volatile|]
-                                     Nonvolatile -> []
+            <*> pure [C.cty|$tyquals:(volQuals vol) $ty:(primTypeToCType restype)*|]
 
         compileLeaf (Index src (Count iexp) restype (Space space) vol) =
           join $ asks envReadScalar
@@ -1628,7 +1628,7 @@
           <*> pure (primTypeToCType restype) <*> pure space <*> pure vol
 
         compileLeaf (SizeOf t) =
-          return [C.cexp|(sizeof($ty:t'))|]
+          return [C.cexp|(typename int32_t)sizeof($ty:t')|]
           where t' = primTypeToCType t
 
 -- | Tell me how to compile a @v@, and I'll Compile any @PrimExp v@ for you.
@@ -1740,10 +1740,10 @@
        }|]
 
 compileCode c
-  | Just (name, t, e, c') <- declareAndSet c = do
+  | Just (name, vol, t, e, c') <- declareAndSet c = do
     let ct = primTypeToCType t
     e' <- compileExp e
-    item [C.citem|$ty:ct $id:name = $exp:e';|]
+    item [C.citem|$tyquals:(volQuals vol) $ty:ct $id:name = $exp:e';|]
     compileCode c'
 
 compileCode (c1 :>>: c2) = compileCode c1 >> compileCode c2
@@ -1754,13 +1754,13 @@
   let onPart (ErrorString s) = return ("%s", [C.cexp|$string:s|])
       onPart (ErrorInt32 x) = ("%d",) <$> compileExp x
   (formatstrs, formatargs) <- unzip <$> mapM onPart parts
-  let formatstr = "Error at\n%s\n" <> concat formatstrs <> "\n"
+  let formatstr = "Error: " ++ concat formatstrs ++ "\n\nBacktrace:\n%s"
   stm [C.cstm|if (!$exp:e') {
-                   ctx->error = msgprintf($string:formatstr, $string:stacktrace, $args:formatargs);
+                   ctx->error = msgprintf($string:formatstr, $args:formatargs, $string:stacktrace);
                    $items:free_all_mem
                    return 1;
                  }|]
-  where stacktrace = prettyStacktrace $ reverse $ map locStr $ loc:locs
+  where stacktrace = prettyStacktrace 0 $ map locStr $ loc:locs
 
 compileCode (Allocate name (Count e) space) = do
   size <- compileExp e
@@ -1818,11 +1818,9 @@
   dest' <- rawMem dest
   deref <- derefPointer dest'
            <$> compileExp idx
-           <*> pure [C.cty|$tyquals:vol' $ty:(primTypeToCType elemtype)*|]
+           <*> pure [C.cty|$tyquals:(volQuals vol) $ty:(primTypeToCType elemtype)*|]
   elemexp' <- compileExp elemexp
   stm [C.cstm|$exp:deref = $exp:elemexp';|]
-  where vol' = case vol of Volatile -> [C.ctyquals|volatile|]
-                           Nonvolatile -> []
 
 compileCode (Write dest (Count idx) elemtype (Space space) vol elemexp) =
   join $ asks envWriteScalar
@@ -1836,9 +1834,9 @@
 compileCode (DeclareMem name space) =
   declMem name space
 
-compileCode (DeclareScalar name t) = do
+compileCode (DeclareScalar name vol t) = do
   let ct = primTypeToCType t
-  decl [C.cdecl|$ty:ct $id:name;|]
+  decl [C.cdecl|$tyquals:(volQuals vol) $ty:ct $id:name;|]
 
 compileCode (DeclareArray name DefaultSpace t vs) = do
   name_realtype <- newVName $ baseString name ++ "_realtype"
@@ -1921,11 +1919,11 @@
         setRetVal' p (ScalarParam name _) =
           stm [C.cstm|*$exp:p = $id:name;|]
 
-declareAndSet :: Code op -> Maybe (VName, PrimType, Exp, Code op)
-declareAndSet (DeclareScalar name t :>>: (SetScalar dest e :>>: c))
-  | name == dest = Just (name, t, e, c)
-declareAndSet ((DeclareScalar name t :>>: SetScalar dest e) :>>: c)
-  | name == dest = Just (name, t, e, c)
+declareAndSet :: Code op -> Maybe (VName, Volatility, PrimType, Exp, Code op)
+declareAndSet (DeclareScalar name vol t :>>: (SetScalar dest e :>>: c))
+  | name == dest = Just (name, vol, t, e, c)
+declareAndSet ((DeclareScalar name vol t :>>: SetScalar dest e) :>>: c)
+  | name == dest = Just (name, vol, t, e, c)
 declareAndSet _ = Nothing
 
 assignmentOperator :: BinOp -> Maybe (VName -> C.Exp -> C.Exp)
diff --git a/src/Futhark/CodeGen/Backends/GenericCSharp.hs b/src/Futhark/CodeGen/Backends/GenericCSharp.hs
--- a/src/Futhark/CodeGen/Backends/GenericCSharp.hs
+++ b/src/Futhark/CodeGen/Backends/GenericCSharp.hs
@@ -85,7 +85,6 @@
 import Futhark.CodeGen.Backends.GenericCSharp.Definitions
 import Futhark.Util (zEncodeString)
 import Futhark.Representation.AST.Attributes (builtInFunctions)
-import Text.Printf (printf)
 
 -- | A substitute expression compiler, tried before the main
 -- compilation function.
@@ -1242,9 +1241,9 @@
 
 compileCode (Imp.DeclareMem v space) = declMem v space
 
-compileCode (Imp.DeclareScalar v Cert) =
+compileCode (Imp.DeclareScalar v _ Cert) =
   stm $ Assign (Var $ compileName v) $ Bool True
-compileCode (Imp.DeclareScalar v t) =
+compileCode (Imp.DeclareScalar v _ t) =
   stm $ AssignTyped t' (Var $ compileName v) Nothing
   where t' = compilePrimTypeToAST t
 
@@ -1274,10 +1273,12 @@
   e' <- compileExp e
   let onPart (i, Imp.ErrorString s) = return (printFormatArg i, String s)
       onPart (i, Imp.ErrorInt32 x) = (printFormatArg i,) <$> compileExp x
-  (formatstrs, formatargs) <- unzip <$> mapM onPart (zip ([1..] :: [Integer]) parts)
-  stm $ Assert e' $ String ("Error at {0}:\n" <> concat formatstrs) : (String stacktrace : formatargs)
-  where stacktrace = prettyStacktrace $ reverse $ map locStr $ loc:locs
-        printFormatArg = printf "{%d}"
+  (formatstrs, formatargs) <- unzip <$> mapM onPart (zip ([0..] :: [Integer]) parts)
+  stm $ Assert e' $ String ("Error: " <> concat formatstrs <>
+                            "\n\nBacktrace:\n" ++ "{" ++ show (length formatargs) ++ "}") :
+    (formatargs ++ [String stacktrace])
+  where stacktrace = prettyStacktrace 0 $ map locStr $ loc:locs
+        printFormatArg i = "{" ++ show i ++ "}"
 
 compileCode (Imp.Call dests fname args) = do
   args' <- mapM compileArg args
@@ -1324,7 +1325,8 @@
   let dest' = Var (compileName dest)
   let src' = Var (compileName src)
   size' <- compileExp size
-  stm $ Exp $ simpleCall "Buffer.BlockCopy" [src', srcoffset', dest', destoffset', size']
+  stm $ Exp $ simpleCall "Buffer.BlockCopy" [src', srcoffset', dest', destoffset',
+                                             Cast (Primitive $ CSInt Int32T) size']
 
 compileCode (Imp.Copy dest (Imp.Count destoffset) destspace src (Imp.Count srcoffset) srcspace (Imp.Count size)) = do
   copy <- asks envCopy
diff --git a/src/Futhark/CodeGen/Backends/GenericPython.hs b/src/Futhark/CodeGen/Backends/GenericPython.hs
--- a/src/Futhark/CodeGen/Backends/GenericPython.hs
+++ b/src/Futhark/CodeGen/Backends/GenericPython.hs
@@ -871,7 +871,7 @@
   stm $ Assign name' exp1'
 
 compileCode Imp.DeclareMem{} = return ()
-compileCode (Imp.DeclareScalar v Cert) =
+compileCode (Imp.DeclareScalar v _ Cert) =
   stm $ Assign (Var $ compileName v) $ Var "True"
 compileCode Imp.DeclareScalar{} = return ()
 
@@ -910,9 +910,9 @@
       onPart (Imp.ErrorInt32 x) = ("%d",) <$> compileExp x
   (formatstrs, formatargs) <- unzip <$> mapM onPart parts
   stm $ Assert e' (BinOp "%"
-                   (String $ "Error at\n" ++ stacktrace ++ "\n: " ++ concat formatstrs)
+                   (String $ "Error: " ++ concat formatstrs ++ "\n\nBacktrace:\n" ++ stacktrace)
                    (Tuple formatargs))
-  where stacktrace = prettyStacktrace $ reverse $ map locStr $ loc:locs
+  where stacktrace = prettyStacktrace 0 $ map locStr $ loc:locs
 
 compileCode (Imp.Call dests fname args) = do
   args' <- mapM compileArg args
diff --git a/src/Futhark/CodeGen/Backends/SequentialC.hs b/src/Futhark/CodeGen/Backends/SequentialC.hs
--- a/src/Futhark/CodeGen/Backends/SequentialC.hs
+++ b/src/Futhark/CodeGen/Backends/SequentialC.hs
@@ -36,8 +36,8 @@
              [C.cedecl|struct $id:s { int debugging; };|])
 
           GC.publicDef_ "context_config_new" GC.InitDecl $ \s ->
-            ([C.cedecl|struct $id:cfg* $id:s();|],
-             [C.cedecl|struct $id:cfg* $id:s() {
+            ([C.cedecl|struct $id:cfg* $id:s(void);|],
+             [C.cedecl|struct $id:cfg* $id:s(void) {
                                  struct $id:cfg *cfg = (struct $id:cfg*) malloc(sizeof(struct $id:cfg));
                                  if (cfg == NULL) {
                                    return NULL;
@@ -62,7 +62,7 @@
              ([C.cedecl|void $id:s(struct $id:cfg* cfg, int flag);|],
               [C.cedecl|void $id:s(struct $id:cfg* cfg, int detail) {
                                  /* Does nothing for this backend. */
-                                 cfg = cfg; detail=detail;
+                                 (void)cfg; (void)detail;
                                }|])
 
           (fields, init_fields) <- GC.contextContents
@@ -103,7 +103,7 @@
           GC.publicDef_ "context_sync" GC.InitDecl $ \s ->
             ([C.cedecl|int $id:s(struct $id:ctx* ctx);|],
              [C.cedecl|int $id:s(struct $id:ctx* ctx) {
-                                 ctx=ctx;
+                                 (void)ctx;
                                  return 0;
                                }|])
           GC.publicDef_ "context_get_error" GC.InitDecl $ \s ->
diff --git a/src/Futhark/CodeGen/Backends/SimpleRepresentation.hs b/src/Futhark/CodeGen/Backends/SimpleRepresentation.hs
--- a/src/Futhark/CodeGen/Backends/SimpleRepresentation.hs
+++ b/src/Futhark/CodeGen/Backends/SimpleRepresentation.hs
@@ -194,16 +194,16 @@
           [C.cedecl|static inline $ty:ct $id:(taggedI s t)($ty:ct x, $ty:ct y) { return $exp:e; }|]
             where ct = intTypeToCType t
         intCmpOp s e t =
-          [C.cedecl|static inline char $id:(taggedI s t)($ty:ct x, $ty:ct y) { return $exp:e; }|]
+          [C.cedecl|static inline typename bool $id:(taggedI s t)($ty:ct x, $ty:ct y) { return $exp:e; }|]
             where ct = intTypeToCType t
         uintCmpOp s e t =
-          [C.cedecl|static inline char $id:(taggedI s t)($ty:ct x, $ty:ct y) { return $exp:e; }|]
+          [C.cedecl|static inline typename bool $id:(taggedI s t)($ty:ct x, $ty:ct y) { return $exp:e; }|]
             where ct = uintTypeToCType t
 
 cIntPrimFuns :: [C.Definition]
 cIntPrimFuns =
   [C.cunit|
-$esc:("#ifdef __OPENCL_VERSION__")
+$esc:("#if defined(__OPENCL_VERSION__)")
    typename int32_t $id:(funName' "popc8") (typename int8_t x) {
       return popcount(x);
    }
@@ -216,7 +216,7 @@
    typename int32_t $id:(funName' "popc64") (typename int64_t x) {
       return popcount(x);
    }
-$esc:("#elif __CUDA_ARCH__")
+$esc:("#elif defined(__CUDA_ARCH__)")
    typename int32_t $id:(funName' "popc8") (typename int8_t x) {
       return __popc(zext_i8_i32(x));
    }
@@ -260,7 +260,7 @@
    }
 $esc:("#endif")
 
-$esc:("#ifdef __OPENCL_VERSION__")
+$esc:("#if defined(__OPENCL_VERSION__)")
    typename int32_t $id:(funName' "clz8") (typename int8_t x) {
       return clz(x);
    }
@@ -273,7 +273,7 @@
    typename int32_t $id:(funName' "clz64") (typename int64_t x) {
       return clz(x);
    }
-$esc:("#elif __CUDA_ARCH__")
+$esc:("#elif defined(__CUDA_ARCH__)")
    typename int32_t $id:(funName' "clz8") (typename int8_t x) {
       return __clz(zext_i8_i32(x))-24;
    }
@@ -365,7 +365,7 @@
 
         mkFPConv from_f to_f s from_t to_t =
           [C.cedecl|static inline $ty:to_ct
-                    $id:(convOp s from_t to_t)($ty:from_ct x) { return x;} |]
+                    $id:(convOp s from_t to_t)($ty:from_ct x) { return ($ty:to_ct)x;} |]
           where from_ct = from_f from_t
                 to_ct = to_f to_t
 
@@ -379,7 +379,7 @@
           [C.cedecl|static inline $ty:ct $id:(taggedF s t)($ty:ct x, $ty:ct y) { return $exp:e; }|]
             where ct = floatTypeToCType t
         floatCmpOp s e t =
-          [C.cedecl|static inline char $id:(taggedF s t)($ty:ct x, $ty:ct y) { return $exp:e; }|]
+          [C.cedecl|static inline typename bool $id:(taggedF s t)($ty:ct x, $ty:ct y) { return $exp:e; }|]
             where ct = floatTypeToCType t
 
 cFloat32Funs :: [C.Definition]
@@ -440,11 +440,11 @@
       return lgamma(x);
     }
 
-    static inline char $id:(funName' "isnan32")(float x) {
+    static inline typename bool $id:(funName' "isnan32")(float x) {
       return isnan(x);
     }
 
-    static inline char $id:(funName' "isinf32")(float x) {
+    static inline typename bool $id:(funName' "isinf32")(float x) {
       return isinf(x);
     }
 
@@ -571,11 +571,11 @@
       return floor(x);
     }
 
-    static inline char $id:(funName' "isnan64")(double x) {
+    static inline typename bool $id:(funName' "isnan64")(double x) {
       return isnan(x);
     }
 
-    static inline char $id:(funName' "isinf64")(double x) {
+    static inline typename bool $id:(funName' "isinf64")(double x) {
       return isinf(x);
     }
 
diff --git a/src/Futhark/CodeGen/ImpCode.hs b/src/Futhark/CodeGen/ImpCode.hs
--- a/src/Futhark/CodeGen/ImpCode.hs
+++ b/src/Futhark/CodeGen/ImpCode.hs
@@ -43,9 +43,7 @@
   , withElemType
 
     -- * Converting from sizes
-  , sizeToExp
   , dimSizeToExp
-  , memSizeToExp
 
     -- * Analysis
 
@@ -149,7 +147,7 @@
             | For VName IntType Exp (Code a)
             | While Exp (Code a)
             | DeclareMem VName Space
-            | DeclareScalar VName PrimType
+            | DeclareScalar VName Volatility PrimType
             | DeclareArray VName Space PrimType ArrayContents
               -- ^ Create an array containing the given values.  The
               -- lifetime of the array will be the entire application.
@@ -192,7 +190,9 @@
             | Op a
             deriving (Show)
 
--- | The volatility of a memory access.
+-- | The volatility of a memory access or variable.  Feel free to
+-- ignore this for backends where it makes no sense (anything but C
+-- and similar low-level things)
 data Volatility = Volatile | Nonvolatile
                 deriving (Eq, Ord, Show)
 
@@ -231,17 +231,14 @@
 -- | Convert a count of elements into a count of bytes, given the
 -- per-element size.
 withElemType :: Count Elements Exp -> PrimType -> Count Bytes Exp
-withElemType (Count e) t = bytes $ e * LeafExp (SizeOf t) (IntType Int32)
+withElemType (Count e) t =
+  bytes $ ConvOpExp (SExt Int32 Int64) e * LeafExp (SizeOf t) (IntType Int64)
 
 dimSizeToExp :: DimSize -> Count Elements Exp
-dimSizeToExp = elements . sizeToExp
-
-memSizeToExp :: MemSize -> Count Bytes Exp
-memSizeToExp = bytes . sizeToExp
-
-sizeToExp :: Size -> Exp
-sizeToExp (VarSize v)   = LeafExp (ScalarVar v) (IntType Int32)
-sizeToExp (ConstSize x) = ValueExp $ IntValue $ Int32Value $ fromIntegral x
+dimSizeToExp (VarSize v) =
+  elements $ LeafExp (ScalarVar v) (IntType Int32)
+dimSizeToExp (ConstSize x) =
+  elements $ ValueExp $ IntValue $ Int32Value $ fromIntegral x
 
 var :: VName -> PrimType -> Exp
 var = LeafExp . ScalarVar
@@ -320,8 +317,10 @@
     text "}"
   ppr (DeclareMem name space) =
     text "var" <+> ppr name <> text ": mem" <> parens (ppr space)
-  ppr (DeclareScalar name t) =
-    text "var" <+> ppr name <> text ":" <+> ppr t
+  ppr (DeclareScalar name vol t) =
+    text "var" <+> ppr name <> text ":" <+> vol' <> ppr t
+    where vol' = case vol of Volatile -> text "volatile "
+                             Nonvolatile -> mempty
   ppr (DeclareArray name space t vs) =
     text "array" <+> ppr name <> text "@" <> ppr space <+> text ":" <+> ppr t <+>
     equals <+> ppr vs
@@ -422,8 +421,8 @@
     pure Skip
   traverse _ (DeclareMem name space) =
     pure $ DeclareMem name space
-  traverse _ (DeclareScalar name bt) =
-    pure $ DeclareScalar name bt
+  traverse _ (DeclareScalar name vol bt) =
+    pure $ DeclareScalar name vol bt
   traverse _ (DeclareArray name space t vs) =
     pure $ DeclareArray name space t vs
   traverse _ (Allocate name size s) =
@@ -449,7 +448,7 @@
 
 declaredIn :: Code a -> Names
 declaredIn (DeclareMem name _) = oneName name
-declaredIn (DeclareScalar name _) = oneName name
+declaredIn (DeclareScalar name _ _) = oneName name
 declaredIn (DeclareArray name _ _ _) = oneName name
 declaredIn (If _ t f) = declaredIn t <> declaredIn f
 declaredIn (x :>>: y) = declaredIn x <> declaredIn y
diff --git a/src/Futhark/CodeGen/ImpGen.hs b/src/Futhark/CodeGen/ImpGen.hs
--- a/src/Futhark/CodeGen/ImpGen.hs
+++ b/src/Futhark/CodeGen/ImpGen.hs
@@ -71,7 +71,7 @@
   , dScope
   , dScopes
   , dArray
-  , dPrim, dPrim_, dPrimV_, dPrimV, dPrimVE
+  , dPrim, dPrimVol_, dPrim_, dPrimV_, dPrimV, dPrimVE
 
   , sFor, sWhile
   , sComment
@@ -506,7 +506,7 @@
     copy_to_merge_params <- forM (zip3 mergeparams tmpnames ses) $ \(p,tmp,se) ->
       case typeOf p of
         Prim pt  -> do
-          emit $ Imp.DeclareScalar tmp pt
+          emit $ Imp.DeclareScalar tmp Imp.Nonvolatile pt
           emit $ Imp.SetScalar tmp $ toExp' pt se
           return $ emit $ Imp.SetScalar (paramName p) $ Imp.var tmp pt
         Mem space | Var v <- se -> do
@@ -768,9 +768,14 @@
 dLParams :: ExplicitMemorish lore => [LParam lore] -> ImpM lore op ()
 dLParams = dScope Nothing . scopeOfLParams
 
+dPrimVol_ :: VName -> PrimType -> ImpM lore op ()
+dPrimVol_ name t = do
+ emit $ Imp.DeclareScalar name Imp.Volatile t
+ addVar name $ ScalarVar Nothing $ ScalarEntry t
+
 dPrim_ :: VName -> PrimType -> ImpM lore op ()
 dPrim_ name t = do
- emit $ Imp.DeclareScalar name t
+ emit $ Imp.DeclareScalar name Imp.Nonvolatile t
  addVar name $ ScalarVar Nothing $ ScalarEntry t
 
 dPrim :: String -> PrimType -> ImpM lore op VName
@@ -813,7 +818,7 @@
     MemVar _ entry' ->
       emit $ Imp.DeclareMem name $ entryMemSpace entry'
     ScalarVar _ entry' ->
-      emit $ Imp.DeclareScalar name $ entryScalarType entry'
+      emit $ Imp.DeclareScalar name Imp.Nonvolatile $ entryScalarType entry'
     ArrayVar _ _ ->
       return ()
   addVar name entry
diff --git a/src/Futhark/CodeGen/ImpGen/Kernels.hs b/src/Futhark/CodeGen/ImpGen/Kernels.hs
--- a/src/Futhark/CodeGen/ImpGen/Kernels.hs
+++ b/src/Futhark/CodeGen/ImpGen/Kernels.hs
@@ -149,9 +149,9 @@
 
   | bt_size <- primByteSize bt,
     ixFunMatchesInnerShape
-      (Shape $ map Imp.sizeToExp destshape) destIxFun,
+      (Shape $ map (Imp.unCount . Imp.dimSizeToExp) destshape) destIxFun,
     ixFunMatchesInnerShape
-      (Shape $ map Imp.sizeToExp srcshape) srcIxFun,
+      (Shape $ map (Imp.unCount . Imp.dimSizeToExp) srcshape) srcIxFun,
     Just destoffset <-
       IxFun.linearWithOffset destIxFun bt_size,
     Just srcoffset  <-
@@ -244,9 +244,9 @@
 
         transpose_code =
           Imp.If input_is_empty mempty $ mconcat
-          [ Imp.DeclareScalar muly (IntType Int32)
+          [ Imp.DeclareScalar muly Imp.Nonvolatile (IntType Int32)
           , Imp.SetScalar muly $ block_dim `quot` v32 x
-          , Imp.DeclareScalar mulx (IntType Int32)
+          , Imp.DeclareScalar mulx Imp.Nonvolatile (IntType Int32)
           , Imp.SetScalar mulx $ block_dim `quot` v32 y
           , Imp.If can_use_copy copy_code $
             Imp.If should_use_lowwidth (callTransposeKernel TransposeLowWidth) $
diff --git a/src/Futhark/CodeGen/ImpGen/Kernels/Base.hs b/src/Futhark/CodeGen/ImpGen/Kernels/Base.hs
--- a/src/Futhark/CodeGen/ImpGen/Kernels/Base.hs
+++ b/src/Futhark/CodeGen/ImpGen/Kernels/Base.hs
@@ -338,6 +338,8 @@
       forM_ (zip red_pes tmp_arrs) $ \(pe, arr) ->
         copyDWIM (patElemName pe) segment_is (Var arr) (segment_is ++ [last dims'-1])
 
+      sOp Imp.LocalBarrier
+
 compileGroupOp constants pat (Inner (SegOp (SegHist lvl space ops _ kbody))) = do
   compileGroupSpace constants lvl space
   let ltids = map fst $ unSegSpace space
@@ -474,7 +476,9 @@
 
 atomicUpdateLocking op = AtomicLocking $ \locking space arrs bucket -> do
   old <- dPrim "old" int32
-  continue <- dPrimV "continue" true
+  continue <- newVName "continue"
+  dPrimVol_ continue Bool
+  continue <-- true
 
   -- Correctly index into locks.
   (locks', _locks_space, locks_offset) <-
@@ -1225,9 +1229,9 @@
   n = do
   -- Note that the shape of the destination and the source are
   -- necessarily the same.
-  let shape = map Imp.sizeToExp srcshape
+  let shape = map dimSizeToExp srcshape
       shape_se = map (Imp.unCount . dimSizeToExp) srcshape
-      kernel_size = Imp.unCount n * product (drop 1 shape)
+      kernel_size = Imp.unCount $ n * product (drop 1 shape)
 
   (constants, set_constants) <- simpleKernelConstants kernel_size "copy"
 
@@ -1281,7 +1285,7 @@
   sWhen (isActive $ zip is_for_thread $ map fst dims) $
     copyDWIM (patElemName pe) (map Imp.vi32 is_for_thread) (Var what) local_is
 
-compileGroupResult space constants pe (Returns what) = do
+compileGroupResult space constants pe (Returns _ what) = do
   in_local_memory <- arrayInLocalMemory what
   let gids = map (Imp.vi32 . fst) $ unSegSpace space
 
@@ -1305,7 +1309,7 @@
                     -> KernelConstants -> PatElem ExplicitMemory -> KernelResult
                     -> InKernelGen ()
 
-compileThreadResult space _ pe (Returns what) = do
+compileThreadResult space _ pe (Returns _ what) = do
   let is = map (Imp.vi32 . fst) $ unSegSpace space
   copyDWIM (patElemName pe) is what []
 
diff --git a/src/Futhark/CodeGen/ImpGen/Kernels/SegHist.hs b/src/Futhark/CodeGen/ImpGen/Kernels/SegHist.hs
--- a/src/Futhark/CodeGen/ImpGen/Kernels/SegHist.hs
+++ b/src/Futhark/CodeGen/ImpGen/Kernels/SegHist.hs
@@ -42,6 +42,7 @@
   where
 
 import Control.Monad.Except
+import Control.Monad.Reader
 import Data.Maybe
 import Data.List
 
@@ -214,8 +215,9 @@
   -- tunable knob with a hopefully sane default.
   let hist_L2_def = 5632 * 1024
   hist_L2 <- dPrim "L2_size" int32
+  entry <- asks envFunction
   -- Equivalent to F_L2*L2 in paper.
-  sOp $ Imp.GetSize hist_L2 (nameFromString $ pretty hist_L2) $
+  sOp $ Imp.GetSize hist_L2 (entry <> "." <> nameFromString (pretty hist_L2)) $
     Imp.SizeBespoke (nameFromString "L2_for_histogram") hist_L2_def
 
   let hist_L2_ln_sz = 16*4 -- L2 cache line size approximation
diff --git a/src/Futhark/CodeGen/ImpGen/Kernels/ToOpenCL.hs b/src/Futhark/CodeGen/ImpGen/Kernels/ToOpenCL.hs
--- a/src/Futhark/CodeGen/ImpGen/Kernels/ToOpenCL.hs
+++ b/src/Futhark/CodeGen/ImpGen/Kernels/ToOpenCL.hs
@@ -549,7 +549,7 @@
 typesInCode (For _ it e c) = IntType it `S.insert` typesInExp e <> typesInCode c
 typesInCode (While e c) = typesInExp e <> typesInCode c
 typesInCode DeclareMem{} = mempty
-typesInCode (DeclareScalar _ t) = S.singleton t
+typesInCode (DeclareScalar _ _ t) = S.singleton t
 typesInCode (DeclareArray _ _ t _) = S.singleton t
 typesInCode (Allocate _ (Count e) _) = typesInExp e
 typesInCode Free{} = mempty
diff --git a/src/Futhark/CodeGen/ImpGen/Kernels/Transpose.hs b/src/Futhark/CodeGen/ImpGen/Kernels/Transpose.hs
--- a/src/Futhark/CodeGen/ImpGen/Kernels/Transpose.hs
+++ b/src/Futhark/CodeGen/ImpGen/Kernels/Transpose.hs
@@ -133,7 +133,7 @@
                    ]
       ]
 
-  where dec v e = DeclareScalar v int32 <> SetScalar v e
+  where dec v e = DeclareScalar v Nonvolatile int32 <> SetScalar v e
         v32 = flip var int32
         tile_dim = 2 * block_dim
 
@@ -164,17 +164,17 @@
           , "j"]
 
         get_ids =
-          mconcat [ DeclareScalar get_global_id_0 int32
+          mconcat [ DeclareScalar get_global_id_0 Nonvolatile int32
                   , Op $ GetGlobalId get_global_id_0 0
-                  , DeclareScalar get_local_id_0 int32
+                  , DeclareScalar get_local_id_0 Nonvolatile int32
                   , Op $ GetLocalId get_local_id_0 0
-                  , DeclareScalar get_local_id_1 int32
+                  , DeclareScalar get_local_id_1 Nonvolatile int32
                   , Op $ GetLocalId get_local_id_1 1
-                  , DeclareScalar get_group_id_0 int32
+                  , DeclareScalar get_group_id_0 Nonvolatile int32
                   , Op $ GetGroupId get_group_id_0 0
-                  , DeclareScalar get_group_id_1 int32
+                  , DeclareScalar get_group_id_1 Nonvolatile int32
                   , Op $ GetGroupId get_group_id_1 1
-                  , DeclareScalar get_group_id_2 int32
+                  , DeclareScalar get_group_id_2 Nonvolatile int32
                   , Op $ GetGroupId get_group_id_2 2
                   ]
 
diff --git a/src/Futhark/CodeGen/SetDefaultSpace.hs b/src/Futhark/CodeGen/SetDefaultSpace.hs
--- a/src/Futhark/CodeGen/SetDefaultSpace.hs
+++ b/src/Futhark/CodeGen/SetDefaultSpace.hs
@@ -69,8 +69,8 @@
   Comment s $ setBodySpace space c
 setBodySpace _ Skip =
   Skip
-setBodySpace _ (DeclareScalar name bt) =
-  DeclareScalar name bt
+setBodySpace _ (DeclareScalar name vol bt) =
+  DeclareScalar name vol bt
 setBodySpace space (SetScalar name e) =
   SetScalar name $ setExpSpace space e
 setBodySpace space (SetMem to from old_space) =
diff --git a/src/Futhark/Compiler.hs b/src/Futhark/Compiler.hs
--- a/src/Futhark/Compiler.hs
+++ b/src/Futhark/Compiler.hs
@@ -31,7 +31,6 @@
 import qualified Futhark.Representation.SOACS as I
 import qualified Futhark.TypeCheck as I
 import Futhark.Compiler.Program
-import qualified Language.Futhark as E
 import Futhark.Util.Log
 
 data FutharkConfig = FutharkConfig
@@ -106,16 +105,11 @@
   putNameSource namesrc
   when (pipelineVerbose pipeline_config) $
     logMsg ("Internalising program" :: String)
-  res <- internaliseProg (futharkSafe config) prog_imports
-  case res of
-    Left err ->
-      internalErrorS ("During internalisation: " <> pretty err) $ E.Prog Nothing $
-      concatMap (E.progDecs . fileProg . snd) prog_imports
-    Right int_prog -> do
-      when (pipelineVerbose pipeline_config) $
-        logMsg ("Type-checking internalised program" :: String)
-      typeCheckInternalProgram int_prog
-      runPasses pipeline pipeline_config int_prog
+  int_prog <- internaliseProg (futharkSafe config) prog_imports
+  when (pipelineVerbose pipeline_config) $
+    logMsg ("Type-checking internalised program" :: String)
+  typeCheckInternalProgram int_prog
+  runPasses pipeline pipeline_config int_prog
   where pipeline_config =
           PipelineConfig { pipelineVerbose = fst (futharkVerbose config) > NotVerbose
                          , pipelineValidate = True
diff --git a/src/Futhark/Doc/Generator.hs b/src/Futhark/Doc/Generator.hs
--- a/src/Futhark/Doc/Generator.hs
+++ b/src/Futhark/Doc/Generator.hs
@@ -344,9 +344,9 @@
   fullRow <$> typeBindHtml name' tb
 
 typeBindHtml :: Html -> TypeBind -> DocM Html
-typeBindHtml name' (TypeBind _ tparams t _ _) = do
+typeBindHtml name' (TypeBind _ l tparams t _ _) = do
   t' <- noLink (map typeParamName tparams) $ typeDeclHtml t
-  return $ typeAbbrevHtml Unlifted name' tparams <> " = " <> t'
+  return $ typeAbbrevHtml l name' tparams <> " = " <> t'
 
 renderEnv :: Env -> DocM Html
 renderEnv (Env vtable ttable sigtable modtable _) = do
@@ -475,7 +475,8 @@
   TypeSpec l name ps _ _ ->
     return $ fullRow $ keyword l' <> vnameSynopsisDef name <> mconcat (map ((" "<>) . typeParamHtml) ps)
     where l' = case l of Unlifted -> "type "
-                         Lifted   -> "type^ "
+                         SizeLifted -> "type~ "
+                         Lifted -> "type^ "
   ValSpec name tparams rettype _ _ -> do
     let tparams' = map typeParamHtml tparams
     rettype' <- noLink (map typeParamName tparams) $
@@ -578,14 +579,12 @@
 
 typeParamHtml :: TypeParam -> Html
 typeParamHtml (TypeParamDim name _) = brackets $ vnameHtml name
-typeParamHtml (TypeParamType Unlifted name _) = "'" <> vnameHtml name
-typeParamHtml (TypeParamType Lifted name _) = "'^" <> vnameHtml name
+typeParamHtml (TypeParamType l name _) = fromString (pretty l) <> vnameHtml name
 
 typeAbbrevHtml :: Liftedness -> Html -> [TypeParam] -> Html
 typeAbbrevHtml l name params =
   what <> name <> mconcat (map ((" "<>) . typeParamHtml) params)
-  where what = case l of Lifted -> keyword "type " <> "^"
-                         Unlifted -> keyword "type "
+  where what = keyword $ "type" ++ pretty l ++ " "
 
 docHtml :: Maybe DocComment -> DocM Html
 docHtml (Just (DocComment doc loc)) =
diff --git a/src/Futhark/Internalise.hs b/src/Futhark/Internalise.hs
--- a/src/Futhark/Internalise.hs
+++ b/src/Futhark/Internalise.hs
@@ -42,13 +42,13 @@
 -- | Convert a program in source Futhark to a program in the Futhark
 -- core language.
 internaliseProg :: MonadFreshNames m =>
-                   Bool -> Imports -> m (Either String (I.Prog SOACS))
+                   Bool -> Imports -> m (I.Prog SOACS)
 internaliseProg always_safe prog = do
   prog_decs <- Defunctorise.transformProg prog
   prog_decs' <- Monomorphise.transformProg prog_decs
   prog_decs'' <- Defunctionalise.transformProg prog_decs'
-  prog' <- fmap (fmap I.Prog) $ runInternaliseM always_safe $ internaliseValBinds prog_decs''
-  traverse I.renameProg prog'
+  prog' <- I.Prog <$> runInternaliseM always_safe (internaliseValBinds prog_decs'')
+  I.renameProg prog'
 
 internaliseValBinds :: [E.ValBind] -> InternaliseM ()
 internaliseValBinds = mapM_ internaliseValBind
@@ -67,7 +67,7 @@
 
 internaliseValBind :: E.ValBind -> InternaliseM ()
 internaliseValBind fb@(E.ValBind entry fname retdecl (Info rettype) tparams params body _ loc) = do
-  info <- bindingParams tparams params $ \pcm shapeparams params' -> do
+  bindingParams tparams params $ \pcm shapeparams params' -> do
     (rettype_bad, rcm) <- internaliseReturnType rettype
     let rettype' = zeroExts rettype_bad
 
@@ -106,15 +106,18 @@
 
     addFunction $ I.FunDef Nothing fname' rettype' all_params body'
 
-    return (fname',
-            pcm<>rcm,
-            map I.paramName free_params,
-            shapenames,
-            map declTypeOf $ concat params',
-            all_params,
-            applyRetType rettype' all_params)
+    if null params'
+      then bindConstant fname (fname',
+                               pcm<>rcm,
+                               applyRetType rettype' constparams)
+      else bindFunction fname (fname',
+                               pcm<>rcm,
+                               map I.paramName free_params,
+                               shapenames,
+                               map declTypeOf $ concat params',
+                               all_params,
+                               applyRetType rettype' all_params)
 
-  bindFunction fname info
   case entry of Just (Info entry') -> generateEntryPoint entry' fb
                 Nothing -> return ()
 
@@ -167,7 +170,14 @@
         args = map (I.Var . I.paramName) $ concat params'
 
     entry_body <- insertStmsM $ do
-      vals <- fst <$> funcall "entry_result" (E.qualName ofname) args loc
+      -- Special case the (rare) situation where the entry point is
+      -- not a function.
+      maybe_const <- internaliseIfConst loc ofname
+      vals <- case maybe_const of
+                Just ses ->
+                  return ses
+                Nothing ->
+                  fst <$> funcall "entry_result" (E.qualName ofname) args loc
       ctx <- extractShapeContext (concat entry_rettype) <$>
              mapM (fmap I.arrayDims . subExpType) vals
       resultBodyM (ctx ++ vals)
@@ -256,6 +266,10 @@
 internaliseExp desc (E.QualParens _ e _) =
   internaliseExp desc e
 
+internaliseExp desc (E.StringLit vs _) =
+  fmap pure $ letSubExp desc $
+  I.BasicOp $ I.ArrayLit (map constant vs) $ I.Prim int8
+
 internaliseExp _ (E.Var (E.QualName _ name) (Info t) loc) = do
   subst <- asks $ M.lookup name . envSubsts
   case subst of
@@ -263,7 +277,7 @@
     Nothing     -> do
       -- If this identifier is the name of a constant, we have to turn it
       -- into a call to the corresponding function.
-      is_const <- lookupConstant loc name
+      is_const <- internaliseIfConst loc name
       case is_const of
         Just ses -> return ses
         Nothing -> (:[]) . I.Var <$> internaliseIdent (E.Ident name (Info t) loc)
@@ -333,13 +347,35 @@
         isArrayLiteral e =
           Just ([], [e])
 
-internaliseExp desc (E.Range start maybe_second end _ _) = do
+internaliseExp desc (E.Range start maybe_second end _ loc) = do
   start' <- internaliseExp1 "range_start" start
   end' <- internaliseExp1 "range_end" $ case end of
     DownToExclusive e -> e
     ToInclusive e -> e
     UpToExclusive e -> e
+  maybe_second' <-
+    traverse (internaliseExp1 "range_second") maybe_second
 
+  -- Construct an error message in case the range is invalid.
+  let conv = case E.typeOf start of
+               E.Scalar (E.Prim (E.Unsigned _)) -> asIntZ Int32
+               _ -> asIntS Int32
+  start'_i32 <- conv start'
+  end'_i32 <- conv end'
+  maybe_second'_i32 <- traverse conv maybe_second'
+  let errmsg =
+        errorMsg $
+        ["Range "] ++
+        [ErrorInt32 start'_i32] ++
+        (case maybe_second'_i32 of
+           Nothing -> []
+           Just second_i32 -> ["..", ErrorInt32 second_i32]) ++
+        (case end of
+           DownToExclusive{} -> ["..>"]
+           ToInclusive{} -> ["..."]
+           UpToExclusive{} -> ["..<"]) ++
+        [ErrorInt32 end'_i32, " is invalid."]
+
   (it, le_op, lt_op) <-
     case E.typeOf start of
       E.Scalar (E.Prim (E.Signed it)) -> return (it, CmpSle it, CmpSlt it)
@@ -352,9 +388,8 @@
                                  ToInclusive{} -> one
                                  UpToExclusive{} -> one
 
-  (step, step_zero) <- case maybe_second of
-    Just second -> do
-      second' <- internaliseExp1 "range_second" second
+  (step, step_zero) <- case maybe_second' of
+    Just second' -> do
       subtracted_step <- letSubExp "subtracted_step" $ I.BasicOp $ I.BinOp (I.Sub it) second' start'
       step_zero <- letSubExp "step_zero" $ I.BasicOp $ I.CmpOp (I.CmpEq $ IntType it) start' second'
       return (subtracted_step, step_zero)
@@ -411,18 +446,25 @@
 
   step_invalid <- letSubExp "step_invalid" $
                   I.BasicOp $ I.BinOp I.LogOr step_wrong_dir step_zero
-  invalid <- letSubExp "range_invalid" $
-             I.BasicOp $ I.BinOp I.LogOr step_invalid bounds_invalid
 
+  cs <- assertingOne $ do
+    invalid <- letSubExp "range_invalid" $
+               I.BasicOp $ I.BinOp I.LogOr step_invalid bounds_invalid
+    valid <- letSubExp "valid" $ I.BasicOp $ I.UnOp I.Not invalid
+
+    letExp "range_valid_c" $
+      I.BasicOp $ I.Assert valid errmsg (loc, mempty)
+
   step_i32 <- asIntS Int32 step
   pos_step <- letSubExp "pos_step" $
               I.BasicOp $ I.BinOp (Mul Int32) step_i32 step_sign_i32
-  num_elems <- letSubExp "num_elems" =<<
-               eIf (eSubExp invalid)
-               (eBody [eSubExp $ intConst Int32 0])
-               (eBody [eDivRoundingUp Int32 (eSubExp distance) (eSubExp pos_step)])
-  pure <$> letSubExp desc (I.BasicOp $ I.Iota num_elems start' step it)
+  num_elems <- certifying cs $
+               letSubExp "num_elems" =<<
+               eDivRoundingUp Int32 (eSubExp distance) (eSubExp pos_step)
 
+  se <- letSubExp desc (I.BasicOp $ I.Iota num_elems start' step it)
+  return [se]
+
 internaliseExp desc (E.Ascript e (TypeDecl dt (Info et)) _ loc) = do
   es <- internaliseExp desc e
   (ts, cm) <- internaliseReturnType et
@@ -445,7 +487,7 @@
              _ -> fail "Futhark.Internalise.internaliseExp: non-numeric type in Negate"
 
 internaliseExp desc e@E.Apply{} = do
-  (qfname, args, _) <- findFuncall e
+  (qfname, args) <- findFuncall e
   let fname = nameFromString $ pretty $ baseName $ qualLeaf qfname
       loc = srclocOf e
       arg_desc = nameToString fname ++ "_arg"
@@ -1248,14 +1290,12 @@
 simpleCmpOp desc op x y =
   letTupExp' desc $ I.BasicOp $ I.CmpOp op x y
 
-findFuncall :: E.Exp -> InternaliseM (E.QualName VName, [E.Exp], [E.StructType])
-findFuncall (E.Var fname (Info t) _) =
-  let (remaining, _) = unfoldFunType t
-  in return (fname, [], map E.toStruct remaining)
-findFuncall (E.Apply f arg _ (Info t) _) = do
-  let (remaining, _) = unfoldFunType t
-  (fname, args, _) <- findFuncall f
-  return (fname, args ++ [arg], map E.toStruct remaining)
+findFuncall :: E.Exp -> InternaliseM (E.QualName VName, [E.Exp])
+findFuncall (E.Var fname _ _) =
+  return (fname, [])
+findFuncall (E.Apply f arg _ _ _) = do
+  (fname, args) <- findFuncall f
+  return (fname, args ++ [arg])
 findFuncall e =
   fail $ "Invalid function expression in application: " ++ pretty e
 
@@ -1608,17 +1648,17 @@
 
 -- | Is the name a value constant?  If so, create the necessary
 -- function call and return the corresponding subexpressions.
-lookupConstant :: SrcLoc -> VName -> InternaliseM (Maybe [SubExp])
-lookupConstant loc name = do
-  is_const <- lookupFunction' name
+internaliseIfConst :: SrcLoc -> VName -> InternaliseM (Maybe [SubExp])
+internaliseIfConst loc name = do
+  is_const <- lookupConst name
   scope <- askScope
   case is_const of
-    Just (fname, constparams, _, _, _, _, mk_rettype)
+    Just (fname, constparams, mk_rettype)
       | name `M.notMember` scope -> do
       (constargs, const_ds, const_ts) <- unzip3 <$> constFunctionArgs loc constparams
       safety <- askSafety
       case mk_rettype $ zip constargs $ map I.fromDecl const_ts of
-        Nothing -> fail $ "lookupConstant: " ++
+        Nothing -> fail $ "internaliseIfConst: " ++
                    unwords (pretty name : zipWith (curry pretty) constargs const_ts) ++
                    " failed"
         Just rettype ->
diff --git a/src/Futhark/Internalise/Defunctionalise.hs b/src/Futhark/Internalise/Defunctionalise.hs
--- a/src/Futhark/Internalise/Defunctionalise.hs
+++ b/src/Futhark/Internalise/Defunctionalise.hs
@@ -10,6 +10,7 @@
 import           Data.List
 import qualified Data.List.NonEmpty as NE
 import           Data.Loc
+import           Data.Maybe
 import qualified Data.Map.Strict as M
 import qualified Data.Set as S
 import qualified Data.Sequence as Seq
@@ -137,12 +138,22 @@
   -- Construct a record literal that closes over the environment of
   -- the lambda.  Closed-over 'DynamicFun's are converted to their
   -- closure representation.
-  env <- restrictEnvTo $
-         freeVars (Lambda pats e0 Nothing (Info (closure, ret)) loc) `without`
-         mconcat (map (oneName . typeParamName) tparams)
+  let used = freeVars (Lambda pats e0 Nothing (Info (closure, ret)) loc)
+             `without` mconcat (map (oneName . typeParamName) tparams)
+  env <- restrictEnvTo used
+
   let (fields, env') = unzip $ map closureFromDynamicFun $ M.toList env
-  return (RecordLit fields loc, LambdaSV dims pat ret' e0' $ M.fromList env')
+      env'' = M.fromList env'
+      dimIfNotInClosure v = do
+        guard $ v `M.notMember` env''
+        guard $ v `notElem` dims
+        return v
+      closure_dims =
+        mapMaybe dimIfNotInClosure $ S.toList $ patternDimNames pat
 
+  return (RecordLit fields loc,
+          LambdaSV (dims++closure_dims) pat ret' e0' env'')
+
   where closureFromDynamicFun (vn, DynamicFun (clsr_env, sv) _) =
           let name = nameFromString $ pretty vn
           in (RecordFieldExplicit name clsr_env noLoc, (vn, sv))
@@ -166,6 +177,9 @@
 defuncExp e@FloatLit{} =
   return (e, Dynamic $ typeOf e)
 
+defuncExp e@StringLit{} =
+  return (e, Dynamic $ typeOf e)
+
 defuncExp (Parens e loc) = do
   (e', sv) <- defuncExp e
   return (Parens e' loc, sv)
@@ -176,8 +190,7 @@
 
 defuncExp (TupLit es loc) = do
   (es', svs) <- unzip <$> mapM defuncExp es
-  return (TupLit es' loc, RecordSV $ zip fields svs)
-  where fields = map (nameFromString . show) [(1 :: Int) ..]
+  return (TupLit es' loc, RecordSV $ zip tupleFieldNames svs)
 
 defuncExp (RecordLit fs loc) = do
   (fs', names_svs) <- unzip <$> mapM defuncField fs
@@ -449,21 +462,24 @@
 -- | Defunctionalize a let-bound function, while preserving parameters
 -- that have order 0 types (i.e., non-functional).
 defuncLet :: [TypeParam] -> [Pattern] -> Exp -> Info StructType
-          -> DefM ([Pattern], Exp, StaticVal)
+          -> DefM ([TypeParam], [Pattern], Exp, StaticVal)
 defuncLet dims ps@(pat:pats) body (Info rettype)
   | patternOrderZero pat = do
-      let env = envFromPattern pat
-          bound_by_pat = (`S.member` patternDimNames pat) . typeParamName
-          (_pat_dims, rest_dims) = partition bound_by_pat dims
-      (pats', body', sv) <- localEnv env $ defuncLet rest_dims pats body (Info rettype)
+
+      let bound_by_pat = (`S.member` patternDimNames pat) . typeParamName
+          -- Take care to not include more size parameters than necessary.
+          (pat_dims, rest_dims) = partition bound_by_pat dims
+          env = envFromPattern pat <> envFromShapeParams pat_dims
+      (rest_dims', pats', body', sv) <- localEnv env $ defuncLet rest_dims pats body (Info rettype)
       closure <- defuncFun dims ps body (mempty, rettype) noLoc
-      return (pat : pats', body', DynamicFun closure sv)
+      return (pat_dims ++ rest_dims', pat : pats', body', DynamicFun closure sv)
   | otherwise = do
       (e, sv) <- defuncFun dims ps body (mempty, rettype) noLoc
-      return ([], e, sv)
+      return ([], [], e, sv)
+
 defuncLet _ [] body (Info rettype) = do
   (body', sv) <- defuncExp body
-  return ([], body', imposeType sv rettype )
+  return ([], [], body', imposeType sv rettype )
   where imposeType Dynamic{} t =
           Dynamic $ fromStruct t
         imposeType (RecordSV fs1) (Scalar (Record fs2)) =
@@ -659,8 +675,10 @@
         problematic v = (v `member` bound) && not (boundAsUnique v)
         comb (Scalar (Record fs_annot)) (Scalar (Record fs_got)) =
           Scalar $ Record $ M.intersectionWith comb fs_annot fs_got
-        comb (Scalar Arrow{}) t = descend t
-        comb got et = descend $ fromStruct got `setUniqueness` uniqueness et `setAliases` aliases et
+        comb (Scalar Arrow{}) t =
+          descend t
+        comb got et =
+          descend $ fromStruct got `setUniqueness` uniqueness et `setAliases` aliases et
 
         descend t@Array{}
           | any (problematic . aliasVar) (aliases t) = t `setUniqueness` Nonunique
@@ -801,6 +819,7 @@
   Literal{}            -> mempty
   IntLit{}             -> mempty
   FloatLit{}           -> mempty
+  StringLit{}          -> mempty
   Parens e _           -> freeVars e
   QualParens _ e _     -> freeVars e
   TupLit es _          -> foldMap freeVars es
@@ -889,12 +908,7 @@
         onDim _            = AnyDim
 
 defuncValBind valbind@(ValBind _ name retdecl rettype tparams params body _ _) = do
-  let env = envFromShapeParams tparams
-  (params', body', sv) <- localEnv env $ defuncLet tparams params body rettype
-  -- Remove any shape parameters that no longer occur in the value parameters.
-  let dim_names = foldMap patternDimNames params'
-      tparams' = filter ((`S.member` dim_names) . typeParamName) tparams
-
+  (tparams', params', body', sv) <- defuncLet tparams params body rettype
   let rettype' = anyDimShapeAnnotations $ toStruct $ typeOf body'
   return ( valbind { valBindRetDecl    = retdecl
                    , valBindRetType    = Info $ combineTypeShapes
diff --git a/src/Futhark/Internalise/Defunctorise.hs b/src/Futhark/Internalise/Defunctorise.hs
--- a/src/Futhark/Internalise/Defunctorise.hs
+++ b/src/Futhark/Internalise/Defunctorise.hs
@@ -244,9 +244,9 @@
   TypeDecl <$> transformTypeExp dt <*> (Info <$> transformStructType et)
 
 transformTypeBind :: TypeBind -> TransformM ()
-transformTypeBind (TypeBind name tparams te doc loc) = do
+transformTypeBind (TypeBind name l tparams te doc loc) = do
   name' <- transformName name
-  emit =<< TypeDec <$> (TypeBind name' <$> traverse transformNames tparams
+  emit =<< TypeDec <$> (TypeBind name' l <$> traverse transformNames tparams
                         <*> transformTypeDecl te <*> pure doc <*> pure loc)
 
 transformModBind :: ModBind -> TransformM Scope
diff --git a/src/Futhark/Internalise/Monad.hs b/src/Futhark/Internalise/Monad.hs
--- a/src/Futhark/Internalise/Monad.hs
+++ b/src/Futhark/Internalise/Monad.hs
@@ -7,15 +7,17 @@
   , InternaliseEnv (..)
   , ConstParams
   , Closure
-  , FunInfo
+  , FunInfo, ConstInfo
 
   , substitutingVars
   , addFunction
 
   , lookupFunction
   , lookupFunction'
+  , lookupConst
 
   , bindFunction
+  , bindConstant
 
   , asserting
   , assertingOne
@@ -58,6 +60,10 @@
 
 type FunTable = M.Map VName FunInfo
 
+type ConstInfo = (Name, ConstParams, [(SubExp,Type)] -> Maybe [DeclExtType])
+
+type ConstTable = M.Map VName ConstInfo
+
 -- | A mapping from external variable names to the corresponding
 -- internalised subexpressions.
 type VarSubstitutions = M.Map VName [SubExp]
@@ -71,23 +77,22 @@
 data InternaliseState = InternaliseState {
     stateNameSource :: VNameSource
   , stateFunTable :: FunTable
+  , stateConstTable :: ConstTable
   }
 
 newtype InternaliseResult = InternaliseResult [FunDef SOACS]
   deriving (Semigroup, Monoid)
 
 newtype InternaliseM  a = InternaliseM (BinderT SOACS
-                                        (RWST
+                                        (RWS
                                          InternaliseEnv
                                          InternaliseResult
-                                         InternaliseState
-                                         (Except String))
+                                         InternaliseState)
                                         a)
   deriving (Functor, Applicative, Monad,
             MonadReader InternaliseEnv,
             MonadState InternaliseState,
             MonadFreshNames,
-            MonadError String,
             HasScope SOACS,
             LocalScope SOACS)
 
@@ -96,7 +101,7 @@
   putNameSource src = modify $ \s -> s { stateNameSource = src }
 
 instance Fail.MonadFail InternaliseM where
-  fail = InternaliseM . throwError
+  fail = error . ("InternaliseM: "++)
 
 instance MonadBinder InternaliseM where
   type Lore InternaliseM = SOACS
@@ -110,14 +115,12 @@
 
 runInternaliseM :: MonadFreshNames m =>
                    Bool -> InternaliseM ()
-                -> m (Either String [FunDef SOACS])
+                -> m [FunDef SOACS]
 runInternaliseM safe (InternaliseM m) =
-  modifyNameSource $ \src -> do
-  let onError e             = (Left e, src)
-      onSuccess (funs,src') = (Right funs, src')
-  either onError onSuccess $ runExcept $ do
-    (_, s, InternaliseResult funs) <- runRWST (runBinderT m mempty) newEnv (newState src)
-    return (funs, stateNameSource s)
+  modifyNameSource $ \src ->
+  let (_, s, InternaliseResult funs) =
+        runRWS (runBinderT m mempty) newEnv (newState src)
+  in (funs, stateNameSource s)
   where newEnv = InternaliseEnv {
                    envSubsts = mempty
                  , envDoBoundsChecks = True
@@ -126,6 +129,7 @@
         newState src =
           InternaliseState { stateNameSource = src
                            , stateFunTable = mempty
+                           , stateConstTable = mempty
                            }
 
 substitutingVars :: VarSubstitutions -> InternaliseM a -> InternaliseM a
@@ -142,10 +146,17 @@
 lookupFunction fname = maybe bad return =<< lookupFunction' fname
   where bad = fail $ "Internalise.lookupFunction: Function '" ++ pretty fname ++ "' not found."
 
+lookupConst :: VName -> InternaliseM (Maybe ConstInfo)
+lookupConst fname = gets $ M.lookup fname . stateConstTable
+
 bindFunction :: VName -> FunInfo -> InternaliseM ()
 bindFunction fname info =
   modify $ \s -> s { stateFunTable = M.insert fname info $ stateFunTable s }
 
+bindConstant :: VName -> ConstInfo -> InternaliseM ()
+bindConstant cname info =
+  modify $ \s -> s { stateConstTable = M.insert cname info $ stateConstTable s }
+
 -- | Execute the given action if 'envDoBoundsChecks' is true, otherwise
 -- just return an empty list.
 asserting :: InternaliseM Certificates
@@ -172,8 +183,7 @@
   InternaliseTypeM (ReaderT TypeEnv (StateT TypeState InternaliseM) a)
   deriving (Functor, Applicative, Monad,
             MonadReader TypeEnv,
-            MonadState TypeState,
-            MonadError String)
+            MonadState TypeState)
 
 liftInternaliseM :: InternaliseM a -> InternaliseTypeM a
 liftInternaliseM = InternaliseTypeM . lift . lift
diff --git a/src/Futhark/Internalise/Monomorphise.hs b/src/Futhark/Internalise/Monomorphise.hs
--- a/src/Futhark/Internalise/Monomorphise.hs
+++ b/src/Futhark/Internalise/Monomorphise.hs
@@ -163,6 +163,7 @@
 transformExp e@Literal{} = return e
 transformExp e@IntLit{} = return e
 transformExp e@FloatLit{} = return e
+transformExp e@StringLit{} = return e
 
 transformExp (Parens e loc) =
   Parens <$> transformExp e <*> pure loc
@@ -584,11 +585,11 @@
   return mempty { envPolyBindings = M.singleton (valBindName valbind) valbind' }
 
 transformTypeBind :: TypeBind -> MonoM Env
-transformTypeBind (TypeBind name tparams tydecl _ _) = do
+transformTypeBind (TypeBind name l tparams tydecl _ _) = do
   subs <- asks $ M.map TypeSub . envTypeBindings
   noticeDims $ unInfo $ expandedType tydecl
   let tp = substituteTypes subs . unInfo $ expandedType tydecl
-      tbinding = TypeAbbr Lifted tparams tp -- The Lifted is arbitrary.
+      tbinding = TypeAbbr l tparams tp
   return mempty { envTypeBindings = M.singleton name tbinding }
 
 -- | Monomorphize a list of top-level declarations. A module-free input program
diff --git a/src/Futhark/Internalise/TypesValues.hs b/src/Futhark/Internalise/TypesValues.hs
--- a/src/Futhark/Internalise/TypesValues.hs
+++ b/src/Futhark/Internalise/TypesValues.hs
@@ -92,17 +92,22 @@
   where namedDim (E.QualName _ name) = do
           subst <- liftInternaliseM $ asks $ M.lookup name . envSubsts
           is_dim <- lookupDim name
-          case (is_dim, subst) of
-            (Just dim, _) -> return dim
-            (Nothing, Just [v]) -> return $ I.Free v
-            _ -> do -- Then it must be a constant.
-              let fname = nameFromString $ pretty name ++ "f"
+          is_const <- liftInternaliseM $ lookupConst name
+
+          case (is_dim, is_const, subst) of
+            (Just dim, _, _) -> return dim
+
+            (Nothing, Nothing, Just [v]) -> return $ I.Free v
+
+            (_, Just (fname, _, _), _) -> do
               (i,cm) <- get
               case find ((==fname) . fst) cm of
                 Just (_, known) -> return $ I.Free $ I.Var known
                 Nothing -> do new <- liftInternaliseM $ newVName $ baseString name
                               put (i, (fname,new):cm)
                               return $ I.Free $ I.Var new
+
+            _ -> return $ I.Free $ I.Var name
 
 internaliseTypeM :: E.StructType
                  -> InternaliseTypeM [I.TypeBase ExtShape Uniqueness]
diff --git a/src/Futhark/Optimise/Fusion.hs b/src/Futhark/Optimise/Fusion.hs
--- a/src/Futhark/Optimise/Fusion.hs
+++ b/src/Futhark/Optimise/Fusion.hs
@@ -96,7 +96,7 @@
 gatherStmPattern pat e = binding $ zip idents aliases
   where idents = patternIdents pat
         aliases = replicate (length (patternContextNames pat)) mempty ++
-                  expAliases (Alias.analyseExp e)
+                  expAliases (Alias.analyseExp mempty e)
 
 bindingPat :: Pattern -> FusionGM a -> FusionGM a
 bindingPat = binding . (`zip` repeat mempty) . patternIdents
@@ -650,7 +650,7 @@
 
   where cs = stmCerts bnd
         rem_bnds = bnd : bnds
-        consumed = consumedInExp $ Alias.analyseExp e
+        consumed = consumedInExp $ Alias.analyseExp mempty e
 
         reduceLike soac lambdas nes = do
           (used_lam, lres)  <- foldM fusionGatherLam (mempty, fres) lambdas
diff --git a/src/Futhark/Optimise/InPlaceLowering/LowerIntoStm.hs b/src/Futhark/Optimise/InPlaceLowering/LowerIntoStm.hs
--- a/src/Futhark/Optimise/InPlaceLowering/LowerIntoStm.hs
+++ b/src/Futhark/Optimise/InPlaceLowering/LowerIntoStm.hs
@@ -78,7 +78,7 @@
                       -> SegSpace -> KernelBody (Aliases Kernels)
                       -> Maybe (KernelBody (Aliases Kernels))
 lowerUpdateIntoKernel update kspace kbody = do
-  [Returns se] <- Just $ kernelBodyResult kbody
+  [Returns _ se] <- Just $ kernelBodyResult kbody
   is' <- mapM dimFix is
   let ret = WriteReturns (arrayDims $ snd bindee_attr) src [(is'++map Var gtids, se)]
   return kbody { kernelBodyResult = [ret] }
diff --git a/src/Futhark/Optimise/Simplify/Rules.hs b/src/Futhark/Optimise/Simplify/Rules.hs
--- a/src/Futhark/Optimise/Simplify/Rules.hs
+++ b/src/Futhark/Optimise/Simplify/Rules.hs
@@ -604,11 +604,18 @@
           Just $ pure $ SubExpResult mempty $ Var idd
 
       | Just inds' <- sliceIndices inds,
-        Just (e, cs) <- ST.index idd inds' vtable,
+        Just (ST.Indexed cs e) <- ST.index idd inds' vtable,
         worthInlining e,
         all (`ST.elem` vtable) (unCertificates cs) ->
-        Just $ SubExpResult cs <$> (letSubExp "index_primexp" =<< toExp e)
+          Just $ SubExpResult cs <$> (letSubExp "index_primexp" =<< toExp e)
 
+      | Just inds' <- sliceIndices inds,
+        Just (ST.IndexedArray cs arr inds'') <- ST.index idd inds' vtable,
+        all worthInlining inds'',
+        all (`ST.elem` vtable) (unCertificates cs) ->
+          Just $ IndexResult cs arr . map DimFix <$>
+          mapM (letSubExp "index_primexp" <=< toExp) inds''
+
     Nothing -> Nothing
 
     Just (SubExp (Var v), cs) -> Just $ pure $ IndexResult cs v inds
@@ -1037,12 +1044,14 @@
 -- array literals.
 ruleBasicOp vtable pat _ (Update dest is se)
   | Just dest_t <- ST.lookupType dest vtable,
-    isFullSlice (arrayShape dest_t) is =
-      Simplify $ letBind_ pat $ BasicOp $
+    isFullSlice (arrayShape dest_t) is = Simplify $
       case se of
-        Var v | not $ null $ sliceDims is ->
-                  Reshape (map DimNew $ arrayDims dest_t) v
-        _ -> ArrayLit [se] $ rowType dest_t
+        Var v | not $ null $ sliceDims is -> do
+                  v_reshaped <- letExp (baseString v ++ "_reshaped") $
+                                BasicOp $ Reshape (map DimNew $ arrayDims dest_t) v
+                  letBind_ pat $ BasicOp $ Copy v_reshaped
+
+        _ -> letBind_ pat $ BasicOp $ ArrayLit [se] $ rowType dest_t
 
 -- | Simplify a chain of in-place updates and copies.  This chain is
 -- often produced by in-place lowering.
diff --git a/src/Futhark/Optimise/TileLoops.hs b/src/Futhark/Optimise/TileLoops.hs
--- a/src/Futhark/Optimise/TileLoops.hs
+++ b/src/Futhark/Optimise/TileLoops.hs
@@ -67,7 +67,7 @@
           return (mempty, (lvl, initial_kspace, kbody))
   | otherwise =
       return (mempty, (lvl, initial_kspace, kbody))
-  where isSimpleResult (Returns se) = Just se
+  where isSimpleResult (Returns _ se) = Just se
         isSimpleResult _ = Nothing
 
 tileInBody :: Names -> VarianceTable
@@ -273,7 +273,7 @@
 
         mergeinit' <-
           fmap (map Var) $ certifying (stmAuxCerts aux) $
-          tilingSegMap tiling "tiled_loopinit" (scalarLevel tiling) $
+          tilingSegMap tiling "tiled_loopinit" (scalarLevel tiling) ResultNoSimplify $
           \in_bounds slice ->
             fmap (map Var) $ protectOutOfBounds "loopinit" in_bounds merge_ts $ do
             addPrivStms slice inloop_privstms
@@ -304,7 +304,7 @@
 doPrelude :: Tiling -> Stms Kernels -> [VName] -> Binder Kernels [VName]
 doPrelude tiling prestms prestms_live =
   -- Create a SegMap that takes care of the prelude for every thread.
-  tilingSegMap tiling "prelude" (scalarLevel tiling) $
+  tilingSegMap tiling "prelude" (scalarLevel tiling) ResultMaySimplify $
   \in_bounds _slice -> do
     ts <- mapM lookupType prestms_live
     fmap (map Var) $ letTupExp "pre" =<<
@@ -363,7 +363,7 @@
 -- the kernel.
 data Tiling =
   Tiling
-  { tilingSegMap :: String -> SegLevel
+  { tilingSegMap :: String -> SegLevel -> ResultManifest
                  -> (PrimExp VName -> Slice SubExp -> Binder Kernels [SubExp])
                  -> Binder Kernels [VName]
     -- The boolean PrimExp indicates whether they are in-bounds.
@@ -412,7 +412,7 @@
                 -> Stms Kernels -> Result -> [Type]
                 -> Binder Kernels [VName]
 postludeGeneric tiling privstms pat accs' poststms poststms_res res_ts =
-  tilingSegMap tiling "thread_res" (scalarLevel tiling) $ \in_bounds slice -> do
+  tilingSegMap tiling "thread_res" (scalarLevel tiling) ResultMaySimplify $ \in_bounds slice -> do
     -- Read our per-thread result from the tiled loop.
     forM_ (zip (patternNames pat) accs') $ \(us, everyone) ->
       letBindNames_ [us] $ BasicOp $ Index everyone slice
@@ -453,7 +453,7 @@
 
       -- We don't use a Replicate here, because we want to enforce a
       -- scalar memory space.
-      mergeinits <- tilingSegMap tiling "mergeinit" (scalarLevel tiling) $ \in_bounds slice ->
+      mergeinits <- tilingSegMap tiling "mergeinit" (scalarLevel tiling) ResultNoSimplify $ \in_bounds slice ->
         -- Constant neutral elements (a common case) do not need protection from OOB.
         if freeIn red_nes == mempty
           then return red_nes
@@ -513,10 +513,10 @@
   return $ TileReturns tile_dims arr'
 
 segMap1D :: String
-         -> SegLevel
+         -> SegLevel -> ResultManifest
          -> (VName -> Binder Kernels [SubExp])
          -> Binder Kernels [VName]
-segMap1D desc lvl f = do
+segMap1D desc lvl manifest f = do
   ltid <- newVName "ltid"
   ltid_flat <- newVName "ltid_flat"
   let space = SegSpace ltid_flat [(ltid, unCount $ segGroupSize lvl)]
@@ -528,7 +528,7 @@
   Body _ stms' res' <- renameBody $ mkBody stms res
 
   letTupExp desc $ Op $ SegOp $
-    SegMap lvl space ts $ KernelBody () stms' $ map Returns res'
+    SegMap lvl space ts $ KernelBody () stms' $ map (Returns manifest) res'
 
 reconstructGtids1D :: Count GroupSize SubExp -> VName -> VName -> VName
                    -> Binder Kernels ()
@@ -548,7 +548,7 @@
   tile_size gid gtid num_groups group_size
   kind privstms tile_id arrs_and_perms =
 
-  segMap1D "full_tile" (SegThread num_groups group_size SegNoVirt) $ \ltid -> do
+  segMap1D "full_tile" (SegThread num_groups group_size SegNoVirt) ResultNoSimplify $ \ltid -> do
     j <- letSubExp "j" =<<
          toExp (primExpFromSubExp int32 tile_id *
                 primExpFromSubExp int32 tile_size +
@@ -588,7 +588,7 @@
 
   let tile = map fst tiles_and_perm
 
-  segMap1D "acc" (SegThreadScalar num_groups group_size SegNoVirt) $ \ltid -> do
+  segMap1D "acc" (SegThreadScalar num_groups group_size SegNoVirt) ResultMaySimplify $ \ltid -> do
 
     reconstructGtids1D group_size gtid gid ltid
     addPrivStms [DimFix $ Var ltid] privstms
@@ -666,7 +666,7 @@
   -- Number of whole tiles that fit in the input.
   num_whole_tiles <- letSubExp "num_whole_tiles" $ BasicOp $ BinOp (SQuot Int32) w tile_size
   return Tiling
-    { tilingSegMap = \desc lvl' f -> segMap1D desc lvl' $ \ltid -> do
+    { tilingSegMap = \desc lvl' manifest f -> segMap1D desc lvl' manifest $ \ltid -> do
         letBindNames_ [gtid] =<<
           toExp (LeafExp gid int32 * primExpFromSubExp int32 tile_size +
                  LeafExp ltid int32)
@@ -704,10 +704,10 @@
     Nothing
 
 segMap2D :: String
-         -> SegLevel -> (SubExp, SubExp)
+         -> SegLevel -> ResultManifest -> (SubExp, SubExp)
          -> ((VName, VName) -> Binder Kernels [SubExp])
          -> Binder Kernels [VName]
-segMap2D desc lvl (dim_x, dim_y) f = do
+segMap2D desc lvl manifest (dim_x, dim_y) f = do
   ltid_x <- newVName "ltid_x"
   ltid_y <- newVName "ltid_y"
   ltid_flat <- newVName "ltid_flat"
@@ -720,8 +720,7 @@
   Body _ stms' res' <- renameBody $ mkBody stms res
 
   letTupExp desc $ Op $ SegOp $
-    SegMap lvl space ts $ KernelBody () stms' $ map Returns res'
-
+    SegMap lvl space ts $ KernelBody () stms' $ map (Returns manifest) res'
 
 -- Reconstruct the original gtids from group and local IDs.
 reconstructGtids2D :: SubExp -> (VName, VName) -> (VName, VName) -> (VName, VName)
@@ -741,7 +740,8 @@
            -> [(VName, [Int])]
            -> Binder Kernels [VName]
 readTile2D (kdim_x, kdim_y) (gtid_x, gtid_y) (gid_x, gid_y) tile_size num_groups group_size kind privstms tile_id arrs_and_perms =
-  segMap2D "full_tile" (SegThread num_groups group_size SegNoVirt) (tile_size, tile_size) $ \(ltid_x, ltid_y) -> do
+  segMap2D "full_tile" (SegThread num_groups group_size SegNoVirt)
+  ResultNoSimplify (tile_size, tile_size) $ \(ltid_x, ltid_y) -> do
     i <- letSubExp "i" =<<
          toExp (primExpFromSubExp int32 tile_id *
                 primExpFromSubExp int32 tile_size +
@@ -794,7 +794,8 @@
   -- Might be truncated in case of a partial tile.
   actual_tile_size <- arraysSize 0 <$> mapM (lookupType . fst) tiles_and_perms
 
-  segMap2D "acc" (SegThreadScalar num_groups group_size SegNoVirt) (tile_size, tile_size) $ \(ltid_x, ltid_y) -> do
+  segMap2D "acc" (SegThreadScalar num_groups group_size SegNoVirt)
+    ResultMaySimplify (tile_size, tile_size) $ \(ltid_x, ltid_y) -> do
     reconstructGtids2D tile_size (gtid_x, gtid_y) (gid_x, gid_y) (ltid_x, ltid_y)
 
     addPrivStms [DimFix $ Var ltid_x, DimFix $ Var ltid_y] privstms
@@ -882,7 +883,8 @@
   num_whole_tiles <- letSubExp "num_whole_tiles" $
     BasicOp $ BinOp (SQuot Int32) w tile_size
   return Tiling
-    { tilingSegMap = \desc lvl' f -> segMap2D desc lvl' (tile_size, tile_size) $ \(ltid_x, ltid_y) -> do
+    { tilingSegMap = \desc lvl' manifest f ->
+        segMap2D desc lvl' manifest (tile_size, tile_size) $ \(ltid_x, ltid_y) -> do
         reconstructGtids2D tile_size (gtid_x, gtid_y) (gid_x, gid_y) (ltid_x, ltid_y)
         f (LeafExp gtid_x int32 .<. primExpFromSubExp int32 kdim_x .&&.
            LeafExp gtid_y int32 .<. primExpFromSubExp int32 kdim_y)
diff --git a/src/Futhark/Pass/ExplicitAllocations.hs b/src/Futhark/Pass/ExplicitAllocations.hs
--- a/src/Futhark/Pass/ExplicitAllocations.hs
+++ b/src/Futhark/Pass/ExplicitAllocations.hs
@@ -880,7 +880,7 @@
         coalesceReturnOfShape bs [Constant (IntValue (Int32Value d))] = bs * d > 4
         coalesceReturnOfShape _ _ = True
 
-        hint t (Returns _)
+        hint t Returns{}
           | coalesceReturnOfShape (primByteSize (elemType t)) $ arrayDims t = do
               let space_dims = segSpaceDims space
               t_dims <- mapM dimAllocationSize $ arrayDims t
diff --git a/src/Futhark/Pass/ExtractKernels/BlockedKernel.hs b/src/Futhark/Pass/ExtractKernels/BlockedKernel.hs
--- a/src/Futhark/Pass/ExtractKernels/BlockedKernel.hs
+++ b/src/Futhark/Pass/ExtractKernels/BlockedKernel.hs
@@ -138,7 +138,7 @@
       arr_t <- lookupType arr
       letBindNames_ [paramName p] $
         BasicOp $ Index arr $ fullSlice arr_t [DimFix $ Var gtid]
-    map Returns <$> bodyBind (lambdaBody map_lam)
+    map (Returns ResultMaySimplify) <$> bodyBind (lambdaBody map_lam)
 
   return (space, kbody)
 
@@ -246,7 +246,7 @@
       blockedPerThread gtid w size ordering fold_lam' (length nes) arrs
     let concatReturns pe =
           ConcatReturns split_ordering w elems_per_thread_32 $ patElemName pe
-    return (map (Returns . Var . patElemName) chunk_red_pes ++
+    return (map (Returns ResultMaySimplify . Var . patElemName) chunk_red_pes ++
             map concatReturns chunk_map_pes)
 
   let (redout_ts, mapout_ts) = splitAt (length nes) $ lambdaReturnType fold_lam
@@ -320,7 +320,7 @@
       arr_t <- lookupType arr
       letBindNames_ [paramName p] $
         BasicOp $ Index arr $ fullSlice arr_t [DimFix $ Var gtid]
-    map Returns <$> bodyBind (lambdaBody lam)
+    map (Returns ResultMaySimplify) <$> bodyBind (lambdaBody lam)
 
   letBind_ pat $ Op $ SegOp $ SegHist lvl space ops (lambdaReturnType lam) kbody
 
diff --git a/src/Futhark/Pass/ExtractKernels/DistributeNests.hs b/src/Futhark/Pass/ExtractKernels/DistributeNests.hs
--- a/src/Futhark/Pass/ExtractKernels/DistributeNests.hs
+++ b/src/Futhark/Pass/ExtractKernels/DistributeNests.hs
@@ -647,7 +647,7 @@
 
   (k, k_bnds) <- mapKernel mk_lvl ispace kernel_inps rts k_body
 
-  runBinder_ $ do
+  traverse renameStm <=< runBinder_ $ do
     addStms k_bnds
 
     let pat = Pattern [] $ rearrangeShape perm $
diff --git a/src/Futhark/Pass/ExtractKernels/Distribution.hs b/src/Futhark/Pass/ExtractKernels/Distribution.hs
--- a/src/Futhark/Pass/ExtractKernels/Distribution.hs
+++ b/src/Futhark/Pass/ExtractKernels/Distribution.hs
@@ -252,7 +252,7 @@
   inner_body' <- fmap (uncurry (flip (KernelBody ()))) $ runBinder $
                  localScope ispace_scope $ do
     mapM_ readKernelInput $ filter inputIsUsed inps
-    map Returns <$> bodyBind inner_body
+    map (Returns ResultMaySimplify) <$> bodyBind inner_body
 
   (segop, aux_stms) <- lift $ mapKernel mk_lvl ispace [] rts inner_body'
 
diff --git a/src/Futhark/Pass/ExtractKernels/Intragroup.hs b/src/Futhark/Pass/ExtractKernels/Intragroup.hs
--- a/src/Futhark/Pass/ExtractKernels/Intragroup.hs
+++ b/src/Futhark/Pass/ExtractKernels/Intragroup.hs
@@ -263,4 +263,4 @@
   (Acc min_ws avail_ws log, kstms) <-
     runIntraGroupM $ intraGroupStms lvl $ bodyStms body
   return (S.toList min_ws, S.toList avail_ws, log,
-          KernelBody () kstms $ map Returns $ bodyResult body)
+          KernelBody () kstms $ map (Returns ResultMaySimplify) $ bodyResult body)
diff --git a/src/Futhark/Pipeline.hs b/src/Futhark/Pipeline.hs
--- a/src/Futhark/Pipeline.hs
+++ b/src/Futhark/Pipeline.hs
@@ -130,7 +130,7 @@
           let prog'' = Alias.aliasAnalysis prog'
           when (pipelineValidate cfg) $
             case checkProg prog'' of
-              Left err -> validationError pass prog' $ show err
+              Left err -> validationError pass prog'' $ show err
               Right () -> return ()
           return prog'
 
@@ -138,8 +138,8 @@
           [Pass lore lore] -> Pipeline lore lore
 passes = foldl (>>>) id . map onePass
 
-validationError :: PrettyLore tolore =>
-                   Pass fromlore tolore -> Prog tolore -> String -> FutharkM a
+validationError :: PrettyLore lore =>
+                   Pass fromlore tolore -> Prog lore -> String -> FutharkM a
 validationError pass prog err =
   throwError $ InternalError msg (prettyText prog) CompilerBug
   where msg = "Type error after pass '" <> T.pack (passName pass) <> "':\n" <> T.pack err
diff --git a/src/Futhark/Representation/Kernels/Kernel.hs b/src/Futhark/Representation/Kernels/Kernel.hs
--- a/src/Futhark/Representation/Kernels/Kernel.hs
+++ b/src/Futhark/Representation/Kernels/Kernel.hs
@@ -15,6 +15,7 @@
        , KernelBody(..)
        , aliasAnalyseKernelBody
        , consumedInKernelBody
+       , ResultManifest(..)
        , KernelResult(..)
        , kernelResultSubExp
        , SplitOrdering(..)
@@ -151,7 +152,16 @@
 deriving instance Annotations lore => Show (KernelBody lore)
 deriving instance Annotations lore => Eq (KernelBody lore)
 
-data KernelResult = Returns SubExp
+-- | Metadata about whether there is a subtle point to this
+-- 'KernelResult'.  This is used to protect things like tiling, which
+-- might otherwise be removed by the simplifier because they're
+-- semantically redundant.  This has no semantic effect and can be
+-- ignored at code generation.
+data ResultManifest = ResultNoSimplify -- ^ Don't simplify this one!
+                    | ResultMaySimplify -- ^ Go nuts.
+                  deriving (Eq, Show, Ord)
+
+data KernelResult = Returns ResultManifest SubExp
                     -- ^ Each "worker" in the kernel returns this.
                     -- Whether this is a result-per-thread or a
                     -- result-per-group depends on the 'SegLevel'.
@@ -173,13 +183,13 @@
                   deriving (Eq, Show, Ord)
 
 kernelResultSubExp :: KernelResult -> SubExp
-kernelResultSubExp (Returns se) = se
+kernelResultSubExp (Returns _ se) = se
 kernelResultSubExp (WriteReturns _ arr _) = Var arr
 kernelResultSubExp (ConcatReturns _ _ _ v) = Var v
 kernelResultSubExp (TileReturns _ v) = Var v
 
 instance FreeIn KernelResult where
-  freeIn' (Returns what) = freeIn' what
+  freeIn' (Returns _ what) = freeIn' what
   freeIn' (WriteReturns rws arr res) = freeIn' rws <> freeIn' arr <> freeIn' res
   freeIn' (ConcatReturns o w per_thread_elems v) =
     freeIn' o <> freeIn' w <> freeIn' per_thread_elems <> freeIn' v
@@ -199,8 +209,8 @@
     (substituteNames subst res)
 
 instance Substitute KernelResult where
-  substituteNames subst (Returns se) =
-    Returns $ substituteNames subst se
+  substituteNames subst (Returns manifest se) =
+    Returns manifest (substituteNames subst se)
   substituteNames subst (WriteReturns rws arr res) =
     WriteReturns
     (substituteNames subst rws) (substituteNames subst arr)
@@ -228,7 +238,7 @@
                           KernelBody lore
                        -> KernelBody (Aliases lore)
 aliasAnalyseKernelBody (KernelBody attr stms res) =
-  let Body attr' stms' _ = Alias.analyseBody $ Body attr stms []
+  let Body attr' stms' _ = Alias.analyseBody mempty $ Body attr stms []
   in KernelBody attr' stms' res
 
 removeKernelBodyAliases :: CanBeAliased (Op lore) =>
@@ -271,7 +281,7 @@
       ", but body returns " ++ show (length kres) ++ " values."
     zipWithM_ checkKernelResult kres ts
 
-  where checkKernelResult (Returns what) t =
+  where checkKernelResult (Returns _ what) t =
           TC.require [t] what
         checkKernelResult (WriteReturns rws arr res) t = do
           mapM_ (TC.require [Prim int32]) rws
@@ -310,8 +320,10 @@
     text "return" <+> PP.braces (PP.commasep $ map ppr res)
 
 instance Pretty KernelResult where
-  ppr (Returns what) =
-    text "thread returns" <+> ppr what
+  ppr (Returns ResultNoSimplify what) =
+    text "returns (manifest)" <+> ppr what
+  ppr (Returns ResultMaySimplify what) =
+    text "returns" <+> ppr what
   ppr (WriteReturns rws arr res) =
     ppr arr <+> text "with" <+> PP.apply (map ppRes res)
     where ppRes (is, e) =
@@ -400,7 +412,7 @@
 segResultShape :: SegSpace -> Type -> KernelResult -> Type
 segResultShape _ t (WriteReturns rws _ _) =
   t `arrayOfShape` Shape rws
-segResultShape space t (Returns _) =
+segResultShape space t (Returns _ _) =
   foldr (flip arrayOfRow) t $ segSpaceDims space
 segResultShape _ t (ConcatReturns _ w _ _) =
   t `arrayOfRow` w
@@ -812,27 +824,46 @@
 
 instance Attributes lore => ST.IndexOp (SegOp lore) where
   indexOp vtable k (SegMap _ space _ kbody) is = do
-    Returns se <- maybeNth k $ kernelBodyResult kbody
-    let (gtids, _) = unzip $ unSegSpace space
-    guard $ length gtids == length is
-    let prim_table = M.fromList $ zip gtids $ zip is $ repeat mempty
-        prim_table' = foldl expandPrimExpTable prim_table $ kernelBodyStms kbody
+    Returns ResultMaySimplify se <- maybeNth k $ kernelBodyResult kbody
+    guard $ length gtids <= length is
+    let idx_table = M.fromList $ zip gtids $ map (ST.Indexed mempty) is
+        idx_table' = foldl expandIndexedTable idx_table $ kernelBodyStms kbody
     case se of
-      Var v -> M.lookup v prim_table'
+      Var v -> M.lookup v idx_table'
       _ -> Nothing
-    where expandPrimExpTable table stm
+
+    where (gtids, _) = unzip $ unSegSpace space
+          -- Indexes in excess of what is used to index through the
+          -- segment dimensions.
+          excess_is = drop (length gtids) is
+
+          expandIndexedTable table stm
             | [v] <- patternNames $ stmPattern stm,
               Just (pe,cs) <-
                   runWriterT $ primExpFromExp (asPrimExp table) $ stmExp stm =
-                M.insert v (pe, stmCerts stm <> cs) table
+                M.insert v (ST.Indexed (stmCerts stm <> cs) pe) table
+
+            | [v] <- patternNames $ stmPattern stm,
+              BasicOp (Index arr slice) <- stmExp stm,
+              length (sliceDims slice) == length excess_is,
+              arr `ST.elem` vtable,
+              Just (slice', cs) <- asPrimExpSlice table slice =
+                let idx = ST.IndexedArray (stmCerts stm <> cs)
+                          arr (fixSlice slice' excess_is)
+                in M.insert v idx table
+
             | otherwise =
                 table
 
+          asPrimExpSlice table =
+            runWriterT . mapM (traverse (primExpFromSubExpM (asPrimExp table)))
+
           asPrimExp table v
-            | Just (e,cs) <- M.lookup v table = tell cs >> return e
+            | Just (ST.Indexed cs e) <- M.lookup v table = tell cs >> return e
             | Just (Prim pt) <- ST.lookupType v vtable =
                 return $ LeafExp v pt
             | otherwise = lift Nothing
+
   indexOp _ _ _ _ = Nothing
 
 instance Attributes lore => IsOp (SegOp lore) where
diff --git a/src/Futhark/Representation/Kernels/Simplify.hs b/src/Futhark/Representation/Kernels/Simplify.hs
--- a/src/Futhark/Representation/Kernels/Simplify.hs
+++ b/src/Futhark/Representation/Kernels/Simplify.hs
@@ -205,8 +205,8 @@
     SegSpace phys <$> mapM (traverse Engine.simplify) dims
 
 instance Engine.Simplifiable KernelResult where
-  simplify (Returns what) =
-    Returns <$> Engine.simplify what
+  simplify (Returns manifest what) =
+    Returns manifest <$> Engine.simplify what
   simplify (WriteReturns ws a res) =
     WriteReturns <$> Engine.simplify ws <*> Engine.simplify a <*> Engine.simplify res
   simplify (ConcatReturns o w pte what) =
@@ -253,7 +253,7 @@
   where isInvariant Constant{} = True
         isInvariant (Var v) = isJust $ ST.lookup v vtable
 
-        checkForInvarianceResult (_, pe, Returns se)
+        checkForInvarianceResult (_, pe, Returns _ se)
           | isInvariant se = do
               letBindNames_ [patElemName pe] $
                 BasicOp $ Replicate (Shape $ segSpaceDims space) se
@@ -315,7 +315,8 @@
           | (kpes'', kts'', kres'') <- unzip3 kpes_and_kres ->
               Just (kpe, kpes'', kts'', kres'')
         _ -> Nothing
-      where matches (_, _, kre) = kre == Returns (Var $ patElemName pe)
+      where matches (_, _, Returns _ (Var v)) = v == patElemName pe
+            matches _ = False
 distributeKernelResults _ _ _ _ = Skip
 
 -- If a SegRed contains two reduction operations that have the same
diff --git a/src/Futhark/Representation/SOACS/SOAC.hs b/src/Futhark/Representation/SOACS/SOAC.hs
--- a/src/Futhark/Representation/SOACS/SOAC.hs
+++ b/src/Futhark/Representation/SOACS/SOAC.hs
@@ -487,7 +487,7 @@
     let arr_indexes = M.fromList $ catMaybes $ zipWith arrIndex arr_params arrs
         arr_indexes' = foldl expandPrimExpTable arr_indexes $ bodyStms $ lambdaBody lam
     case se of
-      Var v -> M.lookup v arr_indexes'
+      Var v -> uncurry (flip ST.Indexed) <$> M.lookup v arr_indexes'
       _ -> Nothing
       where lambdaAndSubExp (Screma _ (ScremaForm (_, scan_nes) reds map_lam) arrs) =
               nthMapOut (length scan_nes + redResults reds) map_lam arrs
@@ -499,7 +499,7 @@
               return (lam, se, drop num_accs $ lambdaParams lam, arrs)
 
             arrIndex p arr = do
-              (pe,cs) <- ST.index' arr [i] vtable
+              ST.Indexed cs pe <- ST.index' arr [i] vtable
               return (paramName p, (pe,cs))
 
             expandPrimExpTable table stm
diff --git a/src/Futhark/Test.hs b/src/Futhark/Test.hs
--- a/src/Futhark/Test.hs
+++ b/src/Futhark/Test.hs
@@ -72,11 +72,13 @@
 import Prelude
 
 import Futhark.Analysis.Metrics
-import Futhark.Representation.Primitive (IntType(..), FloatType(..), intByteSize, floatByteSize)
+import Futhark.Representation.Primitive
+       (IntType(..), intValue, FloatType(..), intByteSize, floatByteSize)
 import Futhark.Test.Values
 import Futhark.Util (directoryContents, pmapIO)
 import Futhark.Util.Pretty (pretty, prettyText)
-import Language.Futhark.Syntax (PrimType(..), Int32)
+import Language.Futhark.Syntax (PrimType(..), PrimValue(..))
+import Language.Futhark.Attributes (primValueType, primByteSize)
 
 -- | Description of a test to be carried out on a Futhark program.
 -- The Futhark program is stored separately.
@@ -148,8 +150,8 @@
 data GenValue = GenValue [Int] PrimType
                 -- ^ Generate a value of the given rank and primitive
                 -- type.  Scalars are considered 0-ary arrays.
-              | GenInt Int32
-                -- ^ A fixed non-randomised integer.
+              | GenPrim PrimValue
+                -- ^ A fixed non-randomised primitive value.
               deriving (Show)
 
 -- | A prettyprinted representation of type of value produced by a
@@ -157,8 +159,8 @@
 genValueType :: GenValue -> String
 genValueType (GenValue ds t) =
   concatMap (\d -> "[" ++ show d ++ "]") ds ++ pretty t
-genValueType (GenInt x) =
-  show x ++ "i32"
+genValueType (GenPrim v) =
+  pretty v
 
 -- | How a test case is expected to terminate.
 data ExpectedResult values
@@ -239,7 +241,7 @@
                                      return s
 
 parseRunCases :: Parser [TestRun]
-parseRunCases = parseRunCases' (1::Int)
+parseRunCases = parseRunCases' (0::Int)
   where parseRunCases' i = (:) <$> parseRunCase i <*> parseRunCases' (i+1)
                            <|> pure []
         parseRunCase i = do
@@ -289,11 +291,29 @@
 
 parseGenValue :: Parser GenValue
 parseGenValue = choice [ GenValue <$> many dim <*> parsePrimType
-                       , lexeme $ GenInt . read <$> some (satisfy isDigit)
+                       , lexeme $ GenPrim <$> choice [i8, i16, i32, i64,
+                                                      u8, u16, u32, u64,
+                                                      int SignedValue Int32 ""]
                        ]
-  where dim = between (lexstr "[") (lexstr "]") $
-              lexeme $ read <$> some (satisfy isDigit)
+  where digits = some (satisfy isDigit)
+        dim = between (lexstr "[") (lexstr "]") $
+              lexeme $ read <$> digits
 
+        readint :: String -> Integer
+        readint = read -- To avoid warnings.
+
+        int f t s = try $ lexeme $ f . intValue t  . readint <$> digits <*
+                    string s <*
+                    notFollowedBy (satisfy isAlphaNum)
+        i8  = int SignedValue Int8 "i8"
+        i16 = int SignedValue Int16 "i16"
+        i32 = int SignedValue Int32 "i32"
+        i64 = int SignedValue Int64 "i64"
+        u8  = int UnsignedValue Int8 "u8"
+        u16 = int UnsignedValue Int16 "u16"
+        u32 = int UnsignedValue Int32 "u32"
+        u64 = int UnsignedValue Int64 "u64"
+
 parsePrimType :: Parser PrimType
 parsePrimType =
   choice [ lexstr "i8" $> Signed Int8
@@ -360,7 +380,7 @@
 testSpec =
   ProgramTest <$> parseDescription <*> parseTags <*> parseAction
 
-parserState :: Int -> FilePath -> s -> State s
+parserState :: Int -> FilePath -> s -> State s e
 parserState line name t =
   State { stateInput = t
         , stateOffset = 0
@@ -373,6 +393,7 @@
                               , sourceColumn = mkPos 3 }
           , pstateTabWidth = defaultTabWidth
           , pstateLinePrefix = "-- "}
+        , stateParseErrors = []
         }
 
 
@@ -405,16 +426,16 @@
                            (n,s):ss -> (n, s, ss)
       case readTestSpec (1+first_spec_line) path first_spec of
         Left err -> return $ Left $ errorBundlePretty err
-        Right v  -> Right <$> foldM moreCases v rest_specs
+        Right v  -> return $ foldM moreCases v rest_specs
 
   where moreCases test (lineno, cases) =
           case readInputOutputs lineno path cases of
-            Left err     -> error $ errorBundlePretty err
+            Left err     -> Left $ errorBundlePretty err
             Right cases' ->
               case testAction test of
                 RunCases old_cases structures warnings ->
-                  return test { testAction = RunCases (old_cases ++ cases') structures warnings }
-                _ -> fail "Secondary test block provided, but primary test block specifies compilation error."
+                  Right test { testAction = RunCases (old_cases ++ cases') structures warnings }
+                _ -> Left "Secondary test block provided, but primary test block specifies compilation error."
 
 -- | Like 'testSpecFromFile', but kills the process on error.
 testSpecFromFileOrDie :: FilePath -> IO ProgramTest
@@ -565,9 +586,12 @@
 genFileSize :: GenValue -> Integer
 genFileSize = genSize
   where header_size = 1 + 1 + 1 + 4 -- 'b' <version> <num_dims> <type>
+
         genSize (GenValue ds t) = header_size + toInteger (length ds) * 8 +
                                   product (map toInteger ds) * primSize t
-        genSize (GenInt _) = header_size + primSize (Signed Int32)
+        genSize (GenPrim v) =
+          header_size + primByteSize (primValueType v)
+
         primSize (Signed it) = intByteSize it
         primSize (Unsigned it) = intByteSize it
         primSize (FloatType ft) = floatByteSize ft
@@ -643,23 +667,32 @@
 -- compiling the program with the reference compiler and running it on
 -- the input) if necessary.
 ensureReferenceOutput :: (MonadIO m, MonadError [T.Text] m) =>
-                         FilePath -> String -> FilePath -> [InputOutputs]
+                         Maybe Int -> FilePath -> String -> FilePath -> [InputOutputs]
                       -> m ()
-ensureReferenceOutput futhark compiler prog ios = do
+ensureReferenceOutput concurrency futhark compiler prog ios = do
   missing <- filterM isReferenceMissing $ concatMap entryAndRuns ios
+
   unless (null missing) $ do
     void $ compileProgram [] futhark compiler prog
-    liftIO $ void $ flip pmapIO missing $ \(entry, tr) -> do
+
+    res <- liftIO $ flip (pmapIO concurrency) missing $ \(entry, tr) -> do
       (code, stdout, stderr) <- runProgram "" ["-b"] prog entry $ runInput tr
       case code of
         ExitFailure e ->
-          fail $ "Reference dataset generation failed with exit code " ++
-          show e ++ " and stderr:\n" ++
-          map (chr . fromIntegral) (SBS.unpack stderr)
+          return $ Left
+          [T.pack $ "Reference dataset generation failed with exit code " ++
+           show e ++ " and stderr:\n" ++
+           map (chr . fromIntegral) (SBS.unpack stderr)]
         ExitSuccess -> do
           let f = file (entry, tr)
           liftIO $ createDirectoryIfMissing True $ takeDirectory f
           SBS.writeFile f stdout
+          return $ Right ()
+
+    case sequence_ res of
+      Left err -> throwError err
+      Right () -> return ()
+
   where file (entry, tr) =
           takeDirectory prog </> testRunReferenceOutput prog entry tr
 
diff --git a/src/Futhark/TypeCheck.hs b/src/Futhark/TypeCheck.hs
--- a/src/Futhark/TypeCheck.hs
+++ b/src/Futhark/TypeCheck.hs
@@ -40,10 +40,7 @@
   , checkArg
   , checkSOACArrayArgs
   , checkLambda
-  , checkFun'
-  , checkLambdaParams
   , checkBody
-  , checkLambdaBody
   , consume
   , consumeOnlyParams
   , binding
@@ -492,8 +489,7 @@
   context ("In function " ++ nameToString fname) $
     checkFun' (fname,
                retTypeValues rettype,
-               funParamsToNameInfos params,
-               body) consumable $ do
+               funParamsToNameInfos params) consumable $ do
       checkFunParams params
       checkRetType rettype
       context "When checking function body" $ checkFunBody rettype body
@@ -510,9 +506,18 @@
 
 checkFunParams :: Checkable lore =>
                   [FParam lore] -> TypeM lore ()
-checkFunParams = mapM_ $ \param ->
-  context ("In function parameter " ++ pretty param) $
-    checkFParamLore (paramName param) (paramAttr param)
+checkFunParams params = foldM_ check mempty params
+  where param_bound = namesFromList $ map paramName params
+        check prev param =
+          context ("In function parameter " ++ pretty param) $ do
+            checkFParamLore (paramName param) (paramAttr param)
+            case namesToList $
+                 (freeIn param `namesIntersection` param_bound)
+                 `namesSubtract` prev of
+              [] -> return ()
+              v:_ ->
+                bad $ TypeError $ pretty v ++ " bound in a later parameter."
+            return $ oneName (paramName param) <> prev
 
 checkLambdaParams :: Checkable lore =>
                      [LParam lore] -> TypeM lore ()
@@ -523,22 +528,20 @@
 checkFun' :: Checkable lore =>
              (Name,
               [DeclExtType],
-              [(VName, NameInfo (Aliases lore))],
-              BodyT (Aliases lore))
+              [(VName, NameInfo (Aliases lore))])
           -> [(VName, Names)]
-          -> TypeM lore ()
+          -> TypeM lore [Names]
           -> TypeM lore ()
-checkFun' (fname, rettype, params, body) consumable check = do
+checkFun' (fname, rettype, params) consumable check = do
   checkNoDuplicateParams
   binding (M.fromList params) $
     consumeOnlyParams consumable $ do
-      check
+      body_aliases <- check
       scope <- askScope
       let isArray = maybe False ((>0) . arrayRank . typeOf) . (`M.lookup` scope)
       context ("When checking the body aliases: " ++
-               pretty (map namesToList $ bodyAliases body)) $
-        checkReturnAlias $ map (namesFromList . filter isArray . namesToList) $
-        bodyAliases body
+               pretty (map namesToList body_aliases)) $
+        checkReturnAlias $ map (namesFromList . filter isArray . namesToList) body_aliases
   where param_names = map fst params
 
         checkNoDuplicateParams = foldM_ expand [] param_names
@@ -598,19 +601,24 @@
 checkFunBody :: Checkable lore =>
                 [RetType lore]
              -> Body (Aliases lore)
-             -> TypeM lore ()
+             -> TypeM lore [Names]
 checkFunBody rt (Body (_,lore) bnds res) = do
+  checkBodyLore lore
   checkStms bnds $ do
     context "When checking body result" $ checkResult res
     context "When matching declared return type to result of body" $
       matchReturnType rt res
-  checkBodyLore lore
+    map (`namesSubtract` bound_here) <$> mapM subExpAliasesM res
+  where bound_here = namesFromList $ M.keys $ scopeOf bnds
 
 checkLambdaBody :: Checkable lore =>
-                   [Type] -> Body (Aliases lore) -> TypeM lore ()
+                   [Type] -> Body (Aliases lore) -> TypeM lore [Names]
 checkLambdaBody ret (Body (_,lore) bnds res) = do
-  checkStms bnds $ checkLambdaResult ret res
   checkBodyLore lore
+  checkStms bnds $ do
+    checkLambdaResult ret res
+    map (`namesSubtract` bound_here) <$> mapM subExpAliasesM res
+  where bound_here = namesFromList $ M.keys $ scopeOf bnds
 
 checkLambdaResult :: Checkable lore =>
                      [Type] -> Result -> TypeM lore ()
@@ -628,10 +636,13 @@
         " but expected " ++ pretty t
 
 checkBody :: Checkable lore =>
-             Body (Aliases lore) -> TypeM lore ()
+             Body (Aliases lore) -> TypeM lore [Names]
 checkBody (Body (_,lore) bnds res) = do
-  checkStms bnds $ checkResult res
   checkBodyLore lore
+  checkStms bnds $ do
+    checkResult res
+    map (`namesSubtract` bound_here) <$> mapM subExpAliasesM res
+  where bound_here = namesFromList $ M.keys $ scopeOf bnds
 
 checkBasicOp :: Checkable lore =>
                BasicOp (Aliases lore) -> TypeM lore ()
@@ -821,10 +832,9 @@
     context "Inside the loop body" $
       checkFun' (nameFromString "<loop body>",
                  staticShapes rettype,
-                 funParamsToNameInfos mergepat,
-                 loopbody) consumable $ do
+                 funParamsToNameInfos mergepat) consumable $ do
           checkFunParams mergepat
-          checkBody loopbody
+          loopbody_aliases <- checkBody loopbody
 
           let rettype_ext = existentialiseExtTypes (map paramName mergepat) $
                             staticShapes $ map fromDecl rettype
@@ -840,6 +850,8 @@
               bad $ ReturnTypeError (nameFromString "<loop body>")
               (staticShapes rettype') (staticShapes bodyt)
 
+          return loopbody_aliases
+
 checkExp (Op op) = do checker <- asks envCheckOp
                       checker op
 
@@ -1026,8 +1038,7 @@
                staticShapes $ map (`toDecl` Nonunique) rettype,
                [ (paramName param,
                   LParamInfo $ paramAttr param)
-               | param <- params ],
-               body) consumable $ do
+               | param <- params ]) consumable $ do
       checkLambdaParams params
       mapM_ checkType rettype
       checkLambdaBody rettype body
diff --git a/src/Futhark/Util.hs b/src/Futhark/Util.hs
--- a/src/Futhark/Util.hs
+++ b/src/Futhark/Util.hs
@@ -247,12 +247,12 @@
                                  putMVar cell result
               return cell
 
-pmapIO :: (a -> IO b) -> [a] -> IO [b]
-pmapIO f elems = go elems []
+pmapIO :: Maybe Int -> (a -> IO b) -> [a] -> IO [b]
+pmapIO concurrency f elems = go elems []
   where
     go [] res = return res
     go xs res = do
-      numThreads <- getNumCapabilities
+      numThreads <- maybe getNumCapabilities pure concurrency
       let (e,es) = splitAt numThreads xs
       mvars  <- mapM (fork f) e
       result <- mapM takeMVar mvars
diff --git a/src/Language/Futhark/Attributes.hs b/src/Language/Futhark/Attributes.hs
--- a/src/Language/Futhark/Attributes.hs
+++ b/src/Language/Futhark/Attributes.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE FlexibleContexts  #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 -- | This module provides various simple ways to query and manipulate
 -- fundamental Futhark terms, such as types and values.  The intent is to
 -- keep "Futhark.Language.Syntax" simple, and put whatever embellishments
@@ -15,6 +16,7 @@
   , qualify
   , typeName
   , valueType
+  , primValueType
   , leadingOperator
   , progImports
   , decImports
@@ -40,12 +42,14 @@
   , aliases
   , diet
   , arrayRank
+  , arrayShape
   , nestedDims
   , orderZero
   , unfoldFunType
   , foldFunType
   , typeVars
   , typeDimNames
+  , primByteSize
 
   -- * Operations on types
   , rank
@@ -61,9 +65,12 @@
   , removeShapeAnnotations
   , vacuousShapeAnnotations
   , anyDimShapeAnnotations
+  , traverseDims
+  , DimPos(..)
   , tupleRecord
   , isTupleRecord
   , areTupleFields
+  , tupleFields
   , tupleFieldNames
   , sortFields
   , sortConstrs
@@ -104,6 +111,7 @@
 import           Data.Ord
 import           Data.Bifunctor
 import           Data.Bifoldable
+import           Data.Bitraversable (bitraverse)
 
 import           Prelude
 
@@ -164,6 +172,40 @@
                        -> TypeBase newshape as
 modifyShapeAnnotations = first
 
+-- | Where does this dimension occur?
+data DimPos
+  = PosImmediate
+    -- ^ Immediately in the argument to 'traverseDims'.
+  | PosParam
+    -- ^ In a function parameter type.
+  | PosReturn
+    -- ^ In a function return type.
+  deriving (Eq, Ord, Show)
+
+-- | Perform a traversal (possibly including replacement) on sizes
+-- that are parameters in a function type, but also including the type
+-- immediately passed to the function.
+traverseDims :: forall f fdim tdim als.
+                Applicative f =>
+                (DimPos -> fdim -> f tdim)
+             -> TypeBase fdim als
+             -> f (TypeBase tdim als)
+traverseDims f = go PosImmediate
+  where go :: forall als'. DimPos -> TypeBase fdim als' -> f (TypeBase tdim als')
+        go b t@Array{} = bitraverse (f b) pure t
+        go b (Scalar (Record fields)) = Scalar . Record <$> traverse (go b) fields
+        go b (Scalar (TypeVar as u tn targs)) =
+          Scalar <$> (TypeVar as u tn <$> traverse (onTypeArg b) targs)
+        go b (Scalar (Sum cs)) = Scalar . Sum <$> traverse (traverse (go b)) cs
+        go _ (Scalar (Prim t)) = pure $ Scalar $ Prim t
+        go _ (Scalar (Arrow als p t1 t2)) =
+          Scalar <$> (Arrow als p <$> go PosParam t1 <*> go PosReturn t2)
+
+        onTypeArg b (TypeArgDim d loc) =
+          TypeArgDim <$> f b d <*> pure loc
+        onTypeArg b (TypeArgType t loc) =
+          TypeArgType <$> go b t <*> pure loc
+
 -- | Return the uniqueness of a type.
 uniqueness :: TypeBase shape as -> Uniqueness
 uniqueness (Array _ u _ _) = u
@@ -262,6 +304,7 @@
 isTupleRecord (Scalar (Record fs)) = areTupleFields fs
 isTupleRecord _ = Nothing
 
+-- | Does this record map correspond to a tuple?
 areTupleFields :: M.Map Name a -> Maybe [a]
 areTupleFields fs =
   let fs' = sortFields fs
@@ -269,9 +312,13 @@
      then Just $ map snd fs'
      else Nothing
 
--- | Increasing field names for a tuple (starts at 1).
+-- | Construct a record map corresponding to a tuple.
+tupleFields :: [a] -> M.Map Name a
+tupleFields as = M.fromList $ zip tupleFieldNames as
+
+-- | Increasing field names for a tuple (starts at 0).
 tupleFieldNames :: [Name]
-tupleFieldNames = map (nameFromString . show) [(1::Int)..]
+tupleFieldNames = map (nameFromString . show) [(0::Int)..]
 
 -- | Sort fields by their name; taking care to sort numeric fields by
 -- their numeric value.  This ensures that tuples and tuple-like
@@ -346,14 +393,22 @@
 primValueType (FloatValue v)    = FloatType $ floatValueType v
 primValueType BoolValue{}       = Bool
 
+-- | The type of the value.
 valueType :: Value -> ValueType
 valueType (PrimValue bv) = Scalar $ Prim $ primValueType bv
 valueType (ArrayValue _ t) = t
 
--- | Construct a 'ShapeDecl' with the given number of zero-information
+-- | The size of values of this type, in bytes.
+primByteSize :: Num a => PrimType -> a
+primByteSize (Signed it) = Primitive.intByteSize it
+primByteSize (Unsigned it) = Primitive.intByteSize it
+primByteSize (FloatType ft) = Primitive.floatByteSize ft
+primByteSize Bool = 1
+
+-- | Construct a 'ShapeDecl' with the given number of 'AnyDim'
 -- dimensions.
-rank :: Int -> ShapeDecl ()
-rank n = ShapeDecl $ replicate n ()
+rank :: Int -> ShapeDecl (DimDecl VName)
+rank n = ShapeDecl $ replicate n AnyDim
 
 -- | The type is leaving a scope, so clean up any aliases that
 -- reference the bound variables, and turn any dimensions that name
@@ -365,13 +420,16 @@
         onDim (NamedDim qn) | qualLeaf qn `S.member` bound_here = AnyDim
         onDim d = d
 
--- | Perform some operation on a given record field.
+-- | Perform some operation on a given record field.  Returns
+-- 'Nothing' if that field does not exist.
 onRecordField :: (TypeBase dim als -> TypeBase dim als)
               -> [Name]
-              -> TypeBase dim als -> TypeBase dim als
-onRecordField f (k:ks) (Scalar (Record m)) =
-  Scalar $ Record $ M.adjust (onRecordField f ks) k m
-onRecordField f _ t = f t
+              -> TypeBase dim als -> Maybe (TypeBase dim als)
+onRecordField f [] t = Just $ f t
+onRecordField f (k:ks) (Scalar (Record m)) = do
+  t <- onRecordField f ks =<< M.lookup k m
+  Just $ Scalar $ Record $ M.insert k t m
+onRecordField _ _ _ = Nothing
 
 -- | The type of an Futhark term.  The aliasing will refer to itself, if
 -- the term is a non-tuple-typed variable.
@@ -390,6 +448,8 @@
           M.singleton (baseName name) $ t
           `addAliases` S.insert (AliasBound name)
 typeOf (ArrayLit _ (Info t) _) = t
+typeOf (StringLit _ _) =
+  Array mempty Unique (Prim (Unsigned Int8)) (ShapeDecl [AnyDim])
 typeOf (Range _ _ _ (Info t) _) = t
 typeOf (BinOp _ _ _ _ (Info t) _) = t
 typeOf (Project _ _ (Info t) _) = t
@@ -560,10 +620,9 @@
 -- type, with 'Nothing' representing the overloaded parameter type.
 data Intrinsic = IntrinsicMonoFun [PrimType] PrimType
                | IntrinsicOverloadedFun [PrimType] [Maybe PrimType] (Maybe PrimType)
-               | IntrinsicPolyFun [TypeParamBase VName] [TypeBase () ()] (TypeBase () ())
+               | IntrinsicPolyFun [TypeParamBase VName] [StructType] StructType
                | IntrinsicType PrimType
                | IntrinsicEquality -- Special cased.
-               | IntrinsicOpaque
 
 -- | A map of all built-ins.
 intrinsics :: M.Map VName Intrinsic
@@ -571,7 +630,7 @@
 
              map primFun (M.toList Primitive.primFuns) ++
 
-             [("opaque", IntrinsicOpaque)] ++
+             [("opaque", IntrinsicPolyFun [tp_a] [Scalar t_a] $ Scalar t_a)] ++
 
              map unOpFun Primitive.allUnOps ++
 
@@ -660,25 +719,25 @@
 
               ("map_stream",
                IntrinsicPolyFun [tp_a, tp_b]
-                [Scalar (Prim $ Signed Int32) `arr` (arr_a `arr` arr_b), arr_a]
+                [Scalar (Prim $ Signed Int32) `karr` (arr_ka `arr` arr_kb), arr_a]
                 uarr_b),
 
               ("map_stream_per",
                IntrinsicPolyFun [tp_a, tp_b]
-                [Scalar (Prim $ Signed Int32) `arr` (arr_a `arr` arr_b), arr_a]
+                [Scalar (Prim $ Signed Int32) `karr` (arr_ka `arr` arr_kb), arr_a]
                 uarr_b),
 
               ("reduce_stream",
                IntrinsicPolyFun [tp_a, tp_b]
                 [Scalar t_b `arr` (Scalar t_b `arr` Scalar t_b),
-                 Scalar (Prim $ Signed Int32) `arr` (arr_a `arr` Scalar t_b),
+                 Scalar (Prim $ Signed Int32) `karr` (arr_ka `arr` Scalar t_b),
                  arr_a] $
                 Scalar t_b),
 
               ("reduce_stream_per",
                IntrinsicPolyFun [tp_a, tp_b]
                 [Scalar t_b `arr` (Scalar t_b `arr` Scalar t_b),
-                 Scalar (Prim $ Signed Int32) `arr` (arr_a `arr` Scalar t_b),
+                 Scalar (Prim $ Signed Int32) `karr` (arr_ka `arr` Scalar t_b),
                  arr_a] $
                 Scalar t_b),
 
@@ -704,6 +763,11 @@
         t_arr_a_arr_b = Scalar $ Record $ M.fromList $ zip tupleFieldNames [arr_a, arr_b]
 
         arr x y = Scalar $ Arrow mempty Unnamed x y
+
+        kv = VName (nameFromString "k") 2
+        arr_ka = Array () Nonunique t_a (ShapeDecl [NamedDim $ qualName kv])
+        arr_kb = Array () Nonunique t_b (ShapeDecl [NamedDim $ qualName kv])
+        karr x y = Scalar $ Arrow mempty (Named kv) x y
 
         namify i (k,v) = (VName (nameFromString k) i, v)
 
diff --git a/src/Language/Futhark/Core.hs b/src/Language/Futhark/Core.hs
--- a/src/Language/Futhark/Core.hs
+++ b/src/Language/Futhark/Core.hs
@@ -112,23 +112,31 @@
 --
 -- This function assumes that both start and end position is in the
 -- same file (it is not clear what the alternative would even mean).
-locStr :: SrcLoc -> String
-locStr (SrcLoc NoLoc) = "unknown location"
-locStr (SrcLoc (Loc (Pos file line1 col1 _) (Pos _ line2 col2 _)))
-  -- Do not show line2 if it is identical to line1.
-  | line1 == line2 =
-      first_part ++ "-" ++ show col2
-  | otherwise =
-      first_part ++ "-" ++ show line2 ++ ":" ++ show col2
-  where first_part = file ++ ":" ++ show line1 ++ ":" ++ show col1
+locStr :: Located a => a -> String
+locStr a =
+  case locOf a of
+    NoLoc -> "unknown location"
+    Loc (Pos file line1 col1 _) (Pos _ line2 col2 _)
+    -- Do not show line2 if it is identical to line1.
+      | line1 == line2 ->
+          first_part ++ "-" ++ show col2
+      | otherwise ->
+          first_part ++ "-" ++ show line2 ++ ":" ++ show col2
+      where first_part = file ++ ":" ++ show line1 ++ ":" ++ show col1
 
--- | Given a list of strings representing entries in the stack trace,
--- produce a final newline-terminated string for showing to the user.
--- This string should also be preceded by a newline.
-prettyStacktrace :: [String] -> String
-prettyStacktrace = unlines . reverse . stacktrace' . reverse
-  where stacktrace' (x:xs) = (" `-> " ++ x) : map (" |-> "++) xs
-        stacktrace' [] = []
+-- | Given a list of strings representing entries in the stack trace
+-- and the index of the frame to highlight, produce a final
+-- newline-terminated string for showing to the user.  This string
+-- should also be preceded by a newline.  The most recent stack frame
+-- must come first in the list.
+prettyStacktrace :: Int -> [String] -> String
+prettyStacktrace cur = unlines . zipWith f [(0::Int)..]
+  where -- Formatting hack: assume no stack is deeper than 100
+        -- elements.  Since Futhark does not support recursion, going
+        -- beyond that would require a truly perverse program.
+        f i x = (if cur == i then "-> " else "   ") ++
+                '#' : show i ++
+                (if i > 9 then "" else " ") ++ " " ++ x
 
 -- | A name tagged with some integer.  Only the integer is used in
 -- comparisons, no matter the type of @vn@.
diff --git a/src/Language/Futhark/Interpreter.hs b/src/Language/Futhark/Interpreter.hs
--- a/src/Language/Futhark/Interpreter.hs
+++ b/src/Language/Futhark/Interpreter.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE TupleSections #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 module Language.Futhark.Interpreter
   ( Ctx(..)
@@ -10,6 +9,7 @@
   , interpretImport
   , interpretFunction
   , ExtOp(..)
+  , StackFrame(..)
   , typeEnv
   , Value (ValuePrim, ValueArray, ValueRecord)
   , fromTuple
@@ -41,19 +41,22 @@
 
 import Prelude hiding (mod, break)
 
-data ExtOp a = ExtOpTrace SrcLoc String a
-             | ExtOpBreak [SrcLoc] Ctx T.Env a
+data StackFrame = StackFrame { stackFrameLoc :: Loc
+                             , stackFrameCtx :: Ctx
+                             }
+
+instance Located StackFrame where
+  locOf = stackFrameLoc
+
+data ExtOp a = ExtOpTrace Loc String a
+             | ExtOpBreak (NE.NonEmpty StackFrame) a
              | ExtOpError InterpreterError
 
 instance Functor ExtOp where
   fmap f (ExtOpTrace w s x) = ExtOpTrace w s $ f x
-  fmap f (ExtOpBreak w ctx env x) = ExtOpBreak w ctx env $ f x
+  fmap f (ExtOpBreak stack x) = ExtOpBreak stack $ f x
   fmap _ (ExtOpError err) = ExtOpError err
 
-data StackFrame = StackFrame { stackFrameSrcLoc :: SrcLoc
-                             , stackFrameEnv :: Env
-                             }
-
 type Stack = [StackFrame]
 
 -- | The monad in which evaluation takes place.
@@ -71,12 +74,15 @@
 
 stacking :: SrcLoc -> Env -> EvalM a -> EvalM a
 stacking loc env = local $ \(ss, imports) ->
-  if isNoLoc loc then (ss, imports) else (StackFrame loc env:ss, imports)
+  if isNoLoc loc
+  then (ss, imports)
+  else let s = StackFrame (locOf loc) (Ctx env imports)
+       in (s:ss, imports)
   where isNoLoc :: SrcLoc -> Bool
         isNoLoc = (==NoLoc) . locOf
 
-stacktrace :: EvalM [SrcLoc]
-stacktrace = asks $ map stackFrameSrcLoc . reverse . fst
+stacktrace :: EvalM [Loc]
+stacktrace = asks $ map stackFrameLoc . fst
 
 lookupImport :: FilePath -> EvalM (Maybe Env)
 lookupImport f = asks $ M.lookup f . snd
@@ -237,15 +243,15 @@
 
 bad :: SrcLoc -> Env -> String -> EvalM a
 bad loc env s = stacking loc env $ do
-  ss <- map locStr <$> stacktrace
-  liftF $ ExtOpError $ InterpreterError $ "Error at\n" ++ prettyStacktrace ss ++ s
+  ss <- map (locStr . srclocOf) <$> stacktrace
+  liftF $ ExtOpError $ InterpreterError $ "Error at\n" ++ prettyStacktrace 0 ss ++ s
 
 trace :: Value -> EvalM ()
 trace v = do
-  -- We take the second-to-last element of the stack, because any
+  -- We take the second-to-top element of the stack, because any
   -- actual call to 'implicits.trace' is going to be in the trace
   -- function in the prelude, which is not interesting.
-  top <- fromMaybe noLoc . maybeHead . drop 1 . reverse <$> stacktrace
+  top <- fromMaybe noLoc . maybeHead . drop 1 <$> stacktrace
   liftF $ ExtOpTrace top (pretty v) ()
 
 typeEnv :: Env -> T.Env
@@ -266,14 +272,9 @@
   -- wrapper function (intrinsics are never called directly).
   -- This is why we go a step up the stack.
   stack <- asks $ drop 1 . fst
-  case stack of
-    [] -> return ()
-    top:_ -> do
-      let env = stackFrameEnv top
-      imports <- asks snd
-      liftF $ ExtOpBreak
-        (map stackFrameSrcLoc $ reverse stack)
-        (Ctx env imports) (typeEnv env) ()
+  case NE.nonEmpty stack of
+    Nothing -> return ()
+    Just stack' -> liftF $ ExtOpBreak stack' ()
 
 fromArray :: Value -> [Value]
 fromArray (ValueArray as) = elems as
@@ -596,20 +597,38 @@
 
 eval env (ArrayLit vs _ _) = toArray =<< mapM (eval env) vs
 
-eval env (Range start maybe_second end (Info t) _) = do
+eval _ (StringLit vs _) =
+  toArray $ map (ValuePrim . UnsignedValue . Int8Value . fromIntegral) vs
+
+eval env (Range start maybe_second end (Info t) loc) = do
   start' <- asInteger <$> eval env start
   maybe_second' <- traverse (fmap asInteger . eval env) maybe_second
-  (end', dir) <- case end of
-    DownToExclusive e -> (,-1) . (+1) . asInteger <$> eval env e
-    ToInclusive e -> (,maybe 1 (signum . subtract start') maybe_second') .
-                     asInteger <$> eval env e
-    UpToExclusive e -> (,1) . subtract 1 . asInteger <$> eval env e
+  end' <- traverse (fmap asInteger . eval env) end
 
-  let second = fromMaybe (start' + dir) maybe_second'
-      step = second - start'
-  if step == 0 || dir /= signum step then toArray []
-    else toArray $ map toInt [start',second..end']
+  let (end_adj, step, ok) =
+        case (end', maybe_second') of
+          (DownToExclusive end'', Nothing) ->
+            (end'' + 1, -1, start' >= end'')
+          (DownToExclusive end'', Just second') ->
+            (end'' + 1, second' - start', start' >= end'' && second' < start')
 
+          (ToInclusive end'', Nothing) ->
+            (end'', 1, start' <= end'')
+          (ToInclusive end'', Just second')
+            | second' > start' ->
+                (end'', second' - start', start' <= end'')
+            | otherwise ->
+                (end'', second' - start', start' >= end'' && second' /= start')
+
+          (UpToExclusive x, Nothing) ->
+            (x-1, 1, start' <= x)
+          (UpToExclusive x, Just second') ->
+            (x-1, second' - start', start' <= x && second' > start')
+
+  if ok
+    then toArray $ map toInt [start',start'+step..end_adj]
+    else bad loc env $ badRange start' maybe_second' end'
+
   where toInt =
           case stripArray 1 t of
             Scalar (Prim (Signed t')) ->
@@ -618,6 +637,17 @@
               ValuePrim . UnsignedValue . intValue t'
             _ -> error $ "Nonsensical range type: " ++ show t
 
+        badRange start' maybe_second' end' =
+          "Range " ++ pretty start' ++
+          (case maybe_second' of
+             Nothing -> ""
+             Just second' -> ".." ++ pretty second') ++
+          (case end' of
+             DownToExclusive x -> "..>" ++ pretty x
+             ToInclusive x -> "..." ++ pretty x
+             UpToExclusive x -> "..<"++ pretty x) ++
+          " is invalid."
+
 eval env (Var qv _ _) = evalTermVar env qv
 
 eval env (Ascript e td _ loc) = do
@@ -899,8 +929,8 @@
 
 evalDec env (LocalDec d _) = evalDec env d
 evalDec env SigDec{} = return env
-evalDec env (TypeDec (TypeBind v ps t _ _)) = do
-  let abbr = T.TypeAbbr Lifted ps $
+evalDec env (TypeDec (TypeBind v l ps t _ _)) = do
+  let abbr = T.TypeAbbr l ps $
              evalType env $ unInfo $ expandedType t
   return env { envType = M.insert v abbr $ envType env }
 evalDec env (ModDec (ModBind v ps ret body _ loc)) = do
diff --git a/src/Language/Futhark/Parser/Lexer.x b/src/Language/Futhark/Parser/Lexer.x
--- a/src/Language/Futhark/Parser/Lexer.x
+++ b/src/Language/Futhark/Parser/Lexer.x
@@ -77,9 +77,12 @@
   "_"                      { tokenC UNDERSCORE }
   "->"                     { tokenC RIGHT_ARROW }
   ":"                      { tokenC COLON }
+  ":>"                     { tokenC COLON_GT }
   "\"                      { tokenC BACKSLASH }
+  "~"                      { tokenC TILDE }
   "'"                      { tokenC APOSTROPHE }
   "'^"                     { tokenC APOSTROPHE_THEN_HAT }
+  "'~"                     { tokenC APOSTROPHE_THEN_TILDE }
   "`"                      { tokenC BACKTICK }
   "..<"                    { tokenC TWO_DOTS_LT }
   "..>"                    { tokenC TWO_DOTS_GT }
@@ -319,9 +322,11 @@
            | CHARLIT Char
 
            | COLON
+           | COLON_GT
            | BACKSLASH
            | APOSTROPHE
            | APOSTROPHE_THEN_HAT
+           | APOSTROPHE_THEN_TILDE
            | BACKTICK
            | TWO_DOTS
            | TWO_DOTS_LT
@@ -343,6 +348,7 @@
            | NEGATE
            | LTH
            | HAT
+           | TILDE
            | PIPE
 
            | IF
diff --git a/src/Language/Futhark/Parser/Parser.y b/src/Language/Futhark/Parser/Parser.y
--- a/src/Language/Futhark/Parser/Parser.y
+++ b/src/Language/Futhark/Parser/Parser.y
@@ -103,6 +103,7 @@
       '-'             { L $$ NEGATE }
       '<'             { L $$ LTH }
       '^'             { L $$ HAT }
+      '~'             { L $$ TILDE }
       '|'             { L $$ PIPE  }
 
       '+...'          { L _ (SYMBOL Plus _ _) }
@@ -141,10 +142,12 @@
       '\\'            { L $$ BACKSLASH }
       '\''            { L $$ APOSTROPHE }
       '\'^'           { L $$ APOSTROPHE_THEN_HAT }
+      '\'~'           { L $$ APOSTROPHE_THEN_TILDE }
       '`'             { L $$ BACKTICK }
       entry           { L $$ ENTRY }
       '->'            { L $$ RIGHT_ARROW }
       ':'             { L $$ COLON }
+      ':>'            { L $$ COLON_GT }
       for             { L $$ FOR }
       do              { L $$ DO }
       with            { L $$ WITH }
@@ -165,7 +168,7 @@
 %left bottom
 %left ifprec letprec unsafe caseprec typeprec enumprec sumprec
 %left ',' case id constructor '(' '{'
-%right ':'
+%right ':' ':>'
 %right '...' '..<' '..>' '..'
 %left '`'
 %right '->'
@@ -283,6 +286,11 @@
            : ModParam ModParams { $1 : $2 }
            |                    { [] }
 
+Liftedness :: { Liftedness }
+            :     { Unlifted }
+            | '~' { SizeLifted }
+            | '^' { Lifted }
+
 Spec :: { SpecBase NoInfo Name }
       : val id TypeParams ':' TypeExpDecl
         { let L loc (ID name) = $2
@@ -293,18 +301,14 @@
         { ValSpec $2 $3 $5 Nothing (srcspan $1 $>) }
       | TypeAbbr
         { TypeAbbrSpec $1 }
-      | type id TypeParams
-        { let L _ (ID name) = $2
-          in TypeSpec Unlifted name $3 Nothing (srcspan $1 $>) }
-      | type 'id[' id ']' TypeParams
-        { let L _ (INDEXING name) = $2; L ploc (ID pname) = $3
-          in TypeSpec Unlifted name (TypeParamDim pname ploc : $5) Nothing (srcspan $1 $>) }
-      | type '^' id TypeParams
+
+      | type Liftedness id TypeParams
         { let L _ (ID name) = $3
-          in TypeSpec Lifted name $4 Nothing (srcspan $1 $>) }
-      | type '^' 'id[' id ']' TypeParams
+          in TypeSpec $2 name $4 Nothing (srcspan $1 $>) }
+      | type Liftedness 'id[' id ']' TypeParams
         { let L _ (INDEXING name) = $3; L ploc (ID pname) = $4
-          in TypeSpec Lifted name (TypeParamDim pname ploc : $6) Nothing (srcspan $1 $>) }
+          in TypeSpec $2 name (TypeParamDim pname ploc : $6) Nothing (srcspan $1 $>) }
+
       | module id ':' SigExp
         { let L _ (ID name) = $2
           in ModSpec name $4 Nothing (srcspan $1 $>) }
@@ -320,6 +324,7 @@
 TypeParam :: { TypeParamBase Name }
            : '[' id ']' { let L _ (ID name) = $2 in TypeParamDim name (srcspan $1 $>) }
            | '\'' id { let L _ (ID name) = $2 in TypeParamType Unlifted name (srcspan $1 $>) }
+           | '\'~' id { let L _ (ID name) = $2 in TypeParamType SizeLifted name (srcspan $1 $>) }
            | '\'^' id { let L _ (ID name) = $2 in TypeParamType Lifted name (srcspan $1 $>) }
 
 TypeParams :: { [TypeParamBase Name] }
@@ -406,12 +411,12 @@
              : TypeExp %prec bottom { TypeDecl $1 NoInfo }
 
 TypeAbbr :: { TypeBindBase NoInfo Name }
-TypeAbbr : type id TypeParams '=' TypeExpDecl
-           { let L _ (ID name) = $2
-              in TypeBind name $3 $5 Nothing (srcspan $1 $>) }
-         | type 'id[' id ']' TypeParams '=' TypeExpDecl
-           { let L loc (INDEXING name) = $2; L ploc (ID pname) = $3
-             in TypeBind name (TypeParamDim pname ploc:$5) $7 Nothing (srcspan $1 $>) }
+TypeAbbr : type Liftedness id TypeParams '=' TypeExpDecl
+           { let L _ (ID name) = $3
+              in TypeBind name $2 $4 $6 Nothing (srcspan $1 $>) }
+         | type Liftedness 'id[' id ']' TypeParams '=' TypeExpDecl
+           { let L loc (INDEXING name) = $3; L ploc (ID pname) = $4
+             in TypeBind name $2 (TypeParamDim pname ploc:$6) $8 Nothing (srcspan $1 $>) }
 
 TypeExp :: { UncheckedTypeExp }
          : '(' id ':' TypeExp ')' '->' TypeExp
@@ -523,6 +528,7 @@
 -- array slices).
 Exp :: { UncheckedExp }
      : Exp ':' TypeExpDecl { Ascript $1 $3 NoInfo (srcspan $1 $>) }
+     | Exp ':>' TypeExpDecl { Ascript $1 $3 NoInfo (srcspan $1 $>) }
      | Exp2 %prec ':'      { $1 }
 
 Exp2 :: { UncheckedExp }
@@ -616,7 +622,7 @@
      | intlit         { let L loc (INTLIT x) = $1 in IntLit x NoInfo loc }
      | floatlit       { let L loc (FLOATLIT x) = $1 in FloatLit x NoInfo loc }
      | stringlit      { let L loc (STRINGLIT s) = $1 in
-                        ArrayLit (map (flip Literal loc . UnsignedValue . Int8Value . fromIntegral) $ encode s) NoInfo loc }
+                        StringLit (encode s) loc }
      | '(' Exp ')' FieldAccesses
        { foldl (\x (y, _) -> Project y x NoInfo (srclocOf x))
                (Parens $2 (srcspan $1 $3))
@@ -788,7 +794,7 @@
              | intlit         { let L loc (INTLIT x) = $1 in (IntLit x NoInfo loc, loc) }
              | floatlit       { let L loc (FLOATLIT x) = $1 in (FloatLit x NoInfo loc, loc) }
              | stringlit      { let L loc (STRINGLIT s) = $1 in
-                              (ArrayLit (map (flip Literal loc . UnsignedValue . Int8Value . fromIntegral) $ encode s) NoInfo loc, loc) }
+                              (StringLit (encode s) loc, loc) }
 
 LoopForm :: { LoopFormBase NoInfo Name }
 LoopForm : for VarId '<' Exp
@@ -934,14 +940,16 @@
 
 ArrayValue :: { Value }
 ArrayValue :  '[' Value ']'
-             {% return $ ArrayValue (arrayFromList [$2]) $ toStruct $ valueType $2
+             {% return $ ArrayValue (arrayFromList [$2]) $
+                arrayOf (valueType $2) (ShapeDecl [1]) Unique
              }
            |  '[' Value ',' Values ']'
              {% case combArrayElements $2 $4 of
                   Left e -> throwError e
-                  Right v -> return $ ArrayValue (arrayFromList $ $2:$4) $ valueType v
+                  Right v -> return $ ArrayValue (arrayFromList $ $2:$4) $
+                             arrayOf (valueType v) (ShapeDecl [1+fromIntegral (length $4)]) Unique
              }
-           | id '(' RowType ')'
+           | id '(' ValueType ')'
              {% ($1 `mustBe` "empty") >> mustBeEmpty (srcspan $2 $4) $3 >> return (ArrayValue (listArray (0,-1) []) $3) }
 
            -- Errors
@@ -951,9 +959,9 @@
 Dim :: { Int32 }
 Dim : intlit { let L _ (INTLIT num) = $1 in fromInteger num }
 
-RowType :: { ValueType }
-RowType : '[' Dim ']' RowType  { arrayOf $4 (ShapeDecl [$2]) Nonunique }
-        | '[' Dim ']' PrimType { arrayOf (Scalar (Prim $4)) (ShapeDecl [$2]) Nonunique }
+ValueType :: { ValueType }
+ValueType : '[' Dim ']' ValueType  { arrayOf $4 (ShapeDecl [$2]) Nonunique }
+          | '[' Dim ']' PrimType { arrayOf (Scalar (Prim $4)) (ShapeDecl [$2]) Nonunique }
 
 Values :: { [Value] }
 Values : Value ',' Values { $1 : $3 }
diff --git a/src/Language/Futhark/Pretty.hs b/src/Language/Futhark/Pretty.hs
--- a/src/Language/Futhark/Pretty.hs
+++ b/src/Language/Futhark/Pretty.hs
@@ -15,6 +15,7 @@
 where
 
 import           Control.Monad
+import           Codec.Binary.UTF8.String (decode)
 import           Data.Array
 import           Data.Functor
 import qualified Data.Map.Strict       as M
@@ -129,13 +130,13 @@
     | otherwise =
         oneLine (braces $ commasep fs')
         <|> braces (mconcat $ punctuate (text "," <> line) fs')
-    where ppField (name, t) = text (nameToString name) <> colon <+> ppr t
+    where ppField (name, t) = text (nameToString name) <> colon <+> align (ppr t)
           fs' = map ppField $ M.toList fs
   pprPrec p (Arrow _ (Named v) t1 t2) =
     parensIf (p > 1) $
-    parens (pprName v <> colon <+> ppr t1) <+> text "->" <+> pprPrec 1 t2
+    parens (pprName v <> colon <+> ppr t1) <+/> text "->" <+> pprPrec 1 t2
   pprPrec p (Arrow _ Unnamed t1 t2) =
-    parensIf (p > 1) $ pprPrec 2 t1 <+> text "->" <+> pprPrec 1 t2
+    parensIf (p > 1) $ pprPrec 2 t1 <+/> text "->" <+> pprPrec 1 t2
   pprPrec p (Sum cs) =
     parensIf (p > 0) $
     oneLine (mconcat $ punctuate (text " | ") cs')
@@ -202,6 +203,7 @@
 
 letBody :: (Eq vn, IsName vn, Annot f) => ExpBase f vn -> Doc
 letBody body@LetPat{} = ppr body
+letBody body@LetFun{} = ppr body
 letBody body          = text "in" <+> align (ppr body)
 
 instance (Eq vn, IsName vn, Annot f) => Pretty (ExpBase f vn) where
@@ -224,6 +226,8 @@
           fieldArray RecordFieldImplicit{} = False
   pprPrec _ (ArrayLit es _ _) =
     brackets $ commasep $ map ppr es
+  pprPrec _ (StringLit s _) =
+    text $ show $ decode s
   pprPrec p (Range start maybe_step end _ _) =
     parensIf (p /= -1) $ ppr start <>
     maybe mempty ((text ".." <>) . ppr) maybe_step <>
@@ -364,14 +368,19 @@
     where maybe_sig' = case maybe_sig of Nothing       -> mempty
                                          Just (sig, _) -> colon <+> ppr sig
 
+instance Pretty Liftedness where
+  ppr Unlifted = text ""
+  ppr SizeLifted = text "~"
+  ppr Lifted = text "^"
+
 instance (Eq vn, IsName vn, Annot f) => Pretty (TypeBindBase f vn) where
-  ppr (TypeBind name params usertype _ _) =
-    text "type" <+> pprName name <+> spread (map ppr params) <+> equals <+> ppr usertype
+  ppr (TypeBind name l params usertype _ _) =
+    text "type" <> ppr l <+> pprName name <+>
+    spread (map ppr params) <+> equals <+> ppr usertype
 
 instance (Eq vn, IsName vn) => Pretty (TypeParamBase vn) where
   ppr (TypeParamDim name _) = brackets $ pprName name
-  ppr (TypeParamType Unlifted name _) = text "'" <> pprName name
-  ppr (TypeParamType Lifted name _) = text "'^" <> pprName name
+  ppr (TypeParamType l name _) = text "'" <> ppr l <> pprName name
 
 instance (Eq vn, IsName vn, Annot f) => Pretty (ValBindBase f vn) where
   ppr (ValBind entry name retdecl rettype tparams args body _ _) =
@@ -386,8 +395,8 @@
 
 instance (Eq vn, IsName vn, Annot f) => Pretty (SpecBase f vn) where
   ppr (TypeAbbrSpec tpsig) = ppr tpsig
-  ppr (TypeSpec Unlifted name ps _ _) = text "type" <+> pprName name <+> spread (map ppr ps)
-  ppr (TypeSpec Lifted name ps _ _) = text "type^" <+> pprName name <+> spread (map ppr ps)
+  ppr (TypeSpec l name ps _ _) =
+    text "type" <> ppr l <+> pprName name <+> spread (map ppr ps)
   ppr (ValSpec name tparams vtype _ _) =
     text "val" <+> pprName name <+> spread (map ppr tparams) <> colon <+> ppr vtype
   ppr (ModSpec name sig _ _) =
diff --git a/src/Language/Futhark/Semantic.hs b/src/Language/Futhark/Semantic.hs
--- a/src/Language/Futhark/Semantic.hs
+++ b/src/Language/Futhark/Semantic.hs
@@ -157,6 +157,7 @@
             p l <+> pprName name <> mconcat (map ((text " "<>) . ppr) tps) <>
             text " =" <+> ppr tp
             where p Lifted = text "type^"
+                  p SizeLifted = text "type~"
                   p Unlifted = text "type"
           renderValBind (name, BoundV tps t) =
             text "val" <+> pprName name <> mconcat (map ((text " "<>) . ppr) tps) <>
diff --git a/src/Language/Futhark/Syntax.hs b/src/Language/Futhark/Syntax.hs
--- a/src/Language/Futhark/Syntax.hs
+++ b/src/Language/Futhark/Syntax.hs
@@ -602,6 +602,10 @@
             | FloatLit Double (f PatternType) SrcLoc
             -- ^ A polymorphic decimal literal.
 
+            | StringLit [Word8] SrcLoc
+            -- ^ A string literal is just a fancy syntax for an array
+            -- of bytes.
+
             | Parens (ExpBase f vn) SrcLoc
             -- ^ A parenthesized expression.
 
@@ -706,6 +710,7 @@
   locOf (RecordLit _ pos)              = locOf pos
   locOf (Project _ _ _ pos)            = locOf pos
   locOf (ArrayLit _ _ pos)             = locOf pos
+  locOf (StringLit _ loc)              = locOf loc
   locOf (Range _ _ _ _ pos)            = locOf pos
   locOf (BinOp _ _ _ _ _ pos)          = locOf pos
   locOf (If _ _ _ _ pos)               = locOf pos
@@ -815,6 +820,7 @@
 
 -- | Type Declarations
 data TypeBindBase f vn = TypeBind { typeAlias        :: vn
+                                  , typeLiftedness   :: Liftedness
                                   , typeParams       :: [TypeParamBase vn]
                                   , typeExp          :: TypeDeclBase f vn
                                   , typeDoc          :: Maybe DocComment
@@ -826,10 +832,17 @@
   locOf = locOf . typeBindLocation
 
 -- | The liftedness of a type parameter.  By the @Ord@ instance,
--- @Unlifted@ is less than @Lifted@.
-data Liftedness = Unlifted -- ^ May only be instantiated with a zero-order type.
-                | Lifted -- ^ May be instantiated to a functional type.
-                deriving (Eq, Ord, Show)
+-- @Unlifted < SizeLifted < Lifted@.
+data Liftedness
+  = Unlifted
+    -- ^ May only be instantiated with a zero-order type of (possibly
+    -- symbolically) known size.
+  | SizeLifted
+    -- ^ May only be instantiated with a zero-order type, but the size
+    -- can be varying.
+  | Lifted
+    -- ^ May be instantiated with a functional type.
+  deriving (Eq, Ord, Show)
 
 data TypeParamBase vn = TypeParamDim vn SrcLoc
                         -- ^ A type parameter that must be a size.
diff --git a/src/Language/Futhark/Traversals.hs b/src/Language/Futhark/Traversals.hs
--- a/src/Language/Futhark/Traversals.hs
+++ b/src/Language/Futhark/Traversals.hs
@@ -53,6 +53,8 @@
     pure loc
   astMap _ (Literal val loc) =
     pure $ Literal val loc
+  astMap _ (StringLit vs loc) =
+    pure $ StringLit vs loc
   astMap tv (IntLit val t loc) =
     IntLit val <$> traverse (mapOnPatternType tv) t <*> pure loc
   astMap tv (FloatLit val t loc) =
diff --git a/src/Language/Futhark/TypeChecker.hs b/src/Language/Futhark/TypeChecker.hs
--- a/src/Language/Futhark/TypeChecker.hs
+++ b/src/Language/Futhark/TypeChecker.hs
@@ -143,7 +143,7 @@
         f (ValDec (ValBind _ name _ _ _ _ _ _ loc)) =
           check Term name loc
 
-        f (TypeDec (TypeBind name _ _ _ loc)) =
+        f (TypeDec (TypeBind name _ _ _ _ loc)) =
           check Type name loc
 
         f (SigDec (SigBind name _ _ loc)) =
@@ -168,6 +168,11 @@
                      M.singleton v $ TypeAbbr l [] $
                      Scalar $ TypeVar () Nonunique (typeName v) [] }
 
+emptyDimParam :: StructType -> Bool
+emptyDimParam = isNothing . traverseDims onDim
+  where onDim pos AnyDim | pos `elem` [PosImmediate, PosParam] = Nothing
+        onDim _ d = Just d
+
 -- In this function, after the recursion, we add the Env of the
 -- current Spec *after* the one that is returned from the recursive
 -- call.  This implements the behaviour that specs later in a module
@@ -181,12 +186,17 @@
 checkSpecs (ValSpec name tparams vtype doc loc : specs) =
   bindSpaced [(Term, name)] $ do
     name' <- checkName Term name loc
-    (tparams', rettype') <-
+    (tparams', vtype') <-
       checkTypeParams tparams $ \tparams' -> bindingTypeParams tparams' $ do
         (vtype', _) <- checkTypeDecl tparams' vtype
         return (tparams', vtype')
 
-    let binding = BoundV tparams' $ unInfo $ expandedType rettype'
+    when (emptyDimParam $ unInfo $ expandedType vtype') $
+      throwError $ TypeError loc $
+      "All function parameters must have non-anonymous sizes.\n" ++
+      "Hint: add size parameters to " ++ quote (prettyName name') ++ "."
+
+    let binding = BoundV tparams' $ unInfo $ expandedType vtype'
         valenv =
           mempty { envVtable = M.singleton name' binding
                  , envNameMap = M.singleton (Term, name) $ qualName name'
@@ -194,7 +204,7 @@
     (abstypes, env, specs') <- localEnv valenv $ checkSpecs specs
     return (abstypes,
             env <> valenv,
-            ValSpec name' tparams' rettype' doc loc : specs')
+            ValSpec name' tparams' vtype' doc loc : specs')
 
 checkSpecs (TypeAbbrSpec tdec : specs) =
   bindSpaced [(Type, typeAlias tdec)] $ do
@@ -420,7 +430,7 @@
         f (ValSpec name _ _ _ loc) =
           check Term name loc
 
-        f (TypeAbbrSpec (TypeBind name _ _ _ loc)) =
+        f (TypeAbbrSpec (TypeBind name _ _ _ _ loc)) =
           check Type name loc
 
         f (TypeSpec _ name _ _ loc) =
@@ -434,13 +444,30 @@
 
 checkTypeBind :: TypeBindBase NoInfo Name
               -> TypeM (Env, TypeBindBase Info VName)
-checkTypeBind (TypeBind name tps (TypeDecl t NoInfo) doc loc) =
+checkTypeBind (TypeBind name l tps td doc loc) =
   checkTypeParams tps $ \tps' -> do
-    (td', l) <- bindingTypeParams tps' $ do
-      checkForDuplicateNamesInType t
-      (t', st, l) <- checkTypeExp t
-      checkShapeParamUses typeExpUses tps' [t']
-      return (TypeDecl t' $ Info st, l)
+    (td', l') <- bindingTypeParams tps' $ checkTypeDecl tps' td
+
+    case (l, l') of
+      (_, Lifted)
+        | l < Lifted ->
+          throwError $ TypeError loc $
+          "Non-lifted type abbreviations may not contain functions.\n" ++
+          "Hint: consider using 'type^'."
+      (_, SizeLifted)
+        | l < SizeLifted ->
+          throwError $ TypeError loc $
+          "Non-size-lifted type abbreviations may not contain size-lifted types.\n" ++
+          "Hint: consider using 'type~'."
+      (Unlifted, _)
+        | emptyDimParam $ unInfo $ expandedType td' ->
+            warn loc $
+            "Non-lifted type abbreviations may not use anonymous sizes in their definition.\n" ++
+            "This will become an error in a future version of the compiler!\n" ++
+            "Hint: use 'type~' or add size parameters to " ++
+            quote (prettyName name) ++ "."
+      _ -> return ()
+
     bindSpaced [(Type, name)] $ do
       name' <- checkName Type name loc
       return (mempty { envTypeTable =
@@ -448,7 +475,7 @@
                        envNameMap =
                          M.singleton (Type, name) $ qualName name'
                      },
-              TypeBind name' tps' td' doc loc)
+               TypeBind name' l tps' td' doc loc)
 
 checkValBind :: ValBindBase NoInfo Name -> TypeM (Env, ValBind)
 checkValBind (ValBind entry fname maybe_tdecl NoInfo tparams params body doc loc) = do
diff --git a/src/Language/Futhark/TypeChecker/Modules.hs b/src/Language/Futhark/TypeChecker/Modules.hs
--- a/src/Language/Futhark/TypeChecker/Modules.hs
+++ b/src/Language/Futhark/TypeChecker/Modules.hs
@@ -23,8 +23,7 @@
 import Language.Futhark.TypeChecker.Monad
 import Language.Futhark.TypeChecker.Unify (doUnification)
 import Language.Futhark.TypeChecker.Types
-import Futhark.Util.Pretty (Pretty)
-
+import Futhark.Util.Pretty
 
 substituteTypesInMod :: TypeSubs -> Mod -> Mod
 substituteTypesInMod substs (ModEnv e) =
@@ -49,15 +48,7 @@
 substituteTypesInBoundV substs (BoundV tps t) =
   BoundV tps (substituteTypes substs t)
 
-allNamesInMTy :: MTy -> S.Set VName
-allNamesInMTy (MTy abs mod) =
-  S.fromList (map qualLeaf $ M.keys abs) <> allNamesInMod mod
-
-allNamesInMod :: Mod -> S.Set VName
-allNamesInMod (ModEnv env) = allNamesInEnv env
-allNamesInMod ModFun{} = mempty
-
--- All names defined anywhere in the env.
+-- | All names defined anywhere in the 'Env'.
 allNamesInEnv :: Env -> S.Set VName
 allNamesInEnv (Env vtable ttable stable modtable _names) =
   S.fromList (M.keys vtable ++ M.keys ttable ++
@@ -67,6 +58,14 @@
            map allNamesInType (M.elems ttable))
   where allNamesInType (TypeAbbr _ ps _) = S.fromList $ map typeParamName ps
 
+allNamesInMod :: Mod -> S.Set VName
+allNamesInMod (ModEnv env) = allNamesInEnv env
+allNamesInMod ModFun{} = mempty
+
+allNamesInMTy :: MTy -> S.Set VName
+allNamesInMTy (MTy abs mod) =
+  S.fromList (map qualLeaf $ M.keys abs) <> allNamesInMod mod
+
 newNamesForMTy :: MTy -> TypeM (MTy, M.Map VName VName)
 newNamesForMTy orig_mty = do
   -- Create unique renames for the module type.
@@ -125,7 +124,8 @@
 
         substituteInType :: StructType -> StructType
         substituteInType (Scalar (TypeVar () u (TypeName qs v) targs)) =
-          Scalar $ TypeVar () u (TypeName (map substitute qs) $ substitute v) $ map substituteInTypeArg targs
+          Scalar $ TypeVar () u (TypeName (map substitute qs) $ substitute v) $
+          map substituteInTypeArg targs
         substituteInType (Scalar (Prim t)) =
           Scalar $ Prim t
         substituteInType (Scalar (Record ts)) =
@@ -195,7 +195,6 @@
         match (TypeParamDim _ _, TypeParamDim _ _) = True
         match _ = False
 
-
 findBinding :: (Env -> M.Map VName v)
             -> Namespace -> Name
             -> Env
@@ -222,21 +221,58 @@
   fmap M.fromList $ forM (M.toList sig_abs) $ \(name, name_l) ->
     case findTypeDef (fmap baseName name) mod of
       Just (name', TypeAbbr mod_l ps t)
-        | Unlifted <- name_l,
-          not (orderZero t) || mod_l == Lifted ->
-            mismatchedLiftedness (map qualLeaf $ M.keys mod_abs) name (ps, t)
+        | mod_l > name_l ->
+            mismatchedLiftedness name_l (map qualLeaf $ M.keys mod_abs)
+            (qualLeaf name) (mod_l, ps, t)
         | Just (abs_name, _) <- M.lookup (fmap baseName name) abs_mapping ->
             return (qualLeaf name, (abs_name, TypeAbbr name_l ps t))
         | otherwise ->
             return (qualLeaf name, (name', TypeAbbr name_l ps t))
       _ ->
         missingType loc $ fmap baseName name
-  where mismatchedLiftedness abs name mod_t =
+  where mismatchedLiftedness name_l abs name mod_t =
           Left $ TypeError loc $
           unlines ["Module defines",
-                   indent $ ppTypeAbbr abs name mod_t,
-                   "but module type requires this type to be non-functional."]
+                   sindent $ ppTypeAbbr abs name mod_t,
+                   "but module type requires " ++ what ++ "."]
+          where what = case name_l of Unlifted -> "a non-lifted type"
+                                      SizeLifted -> "a size-lifted type"
+                                      Lifted -> "a lifted type"
 
+resolveMTyNames :: MTy -> MTy
+                -> M.Map VName (QualName VName)
+resolveMTyNames = resolveMTyNames'
+  where resolveMTyNames' (MTy _mod_abs mod) (MTy _sig_abs sig) =
+          resolveModNames mod sig
+
+        resolveModNames (ModEnv mod_env) (ModEnv sig_env) =
+          resolveEnvNames mod_env sig_env
+        resolveModNames (ModFun mod_fun) (ModFun sig_fun) =
+          resolveModNames (funSigMod mod_fun) (funSigMod sig_fun) <>
+          resolveMTyNames' (funSigMty mod_fun) (funSigMty sig_fun)
+        resolveModNames _ _ =
+          mempty
+
+        resolveEnvNames mod_env sig_env =
+          let mod_substs = resolve Term mod_env $ envModTable sig_env
+              onMod (modname, mod_env_mod) =
+                case M.lookup modname mod_substs of
+                  Just (QualName _ modname')
+                    | Just sig_env_mod <-
+                        M.lookup modname' $ envModTable mod_env ->
+                      resolveModNames mod_env_mod sig_env_mod
+                  _ -> mempty
+          in mconcat [ resolve Term mod_env $ envVtable sig_env
+                     , resolve Type mod_env $ envVtable sig_env
+                     , resolve Signature mod_env $ envVtable sig_env
+                     , mod_substs
+                     , mconcat $ map onMod $ M.toList $ envModTable sig_env
+                     ]
+
+        resolve namespace mod_env = M.mapMaybeWithKey resolve'
+          where resolve' name _ =
+                  M.lookup (namespace, baseName name) $ envNameMap mod_env
+
 missingType :: Pretty a => SrcLoc -> a -> Either TypeError b
 missingType loc name =
   Left $ TypeError loc $
@@ -252,32 +288,32 @@
   Left $ TypeError loc $
   "Module does not define a module named " ++ pretty name ++ "."
 
-mismatchedType :: Pretty a =>
-                  SrcLoc
+mismatchedType :: SrcLoc
                -> [VName]
-               -> a
-               -> ([TypeParam], StructType)
-               -> ([TypeParam], StructType)
+               -> VName
+               -> (Liftedness, [TypeParam], StructType)
+               -> (Liftedness, [TypeParam], StructType)
                -> Either TypeError b
 mismatchedType loc abs name spec_t env_t =
   Left $ TypeError loc $
   unlines ["Module defines",
-           indent $ ppTypeAbbr abs name env_t,
+           sindent $ ppTypeAbbr abs name env_t,
            "but module type requires",
-           indent $ ppTypeAbbr abs name spec_t]
-
-indent :: String -> String
-indent = intercalate "\n" . map ("  "++) . lines
+           sindent $ ppTypeAbbr abs name spec_t]
 
-ppTypeAbbr :: Pretty a => [VName] -> a -> ([TypeParam], StructType) -> String
-ppTypeAbbr abs name (ps, t) =
-  "type " ++ unwords (pretty name : map pretty ps) ++ t'
-  where t' = case t of
-               Scalar (TypeVar () _ tn args)
-                 | typeLeaf tn `elem` abs,
-                   map typeParamToArg ps == args -> ""
-               _ -> " = " ++ pretty t
+sindent :: String -> String
+sindent = intercalate "\n" . map ("  "++) . lines
 
+ppTypeAbbr :: [VName] -> VName -> (Liftedness, [TypeParam], StructType) -> String
+ppTypeAbbr abs name (l, ps, Scalar (TypeVar () _ tn args))
+  | typeLeaf tn `elem` abs,
+    map typeParamToArg ps == args =
+      pretty $ text "type" <> ppr l <+> pprName name <+>
+      spread (map ppr ps)
+ppTypeAbbr _ name (l, ps, t) =
+  pretty $ text "type" <> ppr l <+> pprName name <+>
+  spread (map ppr ps) <+> equals <+/>
+  nest 2 (align (ppr t))
 
 -- Return new renamed/abstracted env, as well as a mapping from
 -- names in the signature to names in the new env.  This is used for
@@ -285,13 +321,16 @@
 -- second the env it must match.
 matchMTys :: MTy -> MTy -> SrcLoc
           -> Either TypeError (M.Map VName VName)
-matchMTys = matchMTys' mempty
+matchMTys orig_mty orig_mty_sig =
+  matchMTys' (M.map (DimSub . NamedDim) $
+              resolveMTyNames orig_mty orig_mty_sig)
+  orig_mty orig_mty_sig
   where
     matchMTys' :: TypeSubs -> MTy -> MTy -> SrcLoc
                -> Either TypeError (M.Map VName VName)
 
     matchMTys' _ (MTy _ ModFun{}) (MTy _ ModEnv{}) loc =
-      Left $ TypeError loc "Cannot match parametric module with non-paramatric module type."
+      Left $ TypeError loc "Cannot match parametric module with non-parametric module type."
 
     matchMTys' _ (MTy _ ModEnv{}) (MTy _ ModFun{}) loc =
       Left $ TypeError loc "Cannot match non-parametric module with paramatric module type."
@@ -311,9 +350,9 @@
     matchMods :: TypeSubs -> Mod -> Mod -> SrcLoc
               -> Either TypeError (M.Map VName VName)
     matchMods _ ModEnv{} ModFun{} loc =
-      Left $ TypeError loc "Cannot match non-parametric module with paramatric module type."
+      Left $ TypeError loc "Cannot match non-parametric module with parametric module type."
     matchMods _ ModFun{} ModEnv{} loc =
-      Left $ TypeError loc "Cannot match parametric module with non-paramatric module type."
+      Left $ TypeError loc "Cannot match parametric module with non-parametric module type."
 
     matchMods abs_subst_to_type (ModEnv mod) (ModEnv sig) loc =
       matchEnvs abs_subst_to_type mod sig loc
@@ -340,6 +379,15 @@
       let visible = S.fromList $ map qualLeaf $ M.elems $ envNameMap sig
           isVisible name = name `S.member` visible
 
+      -- Check that all type abbreviations are correctly defined.
+      abbr_name_substs <- fmap M.fromList $
+                          forM (filter (isVisible . fst) $ M.toList $
+                                envTypeTable sig) $ \(name, TypeAbbr spec_l spec_ps spec_t) ->
+        case findBinding envTypeTable Type (baseName name) env of
+          Just (name', TypeAbbr l ps t) ->
+            matchTypeAbbr loc abs_subst_to_type name spec_l spec_ps spec_t name' l ps t
+          Nothing -> missingType loc $ baseName name
+
       -- Check that all values are defined correctly, substituting the
       -- abstract types first.
       val_substs <- fmap M.fromList $ forM (M.toList $ envVtable sig) $ \(name, spec_bv) -> do
@@ -348,15 +396,6 @@
           Just (name', bv) -> matchVal loc name spec_bv' name' bv
           _ -> missingVal loc (baseName name)
 
-      -- Check that all type abbreviations are correctly defined.
-      abbr_name_substs <- fmap M.fromList $
-                          forM (filter (isVisible . fst) $ M.toList $
-                                envTypeTable sig) $ \(name, TypeAbbr _ spec_ps spec_t) ->
-        case findBinding envTypeTable Type (baseName name) env of
-          Just (name', TypeAbbr _ ps t) ->
-            matchTypeAbbr loc abs_subst_to_type val_substs name spec_ps spec_t name' ps t
-          Nothing -> missingType loc $ baseName name
-
       -- Check for correct modules.
       mod_substs <- fmap M.unions $ forM (M.toList $ envModTable sig) $ \(name, modspec) ->
         case findBinding envModTable Term (baseName name) env of
@@ -367,21 +406,20 @@
 
       return $ val_substs <> mod_substs <> abbr_name_substs
 
-    matchTypeAbbr :: SrcLoc -> TypeSubs -> M.Map VName VName
-                  -> VName -> [TypeParam] -> StructType
-                  -> VName -> [TypeParam] -> StructType
+    matchTypeAbbr :: SrcLoc -> TypeSubs
+                  -> VName -> Liftedness -> [TypeParam] -> StructType
+                  -> VName -> Liftedness -> [TypeParam] -> StructType
                   -> Either TypeError (VName, VName)
-    matchTypeAbbr loc abs_subst_to_type val_substs spec_name spec_ps spec_t name ps t = do
+    matchTypeAbbr loc abs_subst_to_type spec_name spec_l spec_ps spec_t name l ps t = do
       -- We have to create substitutions for the type parameters, too.
-      unless (length spec_ps == length ps) nomatch
+      unless (length spec_ps == length ps) $ nomatch spec_t
       param_substs <- mconcat <$> zipWithM matchTypeParam spec_ps ps
-      let val_substs' = M.map (DimSub . NamedDim . qualName) val_substs
-          spec_t' = substituteTypes (val_substs'<>param_substs<>abs_subst_to_type) spec_t
+      let spec_t' = substituteTypes (param_substs<>abs_subst_to_type) spec_t
       if spec_t' == t
         then return (spec_name, name)
-        else nomatch
-        where nomatch = mismatchedType loc (M.keys abs_subst_to_type)
-                        (baseName spec_name) (spec_ps, spec_t) (ps, t)
+        else nomatch spec_t'
+        where nomatch spec_t' = mismatchedType loc (M.keys abs_subst_to_type)
+                                spec_name (spec_l, spec_ps, spec_t') (l, ps, t)
 
               matchTypeParam (TypeParamDim x _) (TypeParamDim y _) =
                 pure $ M.singleton x $ DimSub $ NamedDim $ qualName y
@@ -392,35 +430,37 @@
                 pure $ M.singleton x $ TypeSub $ TypeAbbr Lifted [] $
                 Scalar $ TypeVar () Nonunique (typeName y) []
               matchTypeParam _ _ =
-                nomatch
+                nomatch spec_t
 
     matchVal :: SrcLoc
              -> VName -> BoundV
              -> VName -> BoundV
              -> Either TypeError (VName, VName)
-    matchVal loc spec_name spec_t name t
-      | matchFunBinding loc spec_t t = return (spec_name, name)
-    matchVal loc spec_name spec_v _ v =
-      Left $ TypeError loc $ unlines $
-      ["Module type specifies"] ++
-      map ("  "++) (lines $ ppValBind spec_name spec_v) ++
-      ["but module provides"] ++
-      map ("  "++) (lines $ppValBind spec_name v)
+    matchVal loc spec_name spec_v name v =
+      case matchValBinding loc spec_v v of
+        Nothing -> return (spec_name, name)
+        Just problem ->
+          Left $ TypeError loc $ pretty $
+          text "Module type specifies" </>
+          indent 2 (ppValBind spec_name spec_v) </>
+          text "but module provides" </>
+          indent 2 (ppValBind spec_name v) </>
+          maybe mempty text problem
 
-    matchFunBinding :: SrcLoc -> BoundV -> BoundV -> Bool
-    matchFunBinding loc (BoundV _ orig_spec_t) (BoundV tps orig_t) =
-      -- Would be nice if we could propagate the actual error here.
-      case doUnification loc tps
-           (toStructural orig_spec_t) (toStructural orig_t) of
-        Left _ -> False
-        Right t -> t `subtypeOf` toStructural orig_spec_t
+    matchValBinding :: SrcLoc -> BoundV -> BoundV -> Maybe (Maybe String)
+    matchValBinding loc (BoundV _ orig_spec_t) (BoundV tps orig_t) =
+      case doUnification loc tps (removeShapeAnnotations orig_spec_t) (removeShapeAnnotations orig_t) of
+        Left (TypeError _ err) -> Just $ Just err
+        -- Even if they unify, we still have to verify the uniqueness
+        -- properties.
+        Right t | t `subtypeOf` removeShapeAnnotations orig_spec_t -> Nothing
+                | otherwise -> Just Nothing
 
     ppValBind v (BoundV tps t) =
-      unwords $ ["val", prettyName v] ++ map pretty tps ++ [":", pretty t]
+      text "val" <+> pprName v <+> spread (map ppr tps) <+> colon </>
+      indent 2 (align (ppr t))
 
-applyFunctor :: SrcLoc
-             -> FunSig
-             -> MTy
+applyFunctor :: SrcLoc -> FunSig -> MTy
              -> TypeM (MTy,
                        M.Map VName VName,
                        M.Map VName VName)
diff --git a/src/Language/Futhark/TypeChecker/Terms.hs b/src/Language/Futhark/TypeChecker/Terms.hs
--- a/src/Language/Futhark/TypeChecker/Terms.hs
+++ b/src/Language/Futhark/TypeChecker/Terms.hs
@@ -144,7 +144,6 @@
                 -- closure.
                 | OverloadedF [PrimType] [Maybe PrimType] (Maybe PrimType)
                 | EqualityF
-                | OpaqueF
                 | WasConsumed SrcLoc
                 deriving (Show)
 
@@ -154,6 +153,7 @@
 data TermEnv = TermEnv { termScope :: TermScope
                        , termBreadCrumbs :: [BreadCrumb]
                          -- ^ Most recent first.
+                       , termLevel :: Level
                        }
 
 data TermScope = TermScope { scopeVtable  :: M.Map VName ValBinding
@@ -180,14 +180,9 @@
 withEnv :: TermEnv -> Env -> TermEnv
 withEnv tenv env = tenv { termScope = termScope tenv <> envToTermScope env }
 
-constraintTypeVars :: Constraints -> Names
-constraintTypeVars = mconcat . map f . M.elems
-  where f (Constraint t _) = typeVars t
-        f _ = mempty
-
 overloadedTypeVars :: Constraints -> Names
 overloadedTypeVars = mconcat . map f . M.elems
-  where f (HasFields fs _) = mconcat $ map typeVars $ M.elems fs
+  where f (_, HasFields fs _) = mconcat $ map typeVars $ M.elems fs
         f _ = mempty
 
 -- | Get the type of an expression, with all type variables
@@ -223,9 +218,11 @@
   newTypeVar loc desc = do
     i <- incCounter
     v <- newID $ mkTypeVarName desc i
-    modifyConstraints $ M.insert v $ NoConstraint Lifted $ mkUsage' loc
+    constrain v $ NoConstraint Lifted $ mkUsage' loc
     return $ Scalar $ TypeVar mempty Nonunique (typeName v) []
 
+  curLevel = asks termLevel
+
 instance MonadBreadCrumbs TermTypeM where
   breadCrumb bc = local $ \env ->
     env { termBreadCrumbs = bc : termBreadCrumbs env }
@@ -236,6 +233,7 @@
   initial_scope <- (initialTermScope <>) . envToTermScope <$> askEnv
   let initial_tenv = TermEnv { termScope = initial_scope
                              , termBreadCrumbs = mempty
+                             , termLevel = 0
                              }
   evalRWST m initial_tenv (mempty, 0)
 
@@ -250,6 +248,14 @@
                 put (x, i+1)
                 return i
 
+constrain :: VName -> Constraint -> TermTypeM ()
+constrain v c = do
+  lvl <- curLevel
+  modifyConstraints $ M.insert v (lvl, c)
+
+incLevel :: TermTypeM a -> TermTypeM a
+incLevel = local $ \env -> env { termLevel = termLevel env + 1 }
+
 initialTermScope :: TermScope
 initialTermScope = TermScope { scopeVtable = initialVtable
                              , scopeTypeTable = mempty
@@ -270,14 +276,12 @@
           Just (name, OverloadedF ts pts rts)
         addIntrinsicF (name, IntrinsicPolyFun tvs pts rt) =
           Just (name, BoundV Global tvs $
-                      fromStruct $ vacuousShapeAnnotations $
+                      fromStruct $ anyDimShapeAnnotations $
                       Scalar $ Arrow mempty Unnamed pts' rt)
           where pts' = case pts of [pt] -> pt
                                    _    -> tupleRecord pts
         addIntrinsicF (name, IntrinsicEquality) =
           Just (name, EqualityF)
-        addIntrinsicF (name, IntrinsicOpaque) =
-          Just (name, OpaqueF)
         addIntrinsicF _ = Nothing
 
 instance MonadTypeChecker TermTypeM where
@@ -326,10 +330,6 @@
             let qual = qualifyTypeVars outer_env tnames qs
             qual . anyDimShapeAnnotations <$> normaliseType t'
 
-      Just OpaqueF -> do
-        argtype <- newTypeVar loc "t"
-        return $ Scalar $ Arrow mempty Unnamed argtype argtype
-
       Just EqualityF -> do
         argtype <- newTypeVar loc "t"
         equalityType usage argtype
@@ -423,7 +423,7 @@
 instantiateTypeParam loc tparam = do
   i <- incCounter
   v <- newID $ mkTypeVarName (takeWhile isAlpha (baseString (typeParamName tparam))) i
-  modifyConstraints $ M.insert v $ NoConstraint l $ mkUsage' loc
+  constrain v $ NoConstraint l $ mkUsage' loc
   return (v, Subst $ Scalar $ TypeVar mempty Nonunique (typeName v) [])
   where l = case tparam of TypeParamType x _ _ -> x
                            _                   -> Lifted
@@ -431,7 +431,7 @@
 newArrayType :: SrcLoc -> String -> Int -> TermTypeM (TypeBase () (), TypeBase () ())
 newArrayType loc desc r = do
   v <- newID $ nameFromString desc
-  modifyConstraints $ M.insert v $ NoConstraint Unlifted $ mkUsage' loc
+  constrain v $ NoConstraint Unlifted $ mkUsage' loc
   let rowt = TypeVar () Nonunique (typeName v) []
   return (Array () Nonunique rowt (ShapeDecl $ replicate r ()),
           Scalar rowt)
@@ -687,7 +687,8 @@
 
 bindingTypes :: [(VName, (TypeBinding, Constraint))] -> TermTypeM a -> TermTypeM a
 bindingTypes types m = do
-  modifyConstraints (<>M.map snd (M.fromList types))
+  lvl <- curLevel
+  modifyConstraints (<>M.map ((lvl,) . snd) (M.fromList types))
   localScope extend m
   where extend scope = scope {
           scopeTypeTable = M.map fst (M.fromList types) <> scopeTypeTable scope
@@ -730,7 +731,7 @@
           -- dimensions.
           mapM_ observe $ mapMaybe typeParamIdent tps'
           let ps'' = reverse ps'
-          checkShapeParamUses patternUses tps' ps''
+          checkShapeParamUses tps' $ map patternStructType ps''
 
           m tps' ps''
 
@@ -747,19 +748,6 @@
 
     m p'
 
--- | Return the shapes used in a given pattern in postive and negative
--- position, respectively.
-patternUses :: Pattern -> ([VName], [VName])
-patternUses Id{} = mempty
-patternUses Wildcard{} = mempty
-patternUses PatternLit{} = mempty
-patternUses (PatternParens p _) = patternUses p
-patternUses (TuplePattern ps _) = foldMap patternUses ps
-patternUses (RecordPattern fs _) = foldMap (patternUses . snd) fs
-patternUses (PatternAscription p (TypeDecl declte _) _) =
-  patternUses p <> typeExpUses declte
-patternUses (PatternConstr _ _ ps _) = foldMap patternUses ps
-
 patternDims :: Pattern -> [Ident]
 patternDims (PatternParens p _) = patternDims p
 patternDims (TuplePattern pats _) = concatMap patternDims pats
@@ -800,6 +788,9 @@
 checkExp (Literal val loc) =
   return $ Literal val loc
 
+checkExp (StringLit vs loc) =
+  return $ StringLit vs loc
+
 checkExp (IntLit val NoInfo loc) = do
   t <- newTypeVar loc "t"
   mustBeOneOf anyNumberType (mkUsage loc "integer literal") t
@@ -874,10 +865,10 @@
     ToInclusive e -> ToInclusive <$>
                      (unifies "use in range expression" start_t =<< checkExp e)
 
-  t <- arrayOfM loc start_t (rank 1) Unique
+  t <- arrayOfM loc (vacuousShapeAnnotations start_t) (rank 1) Unique
 
   return $ Range start' maybe_step' end'
-    (Info (vacuousShapeAnnotations t `setAliases` mempty)) loc
+    (Info (t `setAliases` mempty)) loc
 
 checkExp (Ascript e decl NoInfo loc) = do
   decl' <- checkTypeDecl decl
@@ -993,7 +984,8 @@
         let msg = "of value computed with consumption at " ++ locStr (location c)
         in zeroOrderType (mkUsage loc "consumption in right-hand side of 'let'-binding") msg t
       _ -> return ()
-    bindingPattern pat (Ascribed $ anyDimShapeAnnotations t) $ \pat' -> do
+
+    incLevel $ bindingPattern pat (Ascribed $ anyDimShapeAnnotations t) $ \pat' -> do
       body' <- checkExp body
       body_t <- unscopeType (S.map identName $ patternIdents pat') <$> expType body'
       return $ LetPat pat' e' body' (Info body_t) loc
@@ -1071,6 +1063,9 @@
   where isFix DimFix{} = True
         isFix _        = False
 
+-- Record updates are a bit hacky, because we do not have row typing
+-- (yet?).  For now, we only permit record updates where we know the
+-- full type up to the field we are updating.
 checkExp (RecordUpdate src fields ve NoInfo loc) = do
   src' <- checkExp src
   ve' <- checkExp ve
@@ -1079,8 +1074,13 @@
   r <- foldM (flip $ mustHaveField usage) a fields
   ve_t <- expType ve'
   unify usage (toStructural r) (toStructural ve_t)
-  a' <- onRecordField (`setAliases` aliases ve_t) fields <$> expType src'
-  return $ RecordUpdate src' fields ve' (Info a') loc
+  maybe_a' <- onRecordField (const ve_t) fields <$> expType src'
+  case maybe_a' of
+    Just a' -> return $ RecordUpdate src' fields ve' (Info a') loc
+    Nothing -> typeError loc $ pretty $
+               text "Full type of" </>
+               indent 2 (ppr src) </>
+               text " is not known at this point.  Add a size annotation to the original record to disambiguate."
 
 checkExp (Index e idxes NoInfo loc) = do
   (t, _) <- newArrayType (srclocOf e) "e" $ length idxes
@@ -1102,7 +1102,7 @@
   return $ Assert e1' e2' (Info (pretty e1)) loc
 
 checkExp (Lambda params body rettype_te NoInfo loc) =
-  removeSeminullOccurences $
+  removeSeminullOccurences $ incLevel $
   bindingPatternGroup [] params $ \_ params' -> do
     rettype_checked <- traverse checkTypeExp rettype_te
     let declared_rettype =
@@ -1715,7 +1715,7 @@
 checkOneExp e = fmap fst . runTermTypeM $ do
   e' <- checkExp e
   let t = toStruct $ typeOf e'
-  tparams <- letGeneralise [] t mempty
+  tparams <- letGeneralise [] t
   fixOverloadedTypes
   e'' <- updateExpTypes e'
   return (tparams, e'')
@@ -1756,7 +1756,7 @@
 -- | This is "fixing" as in "setting them", not "correcting them".  We
 -- only make very conservative fixing.
 fixOverloadedTypes :: TermTypeM ()
-fixOverloadedTypes = getConstraints >>= mapM_ fixOverloaded . M.toList
+fixOverloadedTypes = getConstraints >>= mapM_ fixOverloaded . M.toList . M.map snd
   where fixOverloaded (v, Overloaded ots usage)
           | Signed Int32 `elem` ots = do
               unify usage (Scalar (TypeVar () Nonunique (typeName v) [])) $
@@ -1796,10 +1796,8 @@
                  [UncheckedTypeParam], [UncheckedPattern],
                  UncheckedExp, SrcLoc)
              -> TermTypeM ([TypeParam], [Pattern], Maybe (TypeExp VName), StructType, Exp)
-checkBinding (fname, maybe_retdecl, tparams, params, body, loc) = noUnique $ do
-  then_substs <- getConstraints
-
-  bindingPatternGroup tparams params $ \tparams' params' -> do
+checkBinding (fname, maybe_retdecl, tparams, params, body, loc) =
+  noUnique $ incLevel $ bindingPatternGroup tparams params $ \tparams' params' -> do
     maybe_retdecl' <- traverse checkTypeExp maybe_retdecl
 
     body' <- checkFunBody body ((\(_,t,_)->t) <$> maybe_retdecl') (maybe loc srclocOf maybe_retdecl)
@@ -1824,7 +1822,7 @@
             return (Nothing, inferReturnUniqueness params'' body_t)
 
     let fun_t = foldFunType (map patternStructType params'') rettype
-    tparams'' <- letGeneralise tparams' fun_t then_substs
+    tparams'' <- letGeneralise tparams' fun_t
 
     checkGlobalAliases params'' body_t loc
 
@@ -1950,11 +1948,8 @@
         check _ = return ()
         bad = typeError loc "A top-level constant cannot have a unique type."
 
-letGeneralise :: [TypeParam]
-              -> StructType
-              -> Constraints
-              -> TermTypeM [TypeParam]
-letGeneralise tparams t then_substs = do
+letGeneralise :: [TypeParam] -> StructType -> TermTypeM [TypeParam]
+letGeneralise tparams t = do
   now_substs <- getConstraints
   -- Candidates for let-generalisation are those type variables that
   --
@@ -1967,14 +1962,14 @@
   -- are the element types of an incompletely resolved record type).
   -- This is a bit more restrictive than I'd like, and SML for
   -- example does not have this restriction.
-  let then_type_variables = S.fromList $ M.keys then_substs
-      then_type_constraints = constraintTypeVars $
-                              M.filterWithKey (\k _ -> k `S.member` then_type_variables) now_substs
-      keep_type_variables = then_type_variables <>
-                            then_type_constraints <>
-                            overloadedTypeVars now_substs
+  --
+  -- Criteria (1) and (2) is implemented by looking at the binding
+  -- level of the type variables.
+  let keep_type_vars = overloadedTypeVars now_substs
 
-  let new_substs = M.filterWithKey (\k _ -> not (k `S.member` keep_type_variables)) now_substs
+  cur_lvl <- curLevel
+  let candiate k (lvl, _) = (k `S.notMember` keep_type_vars) && lvl >= cur_lvl
+      new_substs = M.filterWithKey candiate now_substs
   tparams' <- closeOverTypes new_substs tparams t
 
   -- We keep those type variables that were not closed over by
@@ -2015,7 +2010,7 @@
 -- produced list of type parameters.
 closeOverTypes :: Constraints -> [TypeParam] -> StructType -> TermTypeM [TypeParam]
 closeOverTypes substs tparams t =
-  fmap ((tparams++) . catMaybes) $ mapM closeOver $ M.toList to_close_over
+  fmap ((tparams++) . catMaybes) $ mapM closeOver $ M.toList $ M.map snd to_close_over
   where to_close_over = M.filterWithKey (\k _ -> k `S.member` visible) substs
         visible = typeVars t
 
@@ -2101,7 +2096,6 @@
   where set (BoundV l tparams t)    = BoundV l tparams $ t `setUniqueness` Nonunique
         set (OverloadedF ts pts rt) = OverloadedF ts pts rt
         set EqualityF               = EqualityF
-        set OpaqueF                 = OpaqueF
         set (WasConsumed loc)       = WasConsumed loc
 
 onlySelfAliasing :: TermTypeM a -> TermTypeM a
@@ -2110,7 +2104,6 @@
                                         t `addAliases` S.intersection (S.singleton (AliasBound k))
         set _ (OverloadedF ts pts rt) = OverloadedF ts pts rt
         set _ EqualityF               = EqualityF
-        set _ OpaqueF                 = OpaqueF
         set _ (WasConsumed loc)       = WasConsumed loc
 
 arrayOfM :: (Pretty (ShapeDecl dim), Monoid as) =>
diff --git a/src/Language/Futhark/TypeChecker/Types.hs b/src/Language/Futhark/TypeChecker/Types.hs
--- a/src/Language/Futhark/TypeChecker/Types.hs
+++ b/src/Language/Futhark/TypeChecker/Types.hs
@@ -8,7 +8,6 @@
   , subuniqueOf
 
   , checkForDuplicateNames
-  , checkForDuplicateNamesInType
   , checkTypeParams
   , typeParamToArg
 
@@ -105,13 +104,10 @@
 checkTypeDecl tps (TypeDecl t NoInfo) = do
   checkForDuplicateNamesInType t
   (t', st, l) <- checkTypeExp t
-  checkShapeParamUses typeExpUses tps $ unfoldTypeExp t'
+  let (pts, ret) = unfoldFunType st
+  checkShapeParamUses tps $ pts ++ [ret]
   return (TypeDecl t' $ Info st, l)
 
-unfoldTypeExp :: TypeExp VName -> [TypeExp VName]
-unfoldTypeExp (TEArrow _ t1 t2 _) = t1 : unfoldTypeExp t2
-unfoldTypeExp t = [t]
-
 checkTypeExp :: MonadTypeChecker m =>
                 TypeExp Name
              -> m (TypeExp VName, StructType, Liftedness)
@@ -120,7 +116,8 @@
   case ps of
     [] -> return (TEVar name' loc, t, l)
     _  -> throwError $ TypeError loc $
-          "Type constructor " ++ quote (pretty name) ++ " used without any arguments."
+          "Type constructor " ++ quote (unwords (pretty name : map pretty ps)) ++
+          " used without any arguments."
 checkTypeExp (TETuple ts loc) = do
   (ts', ts_s, ls) <- unzip3 <$> mapM checkTypeExp ts
   return (TETuple ts' loc, tupleRecord ts_s, foldl' max Unlifted ls)
@@ -142,8 +139,12 @@
   (d', d'') <- checkDimExp d
   case (l, arrayOf st (ShapeDecl [d'']) Nonunique) of
     (Unlifted, st') -> return (TEArray t' d' loc, st', Unlifted)
-    _ -> throwError $ TypeError loc $
-         "Cannot create array with elements of type " ++ quote (pretty st) ++ " (might be functional)."
+    (SizeLifted, _) ->
+      throwError $ TypeError loc $
+      "Cannot create array with elements of size-lifted type " ++ quote (pretty t) ++ " (might cause irregular array)."
+    (Lifted, _) ->
+      throwError $ TypeError loc $
+      "Cannot create array with elements of lifted type " ++ quote (pretty t) ++ " (might contain function)."
   where checkDimExp DimExpAny =
           return (DimExpAny, AnyDim)
         checkDimExp (DimExpConst k dloc) =
@@ -264,43 +265,58 @@
 -- it (normal name shadowing).
 checkForDuplicateNamesInType :: MonadTypeChecker m =>
                                 TypeExp Name -> m ()
-checkForDuplicateNamesInType = checkForDuplicateNames . pats
-  where pats (TEArrow (Just v) t1 t2 loc) = Id v NoInfo loc : pats t1 ++ pats t2
-        pats (TEArrow Nothing t1 t2 _) = pats t1 ++ pats t2
-        pats (TETuple ts _) = concatMap pats ts
-        pats (TERecord fs _) = concatMap (pats . snd) fs
-        pats (TEArray t _ _) = pats t
-        pats (TEUnique t _) = pats t
-        pats (TEApply t1 (TypeArgExpType t2) _) = pats t1 ++ pats t2
-        pats (TEApply t1 TypeArgExpDim{} _) = pats t1
-        pats TEVar{} = []
-        pats (TESum cs _) = concatMap (concatMap pats . snd) cs
+checkForDuplicateNamesInType = check mempty
+  where check seen (TEArrow (Just v) t1 t2 loc)
+          | Just prev_loc <- M.lookup v seen =
+              throwError $ TypeError loc $
+              "Name " ++ quote (pretty v) ++ " also bound at " ++ locStr prev_loc
+          | otherwise =
+              check seen' t1 >> check seen' t2
+              where seen' = M.insert v loc seen
+        check seen (TEArrow Nothing t1 t2 _) =
+          check seen t1 >> check seen t2
+        check seen (TETuple ts _) = mapM_ (check seen) ts
+        check seen (TERecord fs _) = mapM_ (check seen . snd) fs
+        check seen (TEUnique t _) = check seen t
+        check seen (TESum cs _) = mapM_ (mapM (check seen) . snd) cs
+        check seen (TEApply t1 (TypeArgExpType t2) _) =
+          check seen t1 >> check seen t2
+        check seen (TEApply t1 TypeArgExpDim{} _) =
+          check seen t1
+        check _ TEArray{} = return ()
+        check _ TEVar{} = return ()
 
 -- | Ensure that every shape parameter is used in positive position at
 -- least once before being used in negative position.
-checkShapeParamUses :: (MonadTypeChecker m, Located a) =>
-                       (a -> ([VName], [VName])) -> [TypeParam] -> [a]
-                    -> m ()
-checkShapeParamUses getUses tps ps = do
-  pos_uses <- foldM checkShapePositions [] ps
-  mapM_ (checkUsed pos_uses) tps
-  where tp_names = map typeParamName tps
+checkShapeParamUses :: MonadTypeChecker m =>
+                       [TypeParam] -> [StructType] -> m ()
+checkShapeParamUses tps ts = do
+  uses <- foldM onType mempty ts
+  mapM_ (checkIfUsed uses) tps
+  where onDim pos (NamedDim d) =
+          modify $ M.insertWith min (qualLeaf d) pos
+        onDim _ _ = return ()
 
-        checkShapePositions pos_uses p = do
-          let (pos, neg) = getUses p
-              pos_uses' = pos <> pos_uses
-          forM_ neg $ \pv ->
-            unless ((pv `notElem` tp_names) || (pv `elem` pos_uses')) $
-            throwError $ TypeError (srclocOf p) $ "Shape parameter " ++
-            quote (prettyName pv) ++ " must first be given in " ++
-            "a positive position (non-functional parameter)."
-          return pos_uses'
-        checkUsed uses (TypeParamDim pv loc)
-          | pv `elem` uses = return ()
+        onType uses t = do
+          let uses' = execState (traverseDims onDim t) uses
+          mapM_ (checkUsage uses') tps
+          return uses'
+
+        checkUsage uses (TypeParamDim pv loc)
+          | Just pos <- M.lookup pv uses,
+            pos `elem` [PosParam, PosReturn] =
+              throwError $ TypeError loc $
+                "Shape parameter " ++ quote (prettyName pv) ++
+                " must first be used in" ++
+                " a positive position (non-functional parameter)."
+        checkUsage _ _ = return ()
+
+        checkIfUsed uses (TypeParamDim pv loc)
+          | M.member pv uses = return ()
           | otherwise =
               throwError $ TypeError loc $ "Size parameter " ++
               quote (prettyName pv) ++ " unused."
-        checkUsed _ _ = return ()
+        checkIfUsed _ _ = return ()
 
 checkTypeParams :: MonadTypeChecker m =>
                    [TypeParamBase Name]
diff --git a/src/Language/Futhark/TypeChecker/Unify.hs b/src/Language/Futhark/TypeChecker/Unify.hs
--- a/src/Language/Futhark/TypeChecker/Unify.hs
+++ b/src/Language/Futhark/TypeChecker/Unify.hs
@@ -5,6 +5,7 @@
   , Usage
   , mkUsage
   , mkUsage'
+  , Level
   , Constraints
   , lookupSubst
   , MonadUnify(..)
@@ -37,12 +38,6 @@
 import Language.Futhark.TypeChecker.Types
 import Futhark.Util.Pretty (Pretty)
 
--- | Mapping from fresh type variables, instantiated from the type
--- schemes of polymorphic functions, to (possibly) specific types as
--- determined on application and the location of that application, or
--- a partial constraint on their type.
-type Constraints = M.Map VName Constraint
-
 -- | A usage that caused a type constraint.
 data Usage = Usage (Maybe String) SrcLoc
 
@@ -59,6 +54,11 @@
 instance Located Usage where
   locOf (Usage _ loc) = locOf loc
 
+-- | The level at which a type variable is bound.  Higher means
+-- deeper.  We can only unify a type variable at level 'i' with a type
+-- 't' if all type names that occur in 't' are at most at level 'i'.
+type Level = Int
+
 data Constraint = NoConstraint Liftedness Usage
                 | ParamType Liftedness SrcLoc
                 | Constraint (TypeBase () ()) Usage
@@ -77,10 +77,16 @@
   locOf (Equality usage) = locOf usage
   locOf (HasConstrs _ usage) = locOf usage
 
+-- | Mapping from fresh type variables, instantiated from the type
+-- schemes of polymorphic functions, to (possibly) specific types as
+-- determined on application and the location of that application, or
+-- a partial constraint on their type.
+type Constraints = M.Map VName (Level, Constraint)
+
 lookupSubst :: VName -> Constraints -> Maybe (Subst (TypeBase () ()))
 lookupSubst v constraints = case M.lookup v constraints of
-                              Just (Constraint t _) -> Just $ Subst t
-                              Just Overloaded{} -> Just PrimSubst
+                              Just (_, Constraint t _) -> Just $ Subst t
+                              Just (_, Overloaded{}) -> Just PrimSubst
                               _ -> Nothing
 
 class (MonadBreadCrumbs m, MonadError TypeError m) => MonadUnify m where
@@ -93,18 +99,29 @@
 
   newTypeVar :: Monoid als => SrcLoc -> String -> m (TypeBase dim als)
 
+  curLevel :: m Level
+
 normaliseType :: (Substitutable a, MonadUnify m) => a -> m a
 normaliseType t = do constraints <- getConstraints
                      return $ applySubst (`lookupSubst` constraints) t
 
+rigidConstraint :: Constraint -> Bool
+rigidConstraint ParamType{} = True
+rigidConstraint _ = False
+
 -- | Is the given type variable the name of an abstract type or type
 -- parameter, which we cannot substitute?
 isRigid :: VName -> Constraints -> Bool
-isRigid v constraints = case M.lookup v constraints of
-                          Nothing -> True
-                          Just ParamType{} -> True
-                          _ -> False
+isRigid v constraints =
+  maybe True (rigidConstraint . snd) $ M.lookup v constraints
 
+-- | If the given type variable is nonrigid, what is its level?
+isNonRigid :: VName -> Constraints -> Maybe Level
+isNonRigid v constraints = do
+  (lvl, c) <- M.lookup v constraints
+  guard $ not $ rigidConstraint c
+  return lvl
+
 unifySharedConstructors :: MonadUnify m =>
                            Usage
                         -> M.Map Name [TypeBase () ()]
@@ -132,7 +149,7 @@
     subunify t1 t2 = do
       constraints <- getConstraints
 
-      let isRigid' v = isRigid v constraints
+      let nonrigid v = isNonRigid v constraints
           t1' = applySubst (`lookupSubst` constraints) t1
           t2' = applySubst (`lookupSubst` constraints) t2
 
@@ -161,18 +178,20 @@
 
         (Scalar (TypeVar _ _ (TypeName [] v1) []),
          Scalar (TypeVar _ _ (TypeName [] v2) [])) ->
-          case (isRigid' v1, isRigid' v2) of
-            (True, True) -> failure
-            (True, False) -> linkVarToType usage v2 t1'
-            (False, True) -> linkVarToType usage v1 t2'
-            (False, False) -> linkVarToType usage v1 t2'
+          case (nonrigid v1, nonrigid v2) of
+            (Nothing, Nothing) -> failure
+            (Just lvl1, Nothing) -> linkVarToType usage v1 lvl1 t2'
+            (Nothing, Just lvl2) -> linkVarToType usage v2 lvl2 t1'
+            (Just lvl1, Just lvl2)
+              | lvl1 <= lvl2 -> linkVarToType usage v1 lvl1 t2'
+              | otherwise    -> linkVarToType usage v2 lvl2 t1'
 
         (Scalar (TypeVar _ _ (TypeName [] v1) []), _)
-          | not $ isRigid' v1 ->
-              linkVarToType usage v1 t2'
+          | Just lvl <-  nonrigid v1 ->
+              linkVarToType usage v1 lvl t2'
         (_, Scalar (TypeVar _ _ (TypeName [] v2) []))
-          | not $ isRigid' v2 ->
-              linkVarToType usage v2 t1'
+          | Just lvl <- nonrigid v2 ->
+              linkVarToType usage v2 lvl t1'
 
         (Scalar (Arrow _ _ a1 b1),
          Scalar (Arrow _ _ a2 b2)) -> do
@@ -208,75 +227,99 @@
 applySubstInConstraint vn subst (HasConstrs cs loc) =
   HasConstrs (M.map (map (applySubst (flip M.lookup $ M.singleton vn subst))) cs) loc
 
-linkVarToType :: MonadUnify m => Usage -> VName -> TypeBase () () -> m ()
-linkVarToType usage vn tp = do
+occursCheck :: MonadUnify m => Usage -> VName -> TypeBase () () -> m ()
+occursCheck usage vn tp =
+  when (vn `S.member` typeVars tp) $
+  typeError usage $ "Occurs check: cannot instantiate " ++
+  prettyName vn ++ " with " ++ pretty tp
+
+scopeCheck :: MonadUnify m => Usage -> VName -> Level -> TypeBase () () -> m ()
+scopeCheck usage vn max_lvl tp = do
   constraints <- getConstraints
-  if vn `S.member` typeVars tp
-    then typeError usage $ "Occurs check: cannot instantiate " ++
-         prettyName vn ++ " with " ++ pretty tp'
-    else do modifyConstraints $ M.insert vn $ Constraint tp' usage
-            modifyConstraints $ M.map $ applySubstInConstraint vn $ Subst tp'
-            case M.lookup vn constraints of
+  mapM_ (check constraints) $ typeVars tp
+  where check constraints v
+          | Just (lvl, c) <- M.lookup v constraints,
+            lvl > max_lvl =
+              if rigidConstraint c
+              then scopeViolation v
+              else modifyConstraints $ M.insert v (max_lvl, c)
+          | otherwise =
+              return ()
 
-              Just (NoConstraint Unlifted unlift_usage) ->
-                zeroOrderType usage (show unlift_usage) tp'
+        scopeViolation v =
+          typeError usage $ "Cannot unify type variable " ++ quote (prettyName v) ++
+          " with " ++ quote (prettyName vn) ++ " (scope violation).\n" ++
+          "This is because " ++ quote (prettyName vn) ++ " is rigidly bound in a deeper scope."
 
-              Just (Equality _) ->
-                equalityType usage tp'
+linkVarToType :: MonadUnify m => Usage -> VName -> Level -> TypeBase () () -> m ()
+linkVarToType usage vn lvl tp = do
+  occursCheck usage vn tp
+  scopeCheck usage vn lvl tp
 
-              Just (Overloaded ts old_usage)
-                | tp `notElem` map (Scalar . Prim) ts ->
-                    case tp' of
-                      Scalar (TypeVar _ _ (TypeName [] v) [])
-                        | not $ isRigid v constraints ->
-                            linkVarToTypes usage v ts
-                      _ ->
-                        typeError usage $ "Cannot unify " ++ quote (prettyName vn) ++
-                        "' with type\n" ++ indent (pretty tp) ++ "\nas " ++
-                        quote (prettyName vn) ++ " must be one of " ++
-                        intercalate ", " (map pretty ts) ++
-                        " due to " ++ show old_usage ++ ")."
+  constraints <- getConstraints
+  modifyConstraints $ M.insert vn (lvl, Constraint tp' usage)
+  modifyConstraints $ M.map $ fmap $ applySubstInConstraint vn $ Subst tp'
 
-              Just (HasFields required_fields old_usage) ->
-                case tp of
-                  Scalar (Record tp_fields)
-                    | all (`M.member` tp_fields) $ M.keys required_fields ->
-                        mapM_ (uncurry $ unify usage) $ M.elems $
-                        M.intersectionWith (,) required_fields tp_fields
-                  Scalar (TypeVar _ _ (TypeName [] v) [])
-                    | not $ isRigid v constraints ->
-                        modifyConstraints $ M.insert v $
-                        HasFields required_fields old_usage
-                  _ ->
-                    typeError usage $
-                    "Cannot unify " ++ quote (prettyName vn) ++ " with type\n" ++
-                    indent (pretty tp) ++ "\nas " ++ quote (prettyName vn) ++
-                    " must be a record with fields\n" ++
-                    pretty (Record required_fields) ++
-                    "\ndue to " ++ show old_usage ++ "."
+  case snd <$> M.lookup vn constraints of
 
-              Just (HasConstrs required_cs old_usage) ->
-                case tp of
-                  Scalar (Sum ts)
-                    | all (`M.member` ts) $ M.keys required_cs ->
-                        unifySharedConstructors usage required_cs ts
-                  Scalar (TypeVar _ _ (TypeName [] v) [])
-                    | not $ isRigid v constraints -> do
-                        case M.lookup v constraints of
-                          Just (HasConstrs v_cs _) ->
-                            unifySharedConstructors usage required_cs v_cs
-                          _ -> return ()
-                        modifyConstraints $ M.insertWith combineConstrs v $
-                          HasConstrs required_cs old_usage
-                        where combineConstrs (HasConstrs cs1 usage1) (HasConstrs cs2 _) =
-                                HasConstrs (M.union cs1 cs2) usage1
-                              combineConstrs hasCs _ = hasCs
-                  _ -> noSumType
+    Just (NoConstraint Unlifted unlift_usage) ->
+      zeroOrderType usage (show unlift_usage) tp'
 
-              _ -> return ()
+    Just (Equality _) ->
+      equalityType usage tp'
 
+    Just (Overloaded ts old_usage)
+      | tp `notElem` map (Scalar . Prim) ts ->
+          case tp' of
+            Scalar (TypeVar _ _ (TypeName [] v) [])
+              | not $ isRigid v constraints ->
+                  linkVarToTypes usage v ts
+            _ ->
+              typeError usage $ "Cannot unify " ++ quote (prettyName vn) ++
+              "' with type\n" ++ indent (pretty tp) ++ "\nas " ++
+              quote (prettyName vn) ++ " must be one of " ++
+              intercalate ", " (map pretty ts) ++
+              " due to " ++ show old_usage ++ ")."
+
+    Just (HasFields required_fields old_usage) ->
+      case tp of
+        Scalar (Record tp_fields)
+          | all (`M.member` tp_fields) $ M.keys required_fields ->
+              mapM_ (uncurry $ unify usage) $ M.elems $
+              M.intersectionWith (,) required_fields tp_fields
+        Scalar (TypeVar _ _ (TypeName [] v) [])
+          | not $ isRigid v constraints ->
+              modifyConstraints $ M.insert v
+              (lvl, HasFields required_fields old_usage)
+        _ ->
+          typeError usage $
+          "Cannot unify " ++ quote (prettyName vn) ++ " with type\n" ++
+          indent (pretty tp) ++ "\nas " ++ quote (prettyName vn) ++
+          " must be a record with fields\n" ++
+          pretty (Record required_fields) ++
+          "\ndue to " ++ show old_usage ++ "."
+
+    Just (HasConstrs required_cs old_usage) ->
+      case tp of
+        Scalar (Sum ts)
+          | all (`M.member` ts) $ M.keys required_cs ->
+              unifySharedConstructors usage required_cs ts
+        Scalar (TypeVar _ _ (TypeName [] v) [])
+          | not $ isRigid v constraints -> do
+              case M.lookup v constraints of
+                Just (_, HasConstrs v_cs _) ->
+                  unifySharedConstructors usage required_cs v_cs
+                _ -> return ()
+              modifyConstraints $ M.insertWith combineConstrs v
+                (lvl, HasConstrs required_cs old_usage)
+              where combineConstrs (_, HasConstrs cs1 usage1) (_, HasConstrs cs2 _) =
+                      (lvl, HasConstrs (M.union cs1 cs2) usage1)
+                    combineConstrs hasCs _ = hasCs
+        _ -> typeError usage "Cannot unify a sum type with a non-sum type"
+
+    _ -> return ()
+
   where tp' = removeUniqueness tp
-        noSumType = typeError usage "Cannot unify a sum type with a non-sum type"
 
 removeUniqueness :: TypeBase dim as -> TypeBase dim as
 removeUniqueness (Scalar (Record ets)) =
@@ -309,25 +352,27 @@
 linkVarToTypes usage vn ts = do
   vn_constraint <- M.lookup vn <$> getConstraints
   case vn_constraint of
-    Just (Overloaded vn_ts vn_usage) ->
+    Just (lvl, Overloaded vn_ts vn_usage) ->
       case ts `intersect` vn_ts of
         [] -> typeError usage $ "Type constrained to one of " ++
               intercalate "," (map pretty ts) ++ " but also one of " ++
               intercalate "," (map pretty vn_ts) ++ " due to " ++ show vn_usage ++ "."
-        ts' -> modifyConstraints $ M.insert vn $ Overloaded ts' usage
+        ts' -> modifyConstraints $ M.insert vn (lvl, Overloaded ts' usage)
 
-    Just (HasConstrs _ vn_usage) ->
+    Just (_, HasConstrs _ vn_usage) ->
       typeError usage $ "Type constrained to one of " ++
       intercalate "," (map pretty ts) ++ ", but also inferred to be sum type due to " ++
       show vn_usage ++ "."
 
-    Just (HasFields _ vn_usage) ->
+    Just (_, HasFields _ vn_usage) ->
       typeError usage $ "Type constrained to one of " ++
       intercalate "," (map pretty ts) ++ ", but also inferred to be record due to " ++
       show vn_usage ++ "."
 
-    _ -> modifyConstraints $ M.insert vn $ Overloaded ts usage
+    Just (lvl, _) -> modifyConstraints $ M.insert vn (lvl, Overloaded ts usage)
 
+    Nothing -> typeError usage $ "Cannot constrain type to one of " ++ intercalate "," (map pretty ts)
+
 equalityType :: (MonadUnify m, Pretty (ShapeDecl dim), Monoid as) =>
                 Usage -> TypeBase dim as -> m ()
 equalityType usage t = do
@@ -338,21 +383,21 @@
   where mustBeEquality vn = do
           constraints <- getConstraints
           case M.lookup vn constraints of
-            Just (Constraint (Scalar (TypeVar _ _ (TypeName [] vn') [])) _) ->
+            Just (_, Constraint (Scalar (TypeVar _ _ (TypeName [] vn') [])) _) ->
               mustBeEquality vn'
-            Just (Constraint vn_t cusage)
+            Just (_, Constraint vn_t cusage)
               | not $ orderZero vn_t ->
                   typeError usage $
                   unlines ["Type \"" ++ pretty t ++ "\" does not support equality.",
                            "Constrained to be higher-order due to " ++ show cusage ++ "."]
               | otherwise -> return ()
-            Just (NoConstraint _ _) ->
-              modifyConstraints $ M.insert vn (Equality usage)
-            Just (Overloaded _ _) ->
+            Just (lvl, NoConstraint _ _) ->
+              modifyConstraints $ M.insert vn (lvl, Equality usage)
+            Just (_, Overloaded _ _) ->
               return () -- All primtypes support equality.
-            Just Equality{} ->
+            Just (_, Equality{}) ->
               return ()
-            Just (HasConstrs cs _) ->
+            Just (_, HasConstrs cs _) ->
               mapM_ (equalityType usage) $ concat $ M.elems cs
             _ ->
               typeError usage $ "Type " ++ pretty (prettyName vn) ++
@@ -368,14 +413,14 @@
   where mustBeZeroOrder vn = do
           constraints <- getConstraints
           case M.lookup vn constraints of
-            Just (Constraint vn_t old_usage)
+            Just (_, Constraint vn_t old_usage)
               | not $ orderZero t ->
                 typeError usage $ "Type " ++ desc ++
                 " must be non-function, but inferred to be " ++
                 quote (pretty vn_t) ++ " due to " ++ show old_usage ++ "."
-            Just (NoConstraint _ _) ->
-              modifyConstraints $ M.insert vn (NoConstraint Unlifted usage)
-            Just (ParamType Lifted ploc) ->
+            Just (lvl, NoConstraint _ _) ->
+              modifyConstraints $ M.insert vn (lvl, NoConstraint Unlifted usage)
+            Just (_, ParamType Lifted ploc) ->
               typeError usage $ "Type " ++ desc ++
               " must be non-function, but type parameter " ++ quote (prettyName vn) ++ " at " ++
               locStr ploc ++ " may be a function."
@@ -390,15 +435,16 @@
   constraints <- getConstraints
   case t of
     Scalar (TypeVar _ _ (TypeName _ tn) [])
-      | Just NoConstraint{} <- M.lookup tn constraints ->
-          modifyConstraints $ M.insert tn $ HasConstrs (M.singleton c struct_f) usage
-      | Just (HasConstrs cs _) <- M.lookup tn constraints ->
-        case M.lookup c cs of
-          Nothing  -> modifyConstraints $ M.insert tn $ HasConstrs (M.insert c fs cs) usage
-          Just fs'
-            | length fs == length fs' -> zipWithM_ (unify usage) fs fs'
-            | otherwise -> typeError usage $ "Different arity for constructor "
-                           ++ quote (pretty c) ++ "."
+      | Just (lvl, NoConstraint{}) <- M.lookup tn constraints -> do
+          mapM_ (scopeCheck usage tn lvl) struct_f
+          modifyConstraints $ M.insert tn (lvl, HasConstrs (M.singleton c struct_f) usage)
+      | Just (lvl, HasConstrs cs _) <- M.lookup tn constraints ->
+          case M.lookup c cs of
+            Nothing  -> modifyConstraints $ M.insert tn (lvl, HasConstrs (M.insert c fs cs) usage)
+            Just fs'
+              | length fs == length fs' -> zipWithM_ (unify usage) fs fs'
+              | otherwise -> typeError usage $ "Different arity for constructor "
+                             ++ quote (pretty c) ++ "."
 
     Scalar (Sum cs) ->
       case M.lookup c cs of
@@ -419,14 +465,15 @@
   let l_type' = toStructural l_type
   case t of
     Scalar (TypeVar _ _ (TypeName _ tn) [])
-      | Just NoConstraint{} <- M.lookup tn constraints -> do
-          modifyConstraints $ M.insert tn $ HasFields (M.singleton l l_type') usage
+      | Just (lvl, NoConstraint{}) <- M.lookup tn constraints -> do
+          scopeCheck usage tn lvl l_type'
+          modifyConstraints $ M.insert tn (lvl, HasFields (M.singleton l l_type') usage)
           return l_type
-      | Just (HasFields fields _) <- M.lookup tn constraints -> do
+      | Just (lvl, HasFields fields _) <- M.lookup tn constraints -> do
           case M.lookup l fields of
             Just t' -> unify usage l_type' t'
-            Nothing -> modifyConstraints $ M.insert tn $
-                       HasFields (M.insert l l_type' fields) usage
+            Nothing -> modifyConstraints $ M.insert tn
+                       (lvl, HasFields (M.insert l l_type' fields) usage)
           return l_type
     Scalar (Record fields)
       | Just t' <- M.lookup l fields -> do
@@ -450,16 +497,18 @@
 
 instance MonadUnify UnifyM where
   getConstraints = gets fst
-  putConstraints x = modify $ \s -> (x, snd s)
+  putConstraints x = modify $ \(_, i) -> (x, i)
 
   newTypeVar loc desc = do
     i <- do (x, i) <- get
             put (x, i+1)
             return i
     let v = VName (mkTypeVarName desc i) 0
-    modifyConstraints $ M.insert v $ NoConstraint Lifted $ Usage Nothing loc
+    modifyConstraints $ M.insert v (0, NoConstraint Lifted $ Usage Nothing loc)
     return $ Scalar $ TypeVar mempty Nonunique (typeName v) []
 
+  curLevel = pure 0
+
 -- | Construct a the name of a new type variable given a base
 -- description and a tag number (note that this is distinct from
 -- actually constructing a VName; the tag here is intended for human
@@ -485,4 +534,4 @@
 runUnifyM tparams (UnifyM m) = runExcept $ evalStateT m (constraints, 0)
   where constraints = M.fromList $ mapMaybe f tparams
         f TypeParamDim{} = Nothing
-        f (TypeParamType l p loc) = Just (p, NoConstraint l $ Usage Nothing loc)
+        f (TypeParamType l p loc) = Just (p, (0, NoConstraint l $ Usage Nothing loc))