diff --git a/docs/installation.rst b/docs/installation.rst
--- a/docs/installation.rst
+++ b/docs/installation.rst
@@ -98,9 +98,6 @@
 
   You will still likely need to make a C compiler (such as GCC) available on your own.
 
-.. _`Haskell tool stack`: http://docs.haskellstack.org/
-.. _`installing Stack`: http://docs.haskellstack.org/#how-to-install
-
 .. _linux-installation:
 
 Installing Futhark on Linux
diff --git a/docs/language-reference.rst b/docs/language-reference.rst
--- a/docs/language-reference.rst
+++ b/docs/language-reference.rst
@@ -368,8 +368,7 @@
 
 The definition can be an arbitrary expression, including function
 calls and other values, although they must be in scope before the
-value is defined.  A constant value may not have a unique type (see
-`In-place updates`_).  If the return type contains any anonymous sizes
+value is defined.  If the return type contains any anonymous sizes
 (see `Size types`_), new existential sizes will be constructed for
 them.
 
@@ -1054,8 +1053,8 @@
 instantiated with a functional type.  Within a function, a lifted type
 parameter is treated as a functional type.
 
-See also `In-place updates`_ for details on how uniqueness types
-interact with higher-order functions.
+See also `In-place updates`_ for details on how consumption
+interacts with higher-order functions.
 
 Type Inference
 --------------
@@ -1065,7 +1064,7 @@
 cannot in isolation be fully inferred, and may need type annotations
 where their inputs are bound.  The same goes when constructing sum
 types, as Futhark cannot assume that a given constructor only belongs
-to a single type.  Further, unique types (see `In-place updates`_)
+to a single type.  Further, consumed parameters (see `In-place updates`_)
 must be explicitly annotated.
 
 Type inference processes top-level declared in top-down order, and the
@@ -1414,8 +1413,9 @@
 Generally, most language constructs produce new arrays, but some
 (slicing) create arrays that alias their input arrays.
 
-When defining a function parameter or return type, we can mark it as
-*unique* by prefixing it with an asterisk.  For example::
+When defining a function parameter we can mark it as *consuming* by
+prefixing it with an asterisk.  For a return type, we can mark it as
+*alias-free* by prefixing it with an asterisk.  For example::
 
   def modify (a: *[]i32) (i: i32) (x: i32): *[]i32 =
     a with [i] = a[i] + x
@@ -1453,18 +1453,18 @@
 
 * The aliases of a value returned from a function is the most
   interesting case, and depends on whether the return value is
-  declared *unique* (with an asterisk ``*``) or not.  If it is
-  declared unique, then it has no aliases.  Otherwise, it aliases all
-  arguments passed for *non-unique* parameters.
+  declared *alias-free* (with an asterisk ``*``) or not.  If it is
+  declared alias-free, then it has no aliases.  Otherwise, it aliases
+  all arguments passed for *non-consumed* parameters.
 
 In-place Updates and Higher-Order Functions
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-Uniqueness typing generally interacts poorly with higher-order
+Consumption generally interacts inflexibly with higher-order
 functions.  The issue is that we cannot control how many times a
 function argument is applied, or to what, so it is not safe to pass a
 function that consumes its argument.  The following two conservative
-rules govern the interaction between uniqueness types and higher-order
+rules govern the interaction between consumption and higher-order
 functions:
 
 1. In the expression ``let p = e1 in ...``, if *any* in-place update
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
@@ -32,40 +32,7 @@
 OPTIONS
 =======
 
--h
-  Print help text to standard output and exit.
-
---entry-point NAME
-  Treat this top-level function as an entry point.
-
---library
-  Generate a library instead of an executable.  Appends ``.c``/``.h``
-  to the name indicated by the ``-o`` option to determine output
-  file names.
-
--o outfile
-  Where to write the result.  If the source program is named
-  ``foo.fut``, this defaults to ``foo``.
-
---safe
-  Ignore ``unsafe`` in program and perform safety checks unconditionally.
-
---server
-  Generate a server-mode executable that reads commands from stdin.
-
--v verbose
-  Enable debugging output.  If compilation fails due to a compiler
-  error, the result of the last successful compiler step will be
-  printed to standard error.
-
--V
-  Print version information on standard output and exit.
-
--W
-  Do not print any warnings.
-
---Werror
-  Treat warnings as errors.
+Accepts the same options as :ref:`futhark-c(1)`.
 
 ENVIRONMENT VARIABLES
 =====================
diff --git a/docs/man/futhark-literate.rst b/docs/man/futhark-literate.rst
--- a/docs/man/futhark-literate.rst
+++ b/docs/man/futhark-literate.rst
@@ -82,7 +82,7 @@
 -v, --verbose
 
   Print verbose information on stderr about directives as they are
-  executing.
+  executing.  This is also needed to see ``#[trace]`` output.
 
 DIRECTIVES
 ==========
diff --git a/docs/man/futhark-multicore.rst b/docs/man/futhark-multicore.rst
--- a/docs/man/futhark-multicore.rst
+++ b/docs/man/futhark-multicore.rst
@@ -28,41 +28,7 @@
 OPTIONS
 =======
 
--h
-  Print help text to standard output and exit.
-
---entry-point NAME
-  Treat this top-level function as an entry point.
-
---library
-  Generate a library instead of an executable.  Appends ``.c``/``.h``
-  to the name indicated by the ``-o`` option to determine output
-  file names.
-
--o outfile
-  Where to write the result.  If the source program is named
-  ``foo.fut``, this defaults to ``foo``.
-
---safe
-  Ignore ``unsafe`` in program and perform safety checks unconditionally.
-
---server
-  Generate a server-mode executable that reads commands from stdin.
-
--v verbose
-  Enable debugging output.  If compilation fails due to a compiler
-  error, the result of the last successful compiler step will be
-  printed to standard error.
-
--V
-  Print version information on standard output and exit.
-
--W
-  Do not print any warnings.
-
---Werror
-  Treat warnings as errors.
-
+Accepts the same options as :ref:`futhark-c(1)`.
 
 ENVIRONMENT VARIABLES
 =====================
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
@@ -28,40 +28,7 @@
 OPTIONS
 =======
 
--h
-  Print help text to standard output and exit.
-
---entry-point NAME
-  Treat this top-level function as an entry point.
-
---library
-  Generate a library instead of an executable.  Appends ``.c``/``.h``
-  to the name indicated by the ``-o`` option to determine output
-  file names.
-
--o outfile
-  Where to write the result.  If the source program is named
-  ``foo.fut``, this defaults to ``foo``.
-
---safe
-  Ignore ``unsafe`` in program and perform safety checks unconditionally.
-
---server
-  Generate a server-mode executable that reads commands from stdin.
-
--v verbose
-  Enable debugging output.  If compilation fails due to a compiler
-  error, the result of the last successful compiler step will be
-  printed to standard error.
-
--V
-  Print version information on standard output and exit.
-
--W
-  Do not print any warnings.
-
---Werror
-  Treat warnings as errors.
+Accepts the same options as :ref:`futhark-c(1)`.
 
 ENVIRONMENT VARIABLES
 =====================
diff --git a/docs/man/futhark-pyopencl.rst b/docs/man/futhark-pyopencl.rst
--- a/docs/man/futhark-pyopencl.rst
+++ b/docs/man/futhark-pyopencl.rst
@@ -34,43 +34,7 @@
 OPTIONS
 =======
 
--h
-  Print help text to standard output and exit.
-
---entry-point NAME
-  Treat this top-level function as an entry point.
-
---library
-  Instead of compiling to an executable program, generate a Python
-  module that can be imported by other Python code.  The module will
-  contain a class of the same name as the Futhark source file with
-  ``.fut`` removed.  Objects of the class define one method per entry
-  point in the Futhark program, with matching parameters and return
-  value.
-
--o outfile
-  Where to write the resulting binary.  By default, if the source
-  program is named 'foo.fut', the binary will be named 'foo'.
-
---server
-  Generate a server-mode executable that reads commands from stdin.
-
---safe
-  Ignore ``unsafe`` in program and perform safety checks unconditionally.
-
--v verbose
-  Enable debugging output.  If compilation fails due to a compiler
-  error, the result of the last successful compiler step will be
-  printed to standard error.
-
--V
-  Print version information on standard output and exit.
-
--W
-  Do not print any warnings.
-
---Werror
-  Treat warnings as errors.
+Accepts the same options as :ref:`futhark-c(1)`.
 
 SEE ALSO
 ========
diff --git a/docs/man/futhark-python.rst b/docs/man/futhark-python.rst
--- a/docs/man/futhark-python.rst
+++ b/docs/man/futhark-python.rst
@@ -28,43 +28,7 @@
 OPTIONS
 =======
 
--h
-  Print help text to standard output and exit.
-
---entry-point NAME
-  Treat this top-level function as an entry point.
-
---library
-  Instead of compiling to an executable program, generate a Python
-  module that can be imported by other Python code.  The module will
-  contain a class of the same name as the Futhark source file with
-  ``.fut`` removed.  Objects of the class define one method per entry
-  point in the Futhark program, with matching parameters and return
-  value.
-
--o outfile
-  Where to write the resulting binary.  By default, if the source
-  program is named 'foo.fut', the binary will be named 'foo'.
-
---safe
-  Ignore ``unsafe`` in program and perform safety checks unconditionally.
-
---server
-  Generate a server-mode executable that reads commands from stdin.
-
--v verbose
-  Enable debugging output.  If compilation fails due to a compiler
-  error, the result of the last successful compiler step will be
-  printed to standard error.
-
--V
-  Print version information on standard output and exit.
-
--W
-  Do not print any warnings.
-
---Werror
-  Treat warnings as errors.
+Accepts the same options as :ref:`futhark-c(1)`.
 
 SEE ALSO
 ========
diff --git a/docs/man/futhark-wasm-multicore.rst b/docs/man/futhark-wasm-multicore.rst
--- a/docs/man/futhark-wasm-multicore.rst
+++ b/docs/man/futhark-wasm-multicore.rst
@@ -24,74 +24,18 @@
 OPTIONS
 =======
 
--h
-  Print help text to standard output and exit.
-
---entry-point NAME
-  Treat this top-level function as an entry point.
-
---library
-  Generate a library instead of an executable.  Appends ``.js``
-  to the name indicated by the ``-o`` option to determine output
-  file names.
-
--o outfile
-  Where to write the result.  If the source program is named
-  ``foo.fut``, this defaults to ``foo``.
-
---safe
-  Ignore ``unsafe`` in program and perform safety checks unconditionally.
-
---server
-  Generate a server-mode executable that reads commands from stdin.
-
--v verbose
-  Enable debugging output.  If compilation fails due to a compiler
-  error, the result of the last successful compiler step will be
-  printed to standard error.
-
--V
-  Print version information on standard output and exit.
-
--W
-  Do not print any warnings.
-
---Werror
-  Treat warnings as errors.
-
-
+Accepts the same options as :ref:`futhark-c(1)`.
 
 ENVIRONMENT VARIABLES
 =====================
 
-``CFLAGS``
-
-  Space-separated list of options passed to ``emcc``.  Defaults
-  to ``-O3 -std=c99`` if unset.
-
-``EMCFLAGS``
-
-  Space-separated list of options passed to ``emcc``.
+Respects the same environment variables as :ref:`futhark-wasm(1)`.
 
 EXECUTABLE OPTIONS
 ==================
 
-The following options are accepted by executables generated by
-``futhark wasm-multicore``.
-
--h, --help
-
-  Print help text to standard output and exit.
-
--D, --debugging
-
-  Perform possibly expensive internal correctness checks and verbose
-  logging.  Implies ``-L``.
-
--L, --log
-
-  Print various low-overhead logging information to stderr while
-  running.
+Generated executables accept the same options as those generated by
+:ref:`futhark-wasm(1)`.
 
 SEE ALSO
 ========
diff --git a/docs/man/futhark-wasm.rst b/docs/man/futhark-wasm.rst
--- a/docs/man/futhark-wasm.rst
+++ b/docs/man/futhark-wasm.rst
@@ -23,41 +23,7 @@
 OPTIONS
 =======
 
--h
-  Print help text to standard output and exit.
-
---entry-point NAME
-  Treat this top-level function as an entry point.
-
---library
-  Generate a library instead of an executable.  Appends ``.js``
-  to the name indicated by the ``-o`` option to determine output
-  file names.
-
--o outfile
-  Where to write the result.  If the source program is named
-  ``foo.fut``, this defaults to ``foo``.
-
---safe
-  Ignore ``unsafe`` in program and perform safety checks unconditionally.
-
---server
-  Generate a server-mode executable that reads commands from stdin.
-  This is the default.
-
--v verbose
-  Enable debugging output.  If compilation fails due to a compiler
-  error, the result of the last successful compiler step will be
-  printed to standard error.
-
--V
-  Print version information on standard output and exit.
-
--W
-  Do not print any warnings.
-
---Werror
-  Treat warnings as errors.
+Accepts the same options as :ref:`futhark-c(1)`.
 
 ENVIRONMENT VARIABLES
 =====================
diff --git a/docs/man/futhark.rst b/docs/man/futhark.rst
--- a/docs/man/futhark.rst
+++ b/docs/man/futhark.rst
@@ -19,7 +19,7 @@
 developing, or analysing Futhark programs.  Most subcommands are
 documented in their own manpage.  For example, ``futhark opencl`` is
 documented as :ref:`futhark-opencl(1)`.  The remaining subcommands are
-documented in this page.
+documented below.
 
 COMMANDS
 ========
@@ -57,7 +57,7 @@
 
 Print names and locations of every top-level definition in the program
 (including top levels of modules), one per line.  The program need not
-be type-correct, but it must be contain syntax errors.
+be type-correct, but it must not contain syntax errors.
 
 futhark dev options... PROGRAM
 ------------------------------
diff --git a/docs/usage.rst b/docs/usage.rst
--- a/docs/usage.rst
+++ b/docs/usage.rst
@@ -321,6 +321,8 @@
 *out*-parameters for writing the result, for target languages that do
 not support multiple return values from functions.
 
+The entry point should have a name that is also a valid C identifier.
+
 Not all Futhark types can be mapped cleanly to the target language.
 Arrays of tuples, for example, are a common issue.  In such cases,
 *opaque types* are used in the generated code.  Values of these types
diff --git a/futhark.cabal b/futhark.cabal
--- a/futhark.cabal
+++ b/futhark.cabal
@@ -1,6 +1,6 @@
 cabal-version: 2.4
 name:           futhark
-version:        0.21.11
+version:        0.21.12
 synopsis:       An optimising compiler for a functional, array-oriented language.
 
 description:    Futhark is a small programming language designed to be compiled to
@@ -364,7 +364,7 @@
     , filepath >=1.4.1.1
     , free >=4.12.4
     , futhark-data >= 1.1.0.0
-    , futhark-server >= 1.1.2.1
+    , futhark-server >= 1.2.0.0
     , futhark-manifest >= 1.0.0.0
     , githash >=0.1.6.1
     , half >= 0.3
diff --git a/prelude/array.fut b/prelude/array.fut
--- a/prelude/array.fut
+++ b/prelude/array.fut
@@ -70,7 +70,7 @@
 -- | Concatenation where the result has a predetermined size.  If the
 -- provided size is wrong, the function will fail with a run-time
 -- error.
-def concat_to [n] [m] 't (k: i64) (xs: [n]t) (ys: [m]t): *[k]t = xs ++ ys :> *[k]t
+def concat_to [n] [m] 't (k: i64) (xs: [n]t) (ys: [m]t): *[k]t = xs ++ ys :> [k]t
 
 -- | Rotate an array some number of elements to the left.  A negative
 -- rotation amount is also supported.
diff --git a/rts/c/cache.h b/rts/c/cache.h
--- a/rts/c/cache.h
+++ b/rts/c/cache.h
@@ -37,7 +37,7 @@
   // Adaptation of djb2 for larger output size by storing intermediate
   // states.
   uint32_t hash = 5381;
-  for (int i = 0; i < n; i++) {
+  for (size_t i = 0; i < n; i++) {
     hash = ((hash << 5) + hash) + in[i];
     out->hash[i % CACHE_HASH_SIZE] ^= hash;
   }
diff --git a/rts/c/util.h b/rts/c/util.h
--- a/rts/c/util.h
+++ b/rts/c/util.h
@@ -135,8 +135,8 @@
   b->used += needed;
 }
 
-static int lexical_realloc(char **error, unsigned char **ptr, size_t *old_size, size_t new_size) {
-  unsigned char *new = realloc(*ptr, new_size);
+static int lexical_realloc(char **error, unsigned char **ptr, int64_t *old_size, int64_t new_size) {
+  unsigned char *new = realloc(*ptr, (size_t)new_size);
   if (new == NULL) {
     *error = msgprintf("Failed to allocate memory.\nAttempted allocation: %12lld bytes\n",
                        (long long) new_size);
diff --git a/rts/python/scalar.py b/rts/python/scalar.py
--- a/rts/python/scalar.py
+++ b/rts/python/scalar.py
@@ -352,28 +352,28 @@
   if np.isnan(x) or np.isinf(x):
     return np.int8(0)
   else:
-    return np.uint8(np.trunc(x))
+    return np.int8(np.trunc(x))
 fptoui_f16_i8 = fptoui_f32_i8 = fptoui_f64_i8 = fptoui_T_i8
 
 def fptoui_T_i16(x):
   if np.isnan(x) or np.isinf(x):
     return np.int16(0)
   else:
-    return np.uint16(np.trunc(x))
+    return np.int16(np.trunc(x))
 fptoui_f16_i16 = fptoui_f32_i16 = fptoui_f64_i16 = fptoui_T_i16
 
 def fptoui_T_i32(x):
   if np.isnan(x) or np.isinf(x):
     return np.int32(0)
   else:
-    return np.uint32(np.trunc(x))
+    return np.int32(np.trunc(x))
 fptoui_f16_i32 = fptoui_f32_i32 = fptoui_f64_i32 = fptoui_T_i32
 
 def fptoui_T_i64(x):
   if np.isnan(x) or np.isinf(x):
     return np.int64(0)
   else:
-    return np.uint64(np.trunc(x))
+    return np.int64(np.trunc(x))
 fptoui_f16_i64 = fptoui_f32_i64 = fptoui_f64_i64 = fptoui_T_i64
 
 def fpconv_f16_f32(x):
diff --git a/src/Futhark/Actions.hs b/src/Futhark/Actions.hs
--- a/src/Futhark/Actions.hs
+++ b/src/Futhark/Actions.hs
@@ -149,7 +149,7 @@
   Action
     { actionName = "Compile to imperative multicore",
       actionDescription = "Translate program into imperative multicore IL and write it on standard output.",
-      actionProcedure = liftIO . putStrLn . pretty . snd <=< ImpGenMulticore.compileProg
+      actionProcedure = liftIO . putStrLn . pretty . snd <=< ImpGenMulticore.compileProg ImpGenMulticore.AllowDynamicScheduling
     }
 
 -- Lines that we prepend (in comments) to generated code.
diff --git a/src/Futhark/CLI/Dataset.hs b/src/Futhark/CLI/Dataset.hs
--- a/src/Futhark/CLI/Dataset.hs
+++ b/src/Futhark/CLI/Dataset.hs
@@ -195,7 +195,7 @@
 toValueType TESum {} = Left "Cannot handle sumtypes yet."
 toValueType TEDim {} = Left "Cannot handle existential sizes."
 toValueType (TEUnique t _) = toValueType t
-toValueType (TEArray t d _) = do
+toValueType (TEArray d t _) = do
   d' <- constantDim d
   V.ValueType ds t' <- toValueType t
   pure $ V.ValueType (d' : ds) t'
diff --git a/src/Futhark/CLI/Literate.hs b/src/Futhark/CLI/Literate.hs
--- a/src/Futhark/CLI/Literate.hs
+++ b/src/Futhark/CLI/Literate.hs
@@ -43,7 +43,6 @@
 import Futhark.Util.Pretty (prettyText, prettyTextOneLine)
 import qualified Futhark.Util.Pretty as PP
 import Futhark.Util.ProgressBar
-import System.Console.ANSI (clearLine)
 import System.Directory
   ( copyFile,
     createDirectoryIfMissing,
@@ -760,16 +759,15 @@
               liftIO . T.putStr $
                 "\r"
                   <> progressBar
-                    (ProgressBar 40 (fromIntegral num_frames) (fromIntegral j))
+                    (ProgressBar 40 (fromIntegral num_frames - 1) (fromIntegral j))
                   <> "generating frame "
-                  <> prettyText j
+                  <> prettyText (j + 1)
                   <> "/"
                   <> prettyText num_frames
                   <> " "
               liftIO $ hFlush stdout,
             liftIO $ do
-              T.putStr "\r"
-              clearLine
+              T.putStrLn ""
           )
       | otherwise =
           (\_ _ -> pure (), pure ())
@@ -990,7 +988,15 @@
           imgdir_rel = dropExtension (takeFileName mdfile) <> "-img"
           imgdir = takeDirectory mdfile </> imgdir_rel
           run_options = scriptExtraOptions opts
-          cfg = futharkServerCfg ("." </> dropExtension prog) run_options
+          onLine "call" l = T.putStrLn l
+          onLine _ _ = pure ()
+          cfg =
+            (futharkServerCfg ("." </> dropExtension prog) run_options)
+              { cfgOnLine =
+                  if scriptVerbose opts > 0
+                    then onLine
+                    else const . const $ pure ()
+              }
 
       withScriptServer cfg $ \server -> do
         let env =
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
@@ -259,7 +259,7 @@
           -- so force just one data set at a time here.
           ensureReferenceOutput (Just 1) (FutharkExe futhark) "c" program ios
 
-      when (mode == Compiled) $
+      when (mode `elem` [Compile, Compiled]) $
         context ("Compiling with --backend=" <> T.pack backend) $ do
           compileTestProgram extra_compiler_options (FutharkExe futhark) backend program warnings
           mapM_ (testMetrics progs program) structures
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
@@ -250,7 +250,11 @@
       GC.earlyDecl [C.cedecl|static $ty:ct $id:name_realtype[$int:n];|]
       pure n
   -- Fake a memory block.
-  GC.contextField (C.toIdent name mempty) [C.cty|struct memblock_device|] Nothing
+  GC.contextFieldDyn
+    (C.toIdent name mempty)
+    [C.cty|struct memblock_device|]
+    Nothing
+    [C.cstm|cuMemFree(ctx->$id:name.mem);|]
   -- During startup, copy the data to where we need it.
   GC.atInit
     [C.cstm|{
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
@@ -295,7 +295,11 @@
       GC.earlyDecl [C.cedecl|static $ty:ct $id:name_realtype[$int:n];|]
       pure n
   -- Fake a memory block.
-  GC.contextField (C.toIdent name mempty) [C.cty|struct memblock_device|] Nothing
+  GC.contextFieldDyn
+    (C.toIdent name mempty)
+    [C.cty|struct memblock_device|]
+    Nothing
+    [C.cstm|OPENCL_SUCCEED_FATAL(clReleaseMemObject(ctx->$id:name.mem));|]
   -- During startup, copy the data to where we need it.
   GC.atInit
     [C.cstm|{
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
@@ -84,6 +84,7 @@
 import Control.Monad.Reader
 import Control.Monad.State
 import Data.Bifunctor (first)
+import Data.Char (isAlpha, isAlphaNum)
 import qualified Data.DList as DL
 import Data.List (unzip4)
 import Data.Loc
@@ -99,6 +100,7 @@
 import Futhark.IR.Prop (isBuiltInFunction)
 import qualified Futhark.Manifest as Manifest
 import Futhark.MonadFreshNames
+import Futhark.Util (zEncodeString)
 import Futhark.Util.Pretty (prettyText)
 import qualified Language.C.Quote.OpenCL as C
 import qualified Language.C.Syntax as C
@@ -516,9 +518,9 @@
 contextField name ty initial = modify $ \s ->
   s {compCtxFields = compCtxFields s <> DL.singleton (name, ty, initial, Nothing)}
 
-contextFieldDyn :: C.Id -> C.Type -> C.Exp -> C.Stm -> CompilerM op s ()
+contextFieldDyn :: C.Id -> C.Type -> Maybe C.Exp -> C.Stm -> CompilerM op s ()
 contextFieldDyn name ty initial free = modify $ \s ->
-  s {compCtxFields = compCtxFields s <> DL.singleton (name, ty, Just initial, Just free)}
+  s {compCtxFields = compCtxFields s <> DL.singleton (name, ty, initial, Just free)}
 
 profileReport :: C.BlockItem -> CompilerM op s ()
 profileReport x = modify $ \s ->
@@ -1335,6 +1337,18 @@
             [C.cstm|$exp:dest->shape[$int:i] = $id:d;|]
       stms $ zipWith maybeCopyDim shape [0 .. rank - 1]
 
+isValidCName :: Name -> Bool
+isValidCName = check . nameToString
+  where
+    check [] = True -- academic
+    check (c : cs) = isAlpha c && all constituent cs
+    constituent c = isAlphaNum c || c == '_'
+
+entryName :: Name -> String
+entryName v
+  | isValidCName v = "entry_" <> nameToString v
+  | otherwise = "entry_" <> zEncodeString (nameToString v)
+
 onEntryPoint ::
   [C.BlockItem] ->
   Name ->
@@ -1349,7 +1363,7 @@
   outputdecls <- collect $ mapM_ stubParam outputs
   decl_mem <- declAllocatedMem
 
-  entry_point_function_name <- publicName $ "entry_" ++ nameToString ename
+  entry_point_function_name <- publicName $ entryName ename
 
   (inputs', unpack_entry_inputs) <- prepareEntryInputs $ map snd args
   let (entry_point_input_params, entry_point_input_checks) = unzip inputs'
@@ -1550,7 +1564,7 @@
 
   let headerdefs =
         [untrimming|
-// Headers\n")
+// Headers
 #include <stdint.h>
 #include <stddef.h>
 #include <stdbool.h>
@@ -1873,7 +1887,7 @@
           }
 
       declCached (mem, size) =
-        [ [C.citem|size_t $id:size = 0;|],
+        [ [C.citem|typename int64_t $id:size = 0;|],
           [C.citem|$ty:defaultMemBlockType $id:mem = NULL;|]
         ]
 
@@ -1987,10 +2001,10 @@
   pure [C.cexp|fabs($exp:x')|]
 compilePrimExp f (UnOpExp SSignum {} x) = do
   x' <- compilePrimExp f x
-  pure [C.cexp|($exp:x' > 0) - ($exp:x' < 0)|]
+  pure [C.cexp|($exp:x' > 0 ? 1 : 0) - ($exp:x' < 0 ? 1 : 0)|]
 compilePrimExp f (UnOpExp USignum {} x) = do
   x' <- compilePrimExp f x
-  pure [C.cexp|($exp:x' > 0) - ($exp:x' < 0) != 0|]
+  pure [C.cexp|($exp:x' > 0 ? 1 : 0) - ($exp:x' < 0 ? 1 : 0) != 0|]
 compilePrimExp f (UnOpExp op x) = do
   x' <- compilePrimExp f x
   pure [C.cexp|$id:(pretty op)($exp:x')|]
@@ -2139,7 +2153,7 @@
       [C.cstm|if (!($exp:cond')) { $items:fbranch' }|]
     _ ->
       [C.cstm|if ($exp:cond') { $items:tbranch' } else { $items:fbranch' }|]
-compileCode (Copy dest (Count destoffset) DefaultSpace src (Count srcoffset) DefaultSpace (Count size)) =
+compileCode (Copy _ dest (Count destoffset) DefaultSpace src (Count srcoffset) DefaultSpace (Count size)) =
   join $
     copyMemoryDefaultSpace
       <$> rawMem dest
@@ -2147,7 +2161,7 @@
       <*> rawMem src
       <*> compileExp (untyped srcoffset)
       <*> compileExp (untyped size)
-compileCode (Copy dest (Count destoffset) destspace src (Count srcoffset) srcspace (Count size)) = do
+compileCode (Copy _ dest (Count destoffset) destspace src (Count srcoffset) srcspace (Count size)) = do
   copy <- asks envCopy
   join $
     copy
@@ -2223,7 +2237,11 @@
   contextField
     (C.toIdent name noLoc)
     [C.cty|struct memblock|]
-    $ Just [C.cexp|(struct memblock){NULL, (char*)$id:name_realtype, 0}|]
+    $ Just
+      [C.cexp|(struct memblock){NULL,
+                                (unsigned char*)$id:name_realtype,
+                                0,
+                                $string:(pretty name)}|]
   item [C.citem|struct memblock $id:name = ctx->$id:name;|]
 compileCode (DeclareArray name (Space space) t vs) =
   join $
diff --git a/src/Futhark/CodeGen/Backends/GenericC/Server.hs b/src/Futhark/CodeGen/Backends/GenericC/Server.hs
--- a/src/Futhark/CodeGen/Backends/GenericC/Server.hs
+++ b/src/Futhark/CodeGen/Backends/GenericC/Server.hs
@@ -22,6 +22,7 @@
 import Futhark.Util.Pretty (prettyText)
 import qualified Language.C.Quote.OpenCL as C
 import qualified Language.C.Syntax as C
+import Language.Futhark.Core (nameFromText)
 
 genericOptions :: [Option]
 genericOptions =
@@ -168,13 +169,13 @@
 
 oneEntryBoilerplate :: Manifest -> (T.Text, EntryPoint) -> ([C.Definition], C.Initializer)
 oneEntryBoilerplate manifest (name, EntryPoint cfun outputs inputs) =
-  let call_f = "call_" ++ T.unpack name
+  let call_f = "call_" <> nameFromText name
       out_types = map outputType outputs
       in_types = map inputType inputs
-      out_types_name = T.unpack name ++ "_out_types"
-      in_types_name = T.unpack name ++ "_in_types"
-      out_unique_name = T.unpack name ++ "_out_unique"
-      in_unique_name = T.unpack name ++ "_in_unique"
+      out_types_name = nameFromText name <> "_out_types"
+      in_types_name = nameFromText name <> "_in_types"
+      out_unique_name = nameFromText name <> "_out_unique"
+      in_unique_name = nameFromText name <> "_in_unique"
       (out_items, out_args)
         | null out_types = ([C.citems|(void)outs;|], mempty)
         | otherwise = unzip $ zipWith loadOut [0 ..] out_types
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
@@ -1,5 +1,4 @@
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TupleSections #-}
 
@@ -797,41 +796,12 @@
       [PyStmt],
       [PyStmt],
       [PyStmt],
-      [PyStmt],
-      [(Imp.ExternalValue, PyExp)],
-      [PyStmt]
+      [(Imp.ExternalValue, PyExp)]
     )
 prepareEntry (fname, Imp.Function _ outputs inputs _ results args) = do
   let output_paramNames = map (compileName . Imp.paramName) outputs
       funTuple = tupleOrSingle $ fmap Var output_paramNames
 
-  (argexps_mem_copies, prepare_run) <- collect' $
-    forM inputs $ \case
-      Imp.MemParam name space -> do
-        -- A program might write to its input parameters, so create a new memory
-        -- block and copy the source there.  This way the program can be run more
-        -- than once.
-        name' <- newVName $ baseString name <> "_copy"
-        copy <- asks envCopy
-        allocate <- asks envAllocate
-        let size = Var (extName (compileName name) ++ ".nbytes") -- FIXME
-            dest = name'
-            src = name
-            offset = Integer 0
-        case space of
-          Space sid ->
-            allocate (Var (compileName name')) size sid
-          _ ->
-            stm $
-              Assign
-                (Var (compileName name'))
-                (simpleCall "allocateMem" [size]) -- FIXME
-        dest' <- compileVar dest
-        src' <- compileVar src
-        copy dest' offset space src' offset space size (IntType Int32) -- FIXME
-        pure $ Just $ compileName name'
-      _ -> pure Nothing
-
   prepareIn <- collect $ do
     declEntryPointInputSizes $ map snd args
     mapM_ entryPointInput . zip3 [0 ..] (map snd args) $
@@ -839,7 +809,6 @@
   (res, prepareOut) <- collect' $ mapM entryPointOutput results
 
   let argexps_lib = map (compileName . Imp.paramName) inputs
-      argexps_bin = zipWith fromMaybe argexps_lib argexps_mem_copies
       fname' = "self." ++ futharkFun (nameToString fname)
 
       -- We ignore overflow errors and the like for executable entry
@@ -857,10 +826,8 @@
     ( map (extValueDescName . snd) args,
       prepareIn,
       call argexps_lib,
-      call argexps_bin,
       prepareOut,
-      zip results res,
-      prepare_run
+      zip results res
     )
 
 copyMemoryDefaultSpace ::
@@ -890,7 +857,7 @@
   CompilerM op s (Maybe (PyFunDef, (PyExp, PyExp)))
 compileEntryFun sync timing entry
   | Just ename <- Imp.functionEntry $ snd entry = do
-      (params, prepareIn, body_lib, _, prepareOut, res, _) <- prepareEntry entry
+      (params, prepareIn, body_lib, prepareOut, res) <- prepareEntry entry
       let (maybe_sync, ret) =
             case timing of
               DoNotReturnTiming ->
@@ -942,7 +909,7 @@
   CompilerM op s (Maybe (PyFunDef, String, PyExp))
 callEntryFun _ (_, Imp.Function Nothing _ _ _ _ _) = pure Nothing
 callEntryFun pre_timing entry@(fname, Imp.Function (Just ename) _ _ _ _ decl_args) = do
-  (_, prepare_in, _, body_bin, _, res, prepare_run) <- prepareEntry entry
+  (_, prepare_in, body_bin, _, res) <- prepareEntry entry
 
   let str_input = map (readInput . snd) decl_args
       end_of_input = [Exp $ simpleCall "end_of_input" [String $ pretty fname]]
@@ -953,13 +920,13 @@
       (do_run_with_timing, close_runtime_file) = addTiming do_run
 
       do_warmup_run =
-        If (Var "do_warmup_run") (prepare_run ++ do_run) []
+        If (Var "do_warmup_run") do_run []
 
       do_num_runs =
         For
           "i"
           (simpleCall "range" [simpleCall "int" [Var "num_runs"]])
-          (prepare_run ++ do_run_with_timing)
+          do_run_with_timing
 
   str_output <- printValue res
 
@@ -1306,7 +1273,7 @@
   stm =<< Assign <$> compileVar name <*> pure allocate'
 compileCode (Imp.Free name _) =
   stm =<< Assign <$> compileVar name <*> pure None
-compileCode (Imp.Copy dest (Imp.Count destoffset) DefaultSpace src (Imp.Count srcoffset) DefaultSpace (Imp.Count size)) = do
+compileCode (Imp.Copy _ dest (Imp.Count destoffset) DefaultSpace src (Imp.Count srcoffset) DefaultSpace (Imp.Count size)) = do
   destoffset' <- compileExp $ Imp.untyped destoffset
   srcoffset' <- compileExp $ Imp.untyped srcoffset
   dest' <- compileVar dest
@@ -1315,7 +1282,7 @@
   let offset_call1 = simpleCall "addressOffset" [dest', destoffset', Var "ct.c_byte"]
   let offset_call2 = simpleCall "addressOffset" [src', srcoffset', Var "ct.c_byte"]
   stm $ Exp $ simpleCall "ct.memmove" [offset_call1, offset_call2, size']
-compileCode (Imp.Copy dest (Imp.Count destoffset) destspace src (Imp.Count srcoffset) srcspace (Imp.Count size)) = do
+compileCode (Imp.Copy pt dest (Imp.Count destoffset) destspace src (Imp.Count srcoffset) srcspace (Imp.Count size)) = do
   copy <- asks envCopy
   join $
     copy
@@ -1326,7 +1293,7 @@
       <*> compileExp (Imp.untyped srcoffset)
       <*> pure srcspace
       <*> compileExp (Imp.untyped size)
-      <*> pure (IntType Int32) -- FIXME
+      <*> pure pt
 compileCode (Imp.Write _ _ Unit _ _ _) = pure ()
 compileCode (Imp.Write dest (Imp.Count idx) elemtype (Imp.Space space) _ elemexp) =
   join $
diff --git a/src/Futhark/CodeGen/Backends/MulticoreC.hs b/src/Futhark/CodeGen/Backends/MulticoreC.hs
--- a/src/Futhark/CodeGen/Backends/MulticoreC.hs
+++ b/src/Futhark/CodeGen/Backends/MulticoreC.hs
@@ -16,6 +16,7 @@
 where
 
 import Control.Monad
+import Data.Loc
 import qualified Data.Map as M
 import Data.Maybe
 import qualified Data.Text as T
@@ -44,11 +45,11 @@
         [DefaultSpace]
         cliOptions
     )
-    <=< ImpGen.compileProg
+    <=< ImpGen.compileProg ImpGen.AllowDynamicScheduling
 
 -- | Generate the multicore context definitions.  This is exported
 -- because the WASM backend needs it.
-generateContext :: GC.CompilerM op () ()
+generateContext :: GC.CompilerM op s ()
 generateContext = do
   mapM_ GC.earlyDecl [C.cunit|$esc:(T.unpack schedulerH)|]
 
@@ -238,7 +239,7 @@
   ]
 
 -- | Operations for generating multicore code.
-operations :: GC.Operations Multicore ()
+operations :: GC.Operations Multicore s
 operations =
   GC.defaultOperations
     { GC.opsCompiler = compileOp,
@@ -261,12 +262,12 @@
 closureRetvalStructField v =
   nameFromString "retval_" <> nameFromString (pretty v)
 
-data ValueType = Prim | MemBlock | RawMem
+data ValueType = Prim PrimType | MemBlock | RawMem
 
 compileFreeStructFields :: [VName] -> [(C.Type, ValueType)] -> [C.FieldGroup]
 compileFreeStructFields = zipWith field
   where
-    field name (ty, Prim) =
+    field name (ty, Prim _) =
       [C.csdecl|$ty:ty $id:(closureFreeStructField name);|]
     field name (_, _) =
       [C.csdecl|$ty:defaultMemBlockType $id:(closureFreeStructField name);|]
@@ -274,7 +275,7 @@
 compileRetvalStructFields :: [VName] -> [(C.Type, ValueType)] -> [C.FieldGroup]
 compileRetvalStructFields = zipWith field
   where
-    field name (ty, Prim) =
+    field name (ty, Prim _) =
       [C.csdecl|$ty:ty *$id:(closureRetvalStructField name);|]
     field name (_, _) =
       [C.csdecl|$ty:defaultMemBlockType $id:(closureRetvalStructField name);|]
@@ -287,8 +288,8 @@
   [C.Stm]
 compileSetStructValues struct = zipWith field
   where
-    field name (_, Prim) =
-      [C.cstm|$id:struct.$id:(closureFreeStructField name)=$id:name;|]
+    field name (_, Prim pt) =
+      [C.cstm|$id:struct.$id:(closureFreeStructField name)=$exp:(toStorage pt (C.toExp name noLoc));|]
     field name (_, MemBlock) =
       [C.cstm|$id:struct.$id:(closureFreeStructField name)=$id:name.mem;|]
     field name (_, RawMem) =
@@ -300,20 +301,21 @@
   [VName] ->
   [(C.Type, ValueType)] ->
   [C.Stm]
-compileSetRetvalStructValues struct = zipWith field
+compileSetRetvalStructValues struct vnames we = concat $ zipWith field vnames we
   where
-    field name (_, Prim) =
-      [C.cstm|$id:struct.$id:(closureRetvalStructField name)=&$id:name;|]
+    field name (ct, Prim _) =
+      [C.cstms|$id:struct.$id:(closureRetvalStructField name)=(($ty:ct*)&$id:name);|]
     field name (_, MemBlock) =
-      [C.cstm|$id:struct.$id:(closureRetvalStructField name)=$id:name.mem;|]
+      [C.cstms|$id:struct.$id:(closureRetvalStructField name)=$id:name.mem;|]
     field name (_, RawMem) =
-      [C.cstm|$id:struct.$id:(closureRetvalStructField name)=$id:name;|]
+      [C.cstms|$id:struct.$id:(closureRetvalStructField name)=$id:name;|]
 
 compileGetRetvalStructVals :: C.ToIdent a => a -> [VName] -> [(C.Type, ValueType)] -> [C.InitGroup]
 compileGetRetvalStructVals struct = zipWith field
   where
-    field name (ty, Prim) =
-      [C.cdecl|$ty:ty $id:name = *$id:struct->$id:(closureRetvalStructField name);|]
+    field name (ty, Prim pt) =
+      let inner = [C.cexp|*$id:struct->$id:(closureRetvalStructField name)|]
+       in [C.cdecl|$ty:ty $id:name = $exp:(fromStorage pt inner);|]
     field name (ty, _) =
       [C.cdecl|$ty:ty $id:name =
                  {.desc = $string:(pretty name),
@@ -328,8 +330,9 @@
   [C.InitGroup]
 compileGetStructVals struct = zipWith field
   where
-    field name (ty, Prim) =
-      [C.cdecl|$ty:ty $id:name = $id:struct->$id:(closureFreeStructField name);|]
+    field name (ty, Prim pt) =
+      let inner = [C.cexp|$id:struct->$id:(closureFreeStructField name)|]
+       in [C.cdecl|$ty:ty $id:name = $exp:(fromStorage pt inner);|]
     field name (ty, _) =
       [C.cdecl|$ty:ty $id:name =
                  {.desc = $string:(pretty name),
@@ -339,15 +342,15 @@
 compileWriteBackResVals :: C.ToIdent a => a -> [VName] -> [(C.Type, ValueType)] -> [C.Stm]
 compileWriteBackResVals struct = zipWith field
   where
-    field name (_, Prim) =
-      [C.cstm|*$id:struct->$id:(closureRetvalStructField name) = $id:name;|]
+    field name (_, Prim pt) =
+      [C.cstm|*$id:struct->$id:(closureRetvalStructField name) = $exp:(toStorage pt (C.toExp name noLoc));|]
     field name (_, _) =
       [C.cstm|$id:struct->$id:(closureRetvalStructField name) = $id:name.mem;|]
 
 paramToCType :: Param -> GC.CompilerM op s (C.Type, ValueType)
 paramToCType (ScalarParam _ pt) = do
-  let t = GC.primTypeToCType pt
-  pure (t, Prim)
+  let t = primStorageType pt
+  pure (t, Prim pt)
 paramToCType (MemParam name space') = mcMemToCType name space'
 
 mcMemToCType :: VName -> Space -> GC.CompilerM op s (C.Type, ValueType)
@@ -424,17 +427,17 @@
   GC.contextFieldDyn
     (functionRuntime name)
     [C.cty|typename int64_t*|]
-    [C.cexp|calloc(sizeof(typename int64_t), ctx->scheduler.num_threads)|]
+    (Just [C.cexp|calloc(sizeof(typename int64_t), ctx->scheduler.num_threads)|])
     [C.cstm|free(ctx->$id:(functionRuntime name));|]
   GC.contextFieldDyn
     (functionRuns name)
     [C.cty|int*|]
-    [C.cexp|calloc(sizeof(int), ctx->scheduler.num_threads)|]
+    (Just [C.cexp|calloc(sizeof(int), ctx->scheduler.num_threads)|])
     [C.cstm|free(ctx->$id:(functionRuns name));|]
   GC.contextFieldDyn
     (functionIter name)
     [C.cty|typename int64_t*|]
-    [C.cexp|calloc(sizeof(sizeof(typename int64_t)), ctx->scheduler.num_threads)|]
+    (Just [C.cexp|calloc(sizeof(sizeof(typename int64_t)), ctx->scheduler.num_threads)|])
     [C.cstm|free(ctx->$id:(functionIter name));|]
 addBenchmarkFields name Nothing = do
   GC.contextField (functionRuntime name) [C.cty|typename int64_t|] $ Just [C.cexp|0|]
@@ -485,7 +488,9 @@
   s' <- newVName ("futhark_mc_" ++ s)
   pure $ nameFromString $ baseString s' ++ "_" ++ show (baseTag s')
 
-multicoreDef :: String -> (Name -> GC.CompilerM op s C.Definition) -> GC.CompilerM op s Name
+type DefSpecifier s = String -> (Name -> GC.CompilerM Multicore s C.Definition) -> GC.CompilerM Multicore s Name
+
+multicoreDef :: DefSpecifier s
 multicoreDef s f = do
   s' <- multicoreName s
   GC.libDecl =<< f s'
@@ -528,28 +533,31 @@
                       }|]
 
 prepareTaskStruct ::
+  DefSpecifier s ->
   String ->
   [VName] ->
   [(C.Type, ValueType)] ->
   [VName] ->
   [(C.Type, ValueType)] ->
   GC.CompilerM Multicore s Name
-prepareTaskStruct name free_args free_ctypes retval_args retval_ctypes = do
-  fstruct <- multicoreDef name $ \s ->
-    pure
-      [C.cedecl|struct $id:s {
+prepareTaskStruct def name free_args free_ctypes retval_args retval_ctypes = do
+  let makeStruct s =
+        pure
+          [C.cedecl|struct $id:s {
                        struct futhark_context *ctx;
                        $sdecls:(compileFreeStructFields free_args free_ctypes)
                        $sdecls:(compileRetvalStructFields retval_args retval_ctypes)
                      };|]
-  GC.decl [C.cdecl|struct $id:fstruct $id:fstruct;|]
-  GC.stm [C.cstm|$id:fstruct.ctx = ctx;|]
-  GC.stms [C.cstms|$stms:(compileSetStructValues fstruct free_args free_ctypes)|]
-  GC.stms [C.cstms|$stms:(compileSetRetvalStructValues fstruct retval_args retval_ctypes)|]
+  fstruct <- def name makeStruct
+  let fstruct' = fstruct <> "_"
+  GC.decl [C.cdecl|struct $id:fstruct $id:fstruct';|]
+  GC.stm [C.cstm|$id:fstruct'.ctx = ctx;|]
+  GC.stms [C.cstms|$stms:(compileSetStructValues fstruct' free_args free_ctypes)|]
+  GC.stms [C.cstms|$stms:(compileSetRetvalStructValues fstruct' retval_args retval_ctypes)|]
   pure fstruct
 
 -- Generate a segop function for top_level and potentially nested SegOp code
-compileOp :: GC.OpCompiler Multicore ()
+compileOp :: GC.OpCompiler Multicore s
 compileOp (GetLoopBounds start end) = do
   GC.stm [C.cstm|$id:start = start;|]
   GC.stm [C.cstm|$id:end = end;|]
@@ -568,17 +576,17 @@
 
   e' <- GC.compileExp e
 
-  let lexical = lexicalMemoryUsage $ Function Nothing [] params seq_code [] []
+  let lexical = lexicalMemoryUsageMC TraverseKernels $ Function Nothing [] params seq_code [] []
 
   fstruct <-
-    prepareTaskStruct "task" free_args free_ctypes retval_args retval_ctypes
+    prepareTaskStruct multicoreDef "task" free_args free_ctypes retval_args retval_ctypes
 
   fpar_task <- generateParLoopFn lexical (name ++ "_task") seq_code fstruct free retval
   addTimingFields fpar_task
 
   let ftask_name = fstruct <> "_task"
   GC.decl [C.cdecl|struct scheduler_segop $id:ftask_name;|]
-  GC.stm [C.cstm|$id:ftask_name.args = &$id:fstruct;|]
+  GC.stm [C.cstm|$id:ftask_name.args = &$id:(fstruct <> "_");|]
   GC.stm [C.cstm|$id:ftask_name.top_level_fn = $id:fpar_task;|]
   GC.stm [C.cstm|$id:ftask_name.name = $string:(nameToString fpar_task);|]
   GC.stm [C.cstm|$id:ftask_name.iterations = $exp:e';|]
@@ -593,7 +601,7 @@
   -- Generate the nested segop function if available
   fnpar_task <- case par_task of
     Just (ParallelTask nested_code) -> do
-      let lexical_nested = lexicalMemoryUsage $ Function Nothing [] params nested_code [] []
+      let lexical_nested = lexicalMemoryUsageMC TraverseKernels $ Function Nothing [] params nested_code [] []
       fnpar_task <- generateParLoopFn lexical_nested (name ++ "_nested_task") nested_code fstruct free retval
       GC.stm [C.cstm|$id:ftask_name.nested_fn = $id:fnpar_task;|]
       pure $ zip [fnpar_task] [True]
@@ -619,10 +627,10 @@
   free_ctypes <- mapM paramToCType free
   let free_args = map paramName free
 
-  let lexical = lexicalMemoryUsage $ Function Nothing [] free body [] []
+  let lexical = lexicalMemoryUsageMC TraverseKernels $ Function Nothing [] free body [] []
 
   fstruct <-
-    prepareTaskStruct (s' ++ "_parloop_struct") free_args free_ctypes mempty mempty
+    prepareTaskStruct multicoreDef (s' ++ "_parloop_struct") free_args free_ctypes mempty mempty
 
   ftask <- multicoreDef (s' ++ "_parloop") $ \s -> do
     fbody <- benchmarkCode s (Just "tid") <=< GC.inNewFunction $
@@ -641,19 +649,23 @@
         mapM_ GC.item body'
         GC.stm [C.cstm|cleanup: {$stms:free_cached $items:free_mem}|]
     pure
-      [C.cedecl|static int $id:s(void *args, typename int64_t start, typename int64_t end, int subtask_id, int tid) {
+      [C.cedecl|static int $id:s(void *args,
+                                 typename int64_t start,
+                                 typename int64_t end,
+                                 int subtask_id,
+                                 int tid) {
                        int err = 0;
                        struct $id:fstruct *$id:fstruct = (struct $id:fstruct*) args;
                        struct futhark_context *ctx = $id:fstruct->ctx;
                        $items:fbody
                        return err;
-                     }|]
+                }|]
 
   let ftask_name = ftask <> "_task"
   GC.decl [C.cdecl|struct scheduler_parloop $id:ftask_name;|]
   GC.stm [C.cstm|$id:ftask_name.name = $string:(nameToString ftask);|]
   GC.stm [C.cstm|$id:ftask_name.fn = $id:ftask;|]
-  GC.stm [C.cstm|$id:ftask_name.args = &$id:fstruct;|]
+  GC.stm [C.cstm|$id:ftask_name.args = &$id:(fstruct <> "_");|]
   GC.stm [C.cstm|$id:ftask_name.iterations = iterations;|]
   GC.stm [C.cstm|$id:ftask_name.info = info;|]
 
@@ -673,7 +685,7 @@
   mapM_ GC.item code'
   mapM_ GC.profileReport $ multiCoreReport $ zip [ftask, ftask_total] [True, False]
 compileOp (Atomic aop) =
-  atomicOps aop
+  atomicOps aop (\ty _ -> pure [C.cty|$ty:ty*|])
 
 doAtomic ::
   (C.ToIdent a1) =>
@@ -683,42 +695,44 @@
   Exp ->
   String ->
   C.Type ->
+  (C.Type -> VName -> GC.CompilerM op s C.Type) ->
   GC.CompilerM op s ()
-doAtomic old arr ind val op ty = do
+doAtomic old arr ind val op ty castf = do
   ind' <- GC.compileExp $ untyped $ unCount ind
   val' <- GC.compileExp val
+  cast <- castf ty arr
   arr' <- GC.rawMem arr
-  GC.stm [C.cstm|$id:old = $id:op(&(($ty:ty*)$exp:arr')[$exp:ind'], ($ty:ty) $exp:val', __ATOMIC_RELAXED);|]
+  GC.stm [C.cstm|$id:old = $id:op(&(($ty:cast)$exp:arr')[$exp:ind'], ($ty:ty) $exp:val', __ATOMIC_RELAXED);|]
 
-atomicOps :: AtomicOp -> GC.CompilerM op s ()
-atomicOps (AtomicCmpXchg t old arr ind res val) = do
+atomicOps :: AtomicOp -> (C.Type -> VName -> GC.CompilerM op s C.Type) -> GC.CompilerM op s ()
+atomicOps (AtomicCmpXchg t old arr ind res val) castf = do
   ind' <- GC.compileExp $ untyped $ unCount ind
   new_val' <- GC.compileExp val
-  let cast = [C.cty|$ty:(GC.primTypeToCType t)*|]
+  cast <- castf [C.cty|$ty:(GC.primTypeToCType t)|] arr
   arr' <- GC.rawMem arr
   GC.stm
     [C.cstm|$id:res = $id:op(&(($ty:cast)$exp:arr')[$exp:ind'],
-                ($ty:cast)&$id:old,
+                 &$id:old,
                  $exp:new_val',
                  0, __ATOMIC_SEQ_CST, __ATOMIC_RELAXED);|]
   where
     op :: String
     op = "__atomic_compare_exchange_n"
-atomicOps (AtomicXchg t old arr ind val) = do
+atomicOps (AtomicXchg t old arr ind val) castf = do
   ind' <- GC.compileExp $ untyped $ unCount ind
   val' <- GC.compileExp val
-  let cast = [C.cty|$ty:(GC.primTypeToCType t)*|]
+  cast <- castf [C.cty|$ty:(GC.primTypeToCType t)|] arr
   GC.stm [C.cstm|$id:old = $id:op(&(($ty:cast)$id:arr.mem)[$exp:ind'], $exp:val', __ATOMIC_SEQ_CST);|]
   where
     op :: String
     op = "__atomic_exchange_n"
-atomicOps (AtomicAdd t old arr ind val) =
-  doAtomic old arr ind val "__atomic_fetch_add" [C.cty|$ty:(GC.intTypeToCType t)|]
-atomicOps (AtomicSub t old arr ind val) =
-  doAtomic old arr ind val "__atomic_fetch_sub" [C.cty|$ty:(GC.intTypeToCType t)|]
-atomicOps (AtomicAnd t old arr ind val) =
-  doAtomic old arr ind val "__atomic_fetch_and" [C.cty|$ty:(GC.intTypeToCType t)|]
-atomicOps (AtomicOr t old arr ind val) =
-  doAtomic old arr ind val "__atomic_fetch_or" [C.cty|$ty:(GC.intTypeToCType t)|]
-atomicOps (AtomicXor t old arr ind val) =
-  doAtomic old arr ind val "__atomic_fetch_xor" [C.cty|$ty:(GC.intTypeToCType t)|]
+atomicOps (AtomicAdd t old arr ind val) castf =
+  doAtomic old arr ind val "__atomic_fetch_add" [C.cty|$ty:(GC.intTypeToCType t)|] castf
+atomicOps (AtomicSub t old arr ind val) castf =
+  doAtomic old arr ind val "__atomic_fetch_sub" [C.cty|$ty:(GC.intTypeToCType t)|] castf
+atomicOps (AtomicAnd t old arr ind val) castf =
+  doAtomic old arr ind val "__atomic_fetch_and" [C.cty|$ty:(GC.intTypeToCType t)|] castf
+atomicOps (AtomicOr t old arr ind val) castf =
+  doAtomic old arr ind val "__atomic_fetch_or" [C.cty|$ty:(GC.intTypeToCType t)|] castf
+atomicOps (AtomicXor t old arr ind val) castf =
+  doAtomic old arr ind val "__atomic_fetch_xor" [C.cty|$ty:(GC.intTypeToCType t)|] castf
diff --git a/src/Futhark/CodeGen/Backends/MulticoreWASM.hs b/src/Futhark/CodeGen/Backends/MulticoreWASM.hs
--- a/src/Futhark/CodeGen/Backends/MulticoreWASM.hs
+++ b/src/Futhark/CodeGen/Backends/MulticoreWASM.hs
@@ -43,7 +43,7 @@
   Prog MCMem ->
   m (ImpGen.Warnings, (GC.CParts, T.Text, [String]))
 compileProg version prog = do
-  (ws, prog') <- ImpGen.compileProg prog
+  (ws, prog') <- ImpGen.compileProg ImpGen.AllowDynamicScheduling prog
 
   prog'' <-
     GC.compileProg
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
@@ -270,10 +270,11 @@
     -- all memory blocks will be freed with this statement.
     -- Backends are free to ignore it entirely.
     Free VName Space
-  | -- | Destination, offset in destination, destination
-    -- space, source, offset in source, offset space, number
-    -- of bytes.
+  | -- | Element type being copied, destination, offset in
+    -- destination, destination space, source, offset in source,
+    -- offset space, number of bytes.
     Copy
+      PrimType
       VName
       (Count Bytes (TExp Int64))
       Space
@@ -534,10 +535,11 @@
     ppr dest <+> text "<-" <+> ppr from <+> text "@" <> ppr space
   ppr (Assert e msg _) =
     text "assert" <> parens (commasep [ppr msg, ppr e])
-  ppr (Copy dest destoffset destspace src srcoffset srcspace size) =
-    text "memcpy"
+  ppr (Copy t dest destoffset destspace src srcoffset srcspace size) =
+    text "copy"
       <> parens
-        ( ppMemLoc dest destoffset <> ppr destspace <> comma
+        ( ppr t <> comma
+            </> ppMemLoc dest destoffset <> ppr destspace <> comma
             </> ppMemLoc src srcoffset <> ppr srcspace <> comma
             </> ppr size
         )
@@ -617,8 +619,8 @@
     pure $ Allocate name size s
   traverse _ (Free name space) =
     pure $ Free name space
-  traverse _ (Copy dest destoffset destspace src srcoffset srcspace size) =
-    pure $ Copy dest destoffset destspace src srcoffset srcspace size
+  traverse _ (Copy dest pt destoffset destspace src srcoffset srcspace size) =
+    pure $ Copy dest pt destoffset destspace src srcoffset srcspace size
   traverse _ (Write name i bt val space vol) =
     pure $ Write name i bt val space vol
   traverse _ (Read x name i bt space vol) =
@@ -688,7 +690,7 @@
     freeIn' name <> freeIn' size <> freeIn' space
   freeIn' (Free name _) =
     freeIn' name
-  freeIn' (Copy dest x _ src y _ n) =
+  freeIn' (Copy _ dest x _ src y _ n) =
     freeIn' dest <> freeIn' x <> freeIn' src <> freeIn' y <> freeIn' n
   freeIn' (SetMem x y _) =
     freeIn' x <> freeIn' y
diff --git a/src/Futhark/CodeGen/ImpCode/GPU.hs b/src/Futhark/CodeGen/ImpCode/GPU.hs
--- a/src/Futhark/CodeGen/ImpCode/GPU.hs
+++ b/src/Futhark/CodeGen/ImpCode/GPU.hs
@@ -144,8 +144,6 @@
   = GetGroupId VName Int
   | GetLocalId VName Int
   | GetLocalSize VName Int
-  | GetGlobalSize VName Int
-  | GetGlobalId VName Int
   | GetLockstepWidth VName
   | Atomic Space AtomicOp
   | Barrier Fence
@@ -200,12 +198,6 @@
   ppr (GetLocalSize dest i) =
     ppr dest <+> "<-"
       <+> "get_local_size" <> parens (ppr i)
-  ppr (GetGlobalSize dest i) =
-    ppr dest <+> "<-"
-      <+> "get_global_size" <> parens (ppr i)
-  ppr (GetGlobalId dest i) =
-    ppr dest <+> "<-"
-      <+> "get_global_id" <> parens (ppr i)
   ppr (GetLockstepWidth dest) =
     ppr dest <+> "<-"
       <+> "get_lockstep_width()"
diff --git a/src/Futhark/CodeGen/ImpCode/Multicore.hs b/src/Futhark/CodeGen/ImpCode/Multicore.hs
--- a/src/Futhark/CodeGen/ImpCode/Multicore.hs
+++ b/src/Futhark/CodeGen/ImpCode/Multicore.hs
@@ -9,10 +9,13 @@
     SchedulerInfo (..),
     AtomicOp (..),
     ParallelTask (..),
+    KernelHandling (..),
+    lexicalMemoryUsageMC,
     module Futhark.CodeGen.ImpCode,
   )
 where
 
+import qualified Data.Map as M
 import Futhark.CodeGen.ImpCode
 import Futhark.Util.Pretty
 
@@ -22,7 +25,7 @@
 -- | A multicore operation.
 data Multicore
   = SegOp String [Param] ParallelTask (Maybe ParallelTask) [Param] SchedulerInfo
-  | ParLoop String (Code Multicore) [Param]
+  | ParLoop String MCCode [Param]
   | -- | Retrieve inclusive start and exclusive end indexes of the
     -- chunk we are supposed to be executing.  Only valid immediately
     -- inside a 'ParLoop' construct!
@@ -70,7 +73,7 @@
   }
 
 -- | A task for a v'SegOp'.
-newtype ParallelTask = ParallelTask (Code Multicore)
+newtype ParallelTask = ParallelTask MCCode
 
 -- | Whether the Scheduler should schedule the tasks as Dynamic
 -- or it is restainted to Static
@@ -118,7 +121,8 @@
           [ nestedBlock "params {" "}" (ppr params),
             nestedBlock "body {" "}" (ppr body)
           ]
-  ppr (Atomic _) = "AtomicOp"
+  ppr (Atomic _) =
+    "AtomicOp"
 
 instance FreeIn SchedulerInfo where
   freeIn' (SchedulerInfo iter _) = freeIn' iter
@@ -137,4 +141,42 @@
     freeIn' par_code <> freeIn' seq_code <> freeIn' info
   freeIn' (ParLoop _ body _) =
     freeIn' body
-  freeIn' (Atomic aop) = freeIn' aop
+  freeIn' (Atomic aop) =
+    freeIn' aop
+
+data KernelHandling = TraverseKernels | OpaqueKernels
+
+-- | Like @lexicalMemoryUsage@, but traverses some inner multicore ops.
+lexicalMemoryUsageMC :: KernelHandling -> Function Multicore -> M.Map VName Space
+lexicalMemoryUsageMC gokernel func =
+  M.filterWithKey (const . not . (`nameIn` nonlexical)) $
+    declared $ functionBody func
+  where
+    nonlexical =
+      set (functionBody func)
+        <> namesFromList (map paramName (functionOutput func))
+
+    go f (x :>>: y) = f x <> f y
+    go f (If _ x y) = f x <> f y
+    go f (For _ _ x) = f x
+    go f (While _ x) = f x
+    go f (Comment _ x) = f x
+    go _ _ = mempty
+
+    declared (DeclareMem mem spc) =
+      M.singleton mem spc
+    declared x = go declared x
+
+    set (SetMem x y _) = namesFromList [x, y]
+    set (Call _ _ args) = foldMap onArg args
+      where
+        onArg ExpArg {} = mempty
+        onArg (MemArg x) = oneName x
+    -- Critically, don't treat inputs to nested segops as lexical when generating
+    -- ISPC, since we want to use AoS memory for lexical blocks, which is
+    -- incompatible with pointer assignmentes visible in C.
+    set (Op (SegOp _ params _ _ retvals _)) =
+      case gokernel of
+        TraverseKernels -> mempty
+        OpaqueKernels -> namesFromList $ map paramName params <> map paramName retvals
+    set x = go set x
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
@@ -1477,6 +1477,7 @@
         else
           emit $
             Imp.Copy
+              pt
               destmem
               (bytes destoffset)
               destspace
diff --git a/src/Futhark/CodeGen/ImpGen/GPU.hs b/src/Futhark/CodeGen/ImpGen/GPU.hs
--- a/src/Futhark/CodeGen/ImpGen/GPU.hs
+++ b/src/Futhark/CodeGen/ImpGen/GPU.hs
@@ -298,6 +298,7 @@
       destspace <- entryMemSpace <$> lookupMemory destmem
       emit $
         Imp.Copy
+          bt
           destmem
           (bytes $ sExt64 destoffset)
           destspace
@@ -410,6 +411,7 @@
     copy_code =
       let num_bytes = sExt64 $ Imp.le32 x * Imp.le32 y * primByteSize bt
        in Imp.Copy
+            bt
             destmem
             (Imp.Count $ sExt64 $ Imp.le32 destoffset)
             space
diff --git a/src/Futhark/CodeGen/ImpGen/GPU/Base.hs b/src/Futhark/CodeGen/ImpGen/GPU/Base.hs
--- a/src/Futhark/CodeGen/ImpGen/GPU/Base.hs
+++ b/src/Futhark/CodeGen/ImpGen/GPU/Base.hs
@@ -1051,9 +1051,9 @@
   nubOrd <$> readsFromSet actually_free
 
 readsFromSet :: Names -> CallKernelGen [Imp.KernelUse]
-readsFromSet free =
-  fmap catMaybes $
-    forM (namesToList free) $ \var -> do
+readsFromSet = fmap catMaybes . mapM f . namesToList
+  where
+    f var = do
       t <- lookupType var
       vtable <- getVTable
       case t of
@@ -1150,17 +1150,16 @@
           mempty
 
   let set_constants = do
-        dPrim_ global_tid int32
         dPrim_ local_tid int32
         dPrim_ inner_group_size int64
         dPrim_ wave_size int32
         dPrim_ group_id int32
 
-        sOp (Imp.GetGlobalId global_tid 0)
         sOp (Imp.GetLocalId local_tid 0)
         sOp (Imp.GetLocalSize inner_group_size 0)
         sOp (Imp.GetLockstepWidth wave_size)
         sOp (Imp.GetGroupId group_id 0)
+        dPrimV_ global_tid $ le32 group_id * le32 inner_group_size + le32 local_tid
 
   pure (constants, set_constants)
 
@@ -1176,7 +1175,7 @@
 -- | Change every memory block to be in the global address space,
 -- except those who are in the local memory space.  This only affects
 -- generated code - we still need to make sure that the memory is
--- actually present on the device (and dared as variables in the
+-- actually present on the device (and declared as variables in the
 -- kernel).
 makeAllMemoryGlobal :: CallKernelGen a -> CallKernelGen a
 makeAllMemoryGlobal =
@@ -1551,14 +1550,16 @@
   thread_gtid <- newVName $ desc ++ "_gtid"
   thread_ltid <- newVName $ desc ++ "_ltid"
   group_id <- newVName $ desc ++ "_gid"
+  inner_group_size <- newVName "group_size"
   (num_groups, group_size) <- computeMapKernelGroups kernel_size
   let set_constants = do
-        dPrim_ thread_gtid int32
         dPrim_ thread_ltid int32
+        dPrim_ inner_group_size int64
         dPrim_ group_id int32
-        sOp (Imp.GetGlobalId thread_gtid 0)
         sOp (Imp.GetLocalId thread_ltid 0)
+        sOp (Imp.GetLocalSize inner_group_size 0)
         sOp (Imp.GetGroupId group_id 0)
+        dPrimV_ thread_gtid $ le32 group_id * le32 inner_group_size + le32 thread_ltid
 
   pure
     ( KernelConstants
diff --git a/src/Futhark/CodeGen/ImpGen/GPU/ToOpenCL.hs b/src/Futhark/CodeGen/ImpGen/GPU/ToOpenCL.hs
--- a/src/Futhark/CodeGen/ImpGen/GPU/ToOpenCL.hs
+++ b/src/Futhark/CodeGen/ImpGen/GPU/ToOpenCL.hs
@@ -552,15 +552,6 @@
   }
 }
 
-static inline int get_global_id_fn(int block_dim0, int block_dim1, int block_dim2, int d) {
-  return get_group_id(d) * get_local_size(d) + get_local_id(d);
-}
-#define get_global_id(d) get_global_id_fn(block_dim0, block_dim1, block_dim2, d)
-
-static inline int get_global_size(int block_dim0, int block_dim1, int block_dim2, int d) {
-  return get_num_groups(d) * get_local_size(d);
-}
-
 #define CLK_LOCAL_MEM_FENCE 1
 #define CLK_GLOBAL_MEM_FENCE 2
 static inline void barrier(int x) {
@@ -650,10 +641,6 @@
       GC.stm [C.cstm|$id:v = get_local_id($int:i);|]
     kernelOps (GetLocalSize v i) =
       GC.stm [C.cstm|$id:v = get_local_size($int:i);|]
-    kernelOps (GetGlobalId v i) =
-      GC.stm [C.cstm|$id:v = get_global_id($int:i);|]
-    kernelOps (GetGlobalSize v i) =
-      GC.stm [C.cstm|$id:v = get_global_size($int:i);|]
     kernelOps (GetLockstepWidth v) =
       GC.stm [C.cstm|$id:v = LOCKSTEP_WIDTH;|]
     kernelOps (Barrier f) = do
@@ -847,17 +834,8 @@
 typesInCode (DeclareArray _ _ t _) = S.singleton t
 typesInCode (Allocate _ (Count (TPrimExp e)) _) = typesInExp e
 typesInCode Free {} = mempty
-typesInCode
-  ( Copy
-      _
-      (Count (TPrimExp e1))
-      _
-      _
-      (Count (TPrimExp e2))
-      _
-      (Count (TPrimExp e3))
-    ) =
-    typesInExp e1 <> typesInExp e2 <> typesInExp e3
+typesInCode (Copy _ _ (Count (TPrimExp e1)) _ _ (Count (TPrimExp e2)) _ (Count (TPrimExp e3))) =
+  typesInExp e1 <> typesInExp e2 <> typesInExp e3
 typesInCode (Write _ (Count (TPrimExp e1)) t _ _ e2) =
   typesInExp e1 <> S.singleton t <> typesInExp e2
 typesInCode (Read _ _ (Count (TPrimExp e1)) t _ _) =
diff --git a/src/Futhark/CodeGen/ImpGen/GPU/Transpose.hs b/src/Futhark/CodeGen/ImpGen/GPU/Transpose.hs
--- a/src/Futhark/CodeGen/ImpGen/GPU/Transpose.hs
+++ b/src/Futhark/CodeGen/ImpGen/GPU/Transpose.hs
@@ -182,6 +182,7 @@
       get_global_id_0,
       get_local_id_0,
       get_local_id_1,
+      get_local_size_0,
       get_group_id_0,
       get_group_id_1,
       get_group_id_2,
@@ -201,6 +202,7 @@
               "get_global_id_0",
               "get_local_id_0",
               "get_local_id_1",
+              "get_local_size_0",
               "get_group_id_0",
               "get_group_id_1",
               "get_group_id_2",
@@ -210,9 +212,7 @@
 
     get_ids =
       mconcat
-        [ DeclareScalar get_global_id_0 Nonvolatile int32,
-          Op $ GetGlobalId get_global_id_0 0,
-          DeclareScalar get_local_id_0 Nonvolatile int32,
+        [ DeclareScalar get_local_id_0 Nonvolatile int32,
           Op $ GetLocalId get_local_id_0 0,
           DeclareScalar get_local_id_1 Nonvolatile int32,
           Op $ GetLocalId get_local_id_1 1,
@@ -221,7 +221,11 @@
           DeclareScalar get_group_id_1 Nonvolatile int32,
           Op $ GetGroupId get_group_id_1 1,
           DeclareScalar get_group_id_2 Nonvolatile int32,
-          Op $ GetGroupId get_group_id_2 2
+          Op $ GetGroupId get_group_id_2 2,
+          DeclareScalar get_local_size_0 Nonvolatile int32,
+          Op $ GetLocalSize get_local_size_0 0,
+          DeclareScalar get_global_id_0 Nonvolatile int32,
+          SetScalar get_global_id_0 $ untyped $ le32 get_group_id_0 * le32 get_local_size_0 + le32 get_local_id_0
         ]
 
     mkTranspose body =
diff --git a/src/Futhark/CodeGen/ImpGen/Multicore.hs b/src/Futhark/CodeGen/ImpGen/Multicore.hs
--- a/src/Futhark/CodeGen/ImpGen/Multicore.hs
+++ b/src/Futhark/CodeGen/ImpGen/Multicore.hs
@@ -5,6 +5,7 @@
 module Futhark.CodeGen.ImpGen.Multicore
   ( Futhark.CodeGen.ImpGen.Multicore.compileProg,
     Warnings,
+    SchedulingMode (..),
   )
 where
 
@@ -40,19 +41,22 @@
         (Or Int64, Imp.AtomicOr Int64)
       ]
 
+data SchedulingMode = AllowDynamicScheduling | NoDynamicScheduling
+
 -- | Compile the program.
 compileProg ::
   MonadFreshNames m =>
+  SchedulingMode ->
   Prog MCMem ->
   m (Warnings, Imp.Definitions Imp.Multicore)
-compileProg = Futhark.CodeGen.ImpGen.compileProg (HostEnv gccAtomics mempty) ops Imp.DefaultSpace
+compileProg sched = Futhark.CodeGen.ImpGen.compileProg (HostEnv gccAtomics mempty) ops Imp.DefaultSpace
   where
     ops =
       (defaultOperations opCompiler)
         { opsExpCompiler = compileMCExp
         }
     opCompiler dest (Alloc e space) = compileAlloc dest e space
-    opCompiler dest (Inner op) = compileMCOp dest op
+    opCompiler dest (Inner op) = compileMCOp sched dest op
 
 updateAcc :: VName -> [SubExp] -> [SubExp] -> MulticoreGen ()
 updateAcc acc is vs = sComment "UpdateAcc" $ do
@@ -117,11 +121,12 @@
   defCompileExp dest e
 
 compileMCOp ::
+  SchedulingMode ->
   Pat LetDecMem ->
   MCOp MCMem () ->
   ImpM MCMem HostEnv Imp.Multicore ()
-compileMCOp _ (OtherOp ()) = pure ()
-compileMCOp pat (ParOp par_op op) = do
+compileMCOp _ _ (OtherOp ()) = pure ()
+compileMCOp sched pat (ParOp par_op op) = do
   let space = getSpace op
   dPrimV_ (segFlat space) (0 :: Imp.TExp Int64)
   iterations <- getIterationDomain op space
@@ -149,7 +154,9 @@
   free_params <- filter (`notElem` retvals) <$> freeParams (par_task, seq_task)
   emit . Imp.Op $
     Imp.SegOp s free_params seq_task par_task retvals $
-      scheduling_info (decideScheduling' op seq_code)
+      case sched of
+        AllowDynamicScheduling -> scheduling_info (decideScheduling' op seq_code)
+        NoDynamicScheduling -> scheduling_info Imp.Static
 
 compileSegOp ::
   Pat LetDecMem ->
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
@@ -63,8 +63,8 @@
   DeclareMem name $ setSpace space old_space
 setCodeSpace space (DeclareArray name _ t vs) =
   DeclareArray name space t vs
-setCodeSpace space (Copy dest dest_offset dest_space src src_offset src_space n) =
-  Copy dest dest_offset dest_space' src src_offset src_space' n
+setCodeSpace space (Copy t dest dest_offset dest_space src src_offset src_space n) =
+  Copy t dest dest_offset dest_space' src src_offset src_space' n
   where
     dest_space' = setSpace space dest_space
     src_space' = setSpace space src_space
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
@@ -481,7 +481,7 @@
 
 typeHtml :: StructType -> DocM Html
 typeHtml t = case t of
-  Array _ u et shape -> do
+  Array _ u shape et -> do
     shape' <- prettyShapeDecl shape
     et' <- typeHtml $ Scalar et
     pure $ prettyU u <> shape' <> et'
@@ -545,7 +545,7 @@
   SigSpecs ss _ -> braces . (H.table ! A.class_ "specs") . mconcat <$> mapM synopsisSpec ss
   SigWith s (TypeRef v ps t _) _ -> do
     s' <- synopsisSigExp s
-    t' <- typeDeclHtml t
+    t' <- typeExpHtml t
     v' <- qualNameHtml v
     let ps' = mconcat $ map ((" " <>) . typeParamHtml) ps
     pure $ s' <> keyword " with " <> v' <> ps' <> " = " <> t'
@@ -594,11 +594,9 @@
         Unlifted -> "type "
         SizeLifted -> "type~ "
         Lifted -> "type^ "
-  ValSpec name tparams rettype _ _ -> do
+  ValSpec name tparams rettype _ _ _ -> do
     let tparams' = map typeParamHtml tparams
-    rettype' <-
-      noLink (map typeParamName tparams) $
-        typeDeclHtml rettype
+    rettype' <- noLink (map typeParamName tparams) $ typeExpHtml rettype
     pure $
       specRow
         (keyword "val " <> vnameSynopsisDef name)
@@ -608,13 +606,10 @@
     specRow (keyword "module " <> vnameSynopsisDef name) ": " <$> synopsisSigExp sig
   IncludeSpec e _ -> fullRow . (keyword "include " <>) <$> synopsisSigExp e
 
-typeDeclHtml :: TypeDeclBase f VName -> DocM Html
-typeDeclHtml = typeExpHtml . declaredType
-
 typeExpHtml :: TypeExp VName -> DocM Html
 typeExpHtml e = case e of
   TEUnique t _ -> ("*" <>) <$> typeExpHtml t
-  TEArray at d _ -> do
+  TEArray d at _ -> do
     at' <- typeExpHtml at
     d' <- dimExpHtml d
     pure $ d' <> at'
@@ -851,18 +846,16 @@
   H.dl . mconcat <$> mapM describeSpec specs
 
 describeSpec :: Spec -> DocM Html
-describeSpec (ValSpec name tparams t doc _) =
+describeSpec (ValSpec name tparams t _ doc _) =
   describeGeneric name what doc $ \name' -> do
     let tparams' = mconcat $ map ((" " <>) . typeParamHtml) tparams
-    t' <-
-      noLink (map typeParamName tparams) $
-        typeExpHtml $ declaredType t
+    t' <- noLink (map typeParamName tparams) $ typeExpHtml t
     pure $ keyword "val " <> name' <> tparams' <> ": " <> t'
   where
     what =
-      if orderZero (unInfo $ expandedType t)
-        then IndexValue
-        else IxFun
+      case t of
+        TEArrow {} -> IxFun
+        _ -> IndexValue
 describeSpec (TypeAbbrSpec vb) =
   describeGeneric (typeAlias vb) IndexType (typeDoc vb) (`typeBindHtml` vb)
 describeSpec (TypeSpec l name tparams doc _) =
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
@@ -139,14 +139,10 @@
           Literal (SignedValue (Int64Value (fromIntegral d))) loc
         Nothing ->
           Var v (replaceTypeSizes substs <$> t) loc
-    onExp substs (AppExp (Coerce e tdecl loc) (Info (AppRes t ext))) =
-      AppExp (Coerce (onExp substs e) tdecl' loc) (Info (AppRes (replaceTypeSizes substs t) ext))
+    onExp substs (AppExp (Coerce e te loc) (Info (AppRes t ext))) =
+      AppExp (Coerce (onExp substs e) te' loc) (Info (AppRes (replaceTypeSizes substs t) ext))
       where
-        tdecl' =
-          TypeDecl
-            { declaredType = onTypeExp substs $ declaredType tdecl,
-              expandedType = replaceTypeSizes substs <$> expandedType tdecl
-            }
+        te' = onTypeExp substs te
     onExp substs e = onAST substs e
 
     onTypeExpDim substs d@(DimExpNamed v loc) =
@@ -164,8 +160,8 @@
     onTypeArgExp substs (TypeArgExpType te) =
       TypeArgExpType (onTypeExp substs te)
 
-    onTypeExp substs (TEArray te d loc) =
-      TEArray (onTypeExp substs te) (onTypeExpDim substs d) loc
+    onTypeExp substs (TEArray d te loc) =
+      TEArray (onTypeExpDim substs d) (onTypeExp substs te) loc
     onTypeExp substs (TEUnique t loc) =
       TEUnique (onTypeExp substs t) loc
     onTypeExp substs (TEApply t1 t2 loc) =
@@ -289,7 +285,7 @@
     f TypeArgDim {} = mempty
     f (TypeArgType t _) = arraySizes t
 arraySizes (Scalar Prim {}) = mempty
-arraySizes (Array _ _ t shape) =
+arraySizes (Array _ _ shape t) =
   arraySizes (Scalar t) <> foldMap dimName (shapeDims shape)
   where
     dimName :: DimDecl VName -> S.Set VName
@@ -651,7 +647,7 @@
       Monoid als =>
       TypeBase (DimDecl VName) als ->
       TypeBase (DimDecl VName) als
-    defuncType (Array as u t shape) = Array as u (defuncScalar t) shape
+    defuncType (Array as u shape t) = Array as u shape (defuncScalar t)
     defuncType (Scalar t) = Scalar $ defuncScalar t
 
     defuncScalar ::
@@ -720,12 +716,13 @@
 etaExpand e_t e = do
   let (ps, ret) = getType $ RetType [] e_t
   (pats, vars) <- fmap unzip . forM ps $ \(p, t) -> do
+    let t' = fromStruct t
     x <- case p of
       Named x -> pure x
       Unnamed -> newNameFromString "x"
     pure
-      ( Id x (Info t) mempty,
-        Var (qualName x) (Info t) mempty
+      ( Id x (Info t') mempty,
+        Var (qualName x) (Info t') mempty
       )
   let e' =
         foldl'
@@ -885,8 +882,8 @@
             Var
               fname'
               ( Info
-                  ( Scalar . Arrow mempty Unnamed (fromStruct t1) . RetType [] $
-                      Scalar . Arrow mempty Unnamed (fromStruct t2) $ RetType [] rettype
+                  ( Scalar . Arrow mempty Unnamed t1 . RetType [] $
+                      Scalar . Arrow mempty Unnamed t2 $ RetType [] rettype
                   )
               )
               loc
@@ -906,7 +903,7 @@
                         ( Info $
                             AppRes
                               ( Scalar $
-                                  Arrow mempty Unnamed (fromStruct t2) $
+                                  Arrow mempty Unnamed t2 $
                                     RetType [] rettype
                               )
                               []
@@ -1130,9 +1127,9 @@
 
 -- | Construct the type for a fully-applied dynamic function from its
 -- static value and the original types of its arguments.
-dynamicFunType :: StaticVal -> [PatType] -> ([PatType], PatType)
+dynamicFunType :: StaticVal -> [StructType] -> ([PatType], PatType)
 dynamicFunType (DynamicFun _ sv) (p : ps) =
-  let (ps', ret) = dynamicFunType sv ps in (p : ps', ret)
+  let (ps', ret) = dynamicFunType sv ps in (fromStruct p : ps', ret)
 dynamicFunType sv _ = ([], typeFromSV sv)
 
 -- | Match a pattern with its static value. Returns an environment with
@@ -1215,10 +1212,8 @@
 updatePat pat@(Wildcard (Info tp) loc) sv
   | orderZero tp = pat
   | otherwise = Wildcard (Info $ typeFromSV sv) loc
-updatePat (PatAscription pat tydecl loc) sv
-  | orderZero . unInfo $ expandedType tydecl =
-      PatAscription (updatePat pat sv) tydecl loc
-  | otherwise = updatePat pat sv
+updatePat (PatAscription pat _ _) sv =
+  updatePat pat sv
 updatePat p@PatLit {} _ = p
 updatePat pat@(PatConstr c1 (Info t) ps loc) sv@(SumSV _ svs _)
   | orderZero t = pat
diff --git a/src/Futhark/Internalise/Exps.hs b/src/Futhark/Internalise/Exps.hs
--- a/src/Futhark/Internalise/Exps.hs
+++ b/src/Futhark/Internalise/Exps.hs
@@ -160,11 +160,11 @@
     entryPointType t ts
       | E.Scalar (E.Prim E.Unsigned {}) <- E.entryType t =
           I.TypeUnsigned u
-      | E.Array _ _ (E.Prim E.Unsigned {}) _ <- E.entryType t =
+      | E.Array _ _ _ (E.Prim E.Unsigned {}) <- E.entryType t =
           I.TypeUnsigned u
       | E.Scalar E.Prim {} <- E.entryType t =
           I.TypeDirect u
-      | E.Array _ _ E.Prim {} _ <- E.entryType t =
+      | E.Array _ _ _ E.Prim {} <- E.entryType t =
           I.TypeDirect u
       | otherwise =
           I.TypeOpaque u desc $ length ts
@@ -174,7 +174,7 @@
         t' = noSizes (E.entryType t) `E.setUniqueness` Nonunique
     typeExpOpaqueName (TEApply te TypeArgExpDim {} _) =
       typeExpOpaqueName te
-    typeExpOpaqueName (TEArray te _ _) =
+    typeExpOpaqueName (TEArray _ te _) =
       let (d, te') = withoutDims te
        in "arr_" ++ typeExpOpaqueName te'
             ++ "_"
@@ -183,7 +183,7 @@
     typeExpOpaqueName (TEUnique te _) = prettyOneLine te
     typeExpOpaqueName te = prettyOneLine te
 
-    withoutDims (TEArray te _ _) =
+    withoutDims (TEArray _ te _) =
       let (d, te') = withoutDims te
        in (d + 1, te')
     withoutDims te = (0 :: Int, te)
@@ -218,7 +218,7 @@
   es' <- sequence es
   varsRes . concat <$> mapM (letValExp "x") es'
 
-internaliseAppExp :: String -> [VName] -> E.AppExp -> InternaliseM [I.SubExp]
+internaliseAppExp :: String -> E.AppRes -> E.AppExp -> InternaliseM [I.SubExp]
 internaliseAppExp desc _ (E.Index e idxs loc) = do
   vs <- internaliseExpToVars "indexed" e
   dims <- case vs of
@@ -367,9 +367,9 @@
 
   se <- letSubExp desc (I.BasicOp $ I.Iota num_elems start' step it)
   pure [se]
-internaliseAppExp desc ext (E.Coerce e (TypeDecl dt (Info et)) loc) = do
+internaliseAppExp desc (E.AppRes et ext) (E.Coerce e dt loc) = do
   ses <- internaliseExp desc e
-  ts <- internaliseReturnType (E.RetType ext et) =<< mapM subExpType ses
+  ts <- internaliseReturnType (E.RetType ext (E.toStruct et)) =<< mapM subExpType ses
   dt' <- typeExpForError dt
   forM (zip ses ts) $ \(e', t') -> do
     dims <- arrayDims <$> subExpType e'
@@ -388,7 +388,7 @@
       -- easy way to do this is to just ignore the arguments and
       -- create a hole whose type is the type of the entire
       -- application.
-      internaliseExp desc (E.Hole (Info (snd $ E.unfoldFunType t)) loc)
+      internaliseExp desc (E.Hole (Info (fromStruct $ snd $ E.unfoldFunType t)) loc)
     (FunctionName qfname, args) -> do
       -- Argument evaluation is outermost-in so that any existential sizes
       -- created by function applications can be brought into scope.
@@ -621,7 +621,7 @@
     Just substs -> pure substs
     Nothing -> pure [I.Var name]
 internaliseExp desc (E.AppExp e (Info appres)) = do
-  ses <- internaliseAppExp desc (appResExt appres) e
+  ses <- internaliseAppExp desc appres e
   bindExtSizes appres ses
   pure ses
 
@@ -2246,7 +2246,7 @@
   where
     dims' = mconcat (map onDim dims)
     onDim d = "[" <> pretty d <> "]"
-typeExpForError (E.TEArray te d _) = do
+typeExpForError (E.TEArray d te _) = do
   d' <- dimExpForError d
   te' <- typeExpForError te
   pure $ ["[", d', "]"] ++ te'
diff --git a/src/Futhark/Internalise/FreeVars.hs b/src/Futhark/Internalise/FreeVars.hs
--- a/src/Futhark/Internalise/FreeVars.hs
+++ b/src/Futhark/Internalise/FreeVars.hs
@@ -65,8 +65,9 @@
   AppExp (Range e me incl _) _ ->
     freeVars e <> foldMap freeVars me <> foldMap freeVars incl
   Var qn (Info t) _ -> NameSet $ M.singleton (qualLeaf qn) $ toStruct t
-  Ascript e t _ -> freeVars e <> sizes (typeDimNames $ unInfo $ expandedType t)
-  AppExp (Coerce e t _) _ -> freeVars e <> sizes (typeDimNames $ unInfo $ expandedType t)
+  Ascript e _ _ -> freeVars e
+  AppExp (Coerce e _ _) (Info ar) ->
+    freeVars e <> sizes (typeDimNames (appResType ar))
   AppExp (LetPat let_sizes pat e1 e2 _) _ ->
     freeVars e1
       <> ( (sizes (patternDimNames pat) <> freeVars e2)
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
@@ -540,7 +540,7 @@
               (Info (Observe, xext))
               loc
           )
-          (Info $ AppRes (Scalar $ Arrow mempty yp (fromStruct ytype) (RetType [] t)) [])
+          (Info $ AppRes (Scalar $ Arrow mempty yp ytype (RetType [] t)) [])
       rettype' =
         let onDim (NamedDim d)
               | Named p <- xp, qualLeaf d == p = NamedDim $ qualName v1
@@ -582,15 +582,16 @@
 desugarProjectSection :: [Name] -> PatType -> SrcLoc -> MonoM Exp
 desugarProjectSection fields (Scalar (Arrow _ _ t1 (RetType dims t2))) loc = do
   p <- newVName "project_p"
-  let body = foldl project (Var (qualName p) (Info t1) mempty) fields
+  let body = foldl project (Var (qualName p) (Info t1') mempty) fields
   pure $
     Lambda
-      [Id p (Info t1) mempty]
+      [Id p (Info t1') mempty]
       body
       Nothing
       (Info (mempty, RetType dims $ toStruct t2))
       loc
   where
+    t1' = fromStruct t1
     project e field =
       case typeOf e of
         Scalar (Record fs)
@@ -606,14 +607,16 @@
 desugarIndexSection :: [DimIndex] -> PatType -> SrcLoc -> MonoM Exp
 desugarIndexSection idxs (Scalar (Arrow _ _ t1 (RetType dims t2))) loc = do
   p <- newVName "index_i"
-  let body = AppExp (Index (Var (qualName p) (Info t1) loc) idxs loc) (Info (AppRes t2 []))
+  let body = AppExp (Index (Var (qualName p) (Info t1') loc) idxs loc) (Info (AppRes t2 []))
   pure $
     Lambda
-      [Id p (Info t1) mempty]
+      [Id p (Info (fromStruct t1')) mempty]
       body
       Nothing
       (Info (mempty, RetType dims $ toStruct t2))
       loc
+  where
+    t1' = fromStruct t1
 desugarIndexSection _ t _ = error $ "desugarIndexSection: not a function type: " ++ pretty t
 
 noticeDims :: TypeBase (DimDecl VName) as -> MonoM ()
@@ -714,7 +717,7 @@
 noNamedParams :: MonoType -> MonoType
 noNamedParams = f
   where
-    f (Array () u t shape) = Array () u (f' t) shape
+    f (Array () u shape t) = Array () u shape (f' t)
     f (Scalar t) = Scalar $ f' t
     f' (Arrow () _ t1 (RetType dims t2)) =
       Arrow () Unnamed (f t1) (RetType dims (f t2))
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
@@ -136,7 +136,7 @@
   InternaliseTypeM [I.TypeBase ExtShape Uniqueness]
 internaliseTypeM exts orig_t =
   case orig_t of
-    E.Array _ u et shape -> do
+    E.Array _ u shape et -> do
       dims <- internaliseShape shape
       ets <- internaliseTypeM exts $ E.Scalar et
       pure [I.arrayOf et' (Shape dims) $ internaliseUniqueness u | et' <- ets]
@@ -211,7 +211,7 @@
 internalisedTypeSize :: E.TypeBase (E.DimDecl VName) als -> InternaliseM Int
 -- A few special cases for performance.
 internalisedTypeSize (E.Scalar (E.Prim _)) = pure 1
-internalisedTypeSize (E.Array _ _ (E.Prim _) _) = pure 1
+internalisedTypeSize (E.Array _ _ _ (E.Prim _)) = pure 1
 internalisedTypeSize t = length <$> internaliseType (t `E.setAliases` ())
 
 -- | Convert an external primitive to an internal primitive.
diff --git a/src/Futhark/LSP/Diagnostic.hs b/src/Futhark/LSP/Diagnostic.hs
--- a/src/Futhark/LSP/Diagnostic.hs
+++ b/src/Futhark/LSP/Diagnostic.hs
@@ -13,9 +13,9 @@
 import Control.Lens ((^.))
 import Data.Foldable (for_)
 import qualified Data.List.NonEmpty as NE
-import Data.Map (assocs, empty, insertWith)
+import qualified Data.Map as M
 import qualified Data.Text as T
-import Futhark.Compiler.Program (ProgError (ProgError))
+import Futhark.Compiler.Program (ProgError (..))
 import Futhark.LSP.Tool (posToUri, rangeFromLoc, rangeFromSrcLoc)
 import Futhark.Util (debug)
 import Futhark.Util.Loc (Loc (..), SrcLoc, locOf)
@@ -45,32 +45,29 @@
 -- | Send warning diagnostics to the client.
 publishWarningDiagnostics :: [(SrcLoc, Doc)] -> LspT () IO ()
 publishWarningDiagnostics warnings = do
-  let diags_map =
-        foldr
-          ( \(srcloc, msg) acc ->
-              let diag = mkDiagnostic (rangeFromSrcLoc srcloc) DsWarning (prettyText msg)
-               in case locOf srcloc of
-                    NoLoc -> acc
-                    Loc pos _ -> insertWith (++) (posToUri pos) [diag] acc
-          )
-          empty
-          warnings
-  publish $ assocs diags_map
+  publish $ M.assocs $ M.unionsWith (++) $ map onWarn warnings
+  where
+    onWarn (srcloc, msg) =
+      let diag = mkDiagnostic (rangeFromSrcLoc srcloc) DsWarning (prettyText msg)
+       in case locOf srcloc of
+            NoLoc -> mempty
+            Loc pos _ -> M.singleton (posToUri pos) [diag]
 
 -- | Send error diagnostics to the client.
 publishErrorDiagnostics :: NE.NonEmpty ProgError -> LspT () IO ()
-publishErrorDiagnostics errors = do
-  let diags_map =
-        foldr
-          ( \(ProgError loc msg) acc ->
-              let diag = mkDiagnostic (rangeFromLoc loc) DsError (prettyText msg)
-               in case loc of
-                    NoLoc -> acc
-                    Loc pos _ -> insertWith (++) (posToUri pos) [diag] acc
-          )
-          empty
-          errors
-  publish $ assocs diags_map
+publishErrorDiagnostics errors =
+  publish $ M.assocs $ M.unionsWith (++) $ map onDiag $ NE.toList errors
+  where
+    onDiag (ProgError loc msg) =
+      let diag = mkDiagnostic (rangeFromLoc loc) DsError (prettyText msg)
+       in case loc of
+            NoLoc -> mempty
+            Loc pos _ -> M.singleton (posToUri pos) [diag]
+    onDiag (ProgWarning loc msg) =
+      let diag = mkDiagnostic (rangeFromLoc loc) DsError (prettyText msg)
+       in case loc of
+            NoLoc -> mempty
+            Loc pos _ -> M.singleton (posToUri pos) [diag]
 
 -- | The maximum number of diagnostics to report.
 maxDiagnostic :: Int
diff --git a/src/Futhark/Script.hs b/src/Futhark/Script.hs
--- a/src/Futhark/Script.hs
+++ b/src/Futhark/Script.hs
@@ -176,7 +176,7 @@
       guard $ v `notElem` reserved
       pure v
       where
-        constituent c = isAlphaNum c || c == '_'
+        constituent c = isAlphaNum c || c == '\'' || c == '_'
 
 -- | Parse a FutharkScript expression with normal whitespace handling.
 parseExpFromText :: FilePath -> T.Text -> Either T.Text Exp
diff --git a/src/Language/Futhark.hs b/src/Language/Futhark.hs
--- a/src/Language/Futhark.hs
+++ b/src/Language/Futhark.hs
@@ -19,7 +19,6 @@
     Spec,
     Prog,
     TypeBind,
-    TypeDecl,
     StructTypeArg,
     ScalarType,
     TypeParam,
@@ -51,9 +50,6 @@
 
 -- | An constant declaration with type information.
 type ValBind = ValBindBase Info VName
-
--- | A type declaration with type information
-type TypeDecl = TypeDeclBase Info VName
 
 -- | A type binding with type information.
 type TypeBind = TypeBindBase Info VName
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
@@ -171,7 +171,7 @@
 typeShape :: M.Map VName (Shape d) -> TypeBase d () -> Shape d
 typeShape shapes = go
   where
-    go (Array _ _ et shape) =
+    go (Array _ _ shape et) =
       foldr ShapeDim (go (Scalar et)) $ shapeDims shape
     go (Scalar (Record fs)) =
       ShapeRecord $ M.map go fs
@@ -684,11 +684,11 @@
 evalType env (Scalar (Record fs)) = Scalar $ Record $ fmap (evalType env) fs
 evalType env (Scalar (Arrow () p t1 (RetType dims t2))) =
   Scalar $ Arrow () p (evalType env t1) (RetType dims (evalType env t2))
-evalType env t@(Array _ u _ shape) =
+evalType env t@(Array _ u shape _) =
   let et = stripArray (shapeRank shape) t
       et' = evalType env et
       shape' = fmap evalDim shape
-   in arrayOf et' shape' u
+   in arrayOf u shape' et'
   where
     evalDim (NamedDim qn)
       | Just (TermValue _ (ValuePrim (SignedValue (Int64Value x)))) <-
@@ -816,8 +816,8 @@
       resolveExistentials retext (evalType env $ toStruct ret) $ valueShape v
   pure v
 
-evalAppExp :: Env -> AppExp -> EvalM Value
-evalAppExp env (Range start maybe_second end loc) = do
+evalAppExp :: Env -> StructType -> AppExp -> EvalM Value
+evalAppExp env _ (Range start maybe_second end loc) = do
   start' <- asInteger <$> eval env start
   maybe_second' <- traverse (fmap asInteger . eval env) maybe_second
   end' <- traverse (fmap asInteger . eval env) end
@@ -864,31 +864,31 @@
                UpToExclusive x -> "..<" ++ pretty x
            )
         ++ " is invalid."
-evalAppExp env (Coerce e td loc) = do
+evalAppExp env t (Coerce e te loc) = do
   v <- eval env e
-  let t = evalType env $ unInfo $ expandedType td
   case checkShape (structTypeShape (envShapes env) t) (valueShape v) of
     Just _ -> pure v
     Nothing ->
       bad loc env $
         "Value `" <> pretty v <> "` of shape `" ++ pretty (valueShape v)
           ++ "` cannot match shape of type `"
-          <> pretty (declaredType td)
+          <> pretty te
           <> "` (`"
           <> pretty t
           <> "`)"
-evalAppExp env (LetPat sizes p e body _) = do
+evalAppExp env _ (LetPat sizes p e body _) = do
   v <- eval env e
   env' <- matchPat env p v
   let p_t = evalType env $ patternStructType p
       v_s = valueShape v
       env'' = env' <> i64Env (resolveExistentials (map sizeName sizes) p_t v_s)
   eval env'' body
-evalAppExp env (LetFun f (tparams, ps, _, Info ret, fbody) body _) = do
+evalAppExp env _ (LetFun f (tparams, ps, _, Info ret, fbody) body _) = do
   binding <- evalFunctionBinding env tparams ps ret fbody
   eval (env {envTerm = M.insert f binding $ envTerm env}) body
 evalAppExp
   env
+  _
   (BinOp (op, _) op_t (x, Info (_, xext)) (y, Info (_, yext)) loc)
     | baseString (qualLeaf op) == "&&" = do
         x' <- asBool <$> eval env x
@@ -905,20 +905,20 @@
         x' <- evalArg env x xext
         y' <- evalArg env y yext
         apply2 loc env op' x' y'
-evalAppExp env (If cond e1 e2 _) = do
+evalAppExp env _ (If cond e1 e2 _) = do
   cond' <- asBool <$> eval env cond
   if cond' then eval env e1 else eval env e2
-evalAppExp env (Apply f x (Info (_, ext)) loc) = do
+evalAppExp env _ (Apply f x (Info (_, ext)) loc) = do
   -- It is important that 'x' is evaluated first in order to bring any
   -- sizes into scope that may be used in the type of 'f'.
   x' <- evalArg env x ext
   f' <- eval env f
   apply loc env f' x'
-evalAppExp env (Index e is loc) = do
+evalAppExp env _ (Index e is loc) = do
   is' <- mapM (evalDimIndex env) is
   arr <- eval env e
   evalIndex loc env is' arr
-evalAppExp env (LetWith dest src is v body loc) = do
+evalAppExp env _ (LetWith dest src is v body loc) = do
   let Ident src_vn (Info src_t) _ = src
   dest' <-
     maybe oob pure
@@ -929,7 +929,7 @@
   eval (valEnv (M.singleton (identName dest) (Just t, dest')) <> env) body
   where
     oob = bad loc env "Bad update"
-evalAppExp env (DoLoop sparams pat init_e form body _) = do
+evalAppExp env _ (DoLoop sparams pat init_e form body _) = do
   init_v <- eval env init_e
   case form of
     For iv bound -> do
@@ -980,7 +980,7 @@
       env' <- withLoopParams v
       env'' <- matchPat env' in_pat in_v
       eval env'' body
-evalAppExp env (Match e cs _) = do
+evalAppExp env _ (Match e cs _) = do
   v <- eval env e
   match v (NE.toList cs)
   where
@@ -1023,7 +1023,9 @@
   vs' <- mapM (eval env) vs
   pure $ toArray' (valueShape v') (v' : vs')
 eval env (AppExp e (Info (AppRes t retext))) =
-  returned env t retext =<< evalAppExp env e
+  returned env t' retext =<< evalAppExp env t' e
+  where
+    t' = evalType env $ toStruct t
 eval env (Var qv (Info t) _) = evalTermVar env qv (toStruct t)
 eval env (Ascript e _ _) = eval env e
 eval _ (IntLit v (Info t) _) =
@@ -2027,7 +2029,7 @@
     checkInput :: ValueType -> StructType -> Either String ()
     checkInput (Scalar (Prim vt)) (Scalar (Prim pt))
       | vt /= pt = badPrim vt pt
-    checkInput (Array _ _ (Prim vt) _) (Array _ _ (Prim pt) _)
+    checkInput (Array _ _ _ (Prim vt)) (Array _ _ _ (Prim pt))
       | vt /= pt = badPrim vt pt
     checkInput _ _ =
       Right ()
diff --git a/src/Language/Futhark/Parser/Monad.hs b/src/Language/Futhark/Parser/Monad.hs
--- a/src/Language/Futhark/Parser/Monad.hs
+++ b/src/Language/Futhark/Parser/Monad.hs
@@ -69,7 +69,7 @@
 
 addDocSpec :: DocComment -> SpecBase NoInfo Name -> SpecBase NoInfo Name
 addDocSpec doc (TypeAbbrSpec tpsig) = TypeAbbrSpec (tpsig {typeDoc = Just doc})
-addDocSpec doc (ValSpec name ps t _ loc) = ValSpec name ps t (Just doc) loc
+addDocSpec doc (ValSpec name ps t NoInfo _ loc) = ValSpec name ps t NoInfo (Just doc) loc
 addDocSpec doc (TypeSpec l name ps _ loc) = TypeSpec l name ps (Just doc) loc
 addDocSpec doc (ModSpec name se _ loc) = ModSpec name se (Just doc) loc
 addDocSpec _ spec = spec
@@ -91,7 +91,7 @@
     "Only the keyword '" <> expected <> "' may appear here."
 
 mustBeEmpty :: Located loc => loc -> ValueType -> ParserMonad ()
-mustBeEmpty _ (Array _ _ _ (ShapeDecl dims))
+mustBeEmpty _ (Array _ _ (ShapeDecl dims) _)
   | 0 `elem` dims = pure ()
 mustBeEmpty loc t =
   parseErrorAt loc $ Just $ pretty t ++ " is not an empty array."
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
@@ -246,9 +246,9 @@
                                 in SigArrow (Just name) $4 $7 (srcspan $1 $>) }
         | SigExp '->' SigExp  { SigArrow Nothing $1 $3 (srcspan $1 $>) }
 
-TypeRef :: { TypeRefBase NoInfo Name }
+TypeRef :: { TypeRefBase Name }
          : QualName TypeParams '=' TypeExpTerm
-           { TypeRef (fst $1) $2 (TypeDecl $4 NoInfo) (srcspan (snd $1) $>) }
+           { TypeRef (fst $1) $2 $4 (srcspan (snd $1) $>) }
 
 SigBind :: { SigBindBase NoInfo Name }
          : module type id '=' SigExp
@@ -304,11 +304,11 @@
             | '^' { Lifted }
 
 Spec :: { SpecBase NoInfo Name }
-      : val id TypeParams ':' TypeExpDecl
+      : val id TypeParams ':' TypeExp
         { let L loc (ID name) = $2
-          in ValSpec name $3 $5 Nothing (srcspan $1 $>) }
-      | val BindingBinOp TypeParams ':' TypeExpDecl
-        { ValSpec $2 $3 $5 Nothing (srcspan $1 $>) }
+          in ValSpec name $3 $5 NoInfo Nothing (srcspan $1 $>) }
+      | val BindingBinOp TypeParams ':' TypeExp
+        { ValSpec $2 $3 $5 NoInfo Nothing (srcspan $1 $>) }
       | TypeAbbr
         { TypeAbbrSpec $1 }
 
@@ -394,30 +394,30 @@
      | '(' BindingBinOp ')' { ($2, $1) }
 
 Val    :: { ValBindBase NoInfo Name }
-Val     : def BindingId TypeParams FunParams maybeAscription(TypeExpDecl) '=' Exp
+Val     : def BindingId TypeParams FunParams maybeAscription(TypeExp) '=' Exp
           { let (name, _) = $2
-            in ValBind Nothing name (fmap declaredType $5) NoInfo
+            in ValBind Nothing name $5 NoInfo
                $3 $4 $7 Nothing mempty (srcspan $1 $>)
           }
 
-        | entry BindingId TypeParams FunParams maybeAscription(TypeExpDecl) '=' Exp
+        | entry BindingId TypeParams FunParams maybeAscription(TypeExp) '=' Exp
           { let (name, loc) = $2
-            in ValBind (Just NoInfo) name (fmap declaredType $5) NoInfo
+            in ValBind (Just NoInfo) name $5 NoInfo
                $3 $4 $7 Nothing mempty (srcspan $1 $>) }
 
-        | def FunParam BindingBinOp FunParam maybeAscription(TypeExpDecl) '=' Exp
-          { ValBind Nothing $3 (fmap declaredType $5) NoInfo [] [$2,$4] $7
+        | def FunParam BindingBinOp FunParam maybeAscription(TypeExp) '=' Exp
+          { ValBind Nothing $3 $5 NoInfo [] [$2,$4] $7
             Nothing mempty (srcspan $1 $>)
           }
 
         -- The next two for backwards compatibility.
-        | let BindingId TypeParams FunParams maybeAscription(TypeExpDecl) '=' Exp
+        | let BindingId TypeParams FunParams maybeAscription(TypeExp) '=' Exp
           { let (name, _) = $2
-            in ValBind Nothing name (fmap declaredType $5) NoInfo
+            in ValBind Nothing name $5 NoInfo
                $3 $4 $7 Nothing mempty (srcspan $1 $>)
           }
-        | let FunParam BindingBinOp FunParam maybeAscription(TypeExpDecl) '=' Exp
-          { ValBind Nothing $3 (fmap declaredType $5) NoInfo [] [$2,$4] $7
+        | let FunParam BindingBinOp FunParam maybeAscription(TypeExp) '=' Exp
+          { ValBind Nothing $3 $5 NoInfo [] [$2,$4] $7
             Nothing mempty (srcspan $1 $>)
           }
 
@@ -434,9 +434,6 @@
                       "Bind a single name instead."]
           }
 
-TypeExpDecl :: { TypeDeclBase NoInfo Name }
-             : TypeExp %prec bottom { TypeDecl $1 NoInfo }
-
 TypeAbbr :: { TypeBindBase NoInfo Name }
 TypeAbbr : type Liftedness id TypeParams '=' TypeExp
            { let L _ (ID name) = $3
@@ -461,7 +458,7 @@
          : '*' TypeExpTerm
            { TEUnique $2 (srcspan $1 $>) }
          | '[' DimExp ']' TypeExpTerm %prec indexprec
-           { TEArray $4 $2 (srcspan $1 $>) }
+           { TEArray $2 $4 (srcspan $1 $>) }
          | TypeExpApply %prec sumprec { $1 }
 
          -- Errors
@@ -562,9 +559,9 @@
 -- permit inside array indices operations (there is an ambiguity with
 -- array slices).
 Exp :: { UncheckedExp }
-     : Exp ':' TypeExpDecl { Ascript $1 $3 (srcspan $1 $>) }
-     | Exp ':>' TypeExpDecl { AppExp (Coerce $1 $3 (srcspan $1 $>)) NoInfo }
-     | Exp2 %prec ':'      { $1 }
+     : Exp ':' TypeExp  { Ascript $1 $3 (srcspan $1 $>) }
+     | Exp ':>' TypeExp { AppExp (Coerce $1 $3 (srcspan $1 $>)) NoInfo }
+     | Exp2 %prec ':'   { $1 }
 
 Exp2 :: { UncheckedExp }
      : if Exp then Exp else Exp %prec ifprec
@@ -758,9 +755,9 @@
      | let Pat '=' Exp LetBody
        { AppExp (LetPat [] $2 $4 $5 (srcspan $1 $>)) NoInfo }
 
-     | let id TypeParams FunParams1 maybeAscription(TypeExpDecl) '=' Exp LetBody
+     | let id TypeParams FunParams1 maybeAscription(TypeExp) '=' Exp LetBody
        { let L _ (ID name) = $2
-         in AppExp (LetFun name ($3, fst $4 : snd $4, (fmap declaredType $5), NoInfo, $7)
+         in AppExp (LetFun name ($3, fst $4 : snd $4, $5, NoInfo, $7)
                     $8 (srcspan $1 $>))
                    NoInfo}
 
@@ -790,7 +787,7 @@
 
 CPat :: { PatBase NoInfo Name }
           : '#[' AttrInfo ']' CPat    { PatAttr $2 $4 (srcspan $1 $>) }
-          | CInnerPat ':' TypeExpDecl { PatAscription $1 $3 (srcspan $1 $>) }
+          | CInnerPat ':' TypeExp     { PatAscription $1 $3 (srcspan $1 $>) }
           | CInnerPat                 { $1 }
           | Constr ConstrFields       { let (n, loc) = $1;
                                             loc' = srcspan loc $>
@@ -819,7 +816,7 @@
 CFieldPat :: { (Name, PatBase NoInfo Name) }
                : FieldId '=' CPat
                { (fst $1, $3) }
-               | FieldId ':' TypeExpDecl
+               | FieldId ':' TypeExp
                { (fst $1, PatAscription (Id (fst $1) NoInfo (srclocOf (snd $1))) $3 (srcspan (snd $1) $>)) }
                | FieldId
                { (fst $1, Id (fst $1) NoInfo (srclocOf (snd $1))) }
@@ -890,8 +887,8 @@
 
 Pat :: { PatBase NoInfo Name }
      : '#[' AttrInfo ']' Pat  { PatAttr $2 $4 (srcspan $1 $>) }
-     | InnerPat ':' TypeExpDecl { PatAscription $1 $3 (srcspan $1 $>) }
-     | InnerPat                 { $1 }
+     | InnerPat ':' TypeExp   { PatAscription $1 $3 (srcspan $1 $>) }
+     | InnerPat               { $1 }
 
 Pats1 :: { [PatBase NoInfo Name] }
        : Pat                    { [$1] }
@@ -909,7 +906,7 @@
 FieldPat :: { (Name, PatBase NoInfo Name) }
               : FieldId '=' Pat
                 { (fst $1, $3) }
-              | FieldId ':' TypeExpDecl
+              | FieldId ':' TypeExp
                 { (fst $1, PatAscription (Id (fst $1) NoInfo (srclocOf (snd $1))) $3 (srcspan (snd $1) $>)) }
               | FieldId
                 { (fst $1, Id (fst $1) NoInfo (srclocOf (snd $1))) }
@@ -1003,13 +1000,13 @@
 ArrayValue :: { Value }
 ArrayValue :  '[' Value ']'
              {% pure $ ArrayValue (arrayFromList [$2]) $
-                arrayOf (valueType $2) (ShapeDecl [1]) Unique
+                arrayOf Unique (ShapeDecl [1]) (valueType $2)
              }
            |  '[' Value ',' Values ']'
              {% case combArrayElements $2 $4 of
                   Left e -> throwError e
                   Right v -> pure $ ArrayValue (arrayFromList $ $2:$4) $
-                             arrayOf (valueType v) (ShapeDecl [1+fromIntegral (length $4)]) Unique
+                             arrayOf Unique (ShapeDecl [1+fromIntegral (length $4)]) (valueType v)
              }
            | id '(' ValueType ')'
              {% ($1 `mustBe` "empty") >> mustBeEmpty (srcspan $2 $4) $3 >> pure (ArrayValue (listArray (0,-1) []) $3) }
@@ -1022,8 +1019,8 @@
 Dim : intlit { let L _ (INTLIT num) = $1 in fromInteger num }
 
 ValueType :: { ValueType }
-ValueType : '[' Dim ']' ValueType  { arrayOf $4 (ShapeDecl [$2]) Nonunique }
-          | '[' Dim ']' PrimType { arrayOf (Scalar (Prim $4)) (ShapeDecl [$2]) Nonunique }
+ValueType : '[' Dim ']' ValueType  { arrayOf Nonunique (ShapeDecl [$2]) $4 }
+          | '[' Dim ']' PrimType { arrayOf Nonunique (ShapeDecl [$2]) (Scalar (Prim $4)) }
 
 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
@@ -73,9 +73,6 @@
 instance Annot Info where
   unAnnot = Just . unInfo
 
-pprAnnot :: (Annot f, Pretty a, Pretty b) => a -> f b -> Doc
-pprAnnot a b = maybe (ppr a) ppr $ unAnnot b
-
 instance Pretty Value where
   ppr (PrimValue bv) = ppr bv
   ppr (ArrayValue a t)
@@ -157,7 +154,7 @@
 
 instance Pretty (ShapeDecl dim) => Pretty (TypeBase dim as) where
   ppr = pprPrec 0
-  pprPrec _ (Array _ u at shape) = ppr u <> ppr shape <> align (pprPrec 1 at)
+  pprPrec _ (Array _ u shape at) = ppr u <> ppr shape <> align (pprPrec 1 at)
   pprPrec p (Scalar t) = pprPrec p t
 
 instance Pretty (ShapeDecl dim) => Pretty (TypeArg dim) where
@@ -167,7 +164,7 @@
 
 instance (Eq vn, IsName vn) => Pretty (TypeExp vn) where
   ppr (TEUnique t _) = text "*" <> ppr t
-  ppr (TEArray at d _) = brackets (ppr d) <> ppr at
+  ppr (TEArray d at _) = brackets (ppr d) <> ppr at
   ppr (TETuple ts _) = parens $ commasep $ map ppr ts
   ppr (TERecord fs _) = braces $ commasep $ map ppField fs
     where
@@ -189,9 +186,6 @@
   ppr (TypeArgExpDim d _) = brackets $ ppr d
   ppr (TypeArgExpType t) = ppr t
 
-instance (Eq vn, IsName vn, Annot f) => Pretty (TypeDeclBase f vn) where
-  ppr x = pprAnnot (declaredType x) (expandedType x)
-
 instance IsName vn => Pretty (QualName vn) where
   ppr (QualName names name) =
     mconcat $ punctuate (text ".") $ map pprName names ++ [pprName name]
@@ -485,7 +479,7 @@
   ppr (TypeAbbrSpec tpsig) = ppr tpsig
   ppr (TypeSpec l name ps _ _) =
     text "type" <> ppr l <+> pprName name <+> spread (map ppr ps)
-  ppr (ValSpec name tparams vtype _ _) =
+  ppr (ValSpec name tparams vtype _ _ _) =
     text "val" <+> pprName name <+> spread (map ppr tparams) <> colon <+> ppr vtype
   ppr (ModSpec name sig _ _) =
     text "module" <+> pprName name <> colon <+> ppr sig
diff --git a/src/Language/Futhark/Prop.hs b/src/Language/Futhark/Prop.hs
--- a/src/Language/Futhark/Prop.hs
+++ b/src/Language/Futhark/Prop.hs
@@ -92,7 +92,6 @@
     UncheckedType,
     UncheckedTypeExp,
     UncheckedIdent,
-    UncheckedTypeDecl,
     UncheckedDimIndex,
     UncheckedSlice,
     UncheckedExp,
@@ -135,7 +134,7 @@
 
 -- | Return the shape of a type - for non-arrays, this is 'mempty'.
 arrayShape :: TypeBase dim as -> ShapeDecl dim
-arrayShape (Array _ _ _ ds) = ds
+arrayShape (Array _ _ ds _) = ds
 arrayShape _ = mempty
 
 -- | Return any free shape declarations in the type, with duplicates
@@ -143,7 +142,7 @@
 nestedDims :: TypeBase (DimDecl VName) as -> [DimDecl VName]
 nestedDims t =
   case t of
-    Array _ _ a ds ->
+    Array _ _ ds a ->
       nubOrd $ nestedDims (Scalar a) <> shapeDims ds
     Scalar (Record fs) ->
       nubOrd $ foldMap nestedDims fs
@@ -317,14 +316,14 @@
 -- @n@ array dimensions from @t@.  Returns @Nothing@ if @t@ has less
 -- than @n@ dimensions.
 peelArray :: Int -> TypeBase dim as -> Maybe (TypeBase dim as)
-peelArray n (Array als u t shape)
+peelArray n (Array als u shape t)
   | shapeRank shape == n =
       Just $ Scalar t `addAliases` const als
   | otherwise =
-      Array als u t <$> stripDims n shape
+      Array als u <$> stripDims n shape <*> pure t
 peelArray _ _ = Nothing
 
--- | @arrayOf t s u@ constructs an array type.  The convenience
+-- | @arrayOf u s t@ constructs an array type.  The convenience
 -- compared to using the 'Array' constructor directly is that @t@ can
 -- itself be an array.  If @t@ is an @n@-dimensional array, and @s@ is
 -- a list of length @n@, the resulting type is of an @n+m@ dimensions.
@@ -332,31 +331,31 @@
 -- uniqueness of @t@.
 arrayOf ::
   Monoid as =>
-  TypeBase dim as ->
-  ShapeDecl dim ->
   Uniqueness ->
+  ShapeDecl dim ->
+  TypeBase dim as ->
   TypeBase dim as
-arrayOf t = arrayOfWithAliases (t `setUniqueness` Nonunique) mempty
+arrayOf u s t = arrayOfWithAliases mempty u s (t `setUniqueness` Nonunique)
 
 arrayOfWithAliases ::
   Monoid as =>
-  TypeBase dim as ->
   as ->
-  ShapeDecl dim ->
   Uniqueness ->
+  ShapeDecl dim ->
+  TypeBase dim as ->
   TypeBase dim as
-arrayOfWithAliases (Array as1 _ et shape1) as2 shape2 u =
-  Array (as1 <> as2) u et (shape2 <> shape1)
-arrayOfWithAliases (Scalar t) as shape u =
-  Array as u (second (const ()) t) shape
+arrayOfWithAliases as2 u shape2 (Array as1 _ shape1 et) =
+  Array (as1 <> as2) u (shape2 <> shape1) et
+arrayOfWithAliases as u shape (Scalar t) =
+  Array as u shape (second (const ()) t)
 
 -- | @stripArray n t@ removes the @n@ outermost layers of the array.
 -- Essentially, it is the type of indexing an array of type @t@ with
 -- @n@ indexes.
 stripArray :: Int -> TypeBase dim as -> TypeBase dim as
-stripArray n (Array als u et shape)
+stripArray n (Array als u shape et)
   | Just shape' <- stripDims n shape =
-      Array als u et shape'
+      Array als u shape' et
   | otherwise =
       Scalar et `setUniqueness` u `setAliases` als
 stripArray _ t = t
@@ -446,14 +445,12 @@
     f (TypeArgType t1 loc) (TypeArgType t2 _) =
       TypeArgType (combineTypeShapes t1 t2) loc
     f targ _ = targ
-combineTypeShapes (Array als1 u1 et1 shape1) (Array als2 _u2 et2 _shape2) =
+combineTypeShapes (Array als1 u1 shape1 et1) (Array als2 _u2 _shape2 et2) =
   arrayOfWithAliases
-    ( combineTypeShapes (Scalar et1) (Scalar et2)
-        `setAliases` mempty
-    )
     (als1 <> als2)
-    shape1
     u1
+    shape1
+    (combineTypeShapes (Scalar et1) (Scalar et2) `setAliases` mempty)
 combineTypeShapes _ new_tp = new_tp
 
 -- | Match the dimensions of otherwise assumed-equal types.  The
@@ -472,12 +469,11 @@
       forall as'. Monoid as' => [VName] -> TypeBase d1 as' -> TypeBase d2 as' -> m (TypeBase d1 as')
     matchDims' bound t1 t2 =
       case (t1, t2) of
-        (Array als1 u1 et1 shape1, Array als2 u2 et2 shape2) ->
+        (Array als1 u1 shape1 et1, Array als2 u2 shape2 et2) ->
           flip setAliases (als1 <> als2)
-            <$> ( arrayOf
-                    <$> matchDims' bound (Scalar et1) (Scalar et2)
-                    <*> onShapes bound shape1 shape2
-                    <*> pure (min u1 u2)
+            <$> ( arrayOf (min u1 u2)
+                    <$> onShapes bound shape1 shape2
+                      <*> matchDims' bound (Scalar et1) (Scalar et2)
                 )
         (Scalar (Record f1), Scalar (Record f2)) ->
           Scalar . Record
@@ -498,11 +494,14 @@
         ( Scalar (TypeVar als1 u v targs1),
           Scalar (TypeVar als2 _ _ targs2)
           ) ->
-            Scalar . TypeVar (als1 <> als2) u v <$> zipWithM matchTypeArg targs1 targs2
+            Scalar . TypeVar (als1 <> als2) u v
+              <$> zipWithM (matchTypeArg bound) targs1 targs2
         _ -> pure t1
 
-    matchTypeArg ta@TypeArgType {} _ = pure ta
-    matchTypeArg a _ = pure a
+    matchTypeArg _ ta@TypeArgType {} _ = pure ta
+    matchTypeArg bound (TypeArgDim x loc) (TypeArgDim y _) =
+      TypeArgDim <$> onDims bound x y <*> pure loc
+    matchTypeArg _ a _ = pure a
 
     maybePName (Named v) = Just v
     maybePName Unnamed = Nothing
@@ -513,8 +512,8 @@
 -- | Set the uniqueness attribute of a type.  If the type is a record
 -- or sum type, the uniqueness of its components will be modified.
 setUniqueness :: TypeBase dim as -> Uniqueness -> TypeBase dim as
-setUniqueness (Array als _ et shape) u =
-  Array als u et shape
+setUniqueness (Array als _ shape et) u =
+  Array als u shape et
 setUniqueness (Scalar (TypeVar als _ t targs)) u =
   Scalar $ TypeVar als u t targs
 setUniqueness (Scalar (Record ets)) u =
@@ -582,8 +581,8 @@
   Array
     mempty
     Unique
-    (Prim (Unsigned Int8))
     (ShapeDecl [ConstDim $ genericLength vs])
+    (Prim (Unsigned Int8))
 typeOf (Project _ _ (Info t) _) = t
 typeOf (Var _ (Info t) _) = t
 typeOf (Hole (Info t) _) = t
@@ -605,9 +604,9 @@
 typeOf (OpSection _ (Info t) _) =
   t
 typeOf (OpSectionLeft _ _ _ (_, Info (pn, pt2)) (Info ret, _) _) =
-  Scalar $ Arrow mempty pn (fromStruct pt2) ret
+  Scalar $ Arrow mempty pn pt2 ret
 typeOf (OpSectionRight _ _ _ (Info (pn, pt1), _) (Info ret) _) =
-  Scalar $ Arrow mempty pn (fromStruct pt1) ret
+  Scalar $ Arrow mempty pn pt1 ret
 typeOf (ProjectSection _ (Info t) _) = t
 typeOf (IndexSection _ (Info t) _) = t
 typeOf (Constr _ _ (Info t) _) = t
@@ -616,20 +615,25 @@
 
 -- | @foldFunType ts ret@ creates a function type ('Arrow') that takes
 -- @ts@ as parameters and returns @ret@.
-foldFunType :: Monoid as => [TypeBase dim as] -> RetTypeBase dim as -> TypeBase dim as
+foldFunType ::
+  Monoid as =>
+  [TypeBase dim pas] ->
+  RetTypeBase dim as ->
+  TypeBase dim as
 foldFunType ps ret =
   let RetType _ t = foldr arrow ret ps
    in t
   where
-    arrow t1 t2 = RetType [] $ Scalar $ Arrow mempty Unnamed t1 t2
+    arrow t1 t2 =
+      RetType [] $ Scalar $ Arrow mempty Unnamed (toStruct t1) t2
 
 -- | Extract the parameter types and return type from a type.
 -- If the type is not an arrow type, the list of parameter types is empty.
-unfoldFunType :: TypeBase dim as -> ([TypeBase dim as], TypeBase dim as)
+unfoldFunType :: TypeBase dim as -> ([TypeBase dim ()], TypeBase dim ())
 unfoldFunType (Scalar (Arrow _ _ t1 (RetType _ t2))) =
   let (ps, r) = unfoldFunType t2
    in (t1 : ps, r)
-unfoldFunType t = ([], t)
+unfoldFunType t = ([], toStruct t)
 
 -- | The type scheme of a value binding, comprising the type
 -- parameters and the actual type.
@@ -667,7 +671,7 @@
     Scalar (Arrow _ _ t1 (RetType _ t2)) -> typeVars t1 <> typeVars t2
     Scalar (Record fields) -> foldMap typeVars fields
     Scalar (Sum cs) -> mconcat $ (foldMap . fmap) typeVars cs
-    Array _ _ rt _ -> typeVars $ Scalar rt
+    Array _ _ _ rt -> typeVars $ Scalar rt
   where
     typeVarFree = S.singleton . typeLeaf
     typeArgFree (TypeArgType ta _) = typeVars ta
@@ -691,8 +695,7 @@
 patternDimNames (PatParens p _) = patternDimNames p
 patternDimNames (Id _ (Info tp) _) = typeDimNames tp
 patternDimNames (Wildcard (Info tp) _) = typeDimNames tp
-patternDimNames (PatAscription p (TypeDecl _ (Info t)) _) =
-  patternDimNames p <> typeDimNames t
+patternDimNames (PatAscription p _ _) = patternDimNames p
 patternDimNames (PatLit _ (Info tp) _) = typeDimNames tp
 patternDimNames (PatConstr _ _ ps _) = foldMap patternDimNames ps
 patternDimNames (PatAttr _ p _) = patternDimNames p
@@ -772,8 +775,8 @@
   patternParam p
 patternParam (PatAttr _ p _) =
   patternParam p
-patternParam (PatAscription (Id v _ _) td _) =
-  (Named v, unInfo $ expandedType td)
+patternParam (PatAscription (Id v (Info t) _) _ _) =
+  (Named v, toStruct t)
 patternParam (Id v (Info t) _) =
   (Named v, toStruct t)
 patternParam p =
@@ -854,18 +857,18 @@
           ++ [ ( "flatten",
                  IntrinsicPolyFun
                    [tp_a, sp_n, sp_m]
-                   [Array () Nonunique t_a (shape [n, m])]
-                   $ RetType [k] $ Array () Nonunique t_a $ shape [k]
+                   [Array () Nonunique (shape [n, m]) t_a]
+                   $ RetType [k] $ Array () Nonunique (shape [k]) t_a
                ),
                ( "unflatten",
                  IntrinsicPolyFun
                    [tp_a, sp_n]
                    [ Scalar $ Prim $ Signed Int64,
                      Scalar $ Prim $ Signed Int64,
-                     Array () Nonunique t_a (shape [n])
+                     Array () Nonunique (shape [n]) t_a
                    ]
                    $ RetType [k, m] $
-                     Array () Nonunique t_a $ shape [k, m]
+                     Array () Nonunique (shape [k, m]) t_a
                ),
                ( "concat",
                  IntrinsicPolyFun
@@ -888,18 +891,18 @@
                ( "scatter",
                  IntrinsicPolyFun
                    [tp_a, sp_n, sp_l]
-                   [ Array () Unique t_a (shape [n]),
-                     Array () Nonunique (Prim $ Signed Int64) (shape [l]),
-                     Array () Nonunique t_a (shape [l])
+                   [ Array () Unique (shape [n]) t_a,
+                     Array () Nonunique (shape [l]) (Prim $ Signed Int64),
+                     Array () Nonunique (shape [l]) t_a
                    ]
-                   $ RetType [] $ Array () Unique t_a (shape [n])
+                   $ RetType [] $ Array () Unique (shape [n]) t_a
                ),
                ( "scatter_2d",
                  IntrinsicPolyFun
                    [tp_a, sp_n, sp_m, sp_l]
                    [ uarr_a $ shape [n, m],
-                     Array () Nonunique (tupInt64 2) (shape [l]),
-                     Array () Nonunique t_a (shape [l])
+                     Array () Nonunique (shape [l]) (tupInt64 2),
+                     Array () Nonunique (shape [l]) t_a
                    ]
                    $ RetType [] $ uarr_a $ shape [n, m]
                ),
@@ -907,8 +910,8 @@
                  IntrinsicPolyFun
                    [tp_a, sp_n, sp_m, sp_k, sp_l]
                    [ uarr_a $ shape [n, m, k],
-                     Array () Nonunique (tupInt64 3) (shape [l]),
-                     Array () Nonunique t_a (shape [l])
+                     Array () Nonunique (shape [l]) (tupInt64 3),
+                     Array () Nonunique (shape [l]) t_a
                    ]
                    $ RetType [] $ uarr_a $ shape [n, m, k]
                ),
@@ -932,7 +935,7 @@
                      uarr_a $ shape [m],
                      Scalar t_a `arr` (Scalar t_a `arr` Scalar t_a),
                      Scalar t_a,
-                     Array () Nonunique (tupInt64 1) (shape [n]),
+                     Array () Nonunique (shape [n]) (tupInt64 1),
                      arr_a (shape [n])
                    ]
                    $ RetType [] $ uarr_a $ shape [m]
@@ -944,7 +947,7 @@
                      uarr_a $ shape [m, k],
                      Scalar t_a `arr` (Scalar t_a `arr` Scalar t_a),
                      Scalar t_a,
-                     Array () Nonunique (tupInt64 2) (shape [n]),
+                     Array () Nonunique (shape [n]) (tupInt64 2),
                      arr_a (shape [n])
                    ]
                    $ RetType [] $ uarr_a $ shape [m, k]
@@ -956,7 +959,7 @@
                      uarr_a $ shape [m, k, l],
                      Scalar t_a `arr` (Scalar t_a `arr` Scalar t_a),
                      Scalar t_a,
-                     Array () Nonunique (tupInt64 3) (shape [n]),
+                     Array () Nonunique (shape [n]) (tupInt64 3),
                      arr_a (shape [n])
                    ]
                    $ RetType [] $ uarr_a $ shape [m, k, l]
@@ -1006,7 +1009,7 @@
                    ( RetType [m] . Scalar $
                        tupleRecord
                          [ uarr_a $ shape [k],
-                           Array () Unique (Prim $ Signed Int64) (shape [n])
+                           Array () Unique (shape [n]) (Prim $ Signed Int64)
                          ]
                    )
                ),
@@ -1183,31 +1186,32 @@
     [a, b, n, m, k, l, p, q] = zipWith VName (map nameFromString ["a", "b", "n", "m", "k", "l", "p", "q"]) [0 ..]
 
     t_a = TypeVar () Nonunique (typeName a) []
-    arr_a = Array () Nonunique t_a
-    uarr_a = Array () Unique t_a
+    arr_a s = Array () Nonunique s t_a
+    uarr_a s = Array () Unique s t_a
     tp_a = TypeParamType Unlifted a mempty
 
     t_b = TypeVar () Nonunique (typeName b) []
-    arr_b = Array () Nonunique t_b
-    uarr_b = Array () Unique t_b
+    arr_b s = Array () Nonunique s t_b
+    uarr_b s = Array () Unique s t_b
     tp_b = TypeParamType Unlifted b mempty
 
     [sp_n, sp_m, sp_k, sp_l, sp_p, sp_q] = map (`TypeParamDim` mempty) [n, m, k, l, p, q]
 
     shape = ShapeDecl . map (NamedDim . qualName)
 
-    tuple_arr x y =
+    tuple_arr x y s =
       Array
         ()
         Nonunique
+        s
         (Record (M.fromList $ zip tupleFieldNames [x, y]))
     tuple_uarr x y s = tuple_arr x y s `setUniqueness` Unique
 
     arr x y = Scalar $ Arrow mempty Unnamed x (RetType [] y)
 
-    arr_ka = Array () Nonunique t_a (ShapeDecl [NamedDim $ qualName k])
-    uarr_ka = Array () Unique t_a (ShapeDecl [NamedDim $ qualName k])
-    arr_kb = Array () Nonunique t_b (ShapeDecl [NamedDim $ qualName k])
+    arr_ka = Array () Nonunique (ShapeDecl [NamedDim $ qualName k]) t_a
+    uarr_ka = Array () Unique (ShapeDecl [NamedDim $ qualName k]) t_a
+    arr_kb = Array () Nonunique (ShapeDecl [NamedDim $ qualName k]) t_b
     karr x y = Scalar $ Arrow mempty (Named k) x (RetType [] y)
 
     accType t =
@@ -1461,9 +1465,6 @@
 
 -- | An expression with no type annotations.
 type UncheckedTypeExp = TypeExp Name
-
--- | A type declaration with no expanded type.
-type UncheckedTypeDecl = TypeDeclBase NoInfo Name
 
 -- | An identifier with no type annotations.
 type UncheckedIdent = IdentBase NoInfo Name
diff --git a/src/Language/Futhark/Query.hs b/src/Language/Futhark/Query.hs
--- a/src/Language/Futhark/Query.hs
+++ b/src/Language/Futhark/Query.hs
@@ -154,8 +154,8 @@
 specDefs :: Spec -> Defs
 specDefs spec =
   case spec of
-    ValSpec v tparams tdecl _ loc ->
-      let vdef = DefBound $ BoundTerm (unInfo $ expandedType tdecl) (locOf loc)
+    ValSpec v tparams _ (Info t) _ loc ->
+      let vdef = DefBound $ BoundTerm t (locOf loc)
        in M.insert v vdef $ mconcat (map typeParamDefs tparams)
     TypeAbbrSpec tbind -> typeBindDefs tbind
     TypeSpec _ v _ _ loc ->
@@ -217,7 +217,7 @@
       msum $ map (`atPosInTypeExp` pos) es
     TERecord fields _ ->
       msum $ map ((`atPosInTypeExp` pos) . snd) fields
-    TEArray te' dim _ ->
+    TEArray dim te' _ ->
       atPosInTypeExp te' pos `mplus` inDim dim
     TEUnique te' _ ->
       atPosInTypeExp te' pos
@@ -249,8 +249,8 @@
   atPosInPat pat pos
 atPosInPat (PatAttr _ pat _) pos =
   atPosInPat pat pos
-atPosInPat (PatAscription pat tdecl _) pos =
-  atPosInPat pat pos `mplus` atPosInTypeExp (declaredType tdecl) pos
+atPosInPat (PatAscription pat te _) pos =
+  atPosInPat pat pos `mplus` atPosInTypeExp te pos
 atPosInPat (PatConstr _ _ pats _) pos =
   msum $ map (`atPosInPat` pos) pats
 atPosInPat PatLit {} _ = Nothing
@@ -273,10 +273,10 @@
   | b `contains` pos = Just $ RawAtName (qualName $ identName b) (locOf b)
 atPosInExp (AppExp (DoLoop _ merge _ _ _ _) _) pos
   | merge `contains` pos = atPosInPat merge pos
-atPosInExp (Ascript _ tdecl _) pos
-  | tdecl `contains` pos = atPosInTypeExp (declaredType tdecl) pos
-atPosInExp (AppExp (Coerce _ tdecl _) _) pos
-  | tdecl `contains` pos = atPosInTypeExp (declaredType tdecl) pos
+atPosInExp (Ascript _ te _) pos
+  | te `contains` pos = atPosInTypeExp te pos
+atPosInExp (AppExp (Coerce _ te _) _) pos
+  | te `contains` pos = atPosInTypeExp te pos
 atPosInExp e pos = do
   guard $ e `contains` pos
   -- Use the Either monad for short-circuiting for efficiency reasons.
@@ -312,7 +312,7 @@
 atPosInSpec :: Spec -> Pos -> Maybe RawAtPos
 atPosInSpec spec pos =
   case spec of
-    ValSpec _ _ tdecl _ _ -> atPosInTypeExp (declaredType tdecl) pos
+    ValSpec _ _ te _ _ _ -> atPosInTypeExp te pos
     TypeAbbrSpec tbind -> atPosInTypeBind tbind pos
     TypeSpec {} -> Nothing
     ModSpec _ se _ _ -> atPosInSigExp se pos
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
@@ -42,7 +42,6 @@
     PatRetType,
     ValueType,
     Diet (..),
-    TypeDeclBase (..),
 
     -- * Values
     IntValue (..),
@@ -357,7 +356,7 @@
   | Sum (M.Map Name [TypeBase dim as])
   | -- | The aliasing corresponds to the lexical
     -- closure of the function.
-    Arrow as PName (TypeBase dim as) (RetTypeBase dim as)
+    Arrow as PName (TypeBase dim ()) (RetTypeBase dim as)
   deriving (Eq, Ord, Show)
 
 instance Bitraversable ScalarTypeBase where
@@ -366,7 +365,7 @@
   bitraverse f g (TypeVar als u t args) =
     TypeVar <$> g als <*> pure u <*> pure t <*> traverse (traverse f) args
   bitraverse f g (Arrow als v t1 t2) =
-    Arrow <$> g als <*> pure v <*> bitraverse f g t1 <*> bitraverse f g t2
+    Arrow <$> g als <*> pure v <*> bitraverse f pure t1 <*> bitraverse f g t2
   bitraverse f g (Sum cs) = Sum <$> (traverse . traverse) (bitraverse f g) cs
 
 instance Bifunctor ScalarTypeBase where
@@ -382,13 +381,13 @@
 -- out arrays-of-arrays.
 data TypeBase dim as
   = Scalar (ScalarTypeBase dim as)
-  | Array as Uniqueness (ScalarTypeBase dim ()) (ShapeDecl dim)
+  | Array as Uniqueness (ShapeDecl dim) (ScalarTypeBase dim ())
   deriving (Eq, Ord, Show)
 
 instance Bitraversable TypeBase where
   bitraverse f g (Scalar t) = Scalar <$> bitraverse f g t
-  bitraverse f g (Array a u t shape) =
-    Array <$> g a <*> pure u <*> bitraverse f pure t <*> traverse f shape
+  bitraverse f g (Array a u shape t) =
+    Array <$> g a <*> pure u <*> traverse f shape <*> bitraverse f pure t
 
 instance Bifunctor TypeBase where
   bimap = bimapDefault
@@ -468,7 +467,7 @@
   = TEVar (QualName vn) SrcLoc
   | TETuple [TypeExp vn] SrcLoc
   | TERecord [(Name, TypeExp vn)] SrcLoc
-  | TEArray (TypeExp vn) (DimExp vn) SrcLoc
+  | TEArray (DimExp vn) (TypeExp vn) SrcLoc
   | TEUnique (TypeExp vn) SrcLoc
   | TEApply (TypeExp vn) (TypeArgExp vn) SrcLoc
   | TEArrow (Maybe vn) (TypeExp vn) (TypeExp vn) SrcLoc
@@ -513,25 +512,6 @@
   locOf (TypeArgExpDim _ loc) = locOf loc
   locOf (TypeArgExpType t) = locOf t
 
--- | A declaration of the type of something.
-data TypeDeclBase f vn = TypeDecl
-  { -- | The type declared by the user.
-    declaredType :: TypeExp vn,
-    -- | The type deduced by the type checker.
-    expandedType :: f StructType
-  }
-
-deriving instance Show (TypeDeclBase Info VName)
-
-deriving instance Show vn => Show (TypeDeclBase NoInfo vn)
-
-deriving instance Eq (TypeDeclBase NoInfo VName)
-
-deriving instance Ord (TypeDeclBase NoInfo VName)
-
-instance Located (TypeDeclBase f vn) where
-  locOf = locOf . declaredType
-
 -- | Information about which parts of a value/type are consumed.
 data Diet
   = -- | Consumes these fields in the record.
@@ -716,7 +696,7 @@
       (f (Diet, Maybe VName))
       SrcLoc
   | -- | Size coercion: @e :> t@.
-    Coerce (ExpBase f vn) (TypeDeclBase f vn) SrcLoc
+    Coerce (ExpBase f vn) (TypeExp vn) SrcLoc
   | Range
       (ExpBase f vn)
       (Maybe (ExpBase f vn))
@@ -866,7 +846,7 @@
   | -- | Array indexing as a section: @(.[i,j])@.
     IndexSection (SliceBase f vn) (f PatType) SrcLoc
   | -- | Type ascription: @e : t@.
-    Ascript (ExpBase f vn) (TypeDeclBase f vn) SrcLoc
+    Ascript (ExpBase f vn) (TypeExp vn) SrcLoc
   | AppExp (AppExpBase f vn) (f AppRes)
 
 deriving instance Show (ExpBase Info VName)
@@ -966,7 +946,7 @@
   | PatParens (PatBase f vn) SrcLoc
   | Id vn (f PatType) SrcLoc
   | Wildcard (f PatType) SrcLoc -- Nothing, i.e. underscore.
-  | PatAscription (PatBase f vn) (TypeDeclBase f vn) SrcLoc
+  | PatAscription (PatBase f vn) (TypeExp vn) SrcLoc
   | PatLit PatLit (f PatType) SrcLoc
   | PatConstr Name (f PatType) [PatBase f vn] SrcLoc
   | PatAttr (AttrInfo vn) (PatBase f vn) SrcLoc
@@ -1113,7 +1093,8 @@
   = ValSpec
       { specName :: vn,
         specTypeParams :: [TypeParamBase vn],
-        specType :: TypeDeclBase f vn,
+        specTypeExp :: TypeExp vn,
+        specType :: f StructType,
         specDoc :: Maybe DocComment,
         specLocation :: SrcLoc
       }
@@ -1128,7 +1109,7 @@
 deriving instance Show (SpecBase NoInfo Name)
 
 instance Located (SpecBase f vn) where
-  locOf (ValSpec _ _ _ _ loc) = locOf loc
+  locOf (ValSpec _ _ _ _ _ loc) = locOf loc
   locOf (TypeAbbrSpec tbind) = locOf tbind
   locOf (TypeSpec _ _ _ _ loc) = locOf loc
   locOf (ModSpec _ _ _ loc) = locOf loc
@@ -1139,7 +1120,7 @@
   = SigVar (QualName vn) (f (M.Map VName VName)) SrcLoc
   | SigParens (SigExpBase f vn) SrcLoc
   | SigSpecs [SpecBase f vn] SrcLoc
-  | SigWith (SigExpBase f vn) (TypeRefBase f vn) SrcLoc
+  | SigWith (SigExpBase f vn) (TypeRefBase vn) SrcLoc
   | SigArrow (Maybe vn) (SigExpBase f vn) (SigExpBase f vn) SrcLoc
 
 deriving instance Show (SigExpBase Info VName)
@@ -1147,13 +1128,13 @@
 deriving instance Show (SigExpBase NoInfo Name)
 
 -- | A type refinement.
-data TypeRefBase f vn = TypeRef (QualName vn) [TypeParamBase vn] (TypeDeclBase f vn) SrcLoc
+data TypeRefBase vn = TypeRef (QualName vn) [TypeParamBase vn] (TypeExp vn) SrcLoc
 
-deriving instance Show (TypeRefBase Info VName)
+deriving instance Show (TypeRefBase VName)
 
-deriving instance Show (TypeRefBase NoInfo Name)
+deriving instance Show (TypeRefBase Name)
 
-instance Located (TypeRefBase f vn) where
+instance Located (TypeRefBase vn) where
   locOf (TypeRef _ _ _ loc) = locOf loc
 
 instance Located (SigExpBase f vn) where
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
@@ -282,18 +282,14 @@
 traverseScalarType f g h (TypeVar als u t args) =
   TypeVar <$> h als <*> pure u <*> f t <*> traverse (traverseTypeArg f g) args
 traverseScalarType f g h (Arrow als v t1 (RetType dims t2)) =
-  Arrow <$> h als <*> pure v <*> traverseType f g h t1
+  Arrow <$> h als <*> pure v <*> traverseType f g pure t1
     <*> (RetType dims <$> traverseType f g h t2)
 traverseScalarType f g h (Sum cs) =
   Sum <$> (traverse . traverse) (traverseType f g h) cs
 
-traverseType ::
-  Applicative f =>
-  TypeTraverser f TypeBase dim1 als1 dims als2
-traverseType f g h (Array als u et shape) =
-  Array <$> h als <*> pure u
-    <*> traverseScalarType f g pure et
-    <*> traverse g shape
+traverseType :: Applicative f => TypeTraverser f TypeBase dim1 als1 dims als2
+traverseType f g h (Array als u shape et) =
+  Array <$> h als <*> pure u <*> traverse g shape <*> traverseScalarType f g pure et
 traverseType f g h (Scalar t) =
   Scalar <$> traverseScalarType f g h t
 
@@ -324,10 +320,6 @@
 instance ASTMappable PatRetType where
   astMap tv (RetType ext t) = RetType ext <$> astMap tv t
 
-instance ASTMappable (TypeDeclBase Info VName) where
-  astMap tv (TypeDecl dt (Info et)) =
-    TypeDecl <$> astMap tv dt <*> (Info <$> mapOnStructType tv et)
-
 instance ASTMappable (IdentBase Info VName) where
   astMap tv (Ident name (Info t) loc) =
     Ident <$> mapOnName tv name <*> (Info <$> mapOnPatType tv t) <*> pure loc
@@ -390,9 +382,6 @@
 -- complex abstraction.  The types ensure that this will be correct
 -- anyway, so it's just tedious, and not actually fragile.
 
-bareTypeDecl :: TypeDeclBase Info VName -> TypeDeclBase NoInfo VName
-bareTypeDecl (TypeDecl te _) = TypeDecl te NoInfo
-
 bareField :: FieldBase Info VName -> FieldBase NoInfo VName
 bareField (RecordFieldExplicit name e loc) =
   RecordFieldExplicit name (bareExp e) loc
@@ -405,8 +394,7 @@
 barePat (PatParens p loc) = PatParens (barePat p) loc
 barePat (Id v _ loc) = Id v NoInfo loc
 barePat (Wildcard _ loc) = Wildcard NoInfo loc
-barePat (PatAscription pat (TypeDecl t _) loc) =
-  PatAscription (barePat pat) (TypeDecl t NoInfo) loc
+barePat (PatAscription pat t loc) = PatAscription (barePat pat) t loc
 barePat (PatLit v _ loc) = PatLit v NoInfo loc
 barePat (PatConstr c _ ps loc) = PatConstr c NoInfo (map barePat ps) loc
 barePat (PatAttr attr p loc) = PatAttr attr (barePat p) loc
@@ -439,8 +427,7 @@
 bareExp (StringLit vs loc) = StringLit vs loc
 bareExp (RecordLit fields loc) = RecordLit (map bareField fields) loc
 bareExp (ArrayLit els _ loc) = ArrayLit (map bareExp els) NoInfo loc
-bareExp (Ascript e tdecl loc) =
-  Ascript (bareExp e) (bareTypeDecl tdecl) loc
+bareExp (Ascript e te loc) = Ascript (bareExp e) te loc
 bareExp (Negate x loc) = Negate (bareExp x) loc
 bareExp (Not x loc) = Not (bareExp x) loc
 bareExp (Update src slice v loc) =
@@ -497,8 +484,8 @@
           LetFun name (fparams, map barePat params, ret, NoInfo, bareExp e) (bareExp body) loc
         Range start next end loc ->
           Range (bareExp start) (fmap bareExp next) (fmap bareExp end) loc
-        Coerce e tdecl loc ->
-          Coerce (bareExp e) (bareTypeDecl tdecl) loc
+        Coerce e te loc ->
+          Coerce (bareExp e) te loc
         Index arr slice loc ->
           Index (bareExp arr) (map bareDimIndex slice) loc
 bareExp (Attr attr e 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
@@ -21,7 +21,6 @@
 import Control.Monad.Except
 import Control.Monad.Writer hiding (Sum)
 import Data.Bifunctor (first, second)
-import Data.Char (isAlpha, isAlphaNum)
 import Data.Either
 import qualified Data.Map.Strict as M
 import Data.Maybe
@@ -201,11 +200,11 @@
         }
 
 checkTypeDecl ::
-  TypeDeclBase NoInfo Name ->
-  TypeM ([VName], TypeDeclBase Info VName, Liftedness)
-checkTypeDecl (TypeDecl te NoInfo) = do
+  UncheckedTypeExp ->
+  TypeM ([VName], TypeExp VName, StructType, Liftedness)
+checkTypeDecl te = do
   (te', svars, RetType dims st, l) <- checkTypeExp te
-  pure (svars ++ dims, TypeDecl te' $ Info st, l)
+  pure (svars ++ dims, te', st, l)
 
 -- In this function, after the recursion, we add the Env of the
 -- current Spec *after* the one that is returned from the recursive
@@ -215,21 +214,21 @@
 -- redundantly imported multiple times).
 checkSpecs :: [SpecBase NoInfo Name] -> TypeM (TySet, Env, [SpecBase Info VName])
 checkSpecs [] = pure (mempty, mempty, [])
-checkSpecs (ValSpec name tparams vtype doc loc : specs) =
+checkSpecs (ValSpec name tparams vtype NoInfo doc loc : specs) =
   bindSpaced [(Term, name)] $ do
     name' <- checkName Term name loc
-    (tparams', vtype') <-
+    (tparams', vtype', vtype_t) <-
       checkTypeParams tparams $ \tparams' -> bindingTypeParams tparams' $ do
-        (ext, vtype', _) <- checkTypeDecl vtype
+        (ext, vtype', vtype_t, _) <- checkTypeDecl vtype
 
         unless (null ext) $
           typeError loc mempty $
             "All function parameters must have non-anonymous sizes."
               </> "Hint: add size parameters to" <+> pquote (pprName name') <> "."
 
-        pure (tparams', vtype')
+        pure (tparams', vtype', vtype_t)
 
-    let binding = BoundV tparams' $ unInfo $ expandedType vtype'
+    let binding = BoundV tparams' vtype_t
         valenv =
           mempty
             { envVtable = M.singleton name' binding,
@@ -239,7 +238,7 @@
     pure
       ( abstypes,
         env <> valenv,
-        ValSpec name' tparams' vtype' doc loc : specs'
+        ValSpec name' tparams' vtype' (Info vtype_t) doc loc : specs'
       )
 checkSpecs (TypeAbbrSpec tdec : specs) =
   bindSpaced [(Type, typeAlias tdec)] $ do
@@ -315,14 +314,14 @@
   checkForDuplicateSpecs specs
   (abstypes, env, specs') <- checkSpecs specs
   pure (abstypes, MTy abstypes $ ModEnv env, SigSpecs specs' loc)
-checkSigExp (SigWith s (TypeRef tname ps td trloc) loc) = do
+checkSigExp (SigWith s (TypeRef tname ps te trloc) loc) = do
   (abs, s_abs, s_env, s') <- checkSigExpToEnv s
   checkTypeParams ps $ \ps' -> do
-    (ext, td', _) <- bindingTypeParams ps' $ checkTypeDecl td
+    (ext, te', te_t, _) <- bindingTypeParams ps' $ checkTypeDecl te
     unless (null ext) $
-      typeError td' mempty "Anonymous dimensions are not allowed here."
-    (tname', s_abs', s_env') <- refineEnv loc s_abs s_env tname ps' $ unInfo $ expandedType td'
-    pure (abs, MTy s_abs' $ ModEnv s_env', SigWith s' (TypeRef tname' ps' td' trloc) loc)
+      typeError te' mempty "Anonymous dimensions are not allowed here."
+    (tname', s_abs', s_env') <- refineEnv loc s_abs s_env tname ps' te_t
+    pure (abs, MTy s_abs' $ ModEnv s_env', SigWith s' (TypeRef tname' ps' te' trloc) loc)
 checkSigExp (SigArrow maybe_pname e1 e2 loc) = do
   (e1_abs, MTy s_abs e1_mod, e1') <- checkSigExp e1
   (env_for_e2, maybe_pname') <-
@@ -533,7 +532,7 @@
           dupDefinitionError namespace name loc loc'
         _ -> pure $ M.insert (namespace, name) loc known
 
-    f (ValSpec name _ _ _ loc) =
+    f (ValSpec name _ _ _ _ loc) =
       check Term name loc
     f (TypeAbbrSpec (TypeBind name _ _ _ _ _ loc)) =
       check Type name loc
@@ -604,12 +603,10 @@
 
     patternEntry (PatParens p _) =
       patternEntry p
-    patternEntry (PatAscription p tdecl _) =
-      EntryParam (patternName p) $
-        EntryType (unInfo (expandedType tdecl)) (Just (declaredType tdecl))
+    patternEntry (PatAscription p te _) =
+      EntryParam (patternName p) $ EntryType (patternStructType p) (Just te)
     patternEntry p =
-      EntryParam (patternName p) $
-        EntryType (patternStructType p) Nothing
+      EntryParam (patternName p) $ EntryType (patternStructType p) Nothing
 
     patternName (Id x _ _) = baseName x
     patternName (PatParens p _) = patternName p
@@ -626,13 +623,6 @@
     onRetType te t =
       ([], EntryType t te)
 
-entryPointNameIsAcceptable :: Name -> Bool
-entryPointNameIsAcceptable = check . nameToString
-  where
-    check [] = True -- academic
-    check (c : cs) = isAlpha c && all constituent cs
-    constituent c = isAlphaNum c || c == '_'
-
 checkValBind :: ValBindBase NoInfo Name -> TypeM (Env, ValBind)
 checkValBind (ValBind entry fname maybe_tdecl NoInfo tparams params body doc attrs loc) = do
   top_level <- atTopLevel
@@ -648,8 +638,6 @@
 
   case entry' of
     Just _
-      | not $ entryPointNameIsAcceptable fname ->
-          typeError loc mempty "Entry point names must start with a letter and contain only letters, digits, and underscores."
       | any isTypeParam tparams' ->
           typeError loc mempty "Entry point functions may not be polymorphic."
       | not (all patternOrderZero params')
@@ -712,14 +700,14 @@
 nastyParameter :: Pat -> Bool
 nastyParameter p = nastyType (patternType p) && not (ascripted p)
   where
-    ascripted (PatAscription _ (TypeDecl te _) _) = niceTypeExp te
+    ascripted (PatAscription _ te _) = niceTypeExp te
     ascripted (PatParens p' _) = ascripted p'
     ascripted _ = False
 
 niceTypeExp :: TypeExp VName -> Bool
 niceTypeExp (TEVar (QualName [] _) _) = True
 niceTypeExp (TEApply te TypeArgExpDim {} _) = niceTypeExp te
-niceTypeExp (TEArray te _ _) = niceTypeExp te
+niceTypeExp (TEArray _ te _) = niceTypeExp te
 niceTypeExp (TEUnique te _) = niceTypeExp te
 niceTypeExp _ = False
 
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
@@ -149,8 +149,8 @@
           Scalar $ Record $ fmap substituteInType ts
         substituteInType (Scalar (Sum ts)) =
           Scalar $ Sum $ (fmap . fmap) substituteInType ts
-        substituteInType (Array () u t shape) =
-          arrayOf (substituteInType $ Scalar t) (substituteInShape shape) u
+        substituteInType (Array () u shape t) =
+          arrayOf u (substituteInShape shape) (substituteInType $ Scalar t)
         substituteInType (Scalar (Arrow als v t1 (RetType dims t2))) =
           Scalar $ Arrow als v (substituteInType t1) $ RetType dims $ substituteInType t2
 
diff --git a/src/Language/Futhark/TypeChecker/Monad.hs b/src/Language/Futhark/TypeChecker/Monad.hs
--- a/src/Language/Futhark/TypeChecker/Monad.hs
+++ b/src/Language/Futhark/TypeChecker/Monad.hs
@@ -413,8 +413,8 @@
       S.Set VName ->
       TypeBase (DimDecl VName) as ->
       TypeBase (DimDecl VName) as
-    onType except (Array as u et shape) =
-      Array as u (onScalar except et) (fmap (onDim except) shape)
+    onType except (Array as u shape et) =
+      Array as u (fmap (onDim except) shape) (onScalar except et)
     onType except (Scalar t) =
       Scalar $ onScalar except t
 
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
@@ -68,11 +68,11 @@
   Slice ->
   TypeBase (DimDecl VName) as ->
   TermTypeM (TypeBase (DimDecl VName) as, [VName])
-sliceShape r slice t@(Array als u et (ShapeDecl orig_dims)) =
+sliceShape r slice t@(Array als u (ShapeDecl orig_dims) et) =
   runStateT (setDims <$> adjustDims slice orig_dims) []
   where
     setDims [] = stripArray (length orig_dims) t
-    setDims dims' = Array als u et $ ShapeDecl dims'
+    setDims dims' = Array als u (ShapeDecl dims') et
 
     -- If the result is supposed to be a nonrigid size variable, then
     -- don't bother trying to create non-existential sizes.  This is
@@ -128,10 +128,10 @@
 lexicalClosure :: [Pat] -> Occurrences -> TermTypeM Aliasing
 lexicalClosure params closure = do
   vtable <- asks $ scopeVtable . termScope
-  let isLocal v = case v `M.lookup` vtable of
-        Just (BoundV Local _ _) -> True
+  let isGlobal v = case v `M.lookup` vtable of
+        Just (BoundV Global _ _) -> True
         _ -> False
-  pure . S.map AliasBound . S.filter isLocal $
+  pure . S.map AliasBound . S.filter (not . isGlobal) $
     allOccurring closure S.\\ mconcat (map patNames params)
 
 noAliasesIfOverloaded :: PatType -> TermTypeM PatType
@@ -145,10 +145,10 @@
 
 checkAscript ::
   SrcLoc ->
-  UncheckedTypeDecl ->
+  UncheckedTypeExp ->
   UncheckedExp ->
-  TermTypeM (TypeDecl, Exp)
-checkAscript loc (TypeDecl te NoInfo) e = do
+  TermTypeM (TypeExp VName, Exp)
+checkAscript loc te e = do
   (te', decl_t, _) <- checkTypeExpNonrigid te
   e' <- checkExp e
   e_t <- toStruct <$> expTypeFully e'
@@ -156,43 +156,27 @@
   onFailure (CheckingAscription decl_t e_t) $
     unify (mkUsage loc "type ascription") decl_t e_t
 
-  -- We also have to make sure that uniqueness matches.  This is done
-  -- explicitly, because uniqueness is ignored by unification.
-  e_t' <- normTypeFully e_t
-  decl_t' <- normTypeFully decl_t
-  unless (noSizes e_t' `subtypeOf` noSizes decl_t') $
-    typeError loc mempty $
-      "Type" <+> pquote (ppr e_t') <+> "is not a subtype of"
-        <+> pquote (ppr decl_t') <> "."
-
-  pure (TypeDecl te' $ Info decl_t', e')
+  pure (te', e')
 
 checkCoerce ::
   SrcLoc ->
-  UncheckedTypeDecl ->
+  UncheckedTypeExp ->
   UncheckedExp ->
-  TermTypeM (TypeDecl, Exp, [VName])
-checkCoerce loc (TypeDecl te NoInfo) e = do
-  (te', decl_t, ext) <- checkTypeExpRigid te RigidCoerce
+  TermTypeM (TypeExp VName, StructType, Exp, [VName])
+checkCoerce loc te e = do
+  (te', te_t, ext) <- checkTypeExpRigid te RigidCoerce
   e' <- checkExp e
   e_t <- toStruct <$> expTypeFully e'
 
   (e_t_nonrigid, _) <-
     allDimsFreshInType loc Nonrigid "coerce_d" e_t
 
-  onFailure (CheckingAscription decl_t e_t) $
-    unify (mkUsage loc "type ascription") decl_t e_t_nonrigid
+  onFailure (CheckingAscription te_t e_t) $
+    unify (mkUsage loc "type ascription") te_t e_t_nonrigid
 
-  -- We also have to make sure that uniqueness matches.  This is done
-  -- explicitly, because uniqueness is ignored by unification.
-  e_t' <- normTypeFully e_t
-  decl_t' <- normTypeFully decl_t
-  unless (noSizes e_t' `subtypeOf` noSizes decl_t') $
-    typeError loc mempty $
-      "Type" <+> pquote (ppr e_t') <+> "is not a subtype of"
-        <+> pquote (ppr decl_t') <> "."
+  te_t' <- normTypeFully te_t
 
-  pure (TypeDecl te' $ Info decl_t', e', ext)
+  pure (te', te_t', e', ext)
 
 unscopeType ::
   SrcLoc ->
@@ -368,14 +352,14 @@
   let res = AppRes (t `setAliases` mempty) (maybeToList retext)
 
   pure $ AppExp (Range start' maybe_step' end' loc) (Info res)
-checkExp (Ascript e decl loc) = do
-  (decl', e') <- checkAscript loc decl e
-  pure $ Ascript e' decl' loc
-checkExp (AppExp (Coerce e decl loc) _) = do
-  (decl', e', ext) <- checkCoerce loc decl e
+checkExp (Ascript e te loc) = do
+  (te', e') <- checkAscript loc te e
+  pure $ Ascript e' te' loc
+checkExp (AppExp (Coerce e te loc) _) = do
+  (te', te_t, e', ext) <- checkCoerce loc te e
   t <- expTypeFully e'
-  t' <- matchDims (const . const pure) t $ fromStruct $ unInfo $ expandedType decl'
-  pure $ AppExp (Coerce e' decl' loc) (Info $ AppRes t' ext)
+  t' <- matchDims (const . const pure) t $ fromStruct te_t
+  pure $ AppExp (Coerce e' te' loc) (Info $ AppRes t' ext)
 checkExp (AppExp (BinOp (op, oploc) NoInfo (e1, _) (e2, _) loc) NoInfo) = do
   (op', ftype) <- lookupVar oploc op
   e1_arg <- checkArg e1
@@ -545,8 +529,6 @@
 
     (elemt, _) <- sliceShape (Just (loc, Nonrigid)) slice' =<< normTypeFully t
 
-    unless (unique src_t) $ notConsumable loc $ pquote $ pprName $ identName src
-
     sequentially (unifies "type of target array" (toStruct elemt) =<< checkExp ve) $ \ve' _ -> do
       ve_t <- expTypeFully ve'
       when (AliasBound (identName src') `S.member` aliases ve_t) $
@@ -567,8 +549,6 @@
     sequentially (checkExp src >>= unifies "type of target array" t) $ \src' _ -> do
       src_t <- expTypeFully src'
 
-      unless (unique src_t) $ notConsumable loc $ pquote $ ppr src
-
       let src_als = aliases src_t
       ve_t <- expTypeFully ve'
       unless (S.null $ src_als `S.intersection` aliases ve_t) $ badLetWithValue src ve loc
@@ -624,37 +604,40 @@
   e1' <- require "being asserted" [Bool] =<< checkExp e1
   e2' <- checkExp e2
   pure $ Assert e1' e2' (Info (pretty e1)) loc
-checkExp (Lambda params body rettype_te NoInfo loc) =
-  removeSeminullOccurrences . noUnique . incLevel . bindingParams [] params $ \_ params' -> do
-    rettype_checked <- traverse checkTypeExpNonrigid rettype_te
-    let declared_rettype =
-          case rettype_checked of
-            Just (_, st, _) -> Just st
-            Nothing -> Nothing
-    (body', closure) <-
-      tapOccurrences $ checkFunBody params' body declared_rettype loc
-    body_t <- expTypeFully body'
+checkExp (Lambda params body rettype_te NoInfo loc) = do
+  (params', body', body_t, rettype', info) <-
+    removeSeminullOccurrences . noUnique . incLevel . bindingParams [] params $ \_ params' -> do
+      rettype_checked <- traverse checkTypeExpNonrigid rettype_te
+      let declared_rettype =
+            case rettype_checked of
+              Just (_, st, _) -> Just st
+              Nothing -> Nothing
+      (body', closure) <-
+        tapOccurrences $ checkFunBody params' body declared_rettype loc
+      body_t <- expTypeFully body'
 
-    params'' <- mapM updateTypes params'
+      params'' <- mapM updateTypes params'
 
-    (rettype', rettype_st) <-
-      case rettype_checked of
-        Just (te, st, ext) -> do
-          let st_structural = toStructural st
-          checkReturnAlias loc st_structural params'' body_t
-          pure (Just te, RetType ext st)
-        Nothing -> do
-          ret <-
-            inferReturnSizes params'' . toStruct $
-              inferReturnUniqueness params'' body_t
-          pure (Nothing, ret)
+      (rettype', rettype_st) <-
+        case rettype_checked of
+          Just (te, st, ext) -> do
+            let st_structural = toStructural st
+            checkReturnAlias loc st_structural params'' body_t
+            pure (Just te, RetType ext st)
+          Nothing -> do
+            ret <-
+              inferReturnSizes params'' . toStruct $
+                inferReturnUniqueness params'' body_t
+            pure (Nothing, ret)
 
-    checkGlobalAliases params' body_t loc
-    verifyFunctionParams Nothing params'
+      closure' <- lexicalClosure params'' closure
 
-    closure' <- lexicalClosure params'' closure
+      pure (params'', body', body_t, rettype', Info (closure', rettype_st))
 
-    pure $ Lambda params'' body' rettype' (Info (closure', rettype_st)) loc
+  checkGlobalAliases params' body_t loc
+  verifyFunctionParams Nothing params'
+
+  pure $ Lambda params' body' rettype' info loc
   where
     -- Inferring the sizes of the return type of a lambda is a lot
     -- like let-generalisation.  We wish to remove any rigid sizes
@@ -726,12 +709,14 @@
   a <- newTypeVar loc "a"
   let usage = mkUsage loc "projection at"
   b <- foldM (flip $ mustHaveField usage) a fields
-  pure $ ProjectSection fields (Info $ Scalar $ Arrow mempty Unnamed a $ RetType [] b) loc
+  let ft = Scalar $ Arrow mempty Unnamed (toStruct a) $ RetType [] b
+  pure $ ProjectSection fields (Info ft) loc
 checkExp (IndexSection slice NoInfo loc) = do
   slice' <- checkSlice slice
   (t, _) <- newArrayType loc "e" $ sliceDims slice'
   (t', retext) <- sliceShape Nothing slice' t
-  pure $ IndexSection slice' (Info $ fromStruct $ Scalar $ Arrow mempty Unnamed t $ RetType retext t') loc
+  let ft = Scalar $ Arrow mempty Unnamed t $ RetType retext $ fromStruct t'
+  pure $ IndexSection slice' (Info ft) loc
 checkExp (AppExp (DoLoop _ mergepat mergeexp form loopbody loc) _) = do
   ((sparams, mergepat', mergeexp', form', loopbody'), appres) <-
     checkDoLoop checkExp (mergepat, mergeexp, form, loopbody) loc
@@ -881,7 +866,7 @@
 
 -- | Extract all those names that are bound inside the type.
 boundInsideType :: TypeBase (DimDecl VName) as -> S.Set VName
-boundInsideType (Array _ _ t _) = boundInsideType (Scalar t)
+boundInsideType (Array _ _ _ t) = boundInsideType (Scalar t)
 boundInsideType (Scalar Prim {}) = mempty
 boundInsideType (Scalar (TypeVar _ _ _ targs)) = foldMap f targs
   where
@@ -911,13 +896,13 @@
   ApplyOp ->
   PatType ->
   Arg ->
-  TermTypeM (PatType, PatType, Maybe VName, [VName])
+  TermTypeM (StructType, PatType, Maybe VName, [VName])
 checkApply
   loc
   (fname, _)
   (Scalar (Arrow as pname tp1 tp2))
   (argexp, argtype, dflow, argloc) =
-    onFailure (CheckingApply fname argexp (toStruct tp1) (toStruct argtype)) $ do
+    onFailure (CheckingApply fname argexp tp1 (toStruct argtype)) $ do
       expect (mkUsage argloc "use as function argument") (toStruct tp1) (toStruct argtype)
 
       -- Perform substitutions of instantiated variables in the types.
@@ -951,8 +936,8 @@
 
       -- Unification ignores uniqueness in higher-order arguments, so
       -- we check for that here.
-      unless (toStructural argtype' `subtypeOf` toStructural tp1') $
-        typeError loc mempty "Uniqueness does not match."
+      unless (toStructural argtype' `subtypeOf` setUniqueness (toStructural tp1') Nonunique) $
+        typeError loc mempty "Consumption/aliasing does not match."
 
       (argext, parsubst) <-
         case pname of
@@ -1006,9 +991,9 @@
   PatType ->
   PatType
 returnType (Array _ Unique et shape) _ _ =
-  Array mempty Unique et shape
+  Array mempty Nonunique et shape -- Intentional!
 returnType (Array als Nonunique et shape) d arg =
-  Array (als <> arg_als) Unique et shape -- Intentional!
+  Array (als <> arg_als) Nonunique et shape
   where
     arg_als = aliases $ maskAliases arg d
 returnType (Scalar (Record fs)) d arg =
@@ -1016,9 +1001,9 @@
 returnType (Scalar (Prim t)) _ _ =
   Scalar $ Prim t
 returnType (Scalar (TypeVar _ Unique t targs)) _ _ =
-  Scalar $ TypeVar mempty Unique t targs
+  Scalar $ TypeVar mempty Nonunique t targs -- Intentional!
 returnType (Scalar (TypeVar als Nonunique t targs)) d arg =
-  Scalar $ TypeVar (als <> arg_als) Unique t targs -- Intentional!
+  Scalar $ TypeVar (als <> arg_als) Unique t targs
   where
     arg_als = aliases $ maskAliases arg d
 returnType (Scalar (Arrow old_als v t1 (RetType dims t2))) d arg =
@@ -1050,12 +1035,6 @@
   concat . M.elems <$> traverse (uncurry $ consumeArg loc) (M.intersectionWith (,) ets ds)
 consumeArg loc (Scalar (Sum ets)) (SumDiet ds) =
   concat <$> traverse (uncurry $ consumeArg loc) (concat $ M.elems $ M.intersectionWith zip ets ds)
-consumeArg loc (Array _ Nonunique _ _) Consume =
-  typeError loc mempty . withIndexLink "consuming-parameter" $
-    "Consuming parameter passed non-unique argument."
-consumeArg loc (Scalar (TypeVar _ Nonunique _ _)) Consume =
-  typeError loc mempty . withIndexLink "consuming-parameter" $
-    "Consuming parameter passed non-unique argument."
 consumeArg loc (Scalar (Arrow _ _ t1 _)) (FuncDiet d _)
   | not $ contravariantArg t1 d =
       typeError loc mempty . withIndexLink "consuming-argument" $
@@ -1350,17 +1329,15 @@
     hidden = param_all_names `S.difference` param_names
 
 inferredReturnType :: SrcLoc -> [Pat] -> PatType -> TermTypeM StructType
-inferredReturnType loc params t =
+inferredReturnType loc params t = do
   -- The inferred type may refer to names that are bound by the
   -- parameter patterns, but which will not be visible in the type.
   -- These we must turn into fresh type variables, which will be
   -- existential in the return type.
   fmap (toStruct . fst) $
-    unscopeType
-      loc
-      (M.filterWithKey (const . (`S.member` hidden)) $ foldMap patternMap params)
-      $ inferReturnUniqueness params t
+    unscopeType loc hidden_params $ inferReturnUniqueness params t
   where
+    hidden_params = M.filterWithKey (const . (`S.member` hidden)) $ foldMap patternMap params
     hidden = hiddenParamNames params
 
 checkReturnAlias :: SrcLoc -> TypeBase () () -> [Pat] -> PatType -> TermTypeM ()
@@ -1443,12 +1420,12 @@
 
     verifyFunctionParams (Just fname) params''
 
-    (tparams'', params''', rettype'') <-
+    (tparams'', params''', rettype') <-
       letGeneralise fname loc tparams' params'' rettype
 
     checkGlobalAliases params'' body_t loc
 
-    pure (tparams'', params''', maybe_retdecl'', rettype'', body')
+    pure (tparams'', params''', maybe_retdecl'', rettype', body')
 
 -- | Extract all the shape names that occur in positive position
 -- (roughly, left side of an arrow) in a given type.
@@ -1468,20 +1445,19 @@
 checkGlobalAliases :: [Pat] -> PatType -> SrcLoc -> TermTypeM ()
 checkGlobalAliases params body_t loc = do
   vtable <- asks $ scopeVtable . termScope
-  let isLocal v = case v `M.lookup` vtable of
-        Just (BoundV Local _ _) -> True
+  let isGlobal v = case v `M.lookup` vtable of
+        Just (BoundV Global _ _) -> True
         _ -> False
   let als =
-        filter (not . isLocal) . S.toList $
+        filter isGlobal . S.toList $
           boundArrayAliases body_t `S.difference` foldMap patNames params
-  case als of
-    v : _
-      | not $ null params ->
-          typeError loc mempty . withIndexLink "alias-free-variable" $
-            "Function result aliases the free variable "
-              <> pquote (pprName v)
-              <> "."
-              </> "Use" <+> pquote "copy" <+> "to break the aliasing."
+  unless (null params) $ case als of
+    v : _ ->
+      typeError loc mempty . withIndexLink "alias-free-variable" $
+        "Function result aliases the free variable "
+          <> pquote (pprName v)
+          <> "."
+          </> "Use" <+> pquote "copy" <+> "to break the aliasing."
     _ ->
       pure ()
 
@@ -1494,7 +1470,7 @@
       delve t'
         | all (`S.member` uniques) (boundArrayAliases t'),
           not $ any ((`S.member` forbidden) . aliasVar) (aliases t') =
-            t'
+            t' `setUniqueness` Unique
         | otherwise =
             t' `setUniqueness` Nonunique
    in delve t
@@ -1735,16 +1711,6 @@
       let usage = mkUsage (srclocOf body) "return type annotation"
       onFailure (CheckingReturn rettype (toStruct body_t')) $
         expect usage rettype $ toStruct body_t'
-
-      -- We also have to make sure that uniqueness matches.  This is done
-      -- explicitly, because uniqueness is ignored by unification.
-      rettype' <- normTypeFully rettype
-      body_t'' <- normTypeFully body_t' -- Substs may have changed.
-      unless (toStructural body_t'' `subtypeOf` toStructural rettype') $
-        typeError (srclocOf body) mempty $
-          "Body type" </> indent 2 (ppr body_t'')
-            </> "is not a subtype of annotated type"
-            </> indent 2 (ppr rettype')
     Nothing -> pure ()
 
   pure body'
@@ -1758,4 +1724,4 @@
   TermTypeM (TypeBase dim as)
 arrayOfM loc t shape u = do
   arrayElemType (mkUsage loc "use as array element") "type used in array" t
-  pure $ arrayOf t shape u
+  pure $ arrayOf u shape t
diff --git a/src/Language/Futhark/TypeChecker/Terms/DoLoop.hs b/src/Language/Futhark/TypeChecker/Terms/DoLoop.hs
--- a/src/Language/Futhark/TypeChecker/Terms/DoLoop.hs
+++ b/src/Language/Futhark/TypeChecker/Terms/DoLoop.hs
@@ -101,10 +101,6 @@
   let -- Make the pattern unique where needed.
       pat' = uniquePat (patNames pat `S.intersection` body_cons) pat
 
-  pat_t <- normTypeFully $ patternType pat'
-  unless (toStructural body_t `subtypeOf` toStructural pat_t) $
-    unexpectedType (srclocOf body_loc) (toStruct body_t) [toStruct pat_t]
-
   -- Check that the new values of consumed merge parameters do not
   -- alias something bound outside the loop, AND that anything
   -- returned for a unique merge parameter does not alias anything
@@ -124,7 +120,7 @@
               "Return value for loop parameter"
                 <+> pquote (pprName pat_v)
                 <+> "aliases"
-                <+> pprName v <> "."
+                <+> pquote (pprName v) <> "."
         | otherwise = do
             (cons, obs) <- get
             unless (S.null $ aliases t `S.intersection` cons) $
diff --git a/src/Language/Futhark/TypeChecker/Terms/Monad.hs b/src/Language/Futhark/TypeChecker/Terms/Monad.hs
--- a/src/Language/Futhark/TypeChecker/Terms/Monad.hs
+++ b/src/Language/Futhark/TypeChecker/Terms/Monad.hs
@@ -77,7 +77,6 @@
     useAfterConsume,
     unusedSize,
     notConsumable,
-    unexpectedType,
     uniqueReturnAliased,
     returnAliased,
     badLetWithValue,
@@ -210,9 +209,15 @@
     cons1 = allConsumed occurs1
     cons2 = allConsumed occurs2
 
--- | Whether something is a global or a local variable.
-data Locality = Local | Global
-  deriving (Show)
+-- | How something was bound.
+data Locality
+  = -- | In the current function
+    Local
+  | -- | In an enclosing function, but not the current one.
+    Nonlocal
+  | -- | At global scope.
+    Global
+  deriving (Show, Eq, Ord)
 
 data ValBinding
   = -- | Aliases in parameters indicate the lexical
@@ -259,17 +264,6 @@
   typeError loc mempty . withIndexLink "unique-return-aliased" $
     "A unique-typed component of the return value is aliased to some other component."
 
-unexpectedType :: MonadTypeChecker m => SrcLoc -> StructType -> [StructType] -> m a
-unexpectedType loc _ [] =
-  typeError loc mempty $
-    "Type of expression at" <+> text (locStr loc)
-      <+> "cannot have any type - possibly a bug in the type checker."
-unexpectedType loc t ts =
-  typeError loc mempty $
-    "Type of expression at" <+> text (locStr loc) <+> "must be one of"
-      <+> commasep (map ppr ts) <> ", but is"
-      <+> ppr t <> "."
-
 notConsumable :: MonadTypeChecker m => SrcLoc -> Doc -> m b
 notConsumable loc v =
   typeError loc mempty . withIndexLink "not-consumable" $
@@ -392,9 +386,12 @@
   where
     vtable = M.mapWithKey valBinding $ envVtable env
     valBinding k (TypeM.BoundV tps v) =
-      BoundV Global tps $
-        v
-          `setAliases` (if arrayRank v > 0 then S.singleton (AliasBound k) else mempty)
+      BoundV Global tps $ selfAliasing (S.singleton (AliasBound k)) v
+    -- FIXME: hack, #1675
+    selfAliasing als (Scalar (Record ts)) =
+      Scalar $ Record $ M.map (selfAliasing als) ts
+    selfAliasing als t =
+      t `setAliases` (if arrayRank t > 0 then als else mempty)
 
 withEnv :: TermEnv -> Env -> TermEnv
 withEnv tenv env = tenv {termScope = termScope tenv <> envToTermScope env}
@@ -744,7 +741,7 @@
   dims <- replicateM r $ newDimVar loc Nonrigid "dim"
   let rowt = TypeVar () Nonunique (typeName v) []
   pure
-    ( Array () Nonunique rowt (ShapeDecl $ map (NamedDim . qualName) dims),
+    ( Array () Nonunique (ShapeDecl $ map (NamedDim . qualName) dims) rowt,
       Scalar rowt
     )
 
@@ -933,7 +930,7 @@
   where
     f scope = scope {scopeVtable = M.map set $ scopeVtable scope}
 
-    set (BoundV l tparams t) = BoundV l tparams $ t `setUniqueness` Nonunique
+    set (BoundV l tparams t) = BoundV (max l Nonlocal) tparams t
     set (OverloadedF ts pts rt) = OverloadedF ts pts rt
     set EqualityF = EqualityF
     set (WasConsumed loc) = WasConsumed loc
@@ -951,11 +948,9 @@
   vtable <- asks $ scopeVtable . termScope
   let consumable v = case M.lookup v vtable of
         Just (BoundV Local _ t)
-          | arrayRank t > 0 -> unique t
-          | Scalar TypeVar {} <- t -> unique t
           | Scalar Arrow {} <- t -> False
           | otherwise -> True
-        Just (BoundV Global _ _) -> False
+        Just (BoundV l _ _) -> l == Local
         _ -> True
   -- The sort ensures that AliasBound vars are shown before AliasFree.
   case map aliasVar $ sort $ filter (not . consumable . aliasVar) $ S.toList als of
diff --git a/src/Language/Futhark/TypeChecker/Terms/Pat.hs b/src/Language/Futhark/TypeChecker/Terms/Pat.hs
--- a/src/Language/Futhark/TypeChecker/Terms/Pat.hs
+++ b/src/Language/Futhark/TypeChecker/Terms/Pat.hs
@@ -58,29 +58,44 @@
     bound AliasBound {} = True
     bound AliasFree {} = False
 
-checkIfUsed :: Occurrences -> Ident -> TermTypeM ()
-checkIfUsed occs v
+checkIfUsed :: Bool -> Occurrences -> Ident -> TermTypeM ()
+checkIfUsed allow_consume occs v
+  | not allow_consume,
+    not $ unique $ unInfo $ identType v,
+    Just occ <- find consumes occs =
+      typeError (srclocOf occ) mempty $
+        "Consuming"
+          <+> pquote (pprName $ identName v)
+          <+> textwrap ("which is a non-consumable parameter bound at " <> locStr (locOf v) <> ".")
   | not $ identName v `S.member` allOccurring occs,
     not $ "_" `isPrefixOf` prettyName (identName v) =
-      warn (srclocOf v) $ "Unused variable" <+> pquote (pprName $ identName v) <+> "."
+      warn (srclocOf v) $
+        "Unused variable" <+> pquote (pprName $ identName v) <+> "."
   | otherwise =
       pure ()
+  where
+    consumes = maybe False (identName v `S.member`) . consumed
 
 -- | Bind these identifiers locally while running the provided action.
 -- Checks that the identifiers are used properly within the scope
 -- (e.g. consumption).
-binding :: [Ident] -> TermTypeM a -> TermTypeM a
-binding stms = check . handleVars
+binding ::
+  -- | Allow consumption, even if the type is not unique.
+  Bool ->
+  [Ident] ->
+  TermTypeM a ->
+  TermTypeM a
+binding allow_consume idents = check . handleVars
   where
     handleVars m =
-      localScope (`bindVars` stms) $ do
+      localScope (`bindVars` idents) $ do
         -- Those identifiers that can potentially also be sizes are
         -- added as type constraints.  This is necessary so that we
         -- can properly detect scope violations during unification.
         -- We do this for *all* identifiers, not just those that are
         -- integers, because they may become integers later due to
         -- inference...
-        forM_ stms $ \ident ->
+        forM_ idents $ \ident ->
           constrain (identName ident) $ ParamSize $ srclocOf ident
         m
 
@@ -91,9 +106,6 @@
     bindVar scope (Ident name (Info tp) _) =
       let inedges = boundAliases $ aliases tp
           update (BoundV l tparams in_t)
-            -- If 'name' is record or sum-typed, don't alias the
-            -- components to 'name', because these no identity
-            -- beyond their components.
             | Array {} <- tp = BoundV l tparams (in_t `addAliases` S.insert (AliasBound name))
             | otherwise = BoundV l tparams in_t
           update b = b
@@ -114,11 +126,11 @@
       (a, usages) <- collectBindingsOccurrences m
       checkOccurrences usages
 
-      mapM_ (checkIfUsed usages) stms
+      mapM_ (checkIfUsed allow_consume usages) idents
 
       pure a
 
-    -- Collect and remove all occurences in @stms@.  This relies
+    -- Collect and remove all occurences of @idents@.  This relies
     -- on the fact that no variables shadow any other.
     collectBindingsOccurrences m = do
       (x, usage) <- collectOccurrences m
@@ -126,19 +138,16 @@
       occur rest
       pure (x, relevant)
       where
-        split =
-          unzip
-            . map
-              ( \occ ->
-                  let (obs1, obs2) = divide $ observed occ
-                      occ_cons = divide <$> consumed occ
-                      con1 = fst <$> occ_cons
-                      con2 = snd <$> occ_cons
-                   in ( occ {observed = obs1, consumed = con1},
-                        occ {observed = obs2, consumed = con2}
-                      )
+        onOcc occ =
+          let (obs1, obs2) = divide $ observed occ
+              occ_cons = divide <$> consumed occ
+              con1 = fst <$> occ_cons
+              con2 = snd <$> occ_cons
+           in ( occ {observed = obs1, consumed = con1},
+                occ {observed = obs2, consumed = con2}
               )
-        names = S.fromList $ map identName stms
+        split = unzip . map onOcc
+        names = S.fromList $ map identName idents
         divide s = (s `S.intersection` names, s `S.difference` names)
 
 bindingTypes ::
@@ -158,7 +167,7 @@
 
 bindingTypeParams :: [TypeParam] -> TermTypeM a -> TermTypeM a
 bindingTypeParams tparams =
-  binding (mapMaybe typeParamIdent tparams)
+  binding False (mapMaybe typeParamIdent tparams)
     . bindingTypes (concatMap typeParamType tparams)
   where
     typeParamType (TypeParamType l v loc) =
@@ -183,7 +192,7 @@
   bindSpaced [(Term, v)] $ do
     v' <- checkName Term v vloc
     let ident = Ident v' (Info t) vloc
-    binding [ident] $ m ident
+    binding True [ident] $ m ident
 
 -- | Bind @let@-bound sizes.  This is usually followed by 'bindingPat'
 -- immediately afterwards.
@@ -193,7 +202,7 @@
   foldM_ lookForDuplicates mempty sizes
   bindSpaced (map sizeWithSpace sizes) $ do
     sizes' <- mapM check sizes
-    binding (map sizeWithType sizes') $ m sizes'
+    binding False (map sizeWithType sizes') $ m sizes'
   where
     lookForDuplicates prev size
       | Just prevloc <- M.lookup (sizeName size) prev =
@@ -212,17 +221,6 @@
     check (SizeBinder v loc) =
       SizeBinder <$> checkName Term v loc <*> pure loc
 
-patternDims :: Pat -> [Ident]
-patternDims (PatParens p _) = patternDims p
-patternDims (TuplePat pats _) = concatMap patternDims pats
-patternDims (PatAscription p (TypeDecl _ (Info t)) _) =
-  patternDims p <> mapMaybe (dimIdent (srclocOf p)) (nestedDims t)
-  where
-    dimIdent _ (AnyDim _) = error "patternDims: AnyDim"
-    dimIdent _ (ConstDim _) = Nothing
-    dimIdent _ NamedDim {} = Nothing
-patternDims _ = []
-
 sizeBinderToParam :: SizeBinder VName -> UncheckedTypeParam
 sizeBinderToParam (SizeBinder v loc) = TypeParamDim (baseName v) loc
 
@@ -235,10 +233,12 @@
   TermTypeM a
 bindingPat sizes p t m = do
   checkForDuplicateNames (map sizeBinderToParam sizes) [p]
-  checkPat sizes p t $ \p' -> binding (S.toList $ patIdents p') $ do
+  checkPat sizes p t $ \p' -> binding True (S.toList $ patIdents p') $ do
     -- Perform an observation of every declared dimension.  This
     -- prevents unused-name warnings for otherwise unused dimensions.
-    mapM_ observe $ patternDims p'
+    let ident (SizeBinder v loc) =
+          Ident v (Info (Scalar $ Prim $ Signed Int64)) loc
+    mapM_ (observe . ident) sizes
 
     let used_sizes = typeDimNames $ patternStructType p'
     case filter ((`S.notMember` used_sizes) . sizeName) sizes of
@@ -323,34 +323,23 @@
   RecordPat . M.toList
     <$> traverse (\p -> checkPat' sizes p NoneInferred) (M.fromList fs)
     <*> pure loc
-checkPat' sizes (PatAscription p (TypeDecl t NoInfo) loc) maybe_outer_t = do
+checkPat' sizes (PatAscription p t loc) maybe_outer_t = do
   (t', st, _) <- checkTypeExpNonrigid t
 
-  let st' = fromStruct st
   case maybe_outer_t of
     Ascribed outer_t -> do
       st_forunify <- nonrigidFor sizes st
       unify (mkUsage loc "explicit type ascription") st_forunify (toStruct outer_t)
 
-      -- We also have to make sure that uniqueness matches.  This is
-      -- done explicitly, because it is ignored by unification.
-      st'' <- normTypeFully st'
       outer_t' <- normTypeFully outer_t
-      case unifyTypesU unifyUniqueness st'' outer_t' of
-        Just outer_t'' ->
-          PatAscription <$> checkPat' sizes p (Ascribed outer_t'')
-            <*> pure (TypeDecl t' (Info st))
-            <*> pure loc
-        Nothing ->
-          typeError loc mempty $
-            "Cannot match type" <+> pquote (ppr outer_t') <+> "with expected type"
-              <+> pquote (ppr st'') <> "."
+      PatAscription
+        <$> checkPat' sizes p (Ascribed (addAliasesFromType st outer_t'))
+        <*> pure t'
+        <*> pure loc
     NoneInferred ->
-      PatAscription <$> checkPat' sizes p (Ascribed st')
-        <*> pure (TypeDecl t' (Info st))
+      PatAscription <$> checkPat' sizes p (Ascribed (fromStruct st))
+        <*> pure t'
         <*> pure loc
-  where
-    unifyUniqueness u1 u2 = if u2 `subuniqueOf` u1 then Just u1 else Nothing
 checkPat' _ (PatLit l NoInfo loc) (Ascribed t) = do
   t' <- patLitMkType l loc
   unify (mkUsage loc "matching against literal") t' (toStruct t)
@@ -415,7 +404,7 @@
   checkTypeParams tps $ \tps' -> bindingTypeParams tps' $ do
     let descend ps' (p : ps) =
           checkPat [] p NoneInferred $ \p' ->
-            binding (S.toList $ patIdents p') $ descend (p' : ps') ps
+            binding False (S.toList $ patIdents p') $ descend (p' : ps') ps
         descend ps' [] = do
           -- Perform an observation of every type parameter.  This
           -- prevents unused-name warnings for otherwise unused
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,9 +8,9 @@
 module Language.Futhark.TypeChecker.Types
   ( checkTypeExp,
     renameRetType,
-    unifyTypesU,
     subtypeOf,
     subuniqueOf,
+    addAliasesFromType,
     checkForDuplicateNames,
     checkTypeParams,
     typeParamToArg,
@@ -36,6 +36,31 @@
 import Language.Futhark.Traversals
 import Language.Futhark.TypeChecker.Monad
 
+addAliasesFromType :: StructType -> PatType -> PatType
+addAliasesFromType (Array _ u1 et1 shape1) (Array als _ _ _) =
+  Array als u1 et1 shape1
+addAliasesFromType
+  (Scalar (TypeVar _ u1 tv1 targs1))
+  (Scalar (TypeVar als2 _ _ _)) =
+    Scalar $ TypeVar als2 u1 tv1 targs1
+addAliasesFromType (Scalar (Record ts1)) (Scalar (Record ts2))
+  | length ts1 == length ts2,
+    sort (M.keys ts1) == sort (M.keys ts2) =
+      Scalar $ Record $ M.intersectionWith addAliasesFromType ts1 ts2
+addAliasesFromType
+  (Scalar (Arrow _ mn1 pt1 (RetType dims1 rt1)))
+  (Scalar (Arrow as2 _ _ (RetType _ rt2))) =
+    Scalar (Arrow as2 mn1 pt1 (RetType dims1 rt1'))
+    where
+      rt1' = addAliasesFromType rt1 rt2
+addAliasesFromType (Scalar (Sum cs1)) (Scalar (Sum cs2))
+  | length cs1 == length cs2,
+    sort (M.keys cs1) == sort (M.keys cs2) =
+      Scalar $ Sum $ M.intersectionWith (zipWith addAliasesFromType) cs1 cs2
+addAliasesFromType (Scalar (Prim t)) _ = Scalar $ Prim t
+addAliasesFromType t1 t2 =
+  error $ "addAliasesFromType invalid args: " ++ show (t1, t2)
+
 -- | @unifyTypes uf t1 t2@ attempts to unify @t1@ and @t2@.  If
 -- unification cannot happen, 'Nothing' is returned, otherwise a type
 -- that combines the aliasing of @t1@ and @t2@ is returned.
@@ -47,10 +72,10 @@
   TypeBase dim als ->
   TypeBase dim als ->
   Maybe (TypeBase dim als)
-unifyTypesU uf (Array als1 u1 et1 shape1) (Array als2 u2 et2 _shape2) =
+unifyTypesU uf (Array als1 u1 shape1 et1) (Array als2 u2 _shape2 et2) =
   Array (als1 <> als2) <$> uf u1 u2
-    <*> unifyScalarTypes uf et1 et2
     <*> pure shape1
+    <*> unifyScalarTypes uf et1 et2
 unifyTypesU uf (Scalar t1) (Scalar t2) = Scalar <$> unifyScalarTypes uf t1 t2
 unifyTypesU _ _ _ = Nothing
 
@@ -164,13 +189,13 @@
       foldl' max Unlifted ls
     )
 --
-evalTypeExp (TEArray t d loc) = do
+evalTypeExp (TEArray d t loc) = do
   (d_svars, d', d'') <- checkDimExp d
   (t', svars, RetType dims st, l) <- evalTypeExp t
-  case (l, arrayOf st (ShapeDecl [d'']) Nonunique) of
+  case (l, arrayOf Nonunique (ShapeDecl [d'']) st) of
     (Unlifted, st') ->
       pure
-        ( TEArray t' d' loc,
+        ( TEArray d' t' loc,
           svars,
           RetType (d_svars ++ dims) st',
           Unlifted
@@ -552,7 +577,6 @@
       error $ "applyType mkSubst: cannot substitute " ++ pretty a ++ " for " ++ pretty p
 
 substTypesRet ::
-  forall as.
   Monoid as =>
   (VName -> Maybe (Subst (RetTypeBase (DimDecl VName) as))) ->
   TypeBase (DimDecl VName) as ->
@@ -581,13 +605,14 @@
               RetType [] t' = substTypesRet (`M.lookup` extsubsts) t
           pure $ RetType ext' t'
 
-    onType :: TypeBase (DimDecl VName) as -> State [VName] (TypeBase (DimDecl VName) as)
+    onType ::
+      forall as.
+      Monoid as =>
+      TypeBase (DimDecl VName) as ->
+      State [VName] (TypeBase (DimDecl VName) as)
 
-    onType (Array als u et shape) = do
-      t <-
-        arrayOf <$> onType (Scalar et `setAliases` mempty)
-          <*> pure (applySubst lookupSubst' shape)
-          <*> pure u
+    onType (Array als u shape et) = do
+      t <- arrayOf u (applySubst lookupSubst' shape) <$> onType (Scalar et)
       pure $ t `setAliases` als
     onType (Scalar (Prim t)) = pure $ Scalar $ Prim t
     onType (Scalar (TypeVar als u v targs)) = do
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
@@ -1044,33 +1044,33 @@
 mustHaveFieldWith onDims usage bound bcs l t = do
   constraints <- getConstraints
   l_type <- newTypeVar (srclocOf usage) "t"
-  let l_type' = toStruct l_type
+  let l_type' = l_type `setAliases` aliases t
   case t of
     Scalar (TypeVar _ _ (TypeName _ tn) [])
       | Just (lvl, NoConstraint {}) <- M.lookup tn constraints -> do
-          scopeCheck usage bcs tn lvl l_type'
-          modifyConstraints $ M.insert tn (lvl, HasFields (M.singleton l l_type') usage)
-          pure l_type
+          scopeCheck usage bcs tn lvl l_type
+          modifyConstraints $ M.insert tn (lvl, HasFields (M.singleton l l_type) usage)
+          pure l_type'
       | Just (lvl, HasFields fields _) <- M.lookup tn constraints -> do
           case M.lookup l fields of
-            Just t' -> unifyWith onDims usage bound bcs l_type' t'
+            Just t' -> unifyWith onDims usage bound bcs l_type t'
             Nothing ->
               modifyConstraints $
                 M.insert
                   tn
-                  (lvl, HasFields (M.insert l l_type' fields) usage)
-          pure l_type
+                  (lvl, HasFields (M.insert l l_type fields) usage)
+          pure l_type'
     Scalar (Record fields)
       | Just t' <- M.lookup l fields -> do
-          unify usage l_type' $ toStruct t'
+          unify usage l_type $ toStruct t'
           pure t'
       | otherwise ->
           unifyError usage mempty bcs $
             "Attempt to access field" <+> pquote (ppr l) <+> " of value of type"
               <+> ppr (toStructural t) <> "."
     _ -> do
-      unify usage (toStruct t) $ Scalar $ Record $ M.singleton l l_type'
-      pure l_type
+      unify usage (toStruct t) $ Scalar $ Record $ M.singleton l l_type
+      pure l_type'
 
 -- | Assert that some type must have a field with this name and type.
 mustHaveField ::
diff --git a/src/Language/Futhark/Warnings.hs b/src/Language/Futhark/Warnings.hs
--- a/src/Language/Futhark/Warnings.hs
+++ b/src/Language/Futhark/Warnings.hs
@@ -12,7 +12,7 @@
 
 import Data.List (sortOn)
 import Data.Monoid
-import Futhark.Util.Console (inRed)
+import Futhark.Util.Console (inYellow)
 import Futhark.Util.Loc
 import Futhark.Util.Pretty
 import Language.Futhark.Core (locStr, prettyStacktrace)
@@ -37,11 +37,11 @@
       rep NoLoc = ("", 0)
       rep (Loc p _) = (posFile p, posCoff p)
       onWarning (loc, [], w) =
-        text (inRed ("Warning at " ++ locStr loc ++ ":"))
+        text (inYellow ("Warning at " ++ locStr loc ++ ":"))
           </> indent 2 w
       onWarning (loc, locs, w) =
         text
-          ( inRed
+          ( inYellow
               ( "Warning at\n"
                   ++ prettyStacktrace 0 (map locStr (loc : locs))
               )
diff --git a/unittests/Language/Futhark/SyntaxTests.hs b/unittests/Language/Futhark/SyntaxTests.hs
--- a/unittests/Language/Futhark/SyntaxTests.hs
+++ b/unittests/Language/Futhark/SyntaxTests.hs
@@ -145,13 +145,8 @@
         ]
 
 pArrayType :: Parser StructType
-pArrayType = do
-  u <- pUniqueness
-  shape <- pShape
-  t <- pScalarNonFun
-  pure $ Array () u t shape
-  where
-    pShape = ShapeDecl <$> some pDimDecl
+pArrayType =
+  Array () <$> pUniqueness <*> (ShapeDecl <$> some pDimDecl) <*> pScalarNonFun
 
 pNonFunType :: Parser StructType
 pNonFunType =