diff --git a/docs/glossary.rst b/docs/glossary.rst
--- a/docs/glossary.rst
+++ b/docs/glossary.rst
@@ -9,6 +9,11 @@
 .. glossary::
    :sorted:
 
+   Abstract type
+
+     A type whose definition has been hidden through a :term:`module
+     ascription`.
+
    Aliases
 
      The *aliases* of a variable is a set of those other variables
@@ -91,6 +96,22 @@
      Futhark. `See also Wikipedia
      <https://en.wikipedia.org/wiki/Data_parallelism>`_.
 
+   Defunctionalisation
+
+     A program transformation always performed by the Futhark compiler,
+     that replaces function values with non-function values.  The goal
+     is to avoid having indirect calls through function pointers at
+     run-time.  To permit zero-overhead defunctionalisation, the
+     Futhark type rules impose restrictions on :term:`lifted types
+     <lifted type>`.
+
+   Defunctorisation
+
+     A program transformation always performed by the Futhark
+     compiler, that compiles away modules using an approach similar to
+     :term:`defunctionalisation`.  This makes using e.g. a
+     :term:`parametric module` completely free at run-time.
+
    Elaboration
 
      The process conducted out by the type checker, where it infers
@@ -118,6 +139,13 @@
      more restrictions than some other backends, particularly with
      respect to :term:`irregular nested data parallelism`.
 
+   Higher-ranked type
+
+     A type that does not describe :term:`values <value>`.  Can be
+     seen as a partially applied :term:`type constructor`.  Not
+     directly supported by Futhark, but a similar effect can be
+     achieved through the :ref:`module-system`.
+
    In-place updates
 
      A somewhat misleading term for the syntactic forms ``x with [i] =
@@ -125,6 +153,10 @@
      updates, but can be operationally understood as thus.  See
      :ref:`in-place-updates`.
 
+   Invariant
+
+     Not :term:`variant`.
+
    Irregular
 
      Something that is not regular.  Usually used as shorthand for
@@ -140,9 +172,9 @@
    Irregular nested data parallelism
 
      An instance of :term:`nested data parallelism`, where the
-     :term:`parallel width` of inner parallelism is term:`variant` to
-     the outer parallelism.  For example, the expression following
-     expression exhibits irregular nested data parallelism::
+     :term:`parallel width` of inner parallelism is :term:`variant` to
+     the outer parallelism.  For example, the following expression
+     exhibits irregular nested data parallelism::
 
        map (\n -> reduce (+) 0 (iota n)) ns
 
@@ -177,16 +209,64 @@
      A function from :term:`modules<module>` to modules.  The most
      powerful form of abstraction provided by Futhark.
 
+   Polymorphic
+
+     Usually means a :term:`polymorphic function`, but sometimes a
+     :term:`parametric modules <parametric module>`.  Should not be
+     used to describe a :term:`type constructor <type constructor>`.
+
+   Polymorphism
+
+     The concept of being :term:`polymorphic`.
+
+   Polymorphic function
+
+     A function with :term:`type parameters <type parameter>`, such
+     that the function can be applied to arguments of various types.
+     Compiled using :term:`monomorphisation`.
+
    Lifted type
 
-     A type that may contain functions.  These have various
-     restrictions on their use.  See :ref:`hofs`.
+     A type that may contain functions, including function types
+     themselves.  These have various restrictions on their use in
+     order to support :term:`defunctionalisation`.  See :ref:`hofs`.
 
    Module
 
      A mapping from names to definitions of types, values, or nested
      modules.  See :ref:`module-system`.
 
+   Module ascription
+
+     A feature of the module system through which the contents of a
+     module can be hidden.  Written as ``m : mt`` where ``m`` is a
+     :term:`module expression` and ``mt`` is a :term:`module type
+     expression`.  See :ref:`module-system`.
+
+   Module expression
+
+     An expression that is evaluated at compile time, through
+     :term:`defunctorisation` to a :term:`module`.  Most commonly just
+     the name of a module.
+
+   Module type
+
+     A description of the interface of a :term:`module`.  Most commonly
+     used to hide contents in a :term:`module ascription` or to
+     require implementation of an interface in a :term:`parametric
+     module`.
+
+   Module type expression
+
+     An expression that is evaluated during type-checking to a
+     :term:`module type`.
+
+   Monomorphisation
+
+     A program transformation that instantiates a copy of each
+     :term:`polymorphic` functions for each type it is used with.
+     Performed by the Futhark compiler.
+
    Nested data parallelism
 
      Nested :term:`data parallelism` occurs when a parallel construct
@@ -202,11 +282,20 @@
      fully exploit the parallelism of the program, although
      :term:`nested data parallelism` muddles the picture.
 
+   Recursion
+
+     A function that calls itself.  Currently not supported in
+     Futhark.
+
    Regular nested data parallelism
 
      An instance of :term:`nested data parallelism` that is not
      :term:`irregular`.  Fully supports by any :term:`GPU backend`.
 
+   Size
+
+     The symbolic size of an array dimension or :term:`abstract type`.
+
    Size types
    Size-dependent types
 
@@ -219,6 +308,21 @@
      array elements, as that might potentially result in an
      :term:`irregular array`.  See :ref:`typeabbrevs`.
 
+   Size argument
+
+     An argument to a :term:`type constructor` in a :term:`type
+     expression` of the form ``[n]`` or ``[]``.  The latter is called
+     an :term:`anonymous size`.  Must match a corresponding
+     :term:`size parameter`.
+
+   Size parameter
+
+     A parameter of a :term:`polymorphic function` or :term:`type
+     constructor` that ranges over :term:`sizes <size>`.  These are
+     written as `[n]` for some `n`, after which `n` is in scope as a
+     term of type ``i64`` within the rest of the definition.  Do not
+     confuse them with :term:`type parameters <type parameter>`.
+
    SOAC
    Second Order Array Combinator
 
@@ -227,6 +331,48 @@
      on.  They are *second order* because they accept a functional
      argument, and so permit :term:`nested data parallelism`.
 
+   Type
+
+     A classification of values.  ``i32`` and ``[10]i32`` are examples
+     of types.
+
+   Type abbreviation
+
+     A shorthand for a longer type, e.g. ``type t = [100]i32``.  Can
+     accept :term:`type parameters <type parameter>` and :term:`size
+     parameters <type parameter>`.  The definition is visible to
+     users, unless hidden with a :term:`module ascription`.  See
+     :ref:`typeabbrevs`.
+
+   Type argument
+
+     An argument to a :term:`type constructor` that is itself a
+     :term:`type`.  Must match a corresponding :term:`type parameter`.
+
+   Type constructor
+
+     A :term:`type abbreviation` or :term:`abstract type` that has at
+     least one :term:`type parameter` or :term:`size parameter`.
+     Futhark does not support :term:`higher-ranked types
+     <higher-ranked type>`, so when referencing a type constructor in
+     a :term:`type expression`, you must provide corresponding
+     :term:`type arguments <type argument>` and :term:`size arguments
+     <size argument>` in an appopriate order.
+
+   Type expression
+
+     A syntactic construct that is evaluated to a :term:`type` in the
+     type checker, but may contain uses of :term:`type abbreviations
+     <type abbreviation>` and :term:`anonymous sizes <anonymous size>`.
+
+   Type parameter
+
+     A parameter of a :term:`polymorphic function` or :term:`type
+     constructor` that ranges over types.  These are written as `'t`
+     for some `t`, after which `t` is in scope as a type within the
+     rest of the definition.  Do not confuse them with :term:`size
+     parameters <size parameter>`.
+
    Uniqueness types
 
      A somewhat misleading term that describes Futhark's system of
@@ -240,3 +386,19 @@
 
      A size produced by invoking a function whose result type contains
      an existentially quantified size, such as ``filter``.
+
+   Value
+
+     An object such as the integer ``123`` or the array ``[1,2,3]``.
+     Expressions variables are bound to values and all valid
+     expressions have a :term:`type` describing the form of values
+     they can return.
+
+   Variant
+
+     When some value ``v`` computed inside a loop takes a different
+     value for each iteration inside the loop, we say that ``v`` is
+     *variant* to the loop (and otherwise :term:`invariant`).  Often
+     used to talk about :term:`irregularity <irregular>`.  When
+     something is nested inside multiple loops, it may be variant to
+     just one of them.
diff --git a/docs/versus-other-languages.rst b/docs/versus-other-languages.rst
--- a/docs/versus-other-languages.rst
+++ b/docs/versus-other-languages.rst
@@ -43,7 +43,7 @@
 
 Identifiers are case-sensitive, and there is no restriction on the
 case of the first letter (unlike Haskell and OCaml, but like Standard
-ML).
+ML and Flix).
 
 User-defined operators are possible, but the fixity of the operator
 depends on its name.  Specifically, the fixity of a user-defined
@@ -52,14 +52,14 @@
 same fixity as ``<<``, and ``=<<`` the same as ``=``.  This rule is the
 same as the rule found in OCaml and F#.
 
-Top-level functions and values are defined with ``def``.  Local
-variables are bound with ``let``.
+Top-level functions and values are defined with ``def`` as in Flix.
+Local variables are bound with ``let``.
 
 Evaluation
 ----------
 
-Futhark is a completely pure language, with no cheating through monads
-or anything of the sort.
+Futhark is a completely pure language, with no cheating through
+monads, effect systems, or anything of the sort.
 
 Evaluation is *eager* or *call-by-value*, like most non-Haskell
 languages.  However, there is no defined evaluation order.
@@ -72,15 +72,15 @@
 
 The evaluation semantics are entirely sequential, with parallelism
 being solely an operational detail.  Hence, race conditions are
-impossible. The Futhark compiler does not automatically go
-looking for parallelism.  Only certain special constructs and built-in
-library functions (in particular ``map``, ``reduce``, ``scan``, and
-``filter``) may be executed in parallel.
+impossible. The Futhark compiler does not automatically go looking for
+parallelism.  Only certain special constructs and built-in library
+functions (such as ``map``, ``reduce``, ``scan``, and ``filter``) may
+be executed in parallel.
 
-Currying and partial application work as usual (although functions
-are not fully first class; see `Types`_).  Some Futhark language
-constructs look like functions, but are not.  This means they cannot
-be partially applied.  These ``assert``.
+Currying and partial application work as usual (although functions are
+not fully first class; see `Types`_).  Although the ``assert``
+construct looks like a function, it is not, and it cannot be partially
+applied.
 
 Lambda terms are written as ``\x -> x + 2``, as in Haskell.
 
@@ -109,9 +109,10 @@
 ``a[i,j]``.  Arrays are 0-indexed.
 
 All types can be combined in tuples as usual, as well as in
-*structurally typed records*, as in Standard ML.  Non-recursive sum
-types are supported, and are also structurally typed.  Abstract types
-are possible via the module system; see :ref:`module-system`.
+*structurally typed records*, as in Standard ML and Flix.
+Non-recursive sum types are supported, and are also structurally
+typed.  Abstract types are possible via the module system; see
+:ref:`module-system`.
 
 If a variable ``foo`` is a record of type ``{a: i32, b: bool}``, then
 we access field ``a`` with dot notation: ``foo.a``.  Tuples are a
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.24.2
+version:        0.24.3
 synopsis:       An optimising compiler for a functional, array-oriented language.
 
 description:    Futhark is a small programming language designed to be compiled to
diff --git a/src/Futhark/CLI/Autotune.hs b/src/Futhark/CLI/Autotune.hs
--- a/src/Futhark/CLI/Autotune.hs
+++ b/src/Futhark/CLI/Autotune.hs
@@ -471,6 +471,9 @@
 
   T.putStrLn $ "Result of autotuning:\n" <> tuning
 
+supportedBackends :: [String]
+supportedBackends = ["opencl", "cuda"]
+
 commandLineOptions :: [FunOptDescr AutotuneOptions]
 commandLineOptions =
   [ Option
@@ -480,12 +483,9 @@
           ( \n ->
               case reads n of
                 [(n', "")] | n' >= 0 ->
-                  Right $ \config ->
-                    config
-                      { optMinRuns = n'
-                      }
+                  Right $ \config -> config {optMinRuns = n'}
                 _ ->
-                  Left $ error $ "'" ++ n ++ "' is not a non-negative integer."
+                  Left $ optionsError $ "'" ++ n ++ "' is not a non-negative integer."
           )
           "RUNS"
       )
@@ -494,10 +494,14 @@
       []
       ["backend"]
       ( ReqArg
-          (\backend -> Right $ \config -> config {optBackend = backend})
+          ( \backend ->
+              if backend `elem` supportedBackends
+                then Right $ \config -> config {optBackend = backend}
+                else Left $ optionsError $ "autotuning is only supported for these backends: " <> unwords supportedBackends
+          )
           "BACKEND"
       )
-      "The compiler used (defaults to 'opencl').",
+      "The backend used (defaults to 'opencl').",
     Option
       []
       ["futhark"]
@@ -534,7 +538,7 @@
                 [(n', "")] ->
                   Right $ \config -> config {optTimeout = n'}
                 _ ->
-                  Left $ error $ "'" ++ n ++ "' is not a non-negative integer."
+                  Left $ optionsError $ "'" ++ n ++ "' is not a non-negative integer."
           )
           "SECONDS"
       )
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
@@ -192,6 +192,7 @@
 toValueType TEArrow {} = Left "Cannot generate functions."
 toValueType TESum {} = Left "Cannot handle sumtypes yet."
 toValueType TEDim {} = Left "Cannot handle existential sizes."
+toValueType (TEParens t _) = toValueType t
 toValueType (TEUnique t _) = toValueType t
 toValueType (TEArray d t _) = do
   d' <- constantDim d
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
@@ -495,8 +495,9 @@
               $ M.keys params
       earlyDecl
         [C.cedecl|static void set_tuning_params(struct futhark_context* ctx) {
-                $stms:set_tuning_params
-              }|]
+                    (void)ctx;
+                    $stms:set_tuning_params
+                  }|]
 
       mapM_ earlyDecl $ concat memfuns
       type_funs <- generateAPITypes arr_space types
@@ -540,10 +541,10 @@
       num_params = length params
   earlyDecl [C.cedecl|struct tuning_params { $sdecls:size_decls };|]
   earlyDecl [C.cedecl|static const int num_tuning_params = $int:num_params;|]
-  earlyDecl [C.cedecl|static const char *tuning_param_names[] = { $inits:size_name_inits };|]
-  earlyDecl [C.cedecl|static const char *tuning_param_vars[] = { $inits:size_var_inits };|]
-  earlyDecl [C.cedecl|static const char *tuning_param_classes[] = { $inits:size_class_inits };|]
-  earlyDecl [C.cedecl|static typename int64_t tuning_param_defaults[] = { $inits:size_default_inits };|]
+  earlyDecl [C.cedecl|static const char *tuning_param_names[] = { $inits:size_name_inits, NULL };|]
+  earlyDecl [C.cedecl|static const char *tuning_param_vars[] = { $inits:size_var_inits, NULL };|]
+  earlyDecl [C.cedecl|static const char *tuning_param_classes[] = { $inits:size_class_inits, NULL };|]
+  earlyDecl [C.cedecl|static typename int64_t tuning_param_defaults[] = { $inits:size_default_inits, 0 };|]
 
 generateCommonLibFuns :: [C.BlockItem] -> CompilerM op s ()
 generateCommonLibFuns memreport = do
diff --git a/src/Futhark/CodeGen/Backends/GenericC/Code.hs b/src/Futhark/CodeGen/Backends/GenericC/Code.hs
--- a/src/Futhark/CodeGen/Backends/GenericC/Code.hs
+++ b/src/Futhark/CodeGen/Backends/GenericC/Code.hs
@@ -6,6 +6,8 @@
     compileExp,
     compileExpToName,
     compileCode,
+    compileDest,
+    compileArg,
     errorMsgString,
     linearCode,
   )
@@ -158,10 +160,36 @@
   iexp' <- compileExp $ untyped iexp
   pure [C.cexp|$id:src[$exp:iexp']|]
 
+memNeedsWrapping :: VName -> CompilerM op s Bool
+memNeedsWrapping v = do
+  refcount <- fatMemory DefaultSpace
+  cached <- isJust <$> cacheMem v
+  pure $ refcount && cached
+
+-- | Compile an argument to a function applicaiton.
 compileArg :: Arg -> CompilerM op s C.Exp
-compileArg (MemArg m) = pure [C.cexp|$exp:m|]
+compileArg (MemArg m) = do
+  -- Function might expect fat memory, so if this is a lexical/cached
+  -- raw pointer, we have to wrap it in a struct.
+  wrap <- memNeedsWrapping m
+  if wrap
+    then pure [C.cexp|($ty:(fatMemType DefaultSpace)) {.references = NULL, .mem = $exp:m}|]
+    else pure [C.cexp|$exp:m|]
 compileArg (ExpArg e) = compileExp e
 
+-- | Prepare a destination for function application.
+compileDest :: VName -> CompilerM op s (VName, [C.Stm])
+compileDest v = do
+  -- Function result be fat memory, so if target is a raw pointer, we
+  -- have to wrap it in a struct and unwrap it afterwards.
+  wrap <- memNeedsWrapping v
+  if wrap
+    then do
+      v' <- newVName $ baseString v <> "_struct"
+      item [C.citem|$ty:(fatMemType DefaultSpace) $id:v' = {.references = NULL, .mem = $exp:v};|]
+      pure (v', [C.cstms|$id:v = $id:v'.mem;|])
+    else pure (v, mempty)
+
 compileCode :: Code op -> CompilerM op s ()
 compileCode (Op op) =
   join $ asks (opsCompiler . envOperations) <*> pure op
@@ -358,9 +386,11 @@
   | isBuiltInFunction fname = do
       args' <- mapM compileArg args
       stm [C.cstm|$id:dest = $id:(funName fname)($args:args');|]
-compileCode (Call dests fname args) =
+compileCode (Call dests fname args) = do
+  (dests', unpack_dest) <- mapAndUnzipM compileDest dests
   join $
     asks (opsCall . envOperations)
-      <*> pure dests
+      <*> pure dests'
       <*> pure fname
       <*> mapM compileArg args
+  stms $ mconcat unpack_dest
diff --git a/src/Futhark/CodeGen/Backends/GenericC/Monad.hs b/src/Futhark/CodeGen/Backends/GenericC/Monad.hs
--- a/src/Futhark/CodeGen/Backends/GenericC/Monad.hs
+++ b/src/Futhark/CodeGen/Backends/GenericC/Monad.hs
@@ -608,7 +608,8 @@
   -- cached.  This is not a deep technical restriction, but merely a
   -- heuristic based on GPU memory usually involving larger
   -- allocations, that do not suffer from the overhead of reference
-  -- counting.
+  -- counting.  Beware: there is code elsewhere in codegen that
+  -- assumes lexical memory is DefaultSpace too.
   let cached = M.keys $ M.filter (== DefaultSpace) lexical
 
   cached' <- forM cached $ \mem -> do
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
@@ -477,9 +477,7 @@
   ftask <- multicoreDef (s' ++ "_parloop") $ \s -> do
     fbody <- benchmarkCode s (Just "tid") <=< GC.inNewFunction $
       GC.cachingMemory lexical $ \decl_cached free_cached -> GC.collect $ do
-        mapM_
-          GC.item
-          [C.citems|$decls:(compileGetStructVals fstruct free_args free_ctypes)|]
+        GC.items [C.citems|$decls:(compileGetStructVals fstruct free_args free_ctypes)|]
 
         GC.decl [C.cdecl|typename int64_t iterations = end-start;|]
 
@@ -496,6 +494,7 @@
                                  typename int64_t end,
                                  int subtask_id,
                                  int tid) {
+                       (void)subtask_id;
                        int err = 0;
                        struct $id:fstruct *$id:fstruct = (struct $id:fstruct*) args;
                        struct futhark_context *ctx = $id:fstruct->ctx;
diff --git a/src/Futhark/CodeGen/Backends/MulticoreISPC.hs b/src/Futhark/CodeGen/Backends/MulticoreISPC.hs
--- a/src/Futhark/CodeGen/Backends/MulticoreISPC.hs
+++ b/src/Futhark/CodeGen/Backends/MulticoreISPC.hs
@@ -630,11 +630,11 @@
       [C.cstm|if (!($exp:cond')) { $items:fbranch' }|]
     _ ->
       [C.cstm|if ($exp:cond') { $items:tbranch' } else { $items:fbranch' }|]
-compileCode (Call dests fname args) =
-  defCallIspc dests fname =<< mapM compileArg args
+compileCode (Call dests fname args) = do
+  (dests', unpack_dest) <- mapAndUnzipM GC.compileDest dests
+  defCallIspc dests' fname =<< mapM GC.compileArg args
+  GC.stms $ mconcat unpack_dest
   where
-    compileArg (MemArg m) = pure [C.cexp|$exp:m|]
-    compileArg (ExpArg e) = compileExp e
     defCallIspc dests' fname' args' = do
       let out_args = [[C.cexp|&$id:d|] | d <- dests']
           args''
diff --git a/src/Futhark/CodeGen/ImpGen/GPU/SegRed.hs b/src/Futhark/CodeGen/ImpGen/GPU/SegRed.hs
--- a/src/Futhark/CodeGen/ImpGen/GPU/SegRed.hs
+++ b/src/Futhark/CodeGen/ImpGen/GPU/SegRed.hs
@@ -83,6 +83,7 @@
   KernelBody GPUMem ->
   CallKernelGen ()
 compileSegRed pat lvl space reds body = do
+  emit $ Imp.DebugPrint "\n# SegRed" Nothing
   KernelAttrs _ _ num_groups group_size <- lvlKernelAttrs lvl
   let grid = KernelGrid num_groups group_size
   compileSegRed' pat grid space reds $ \red_cont ->
@@ -94,6 +95,7 @@
         zipWithM_ (compileThreadResult space) map_arrs map_res
 
       red_cont $ zip (map kernelResultSubExp red_res) $ repeat []
+  emit $ Imp.DebugPrint "" Nothing
 
 -- | Like 'compileSegRed', but where the body is a monadic action.
 compileSegRed' ::
@@ -197,8 +199,6 @@
     dPrimV "num_threads" $
       unCount num_groups' * unCount group_size'
 
-  emit $ Imp.DebugPrint "\n# SegRed" Nothing
-
   sKernelThread "segred_nonseg" (segFlat space) (defKernelAttrs num_groups group_size) $ do
     constants <- kernelConstants <$> askEnv
     sync_arr <- sAllocArray "sync_arr" Bool (Shape [intConst Int32 1]) $ Space "local"
@@ -253,8 +253,6 @@
           group_res_arrs
           red_arrs
 
-  emit $ Imp.DebugPrint "" Nothing
-
 smallSegmentsReduction ::
   Pat LetDecMem ->
   Count NumGroups SubExp ->
@@ -279,7 +277,7 @@
       segments_per_group = unCount group_size' `quot` segment_size_nonzero
       required_groups = sExt32 $ num_segments `divUp` segments_per_group
 
-  emit $ Imp.DebugPrint "\n# SegRed-small" Nothing
+  emit $ Imp.DebugPrint "# SegRed-small" Nothing
   emit $ Imp.DebugPrint "num_segments" $ Just $ untyped num_segments
   emit $ Imp.DebugPrint "segment_size" $ Just $ untyped segment_size
   emit $ Imp.DebugPrint "segments_per_group" $ Just $ untyped segments_per_group
@@ -370,8 +368,6 @@
       -- local memory array first thing in the next iteration.
       sOp $ Imp.Barrier Imp.FenceLocal
 
-  emit $ Imp.DebugPrint "" Nothing
-
 largeSegmentsReduction ::
   Pat LetDecMem ->
   Count NumGroups SubExp ->
@@ -406,7 +402,7 @@
     dPrimV "threads_per_segment" $
       groups_per_segment * unCount group_size'
 
-  emit $ Imp.DebugPrint "\n# SegRed-large" Nothing
+  emit $ Imp.DebugPrint "# SegRed-large" Nothing
   emit $ Imp.DebugPrint "num_segments" $ Just $ untyped num_segments
   emit $ Imp.DebugPrint "segment_size" $ Just $ untyped segment_size
   emit $ Imp.DebugPrint "virt_num_groups" $ Just $ untyped $ tvExp virt_num_groups
@@ -508,8 +504,6 @@
                     copyDWIMFix (patElemName v) (map Imp.le64 segment_gtids) (Var acc) acc_is
 
       sIf (groups_per_segment .==. 1) one_group_per_segment multiple_groups_per_segment
-
-  emit $ Imp.DebugPrint "" Nothing
 
 -- Careful to avoid division by zero here.  We have at least one group
 -- per segment.
diff --git a/src/Futhark/CodeGen/ImpGen/GPU/SegScan.hs b/src/Futhark/CodeGen/ImpGen/GPU/SegScan.hs
--- a/src/Futhark/CodeGen/ImpGen/GPU/SegScan.hs
+++ b/src/Futhark/CodeGen/ImpGen/GPU/SegScan.hs
@@ -63,5 +63,6 @@
       | Just scan' <- canBeSinglePass scans ->
           SinglePass.compileSegScan pat lvl space scan' kbody
     _ -> TwoPass.compileSegScan pat lvl space scans kbody
+  emit $ Imp.DebugPrint "" Nothing
   where
     n = product $ map pe64 $ segSpaceDims 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
@@ -641,6 +641,7 @@
         t' <- typeExpHtml t
         pure $ toHtml (nameToString name) <> ": " <> t'
   TEVar name _ -> qualNameHtml name
+  TEParens te _ -> parens <$> typeExpHtml te
   TEApply t arg _ -> do
     t' <- typeExpHtml t
     arg' <- typeArgExpHtml arg
diff --git a/src/Futhark/IR/Pretty.hs b/src/Futhark/IR/Pretty.hs
--- a/src/Futhark/IR/Pretty.hs
+++ b/src/Futhark/IR/Pretty.hs
@@ -170,19 +170,10 @@
     align . hang 2 $
       "let"
         <+> align (pretty pat)
-        <+> case (linebreak, stmannot) of
-          (True, []) -> equals </> pretty e
-          (False, []) -> equals <+> pretty e
-          (_, ann) -> equals </> (stack ann </> pretty e)
+        <+> case stmannot of
+          [] -> equals </> pretty e
+          _ -> equals </> (stack stmannot </> pretty e)
     where
-      linebreak = case e of
-        BasicOp BinOp {} -> False
-        BasicOp CmpOp {} -> False
-        BasicOp ConvOp {} -> False
-        BasicOp UnOp {} -> False
-        BasicOp SubExp {} -> False
-        _ -> True
-
       stmannot =
         concat
           [ maybeToList (ppExpDec (stmAuxDec aux) e),
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
@@ -169,6 +169,8 @@
       TESum (map (fmap $ map $ onTypeExp substs) ts) loc
     onTypeExp substs (TEDim dims t loc) =
       TEDim dims (onTypeExp substs t) loc
+    onTypeExp substs (TEParens te loc) =
+      TEParens (onTypeExp substs te) loc
     onTypeExp _ (TEVar v loc) =
       TEVar v loc
 
@@ -343,7 +345,9 @@
   StaticVal ->
   m StaticVal
 instStaticVal globals dims t sv_t sv = do
-  fresh_substs <- mkSubsts $ S.toList $ S.fromList dims <> sizesToRename sv
+  fresh_substs <-
+    mkSubsts . filter (`S.notMember` globals) . S.toList $
+      S.fromList dims <> sizesToRename sv
 
   let dims' = map (onName fresh_substs) dims
       isDim k _ = k `elem` dims'
@@ -494,8 +498,7 @@
     HoleSV _ hole_loc ->
       pure (Hole (Info t) hole_loc, sv)
     _ ->
-      let tp = typeFromSV sv
-       in pure (Var qn (Info tp) loc, sv)
+      pure (Var qn (Info (typeFromSV sv)) loc, sv)
 defuncExp (Hole (Info t) loc) =
   pure (Hole (Info t) loc, HoleSV t loc)
 defuncExp (Ascript e0 tydecl loc)
@@ -510,7 +513,7 @@
   | otherwise = defuncExp e0
 defuncExp (AppExp (LetPat sizes pat e1 e2 loc) (Info (AppRes t retext))) = do
   (e1', sv1) <- defuncExp e1
-  let env = matchPatSV pat sv1
+  let env = alwaysMatchPatSV pat sv1
       pat' = updatePat pat sv1
   (e2', sv2) <- localEnv env $ defuncExp e2
   -- To maintain any sizes going out of scope, we need to compute the
@@ -547,7 +550,7 @@
 defuncExp IndexSection {} = error "defuncExp: unexpected projection section."
 defuncExp (AppExp (DoLoop sparams pat e1 form e3 loc) res) = do
   (e1', sv1) <- defuncExp e1
-  let env1 = matchPatSV pat sv1
+  let env1 = alwaysMatchPatSV pat sv1
   (form', env2) <- case form of
     For v e2 -> do
       e2' <- defuncExp' e2
@@ -655,7 +658,10 @@
       ++ locStr loc
 defuncExp (AppExp (Match e cs loc) res) = do
   (e', sv) <- defuncExp e
-  csPairs <- mapM (defuncCase sv) cs
+  let bad = error $ "No case matches StaticVal\n" <> show sv
+  csPairs <-
+    fromMaybe bad . NE.nonEmpty . catMaybes
+      <$> mapM (defuncCase sv) (NE.toList cs)
   let cs' = fmap fst csPairs
       sv' = snd $ NE.head csPairs
   pure (AppExp (Match e' cs' loc) res, sv')
@@ -667,12 +673,15 @@
 defuncExp' :: Exp -> DefM Exp
 defuncExp' = fmap fst . defuncExp
 
-defuncCase :: StaticVal -> Case -> DefM (Case, StaticVal)
+defuncCase :: StaticVal -> Case -> DefM (Maybe (Case, StaticVal))
 defuncCase sv (CasePat p e loc) = do
   let p' = updatePat p sv
-      env = matchPatSV p sv
-  (e', sv') <- localEnv env $ defuncExp e
-  pure (CasePat p' e' loc, sv')
+  case matchPatSV p sv of
+    Just env -> do
+      (e', sv') <- localEnv env $ defuncExp e
+      pure $ Just (CasePat p' e' loc, sv')
+    Nothing ->
+      pure Nothing
 
 -- | Defunctionalize the function argument to a SOAC by eta-expanding if
 -- necessary and then defunctionalizing the body of the introduced lambda.
@@ -862,7 +871,7 @@
   DefM (Exp, StaticVal)
 defuncApplyArg fname_s (f', f_sv@(LambdaSV pat lam_e_t lam_e closure_env)) (((d, argext), arg), _) = do
   (arg', arg_sv) <- defuncExp arg
-  let env' = matchPatSV pat arg_sv
+  let env' = alwaysMatchPatSV pat arg_sv
       dims = mempty
   (lam_e', sv) <-
     localNewEnv (env' <> closure_env) $
@@ -929,8 +938,12 @@
       apply_e = mkApply f' [(d, argext, arg')] callret
   pure (apply_e, sv)
 --
-defuncApplyArg _ (_, sv) _ =
-  error $ "defuncApplyArg: cannot apply StaticVal\n" <> show sv
+defuncApplyArg fname_s (_, sv) _ =
+  error $
+    "defuncApplyArg: cannot apply StaticVal\n"
+      <> show sv
+      <> "\nFunction name: "
+      <> prettyString fname_s
 
 updateReturn :: AppRes -> Exp -> Exp
 updateReturn (AppRes ret1 ext1) (AppExp apply (Info (AppRes ret2 ext2))) =
@@ -1119,43 +1132,49 @@
    in (second fromStruct p : ps', ret)
 dynamicFunType sv _ = ([], typeFromSV sv)
 
--- | Match a pattern with its static value. Returns an environment with
--- the identifier components of the pattern mapped to the corresponding
--- subcomponents of the static value.
-matchPatSV :: PatBase Info VName -> StaticVal -> Env
+-- | Match a pattern with its static value. Returns an environment
+-- with the identifier components of the pattern mapped to the
+-- corresponding subcomponents of the static value.  If this function
+-- returns 'Nothing', then it corresponds to an unmatchable case.
+-- These should only occur for 'Match' expressions.
+matchPatSV :: Pat -> StaticVal -> Maybe Env
 matchPatSV (TuplePat ps _) (RecordSV ls) =
-  mconcat $ zipWith (\p (_, sv) -> matchPatSV p sv) ps ls
+  mconcat <$> zipWithM (\p (_, sv) -> matchPatSV p sv) ps ls
 matchPatSV (RecordPat ps _) (RecordSV ls)
   | ps' <- sortOn fst ps,
     ls' <- sortOn fst ls,
     map fst ps' == map fst ls' =
-      mconcat $ zipWith (\(_, p) (_, sv) -> matchPatSV p sv) ps' ls'
+      mconcat <$> zipWithM (\(_, p) (_, sv) -> matchPatSV p sv) ps' ls'
 matchPatSV (PatParens pat _) sv = matchPatSV pat sv
 matchPatSV (PatAttr _ pat _) sv = matchPatSV pat sv
 matchPatSV (Id vn (Info t) _) sv =
-  -- When matching a pattern with a zero-order STaticVal, the type of
-  -- the pattern wins out.  This is important when matching a
-  -- nonunique pattern with a unique value.
-  if orderZeroSV sv
-    then dim_env <> M.singleton vn (Binding Nothing $ Dynamic t)
-    else dim_env <> M.singleton vn (Binding Nothing sv)
+  -- When matching a zero-order pattern with a StaticVal, the type of
+  -- the pattern wins out.  This is important for propagating sizes
+  -- (but probably reveals a flaw in our bookkeeping).
+  pure $
+    if orderZero t
+      then dim_env <> M.singleton vn (Binding Nothing $ Dynamic t)
+      else dim_env <> M.singleton vn (Binding Nothing sv)
   where
     dim_env =
       M.fromList $ map (,i64) $ S.toList $ freeInType t
     i64 = Binding Nothing $ Dynamic $ Scalar $ Prim $ Signed Int64
-matchPatSV (Wildcard _ _) _ = mempty
+matchPatSV (Wildcard _ _) _ = pure mempty
 matchPatSV (PatAscription pat _ _) sv = matchPatSV pat sv
-matchPatSV PatLit {} _ = mempty
+matchPatSV PatLit {} _ = pure mempty
 matchPatSV (PatConstr c1 _ ps _) (SumSV c2 ls fs)
   | c1 == c2 =
-      mconcat $ zipWith matchPatSV ps ls
-  | Just ts <- lookup c1 fs =
-      mconcat $ zipWith matchPatSV ps $ map svFromType ts
+      mconcat <$> zipWithM matchPatSV ps ls
+  | Just _ <- lookup c1 fs =
+      Nothing
   | otherwise =
       error $ "matchPatSV: missing constructor in type: " ++ prettyString c1
 matchPatSV (PatConstr c1 _ ps _) (Dynamic (Scalar (Sum fs)))
   | Just ts <- M.lookup c1 fs =
-      mconcat $ zipWith matchPatSV ps $ map svFromType ts
+      -- A higher-order pattern can only match an appropriate SumSV.
+      if all orderZero ts
+        then mconcat <$> zipWithM matchPatSV ps (map svFromType ts)
+        else Nothing
   | otherwise =
       error $ "matchPatSV: missing constructor in type: " ++ prettyString c1
 matchPatSV pat (Dynamic t) = matchPatSV pat $ svFromType t
@@ -1167,10 +1186,10 @@
       ++ "\n with static value\n"
       ++ show sv
 
-orderZeroSV :: StaticVal -> Bool
-orderZeroSV Dynamic {} = True
-orderZeroSV (RecordSV fields) = all (orderZeroSV . snd) fields
-orderZeroSV _ = False
+alwaysMatchPatSV :: Pat -> StaticVal -> Env
+alwaysMatchPatSV pat sv = fromMaybe bad $ matchPatSV pat sv
+  where
+    bad = error $ unlines [prettyString pat, "cannot match StaticVal", show sv]
 
 -- | Given a pattern and the static value for the defunctionalized argument,
 -- update the pattern to reflect the changes in the types.
@@ -1220,8 +1239,9 @@
       ++ "\nto reflect the static value\n"
       ++ show sv
 
--- | Convert a record (or tuple) type to a record static value. This is used for
--- "unwrapping" tuples and records that are nested in 'Dynamic' static values.
+-- | Convert a record (or tuple) type to a record static value. This
+-- is used for "unwrapping" tuples and records that are nested in
+-- 'Dynamic' static values.
 svFromType :: PatType -> StaticVal
 svFromType (Scalar (Record fs)) = RecordSV . M.toList $ M.map svFromType fs
 svFromType t = Dynamic t
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
@@ -2151,6 +2151,9 @@
 typeExpForError :: E.TypeExp Info VName -> InternaliseM [ErrorMsgPart SubExp]
 typeExpForError (E.TEVar qn _) =
   pure [ErrorString $ prettyText qn]
+typeExpForError (E.TEParens te _) = do
+  msg <- typeExpForError te
+  pure $ ["("] <> msg <> [")"]
 typeExpForError (E.TEUnique te _) =
   ("*" :) <$> typeExpForError te
 typeExpForError (E.TEDim dims te _) =
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
@@ -488,13 +488,12 @@
                 { $1 }
 
 TypeExpAtom :: { UncheckedTypeExp }
-             : '(' TypeExp ')'                { $2 }
+             : '(' TypeExp ')'                { TEParens $2 (srcspan $1 $>) }
              | '(' ')'                        { TETuple [] (srcspan $1 $>) }
              | '(' TypeExp ',' TupleTypes ')' { TETuple ($2:$4) (srcspan $1 $>) }
              | '{' '}'                        { TERecord [] (srcspan $1 $>) }
              | '{' FieldTypes1 '}'            { TERecord $2 (srcspan $1 $>) }
-             | SizeExp TypeExpTerm
-               { TEArray $1 $2 (srcspan $1 $>) }
+             | SizeExp TypeExpTerm            { TEArray $1 $2 (srcspan $1 $>) }
              | QualName                       { TEVar (fst $1) (srclocOf (snd $1)) }
 
 Constr :: { (Name, Loc) }
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
@@ -175,6 +175,7 @@
     where
       ppField (name, t) = pretty (nameToString name) <> colon <+> pretty t
   pretty (TEVar name _) = pretty name
+  pretty (TEParens te _) = parens $ pretty te
   pretty (TEApply t arg _) = pretty t <+> pretty arg
   pretty (TEArrow (Just v) t1 t2 _) = parens v' <+> "->" <+> pretty t2
     where
@@ -376,11 +377,19 @@
     p name = "." <> pretty name
 prettyExp _ (IndexSection idxs _ _) =
   parens $ "." <> brackets (commasep (map pretty idxs))
-prettyExp _ (Constr n cs t _) =
-  "#" <> pretty n <+> sep (map pretty cs) <> prettyInst t
+prettyExp p (Constr n cs t _) =
+  parensIf (p >= 10) $
+    "#" <> pretty n <+> sep (map (prettyExp 10) cs) <> prettyInst t
 prettyExp _ (Attr attr e _) =
   prettyAttr attr </> prettyExp (-1) e
-prettyExp i (AppExp e _) = prettyAppExp i e
+prettyExp i (AppExp e res)
+  | isEnvVarAtLeast "FUTHARK_COMPILER_DEBUGGING" 2,
+    Just res' <- unAnnot res,
+    not $ null $ appResExt res' =
+      "#"
+        <> brackets (commasep $ map prettyName $ appResExt res')
+        </> parens (prettyAppExp i e)
+  | otherwise = prettyAppExp i e
 
 instance (Eq vn, IsName vn, Annot f) => Pretty (ExpBase f vn) where
   pretty = prettyExp (-1)
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
@@ -212,6 +212,8 @@
     TEVar qn loc -> do
       guard $ loc `contains` pos
       Just $ RawAtName qn $ locOf loc
+    TEParens te' _ ->
+      atPosInTypeExp te' pos
     TETuple es _ ->
       msum $ map (`atPosInTypeExp` pos) es
     TERecord fields _ ->
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
@@ -421,11 +421,13 @@
 
 deriving instance Ord (SizeExp Info VName)
 
--- | An unstructured type with type variables and possibly shape
--- declarations - this is what the user types in the source program.
--- These are used to construct 'TypeBase's in the type checker.
+-- | An unstructured syntactic type with type variables and possibly
+-- shape declarations - this is what the user types in the source
+-- program.  These are used to construct 'TypeBase's in the type
+-- checker.
 data TypeExp f vn
   = TEVar (QualName vn) SrcLoc
+  | TEParens (TypeExp f vn) SrcLoc
   | TETuple [TypeExp f vn] SrcLoc
   | TERecord [(Name, TypeExp f vn)] SrcLoc
   | TEArray (SizeExp f vn) (TypeExp f vn) SrcLoc
@@ -452,6 +454,7 @@
   locOf (TETuple _ loc) = locOf loc
   locOf (TERecord _ loc) = locOf loc
   locOf (TEVar _ loc) = locOf loc
+  locOf (TEParens _ loc) = locOf loc
   locOf (TEUnique _ loc) = locOf loc
   locOf (TEApply _ _ loc) = locOf loc
   locOf (TEArrow _ _ _ loc) = locOf loc
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
@@ -242,6 +242,8 @@
 instance ASTMappable (TypeExp Info VName) where
   astMap tv (TEVar qn loc) =
     TEVar <$> astMap tv qn <*> pure loc
+  astMap tv (TEParens te loc) =
+    TEParens <$> astMap tv te <*> pure loc
   astMap tv (TETuple ts loc) =
     TETuple <$> traverse (astMap tv) ts <*> pure loc
   astMap tv (TERecord ts 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
@@ -665,7 +665,7 @@
           "size-polymorphic-entry"
           "Entry point functions must not be size-polymorphic in their return type."
   | p : _ <- filter nastyParameter params =
-      warn loc $
+      warn p $
         "Entry point parameter\n"
           </> indent 2 (pretty p)
           </> "\nwill have an opaque type, so the entry point will likely not be callable."
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
@@ -16,6 +16,7 @@
 import Control.Monad.Except
 import Control.Monad.Reader
 import Control.Monad.State
+import Data.Bitraversable
 import Data.Either
 import Data.List (find, foldl', genericLength, partition)
 import Data.List.NonEmpty qualified as NE
@@ -163,21 +164,36 @@
   SrcLoc ->
   UncheckedTypeExp ->
   UncheckedExp ->
-  TermTypeM (TypeExp Info VName, StructType, Exp, [VName])
+  TermTypeM (TypeExp Info VName, StructType, Exp)
 checkCoerce loc te e = do
-  (te', te_t, ext) <- checkTypeExpRigid te RigidCoerce
+  (te', te_t, ext) <- checkTypeExpNonrigid te
   e' <- checkExp e
   e_t <- toStruct <$> expTypeFully e'
 
-  (e_t_nonrigid, _) <-
-    allDimsFreshInType loc Nonrigid "coerce_d" e_t
+  te_t_nonrigid <- makeNonExtFresh ext te_t
 
   onFailure (CheckingAscription te_t e_t) $
-    unify (mkUsage loc "type ascription") te_t e_t_nonrigid
-
-  te_t' <- normTypeFully te_t
+    unify (mkUsage loc "size coercion") e_t te_t_nonrigid
 
-  pure (te', te_t', e', ext)
+  -- If the type expression had any anonymous dimensions, these will
+  -- now be in 'ext'.  Those we keep nonrigid and unify with e_t.
+  -- This ensures that 'x :> [1][]i32' does not make the second
+  -- dimension unknown.  Use of matchDims is sensible because the
+  -- structure of e_t' will be fully known due to the unification, and
+  -- te_t because type expressions are complete.
+  pure (te', te_t, e')
+  where
+    makeNonExtFresh ext = bitraverse onDim pure
+      where
+        onDim d@(NamedSize v)
+          | qualLeaf v `elem` ext = pure d
+        onDim _ = do
+          v <- newTypeName "coerce"
+          constrain v . Size Nothing $
+            mkUsage
+              loc
+              "a size coercion where the underlying expression size cannot be determined"
+          pure $ NamedSize $ qualName v
 
 unscopeType ::
   SrcLoc ->
@@ -313,10 +329,10 @@
   (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
+  (te', te_t, e') <- checkCoerce loc te e
   t <- expTypeFully e'
   t' <- matchDims (const . const pure) t $ fromStruct te_t
-  pure $ AppExp (Coerce e' te' loc) (Info $ AppRes t' ext)
+  pure $ AppExp (Coerce e' te' loc) (Info $ AppRes t' [])
 checkExp (AppExp (BinOp (op, oploc) NoInfo (e1, _) (e2, _) loc) NoInfo) = do
   (op', ftype) <- lookupVar oploc op
   e1_arg <- checkArg e1
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
@@ -13,6 +13,7 @@
 import Control.Monad.State
 import Data.Bifunctor
 import Data.Bitraversable
+import Data.List qualified as L
 import Data.Map.Strict qualified as M
 import Data.Maybe
 import Data.Set qualified as S
@@ -26,21 +27,39 @@
 import Language.Futhark.TypeChecker.Unify
 import Prelude hiding (mod)
 
+-- | Retrieve an oracle that can be used to decide whether two are in
+-- the same equivalence class (i.e. have been unified).  This is an
+-- exotic operation.
+getAreSame :: MonadUnify m => m (VName -> VName -> Bool)
+getAreSame = check <$> getConstraints
+  where
+    check constraints x y =
+      case (M.lookup x constraints, M.lookup y constraints) of
+        (Just (_, Size (Just (NamedSize x')) _), _) ->
+          check constraints (qualLeaf x') y
+        (_, Just (_, Size (Just (NamedSize y')) _)) ->
+          check constraints x (qualLeaf y')
+        _ ->
+          x == y
+
 -- | Replace specified sizes with distinct fresh size variables.
 someDimsFreshInType ::
   SrcLoc ->
   Rigidity ->
   Name ->
-  S.Set VName ->
+  [VName] ->
   TypeBase Size als ->
   TermTypeM (TypeBase Size als)
-someDimsFreshInType loc r desc sizes = bitraverse onDim pure
+someDimsFreshInType loc r desc fresh t = do
+  areSameSize <- getAreSame
+  let freshen v = any (areSameSize v) fresh
+  bitraverse (onDim freshen) pure t
   where
-    onDim (NamedSize d)
-      | qualLeaf d `S.member` sizes = do
+    onDim freshen (NamedSize d)
+      | freshen $ qualLeaf d = do
           v <- newDimVar loc r desc
           pure $ NamedSize $ qualName v
-    onDim d = pure d
+    onDim _ d = pure d
 
 -- | Replace the specified sizes with fresh size variables of the
 -- specified ridigity.  Returns the new fresh size variables.
@@ -48,14 +67,16 @@
   SrcLoc ->
   Rigidity ->
   Name ->
-  S.Set VName ->
+  [VName] ->
   TypeBase Size als ->
   TermTypeM (TypeBase Size als, [VName])
-freshDimsInType loc r desc sizes t =
-  second M.elems <$> runStateT (bitraverse onDim pure t) mempty
+freshDimsInType loc r desc fresh t = do
+  areSameSize <- getAreSame
+  let freshen v = any (areSameSize v) fresh
+  second M.elems <$> runStateT (bitraverse (onDim freshen) pure t) mempty
   where
-    onDim (NamedSize d)
-      | qualLeaf d `S.member` sizes = do
+    onDim freshen (NamedSize d)
+      | freshen $ qualLeaf d = do
           prev_subst <- gets $ M.lookup $ qualLeaf d
           case prev_subst of
             Just d' -> pure $ NamedSize $ qualName d'
@@ -63,7 +84,7 @@
               v <- lift $ newDimVar loc r desc
               modify $ M.insert (qualLeaf d) v
               pure $ NamedSize $ qualName v
-    onDim d = pure d
+    onDim _ d = pure d
 
 -- | Mark bindings of names in "consumed" as Unique.
 uniquePat :: Names -> Pat -> Pat
@@ -166,15 +187,11 @@
 wellTypedLoopArg :: ArgSource -> [VName] -> Pat -> Exp -> TermTypeM ()
 wellTypedLoopArg src sparams pat arg = do
   (merge_t, _) <-
-    freshDimsInType (srclocOf arg) Nonrigid "loop" (S.fromList sparams) $
-      toStruct $
-        patternType pat
+    freshDimsInType (srclocOf arg) Nonrigid "loop" sparams $
+      toStruct (patternType pat)
   arg_t <- toStruct <$> expTypeFully arg
   onFailure (checking merge_t arg_t) $
-    unify
-      (mkUsage (srclocOf arg) desc)
-      merge_t
-      arg_t
+    unify (mkUsage (srclocOf arg) desc) merge_t arg_t
   where
     (checking, desc) =
       case src of
@@ -203,6 +220,7 @@
   TermTypeM (CheckedLoop, AppRes)
 checkDoLoop checkExp (mergepat, mergeexp, form, loopbody) loc =
   sequentially (checkExp mergeexp) $ \mergeexp' _ -> do
+    known_before <- M.keysSet <$> getConstraints
     zeroOrderType
       (mkUsage (srclocOf mergeexp) "use as loop variable")
       "type used as loop variable"
@@ -236,17 +254,18 @@
     -- We don't want the loop parameters to alias their initial
     -- values, so we blank them here.  We will actually check them
     -- properly later.
-    (merge_t, new_dims_to_initial_dim) <-
+    (merge_t, new_dims_map) <-
       -- dim handling (1)
-      allDimsFreshInType loc Nonrigid "loop" . flip setAliases mempty
+      allDimsFreshInType loc Nonrigid "loop_d" . flip setAliases mempty
         =<< expTypeFully mergeexp'
-    let new_dims = M.keys new_dims_to_initial_dim
+    let new_dims_to_initial_dim = M.toList new_dims_map
+        new_dims = map fst new_dims_to_initial_dim
 
     -- dim handling (2)
     let checkLoopReturnSize mergepat' loopbody' = do
           loopbody_t <- expTypeFully loopbody'
           pat_t <-
-            someDimsFreshInType loc Nonrigid "loop" (S.fromList new_dims)
+            someDimsFreshInType loc Nonrigid "loop" new_dims
               =<< normTypeFully (patternType mergepat')
 
           -- We are ignoring the dimensions here, because any mismatches
@@ -260,20 +279,22 @@
           -- Figure out which of the 'new_dims' dimensions are variant.
           -- This works because we know that each dimension from
           -- new_dims in the pattern is unique and distinct.
+          areSameSize <- getAreSame
           let onDims _ x y
                 | x == y = pure x
               onDims _ (NamedSize v) d
-                | qualLeaf v `elem` new_dims = do
-                    case M.lookup (qualLeaf v) new_dims_to_initial_dim of
-                      Just d'
-                        | d' == d ->
-                            modify $ first $ M.insert (qualLeaf v) (SizeSubst d)
-                      _ ->
-                        modify $ second (qualLeaf v :)
+                | Just (v', d') <-
+                    L.find (areSameSize (qualLeaf v) . fst) new_dims_to_initial_dim = do
+                    if d' == d
+                      then modify $ first $ M.insert v' (SizeSubst d)
+                      else
+                        unless (qualLeaf v `S.member` known_before) $
+                          modify (second (qualLeaf v :))
                     pure $ NamedSize v
               onDims _ x _ = pure x
           loopbody_t' <- normTypeFully loopbody_t
           merge_t' <- normTypeFully merge_t
+
           let (init_substs, sparams) =
                 execState (matchDims onDims merge_t' loopbody_t') mempty
 
@@ -319,7 +340,7 @@
           bound_t <- expTypeFully uboundexp'
           bindingIdent i bound_t $ \i' ->
             noUnique . bindingPat [] mergepat (Ascribed merge_t) $
-              \mergepat' -> tapOccurrences $ do
+              \mergepat' -> tapOccurrences $ incLevel $ do
                 loopbody' <- noSizeEscape $ checkExp loopbody
                 (sparams, mergepat'') <- checkLoopReturnSize mergepat' loopbody'
                 pure
@@ -337,7 +358,7 @@
               | Just t' <- peelArray 1 t ->
                   bindingPat [] xpat (Ascribed t') $ \xpat' ->
                     noUnique . bindingPat [] mergepat (Ascribed merge_t) $
-                      \mergepat' -> tapOccurrences $ do
+                      \mergepat' -> tapOccurrences $ incLevel $ do
                         loopbody' <- noSizeEscape $ checkExp loopbody
                         (sparams, mergepat'') <- checkLoopReturnSize mergepat' loopbody'
                         pure
@@ -353,6 +374,7 @@
         While cond ->
           noUnique . bindingPat [] mergepat (Ascribed merge_t) $ \mergepat' ->
             tapOccurrences
+              . incLevel
               . sequentially
                 ( checkExp cond
                     >>= unifies "being the condition of a 'while' loop" (Scalar $ Prim Bool)
@@ -390,7 +412,7 @@
     wellTypedLoopArg Initial sparams mergepat'' mergeexp'
 
     (loopt, retext) <-
-      freshDimsInType loc (Rigid RigidLoop) "loop" (S.fromList sparams) $
+      freshDimsInType loc (Rigid RigidLoop) "loop" sparams $
         loopReturnType mergepat'' merge_t'
     -- We set all of the uniqueness to be unique.  This is intentional,
     -- and matches what happens for function calls.  Those arrays that
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
@@ -273,6 +273,10 @@
           <+> dquotes (hsep (pretty name : map pretty ps))
           <+> "used without any arguments."
 --
+evalTypeExp (TEParens te loc) = do
+  (te', svars, ts, ls) <- evalTypeExp te
+  pure (TEParens te' loc, svars, ts, ls)
+--
 evalTypeExp (TETuple ts loc) = do
   (ts', svars, ts_s, ls) <- unzip4 <$> mapM evalTypeExp ts
   pure
@@ -575,6 +579,7 @@
       check seen t
     check _ TEArray {} = pure ()
     check _ TEVar {} = pure ()
+    check seen (TEParens te _) = check seen te
 
 -- | @checkTypeParams ps m@ checks the type parameters @ps@, then
 -- invokes the continuation @m@ with the checked parameters, while