diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,6 +5,40 @@
 The format is based on [Keep a Changelog](http://keepachangelog.com/en/1.0.0/)
 and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.html).
 
+## [0.25.14]
+
+### Added
+
+* The prelude definition of `filter` is now more memory efficient,
+  particularly when the output is much smaller than the input. (#2109)
+
+* New configuration for GPU backends:
+  `futhark_context_config_set_unified_memory`, also available on
+  executables as ``--unified-memory``.
+
+* The "raw" API functions now do something potentially useful, but are
+  still considered experimental.
+
+* `futhark --version` now reports GHC version.
+
+### Fixed
+
+* Incorrect type checking of let-bound sizes occurring multiple times
+  in pattern. (#2103).
+
+* A concatenation simplification would sometimes mess up sizes.
+  (#2104)
+
+* Bug related to monomorphisation of polymorphic local functions
+  (#2106).
+
+* Rare crash in short circuiting.
+
+* Referencing an unbound type parameter could crash the type checker
+  (#2113, #2114).
+
+* Futhark now works with GHC 9.8 (#2105).
+
 ## [0.25.13]
 
 ### Added
diff --git a/docs/c-api.rst b/docs/c-api.rst
--- a/docs/c-api.rst
+++ b/docs/c-api.rst
@@ -258,17 +258,17 @@
    call :c:func:`futhark_free_i32_1d`.  Multi-dimensional arrays are
    assumed to be in row-major form.  Returns ``NULL`` on failure.
 
-.. c:function:: struct futhark_i32_1d *futhark_new_raw_i32_1d(struct futhark_context *ctx, char *data, int64_t offset, int64_t dim0)
+.. c:function:: struct futhark_i32_1d *futhark_new_raw_i32_1d(struct futhark_context *ctx, char *data, int64_t dim0)
 
-   Create an array based on *raw* data, as well as an offset into it.
-   This differs little from :c:func:`futhark_i32_1d` when using the
-   ``c`` backend, but when using e.g. the ``opencl`` backend, the
-   ``data`` parameter will be a ``cl_mem``.  It is the caller's
-   responsibility to eventually call :c:func:`futhark_free_i32_1d`.
-   The ``data`` pointer must remain valid for the lifetime of the
-   array.  Unless you are very careful, this basically means for the
-   lifetime of the context.  Returns ``NULL`` on failure.
+   Create an array based on *raw* data, which is used for the
+   representation of the array. The ``data`` pointer must remain valid
+   for the lifetime of the array and will not be freed by Futhark.
+   Returns ``NULL`` on failure. The type of the ``data`` argument
+   depends on the backend, and is for example ``cl_mem`` when using
+   the OpenCL backend.
 
+   **This is an experimental and unstable interface.**
+
 .. c:function:: int futhark_free_i32_1d(struct futhark_context *ctx, struct futhark_i32_1d *arr)
 
    Free the value.  In practice, this merely decrements the reference
@@ -289,6 +289,16 @@
    must *not* be manually freed.  Assuming ``arr`` is a valid
    object, this function cannot fail.
 
+.. c:function:: char* futhark_values_raw_i32_1d(struct futhark_context *ctx, struct futhark_i32_1d *arr)
+
+   Return a pointer to the underlying storage of the array. The return
+   type depends on the backend, and is for example ``cl_mem`` when
+   using the OpenCL backend. If using unified memory with the ``hip``
+   or ``cuda`` backends, the pointer can be accessed directly from CPU
+   code.
+
+   **This is an experimental and unstable interface.**
+
 .. _opaques:
 
 Opaque Values
@@ -514,6 +524,19 @@
    with :c:func:`futhark_context_config_set_platform`, only the
    devices from matching platforms are considered.
 
+.. c:function:: void futhark_context_config_set_unified_memory(struct futhark_context_config* cfg, int flag);
+
+   Use "unified" memory for GPU arrays. This means arrays are located
+   in memory that is also accessible from the CPU. The details depends
+   on the backend and hardware in use. The following values are
+   supported:
+
+   * 0: never use unified memory (the default on ``hip``).
+
+   * 1: always use unified memory.
+
+   * 2: use managed memory if the device claims to support it (the
+     default on ``cuda``).
 
 Exotic
 ~~~~~~
diff --git a/docs/man/futhark.rst b/docs/man/futhark.rst
--- a/docs/man/futhark.rst
+++ b/docs/man/futhark.rst
@@ -31,11 +31,11 @@
 :ref:`futhark-bench(1)`.  The results show speedup of the latter file
 compared to the former.
 
-futhark check [-w] PROGRAM
---------------------------
+futhark check [-w] [-Werror] PROGRAM
+------------------------------------
 
-Check whether a Futhark program type checks.  With ``-w``, no warnings
-are printed.
+Check whether a Futhark program type checks. With ``-w``, no warnings
+are printed. With ``--Werror``, warnings are treated as errors.
 
 futhark check-syntax PROGRAM
 ----------------------------
diff --git a/docs/usage.rst b/docs/usage.rst
--- a/docs/usage.rst
+++ b/docs/usage.rst
@@ -182,6 +182,11 @@
     nontrivial (and manual) to relate these operations back to source
     Futhark code.
 
+  ``--unified-memory INT``
+
+    Corresponds to
+    :c:func:`futhark_context_config_set_unified_memory`.
+
 OpenCL-specific Options
 ~~~~~~~~~~~~~~~~~~~~~~~
 
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.25.13
+version:        0.25.14
 synopsis:       An optimising compiler for a functional, array-oriented language.
 
 description:    Futhark is a small programming language designed to be compiled to
@@ -284,6 +284,7 @@
       Futhark.IR.TypeCheck
       Futhark.Internalise
       Futhark.Internalise.AccurateSizes
+      Futhark.Internalise.ApplyTypeAbbrs
       Futhark.Internalise.Bindings
       Futhark.Internalise.Defunctionalise
       Futhark.Internalise.Defunctorise
@@ -409,6 +410,7 @@
       Language.Futhark.Tuple
       Language.Futhark.TypeChecker
       Language.Futhark.TypeChecker.Consumption
+      Language.Futhark.TypeChecker.Names
       Language.Futhark.TypeChecker.Match
       Language.Futhark.TypeChecker.Modules
       Language.Futhark.TypeChecker.Monad
@@ -453,7 +455,7 @@
     , free >=5.1.10
     , futhark-data >= 1.1.0.0
     , futhark-server >= 1.2.2.1
-    , futhark-manifest >= 1.3.0.0
+    , futhark-manifest >= 1.4.0.0
     , githash >=0.1.6.1
     , half >= 0.3
     , haskeline
@@ -479,7 +481,7 @@
     , transformers >=0.3
     , vector >=0.12
     , versions >=6.0.0
-    , zlib >=0.6.1.2
+    , zlib >=0.7.0.0
     , statistics
     , mwc-random
     , prettyprinter >= 1.7
diff --git a/prelude/soacs.fut b/prelude/soacs.fut
--- a/prelude/soacs.fut
+++ b/prelude/soacs.fut
@@ -162,16 +162,6 @@
 def scan [n] 'a (op: a -> a -> a) (ne: a) (as: [n]a): *[n]a =
   intrinsics.scan op ne as
 
--- | Remove all those elements of `as` that do not satisfy the
--- predicate `p`.
---
--- **Work:** *O(n ✕ W(p))*
---
--- **Span:** *O(log(n) ✕ W(p))*
-def filter [n] 'a (p: a -> bool) (as: [n]a): *[]a =
-  let (as', is) = intrinsics.partition 1 (\x -> if p x then 0 else 1) as
-  in as'[:is[0]]
-
 -- | Split an array into those elements that satisfy the given
 -- predicate, and those that do not.
 --
@@ -253,3 +243,17 @@
 -- **Span:** *O(1)*
 def scatter_3d 't [k] [n] [o] [l] (dest: *[k][n][o]t) (is: [l](i64, i64, i64)) (vs: [l]t): *[k][n][o]t =
   intrinsics.scatter_3d dest is vs
+
+-- | Remove all those elements of `as` that do not satisfy the
+-- predicate `p`.
+--
+-- **Work:** *O(n ✕ W(p))*
+--
+-- **Span:** *O(log(n) ✕ W(p))*
+def filter [n] 'a (p: a -> bool) (as: [n]a): *[]a =
+  let flags = map (\x -> if p x then 1 else 0) as
+  let offsets = scan (+) 0 flags
+  let m = if n == 0 then 0 else offsets[n-1]
+  in scatter (map (\x -> x) as[:m])
+             (map2 (\f o -> if f==1 then o-1 else -1) flags offsets)
+             as
diff --git a/prelude/zip.fut b/prelude/zip.fut
--- a/prelude/zip.fut
+++ b/prelude/zip.fut
@@ -10,7 +10,7 @@
 -- We need a map to define some of the zip variants, but this file is
 -- depended upon by soacs.fut.  So we just define a quick-and-dirty
 -- internal one here that uses the intrinsic version.
-local def internal_map 'a [n] 'x (f: a -> x) (as: [n]a): [n]x =
+local def internal_map 'a [n] 'x (f: a -> x) (as: [n]a): *[n]x =
   intrinsics.map f as
 
 -- | Construct an array of pairs from two arrays.
diff --git a/rts/c/backends/cuda.h b/rts/c/backends/cuda.h
--- a/rts/c/backends/cuda.h
+++ b/rts/c/backends/cuda.h
@@ -94,6 +94,8 @@
   char* preferred_device;
   int preferred_device_num;
 
+  int unified_memory;
+
   char* dump_ptx_to;
   char* load_ptx_from;
 
@@ -121,6 +123,8 @@
   cfg->dump_ptx_to = NULL;
   cfg->load_ptx_from = NULL;
 
+  cfg->unified_memory = 2;
+
   cfg->default_block_size = 256;
   cfg->default_grid_size = 0; // Set properly later.
   cfg->default_tile_size = 32;
@@ -186,6 +190,10 @@
   cfg->load_ptx_from = strdup(path);
 }
 
+void futhark_context_config_set_unified_memory(struct futhark_context_config* cfg, int flag) {
+  cfg->unified_memory = flag;
+}
+
 void futhark_context_config_set_default_thread_block_size(struct futhark_context_config *cfg, int size) {
   cfg->default_block_size = size;
   cfg->default_block_size_changed = 1;
@@ -830,6 +838,18 @@
 
   free_list_init(&ctx->gpu_free_list);
 
+  if (ctx->cfg->unified_memory == 2) {
+    ctx->cfg->unified_memory = device_query(ctx->dev, MANAGED_MEMORY);
+  }
+
+  if (ctx->cfg->logging) {
+    if (ctx->cfg->unified_memory) {
+      fprintf(ctx->log, "Using managed memory\n");
+    } else {
+      fprintf(ctx->log, "Using unmanaged memory\n");
+    }
+  }
+
   // MAX_SHARED_MEMORY_PER_BLOCK gives bogus numbers (48KiB); probably
   // for backwards compatibility.  Add _OPTIN and you seem to get the
   // right number.
@@ -1082,10 +1102,17 @@
 }
 
 static int gpu_alloc_actual(struct futhark_context *ctx, size_t size, gpu_mem *mem_out) {
-  CUresult res = cuMemAlloc(mem_out, size);
+  CUresult res;
+  if (ctx->cfg->unified_memory) {
+    res = cuMemAllocManaged(mem_out, size, CU_MEM_ATTACH_GLOBAL);
+  } else {
+    res = cuMemAlloc(mem_out, size);
+  }
+
   if (res == CUDA_ERROR_OUT_OF_MEMORY) {
     return FUTHARK_OUT_OF_MEMORY;
   }
+
   CUDA_SUCCEED_OR_RETURN(res);
   return FUTHARK_SUCCESS;
 }
diff --git a/rts/c/backends/hip.h b/rts/c/backends/hip.h
--- a/rts/c/backends/hip.h
+++ b/rts/c/backends/hip.h
@@ -89,6 +89,8 @@
   int num_build_opts;
   char* *build_opts;
 
+  int unified_memory;
+
   char* preferred_device;
   int preferred_device_num;
 
@@ -111,6 +113,8 @@
   cfg->preferred_device = strdup("");
   cfg->program = strconcat(gpu_program);
 
+  cfg->unified_memory = 0;
+
   cfg->default_block_size = 256;
   cfg->default_grid_size = 0; // Set properly later.
   cfg->default_tile_size = 32;
@@ -166,6 +170,10 @@
   cfg->program = strdup(s);
 }
 
+void futhark_context_config_set_unified_memory(struct futhark_context_config* cfg, int flag) {
+  cfg->unified_memory = flag;
+}
+
 void futhark_context_config_set_default_thread_block_size(struct futhark_context_config *cfg, int size) {
   cfg->default_block_size = size;
   cfg->default_block_size_changed = 1;
@@ -686,6 +694,18 @@
 
   free_list_init(&ctx->gpu_free_list);
 
+  if (ctx->cfg->unified_memory == 2) {
+    ctx->cfg->unified_memory = device_query(ctx->dev, hipDeviceAttributeManagedMemory);
+  }
+
+  if (ctx->cfg->logging) {
+    if (ctx->cfg->unified_memory) {
+      fprintf(ctx->log, "Using managed memory\n");
+    } else {
+      fprintf(ctx->log, "Using unmanaged memory\n");
+    }
+  }
+
   ctx->max_shared_memory = device_query(ctx->dev, hipDeviceAttributeMaxSharedMemoryPerBlock);
   ctx->max_thread_block_size = device_query(ctx->dev, hipDeviceAttributeMaxThreadsPerBlock);
   ctx->max_grid_size = device_query(ctx->dev, hipDeviceAttributeMaxGridDimX);
@@ -809,7 +829,7 @@
     HIP_SUCCEED_FATAL(hipEventRecord(event->start, ctx->stream));
   }
   HIP_SUCCEED_OR_RETURN(hipMemcpyWithStream((unsigned char*)dst+dst_offset, (unsigned char*)src+src_offset,
-                                            nbytes, hipMemcpyDeviceToDevice ,ctx->stream));
+                                            nbytes, hipMemcpyDeviceToDevice, ctx->stream));
   if (event != NULL) {
     HIP_SUCCEED_FATAL(hipEventRecord(event->end, ctx->stream));
   }
@@ -938,7 +958,14 @@
 }
 
 static int gpu_alloc_actual(struct futhark_context *ctx, size_t size, gpu_mem *mem_out) {
-  hipError_t res = hipMalloc(mem_out, size);
+  hipError_t res;
+
+  if (ctx->cfg->unified_memory) {
+    res = hipMallocManaged(mem_out, size, hipMemAttachGlobal);
+  } else {
+    res = hipMalloc(mem_out, size);
+  }
+
   if (res == hipErrorOutOfMemory) {
     return FUTHARK_OUT_OF_MEMORY;
   }
diff --git a/rts/c/backends/opencl.h b/rts/c/backends/opencl.h
--- a/rts/c/backends/opencl.h
+++ b/rts/c/backends/opencl.h
@@ -136,6 +136,8 @@
   char* preferred_device;
   int ignore_blacklist;
 
+  int unified_memory;
+
   char* dump_binary_to;
   char* load_binary_from;
 
@@ -166,6 +168,8 @@
   cfg->load_binary_from = NULL;
   cfg->program = strconcat(gpu_program);
 
+  cfg->unified_memory = 2;
+
   // The following are dummy sizes that mean the concrete defaults
   // will be set during initialisation via hardware-inspection-based
   // heuristics.
@@ -430,6 +434,10 @@
 void futhark_context_config_load_binary_from(struct futhark_context_config *cfg, const char *path) {
   free(cfg->load_binary_from);
   cfg->load_binary_from = strdup(path);
+}
+
+void futhark_context_config_set_unified_memory(struct futhark_context_config* cfg, int flag) {
+  cfg->unified_memory = flag;
 }
 
 void futhark_context_config_set_default_thread_block_size(struct futhark_context_config *cfg, int size) {
diff --git a/src/Futhark/Analysis/Interference.hs b/src/Futhark/Analysis/Interference.hs
--- a/src/Futhark/Analysis/Interference.hs
+++ b/src/Futhark/Analysis/Interference.hs
@@ -327,14 +327,6 @@
     helper stm =
       inScopeOf stm $ pure mempty
 
-nameInfoToMemInfo :: (Mem rep inner) => NameInfo rep -> MemBound NoUniqueness
-nameInfoToMemInfo info =
-  case info of
-    FParamName summary -> noUniquenessReturns summary
-    LParamName summary -> summary
-    LetName summary -> letDecMem summary
-    IndexName it -> MemPrim $ IntType it
-
 memInfo :: (LocalScope GPUMem m) => VName -> m (Maybe VName)
 memInfo vname = do
   summary <- asksScope (fmap nameInfoToMemInfo . M.lookup vname)
diff --git a/src/Futhark/Builder/Class.hs b/src/Futhark/Builder/Class.hs
--- a/src/Futhark/Builder/Class.hs
+++ b/src/Futhark/Builder/Class.hs
@@ -36,8 +36,7 @@
     FParamInfo rep ~ DeclType,
     LParamInfo rep ~ Type,
     RetType rep ~ DeclExtType,
-    BranchType rep ~ ExtType,
-    SetType (LetDec rep)
+    BranchType rep ~ ExtType
   ) =>
   Buildable rep
   where
diff --git a/src/Futhark/CLI/Check.hs b/src/Futhark/CLI/Check.hs
--- a/src/Futhark/CLI/Check.hs
+++ b/src/Futhark/CLI/Check.hs
@@ -7,12 +7,13 @@
 import Futhark.Util.Options
 import Futhark.Util.Pretty (hPutDoc)
 import Language.Futhark.Warnings
+import System.Exit
 import System.IO
 
-newtype CheckConfig = CheckConfig {checkWarn :: Bool}
+data CheckConfig = CheckConfig {checkWarn :: Bool, checkWerror :: Bool}
 
 newCheckConfig :: CheckConfig
-newCheckConfig = CheckConfig True
+newCheckConfig = CheckConfig True False
 
 options :: [FunOptDescr CheckConfig]
 options =
@@ -20,7 +21,12 @@
       "w"
       []
       (NoArg $ Right $ \cfg -> cfg {checkWarn = False})
-      "Disable all warnings."
+      "Disable all warnings.",
+    Option
+      []
+      ["Werror"]
+      (NoArg $ Right $ \cfg -> cfg {checkWerror = True})
+      "Treat warnings as errors."
   ]
 
 -- | Run @futhark check@.
@@ -29,8 +35,9 @@
   case args of
     [file] -> Just $ do
       (warnings, _, _) <- readProgramOrDie file
-      when (checkWarn cfg && anyWarnings warnings) $
-        liftIO $
-          hPutDoc stderr $
-            prettyWarnings warnings
+      when (checkWarn cfg && anyWarnings warnings) $ do
+        liftIO $ hPutDoc stderr $ prettyWarnings warnings
+        when (checkWerror cfg) $ do
+          hPutStrLn stderr "\nTreating above warnings as errors due to --Werror."
+          exitWith $ ExitFailure 2
     _ -> Nothing
diff --git a/src/Futhark/CLI/Dev.hs b/src/Futhark/CLI/Dev.hs
--- a/src/Futhark/CLI/Dev.hs
+++ b/src/Futhark/CLI/Dev.hs
@@ -24,6 +24,7 @@
 import Futhark.IR.Seq qualified as Seq
 import Futhark.IR.SeqMem qualified as SeqMem
 import Futhark.IR.TypeCheck (Checkable, checkProg)
+import Futhark.Internalise.ApplyTypeAbbrs as ApplyTypeAbbrs
 import Futhark.Internalise.Defunctionalise as Defunctionalise
 import Futhark.Internalise.Defunctorise as Defunctorise
 import Futhark.Internalise.FullNormalise as FullNormalise
@@ -203,41 +204,41 @@
   pure prog
 kernelsMemProg name rep =
   externalErrorS $
-    "Pass "
-      ++ name
-      ++ " expects GPUMem representation, but got "
-      ++ representation rep
+    "Pass '"
+      <> name
+      <> "' expects GPUMem representation, but got "
+      <> representation rep
 
 soacsProg :: String -> UntypedPassState -> FutharkM (Prog SOACS.SOACS)
 soacsProg _ (SOACS prog) =
   pure prog
 soacsProg name rep =
   externalErrorS $
-    "Pass "
-      ++ name
-      ++ " expects SOACS representation, but got "
-      ++ representation rep
+    "Pass '"
+      <> name
+      <> "' expects SOACS representation, but got "
+      <> representation rep
 
 kernelsProg :: String -> UntypedPassState -> FutharkM (Prog GPU.GPU)
 kernelsProg _ (GPU prog) =
   pure prog
 kernelsProg name rep =
   externalErrorS $
-    "Pass " ++ name ++ " expects GPU representation, but got " ++ representation rep
+    "Pass '" <> name <> "' expects GPU representation, but got " <> representation rep
 
 seqMemProg :: String -> UntypedPassState -> FutharkM (Prog SeqMem.SeqMem)
 seqMemProg _ (SeqMem prog) =
   pure prog
 seqMemProg name rep =
   externalErrorS $
-    "Pass " ++ name ++ " expects SeqMem representation, but got " ++ representation rep
+    "Pass '" <> name <> "' expects SeqMem representation, but got " <> representation rep
 
 mcMemProg :: String -> UntypedPassState -> FutharkM (Prog MCMem.MCMem)
 mcMemProg _ (MCMem prog) =
   pure prog
 mcMemProg name rep =
   externalErrorS $
-    "Pass " ++ name ++ " expects MCMem representation, but got " ++ representation rep
+    "Pass '" <> name <> "' expects MCMem representation, but got " <> representation rep
 
 typedPassOption ::
   (Checkable torep) =>
@@ -324,7 +325,7 @@
         <$> runPipeline (onePass MC.explicitAllocations) config prog
     perform s _ =
       externalErrorS $
-        "Pass '" ++ passDescription pass ++ "' cannot operate on " ++ representation s
+        "Pass '" <> passDescription pass <> "' cannot operate on " <> representation s
 
     long = [passLongOption pass]
     pass = Seq.explicitAllocations
@@ -723,42 +724,49 @@
                   else prettyString $ fileProg fm
         Defunctorise -> do
           (_, imports, src) <- readProgram'
-          liftIO $ p $ evalState (Defunctorise.transformProg imports) src
+          liftIO $
+            p $
+              flip evalState src $
+                Defunctorise.transformProg imports
+                  >>= ApplyTypeAbbrs.transformProg
         FullNormalise -> do
           (_, imports, src) <- readProgram'
           liftIO $
             p $
               flip evalState src $
                 Defunctorise.transformProg imports
+                  >>= ApplyTypeAbbrs.transformProg
                   >>= FullNormalise.transformProg
-        Monomorphise -> do
+        LiftLambdas -> do
           (_, imports, src) <- readProgram'
           liftIO $
             p $
               flip evalState src $
                 Defunctorise.transformProg imports
+                  >>= ApplyTypeAbbrs.transformProg
                   >>= FullNormalise.transformProg
-                  >>= Monomorphise.transformProg
-        LiftLambdas -> do
+                  >>= LiftLambdas.transformProg
+        Monomorphise -> do
           (_, imports, src) <- readProgram'
           liftIO $
             p $
               flip evalState src $
                 Defunctorise.transformProg imports
+                  >>= ApplyTypeAbbrs.transformProg
                   >>= FullNormalise.transformProg
-                  >>= Monomorphise.transformProg
-                  >>= ReplaceRecords.transformProg
                   >>= LiftLambdas.transformProg
+                  >>= Monomorphise.transformProg
         Defunctionalise -> do
           (_, imports, src) <- readProgram'
           liftIO $
             p $
               flip evalState src $
                 Defunctorise.transformProg imports
+                  >>= ApplyTypeAbbrs.transformProg
                   >>= FullNormalise.transformProg
+                  >>= LiftLambdas.transformProg
                   >>= Monomorphise.transformProg
                   >>= ReplaceRecords.transformProg
-                  >>= LiftLambdas.transformProg
                   >>= Defunctionalise.transformProg
         Pipeline {} -> do
           let (base, ext) = splitExtension file
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
@@ -1165,6 +1165,7 @@
 
   let run_options = scriptExtraOptions opts
       onLine "call" l = T.putStrLn l
+      onLine "startup" l = T.putStrLn l
       onLine _ _ = pure ()
       prog' = if is_fut then dropExtension prog else prog
       cfg =
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
@@ -587,11 +587,10 @@
                         { testStatusFail = testStatusFail ts' + 1,
                           testStatusRunPass =
                             testStatusRunPass ts'
-                              + numTestCases test
-                              - length s,
+                              + max 0 (numTestCases test - length s),
                           testStatusRunFail =
                             testStatusRunFail ts'
-                              + length s
+                              + min (numTestCases test) (length s)
                         }
 
   when fancy spaceTable
diff --git a/src/Futhark/CodeGen/Backends/GPU.hs b/src/Futhark/CodeGen/Backends/GPU.hs
--- a/src/Futhark/CodeGen/Backends/GPU.hs
+++ b/src/Futhark/CodeGen/Backends/GPU.hs
@@ -80,7 +80,7 @@
 
 compileBlockDim :: BlockDim -> GC.CompilerM op s C.Exp
 compileBlockDim (Left e) = GC.compileExp e
-compileBlockDim (Right kc) = pure $ kernelConstToExp kc
+compileBlockDim (Right e) = pure $ compileConstExp e
 
 genLaunchKernel ::
   KernelSafety ->
@@ -370,6 +370,13 @@
         optionArgument = RequiredArgument "INT",
         optionDescription = "The default parallelism threshold.",
         optionAction = [C.cstm|futhark_context_config_set_default_threshold(cfg, atoi(optarg));|]
+      },
+    Option
+      { optionLongName = "unified-memory",
+        optionShortName = Nothing,
+        optionArgument = RequiredArgument "INT",
+        optionDescription = "Whether to use unified memory",
+        optionAction = [C.cstm|futhark_context_config_set_unified_memory(cfg, atoi(optarg));|]
       }
   ]
 
@@ -462,3 +469,4 @@
   GC.headerDecl GC.InitDecl [C.cedecl|void futhark_context_config_set_default_tile_size(struct futhark_context_config *cfg, int size);|]
   GC.headerDecl GC.InitDecl [C.cedecl|void futhark_context_config_set_default_reg_tile_size(struct futhark_context_config *cfg, int size);|]
   GC.headerDecl GC.InitDecl [C.cedecl|void futhark_context_config_set_default_threshold(struct futhark_context_config *cfg, int size);|]
+  GC.headerDecl GC.InitDecl [C.cedecl|void futhark_context_config_set_unified_memory(struct futhark_context_config* cfg, int flag);|]
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
@@ -1,4 +1,5 @@
 {-# LANGUAGE QuasiQuotes #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
 
 -- | Translation of ImpCode Exp and Code to C.
 module Futhark.CodeGen.Backends.GenericC.Code
@@ -15,6 +16,7 @@
 where
 
 import Control.Monad
+import Control.Monad.Identity
 import Control.Monad.Reader (asks)
 import Data.Map qualified as M
 import Data.Maybe
@@ -44,9 +46,6 @@
   (formatstrs, formatargs) <- mapAndUnzipM onPart parts
   pure (mconcat formatstrs, formatargs)
 
-compileExp :: Exp -> CompilerM op s C.Exp
-compileExp = compilePrimExp $ \v -> pure [C.cexp|$id:v|]
-
 -- | Tell me how to compile a @v@, and I'll Compile any @PrimExp v@ for you.
 compilePrimExp :: (Monad m) => (v -> m C.Exp) -> PrimExp v -> m C.Exp
 compilePrimExp _ (ValueExp val) =
@@ -112,6 +111,14 @@
 compilePrimExp f (FunExp h args _) = do
   args' <- mapM (compilePrimExp f) args
   pure [C.cexp|$id:(funName (nameFromString h))($args:args')|]
+
+-- | Compile prim expression to C expression.
+compileExp :: Exp -> CompilerM op s C.Exp
+compileExp = compilePrimExp $ \v -> pure [C.cexp|$id:v|]
+
+instance C.ToExp (TExp t) where
+  toExp e _ =
+    runIdentity . compilePrimExp (\v -> pure [C.cexp|$id:v|]) $ untyped e
 
 linearCode :: Code op -> [Code op]
 linearCode = reverse . go []
diff --git a/src/Futhark/CodeGen/Backends/GenericC/Types.hs b/src/Futhark/CodeGen/Backends/GenericC/Types.hs
--- a/src/Futhark/CodeGen/Backends/GenericC/Types.hs
+++ b/src/Futhark/CodeGen/Backends/GenericC/Types.hs
@@ -89,16 +89,11 @@
       [C.cexp|((size_t)$exp:arr_size) * $int:(primByteSize pt::Int)|]
 
   new_raw_body <- collect $ do
-    prepare_new
-    copy
-      CopyNoBarrier
-      [C.cexp|arr->mem.mem|]
-      [C.cexp|0|]
-      space
-      [C.cexp|data|]
-      [C.cexp|offset|]
-      space
-      [C.cexp|((size_t)$exp:arr_size) * $int:(primByteSize pt::Int)|]
+    resetMem [C.cexp|arr->mem|] space
+    stm [C.cstm|arr->mem.mem = data;|]
+    forM_ [0 .. rank - 1] $ \i ->
+      let dim_s = "dim" ++ show i
+       in stm [C.cstm|arr->shape[$int:i] = $id:dim_s;|]
 
   free_body <- collect $ unRefMem [C.cexp|arr->mem|] space
 
@@ -126,7 +121,7 @@
   proto
     [C.cedecl|$ty:array_type* $id:new_array($ty:ctx_ty *ctx, const $ty:pt' *data, $params:shape_params);|]
   proto
-    [C.cedecl|$ty:array_type* $id:new_raw_array($ty:ctx_ty *ctx, $ty:memty data, typename int64_t offset, $params:shape_params);|]
+    [C.cedecl|$ty:array_type* $id:new_raw_array($ty:ctx_ty *ctx, $ty:memty data, $params:shape_params);|]
   proto
     [C.cedecl|int $id:free_array($ty:ctx_ty *ctx, $ty:array_type *arr);|]
   proto
@@ -154,7 +149,7 @@
             return arr;
           }
 
-          $ty:array_type* $id:new_raw_array($ty:ctx_ty *ctx, $ty:memty data, typename int64_t offset, $params:shape_params) {
+          $ty:array_type* $id:new_raw_array($ty:ctx_ty *ctx, $ty:memty data, $params:shape_params) {
             int err = 0;
             $ty:array_type* bad = NULL;
             $ty:array_type *arr = ($ty:array_type*) malloc(sizeof($ty:array_type));
@@ -193,7 +188,9 @@
       { Manifest.arrayFree = free_array,
         Manifest.arrayShape = shape_array,
         Manifest.arrayValues = values_array,
-        Manifest.arrayNew = new_array
+        Manifest.arrayNew = new_array,
+        Manifest.arrayNewRaw = new_raw_array,
+        Manifest.arrayValuesRaw = values_raw_array
       }
 
 lookupOpaqueType :: Name -> OpaqueTypes -> OpaqueType
diff --git a/src/Futhark/CodeGen/Backends/PyOpenCL.hs b/src/Futhark/CodeGen/Backends/PyOpenCL.hs
--- a/src/Futhark/CodeGen/Backends/PyOpenCL.hs
+++ b/src/Futhark/CodeGen/Backends/PyOpenCL.hs
@@ -5,6 +5,7 @@
 where
 
 import Control.Monad
+import Control.Monad.Identity
 import Data.Map qualified as M
 import Data.Text qualified as T
 import Futhark.CodeGen.Backends.GenericPython hiding (compileProg)
@@ -212,9 +213,12 @@
 kernelConstToExp (Imp.SizeMaxConst size_class) =
   Var $ "self.max_" <> prettyString size_class
 
+compileConstExp :: Imp.KernelConstExp -> PyExp
+compileConstExp e = runIdentity $ compilePrimExp (pure . kernelConstToExp) e
+
 compileBlockDim :: Imp.BlockDim -> CompilerM op s PyExp
 compileBlockDim (Left e) = asLong <$> compileExp e
-compileBlockDim (Right kc) = pure $ kernelConstToExp kc
+compileBlockDim (Right e) = pure $ compileConstExp e
 
 callKernel :: OpCompiler Imp.OpenCL ()
 callKernel (Imp.GetSize v key) = do
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
@@ -50,7 +50,7 @@
   deriving (Show)
 
 -- | The size of one dimension of a block.
-type BlockDim = Either Exp KernelConst
+type BlockDim = Either Exp KernelConstExp
 
 -- | A generic kernel containing arbitrary kernel code.
 data Kernel = Kernel
@@ -145,9 +145,9 @@
         ( "blocks"
             <+> brace (pretty $ kernelNumBlocks kernel)
             </> "tblock_size"
-            <+> brace (list $ map (either pretty pretty) $ kernelBlockSize kernel)
+            <+> brace (list $ map pSize $ kernelBlockSize kernel)
             </> "uses"
-            <+> brace (commasep $ map pretty $ kernelUses kernel)
+            <+> brace (stack $ map pretty $ kernelUses kernel)
             </> "failure_tolerant"
             <+> brace (pretty $ kernelFailureTolerant kernel)
             </> "check_shared_memory"
@@ -155,6 +155,9 @@
             </> "body"
             <+> brace (pretty $ kernelBody kernel)
         )
+    where
+      pSize (Left x) = "dyn" <+> pretty x
+      pSize (Right x) = "const" <+> pretty x
 
 -- | When we do a barrier or fence, is it at the local or global
 -- level?  By the 'Ord' instance, global is greater than local.
@@ -313,6 +316,7 @@
 
 instance FreeIn KernelOp where
   freeIn' (Atomic _ op) = freeIn' op
+  freeIn' (SharedAlloc _ size) = freeIn' size
   freeIn' _ = mempty
 
 brace :: Doc a -> Doc a
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
@@ -400,7 +400,7 @@
 -- | Emit a warning about something the user should be aware of.
 warn :: (Located loc) => loc -> [loc] -> T.Text -> ImpM rep r op ()
 warn loc locs problem =
-  warnings $ singleWarning' (srclocOf loc) (map srclocOf locs) (pretty problem)
+  warnings $ singleWarning' (locOf loc) (map locOf locs) (pretty problem)
 
 -- | Emit a function in the generated code.
 emitFunction :: Name -> Imp.Function op -> ImpM rep r op ()
@@ -775,7 +775,10 @@
 caseMatch :: [SubExp] -> [Maybe PrimValue] -> Imp.TExp Bool
 caseMatch ses vs = foldl (.&&.) true (zipWith cmp ses vs)
   where
-    cmp se (Just v) = isBool $ toExp' (primValueType v) se ~==~ ValueExp v
+    cmp se (Just (BoolValue True)) =
+      isBool $ toExp' Bool se
+    cmp se (Just v) =
+      isBool $ toExp' (primValueType v) se ~==~ ValueExp v
     cmp _ Nothing = true
 
 defCompileExp ::
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
@@ -975,7 +975,7 @@
 
   let set_constants = do
         dPrim_ local_tid int32
-        dPrim_ inner_tblock_size int64
+        dPrim_ inner_tblock_size int32
         dPrim_ wave_size int32
         dPrim_ tblock_id int32
 
@@ -1227,7 +1227,7 @@
       x <- isConstExp vtable $ untyped e
       pure $
         case x of
-          Just (LeafExp kc _) -> Right kc
+          Just kc -> Right kc
           _ -> Left $ untyped e
 
     constToUse (v, e) = Imp.ConstUse v e
diff --git a/src/Futhark/CodeGen/ImpGen/GPU/SegHist.hs b/src/Futhark/CodeGen/ImpGen/GPU/SegHist.hs
--- a/src/Futhark/CodeGen/ImpGen/GPU/SegHist.hs
+++ b/src/Futhark/CodeGen/ImpGen/GPU/SegHist.hs
@@ -709,10 +709,13 @@
         sComment "initialize histograms in shared memory" $
           onAllHistograms $ \dest_local dest_global op ne local_subhisto_i global_subhisto_i local_bucket_is global_bucket_is ->
             sComment "First subhistogram is initialised from global memory; others with neutral element." $ do
+              dest_global_shape <- map pe64 . arrayDims <$> lookupType dest_global
               let global_is = map Imp.le64 segment_is ++ [0] ++ global_bucket_is
                   local_is = sExt64 local_subhisto_i : local_bucket_is
+                  global_in_bounds =
+                    inBounds (Slice (map DimFix global_is)) dest_global_shape
               sIf
-                (global_subhisto_i .==. 0)
+                (global_subhisto_i .==. 0 .&&. global_in_bounds)
                 (copyDWIMFix dest_local local_is (Var dest_global) global_is)
                 ( sLoopNest (histOpShape op) $ \is ->
                     copyDWIMFix dest_local (local_is ++ is) ne []
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
@@ -14,6 +14,7 @@
 import Control.Monad.State
 import Data.Bifunctor (second)
 import Data.Foldable (toList)
+import Data.List qualified as L
 import Data.Map.Strict qualified as M
 import Data.Maybe
 import Data.Set qualified as S
@@ -30,7 +31,7 @@
 import Futhark.CodeGen.RTS.OpenCL (copyCL, preludeCL, transposeCL)
 import Futhark.Error (compilerLimitationS)
 import Futhark.MonadFreshNames
-import Futhark.Util (mapAccumLM, zEncodeText)
+import Futhark.Util (zEncodeText)
 import Futhark.Util.IntegralExp (rem)
 import Language.C.Quote.OpenCL qualified as C
 import Language.C.Syntax qualified as C
@@ -330,13 +331,11 @@
     toDevice :: HostOp -> KernelOp
     toDevice _ = bad
 
-isConst :: BlockDim -> Maybe T.Text
+isConst :: BlockDim -> Maybe KernelConstExp
 isConst (Left (ValueExp (IntValue x))) =
-  Just $ prettyText $ intToInt64 x
-isConst (Right (SizeConst v _)) =
-  Just $ zEncodeText $ nameToText v
-isConst (Right (SizeMaxConst size_class)) =
-  Just $ "max_" <> prettyText size_class
+  Just $ ValueExp (IntValue x)
+isConst (Right e) =
+  Just e
 isConst _ = Nothing
 
 onKernel :: KernelTarget -> Kernel -> OnKernelM OpenCL
@@ -359,11 +358,9 @@
       (kernel_consts, (const_defs, const_undefs)) =
         second unzip $ unzip $ mapMaybe (constDef (kernelName kernel)) $ kernelUses kernel
 
-  let (shared_memory_bytes, (shared_memory_params, shared_memory_args, shared_memory_init)) =
-        second unzip3 $
-          evalState
-            (mapAccumLM prepareSharedMemory 0 (kernelSharedMemory kstate))
-            blankNameSource
+  let (_, shared_memory_init) =
+        L.mapAccumL prepareSharedMemory [C.cexp|0|] (kernelSharedMemory kstate)
+      shared_memory_bytes = sum $ map (padTo8 . snd) $ kernelSharedMemory kstate
 
   let (use_params, unpack_params) =
         unzip $ mapMaybe useAsParam $ kernelUses kernel
@@ -429,18 +426,32 @@
       params =
         shared_memory_param
           ++ take (numFailureParams safety) failure_params
-          ++ shared_memory_params
           ++ use_params
 
-      attribute =
+      (attribute_consts, attribute) =
         case mapM isConst $ kernelBlockSize kernel of
           Just [x, y, z] ->
-            "FUTHARK_KERNEL_SIZED" <> prettyText (x, y, z) <> "\n"
+            ( [(xv, x), (yv, y), (zv, z)],
+              "FUTHARK_KERNEL_SIZED" <> prettyText (xv, yv, zv) <> "\n"
+            )
+            where
+              xv = nameFromText $ zEncodeText $ nameToText name <> "_dim1"
+              yv = nameFromText $ zEncodeText $ nameToText name <> "_dim2"
+              zv = nameFromText $ zEncodeText $ nameToText name <> "_dim3"
           Just [x, y] ->
-            "FUTHARK_KERNEL_SIZED" <> prettyText (x, y, 1 :: Int) <> "\n"
+            ( [(xv, x), (yv, y)],
+              "FUTHARK_KERNEL_SIZED" <> prettyText (xv, yv, 1 :: Int) <> "\n"
+            )
+            where
+              xv = nameFromText $ zEncodeText $ nameToText name <> "_dim1"
+              yv = nameFromText $ zEncodeText $ nameToText name <> "_dim2"
           Just [x] ->
-            "FUTHARK_KERNEL_SIZED" <> prettyText (x, 1 :: Int, 1 :: Int) <> "\n"
-          _ -> "FUTHARK_KERNEL\n"
+            ( [(xv, x)],
+              "FUTHARK_KERNEL_SIZED" <> prettyText (xv, 1 :: Int, 1 :: Int) <> "\n"
+            )
+            where
+              xv = nameFromText $ zEncodeText $ nameToText name <> "_dim1"
+          _ -> (mempty, "FUTHARK_KERNEL\n")
 
       kernel_fun =
         attribute
@@ -449,7 +460,7 @@
                     $items:(mconcat unpack_params)
                     $items:const_defs
                     $items:prepare_shared_memory
-                    $items:shared_memory_init
+                    $items:(mconcat shared_memory_init)
                     $items:error_init
                     $items:kernel_body
 
@@ -462,11 +473,11 @@
       { clGPU = M.insert name (safety, kernel_fun) $ clGPU s,
         clUsedTypes = typesInKernel kernel <> clUsedTypes s,
         clFailures = kernelFailures kstate,
-        clConstants = kernel_consts <> clConstants s
+        clConstants = attribute_consts <> kernel_consts <> clConstants s
       }
 
   -- The error handling stuff is automatically added later.
-  let args = shared_memory_args ++ kernelArgs kernel
+  let args = kernelArgs kernel
 
   pure $ LaunchKernel safety name shared_memory_bytes args num_tblocks tblock_size
   where
@@ -475,16 +486,14 @@
     tblock_size = kernelBlockSize kernel
     padTo8 e = e + ((8 - (e `rem` 8)) `rem` 8)
 
-    prepareSharedMemory (Count offset) (mem, Count size) = do
-      param <- newVName $ baseString mem ++ "_offset"
-      let offset' = offset + padTo8 size
-      pure
-        ( bytes offset',
-          ( [C.cparam|typename int64_t $id:param|],
-            ValueKArg (untyped offset) $ IntType Int64,
-            [C.citem|volatile __local $ty:defaultMemBlockType $id:mem = &shared_mem[$id:param];|]
+    prepareSharedMemory offset (mem, Count size) =
+      let offset_v = nameFromText $ prettyText mem <> "_offset"
+       in ( [C.cexp|$id:offset_v|],
+            [C.citems|
+             volatile __local $ty:defaultMemBlockType $id:mem = &shared_mem[$exp:offset];
+             const typename int64_t $id:offset_v = $exp:offset + $exp:(padTo8 size);
+             |]
           )
-        )
 
 useAsParam :: KernelUse -> Maybe (C.Param, [C.BlockItem])
 useAsParam (ScalarUse name pt) = do
diff --git a/src/Futhark/Compiler/Program.hs b/src/Futhark/Compiler/Program.hs
--- a/src/Futhark/Compiler/Program.hs
+++ b/src/Futhark/Compiler/Program.hs
@@ -300,7 +300,7 @@
               NE.:| map warningToError (listWarnings prog_ws)
         (prog_ws, Right (m, src')) ->
           let warnHole (loc, t) =
-                singleWarning (E.srclocOf loc) $ "Hole of type: " <> align (pretty t)
+                singleWarning (E.locOf loc) $ "Hole of type: " <> align (pretty t)
               prog_ws' = prog_ws <> foldMap warnHole (E.progHoles (fileProg m))
            in Right
                 ( imports ++ [LoadedFile path import_name (CheckedFile src prog_ws' m) mod_time],
diff --git a/src/Futhark/Construct.hs b/src/Futhark/Construct.hs
--- a/src/Futhark/Construct.hs
+++ b/src/Futhark/Construct.hs
@@ -688,7 +688,7 @@
   ( ExpDec rep ~ (),
     LetDec rep ~ Type,
     MonadFreshNames m,
-    TypedOp (Op rep),
+    TypedOp (OpC rep),
     HasScope rep m
   ) =>
   [VName] ->
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
@@ -20,7 +20,7 @@
 import Futhark.Version
 import Language.Futhark
 import Language.Futhark.Semantic
-import Language.Futhark.TypeChecker.Monad hiding (warn)
+import Language.Futhark.Warnings
 import System.FilePath (makeRelative, splitPath, (-<.>), (</>))
 import Text.Blaze.Html5 (AttributeValue, Html, toHtml, (!))
 import Text.Blaze.Html5 qualified as H
@@ -85,7 +85,7 @@
 -- can generate an index.
 type Documented = M.Map VName IndexWhat
 
-warn :: SrcLoc -> Doc () -> DocM ()
+warn :: Loc -> Doc () -> DocM ()
 warn loc s = lift $ lift $ tell $ singleWarning loc s
 
 document :: VName -> IndexWhat -> DocM ()
@@ -628,7 +628,7 @@
     specRow (keyword "module " <> vnameSynopsisDef name) ": " <$> synopsisModTypeExp sig
   IncludeSpec e _ -> fullRow . (keyword "include " <>) <$> synopsisModTypeExp e
 
-typeExpHtml :: TypeExp Info VName -> DocM Html
+typeExpHtml :: TypeExp Exp VName -> DocM Html
 typeExpHtml e = case e of
   TEUnique t _ -> ("*" <>) <$> typeExpHtml t
   TEArray d at _ -> do
@@ -709,11 +709,11 @@
 dimDeclHtml :: Size -> DocM Html
 dimDeclHtml = pure . brackets . toHtml . prettyString
 
-dimExpHtml :: SizeExp Info VName -> DocM Html
+dimExpHtml :: SizeExp Exp -> DocM Html
 dimExpHtml (SizeExpAny _) = pure $ brackets mempty
 dimExpHtml (SizeExp e _) = pure $ brackets $ toHtml $ prettyString e
 
-typeArgExpHtml :: TypeArgExp Info VName -> DocM Html
+typeArgExpHtml :: TypeArgExp Exp VName -> DocM Html
 typeArgExpHtml (TypeArgExpSize d) = dimExpHtml d
 typeArgExpHtml (TypeArgExpType d) = typeExpHtml d
 
@@ -734,10 +734,10 @@
   H.preEscapedText
     . GFM.commonmarkToHtml [] [GFM.extAutolink]
     . T.pack
-    <$> identifierLinks loc (T.unpack doc)
+    <$> identifierLinks (locOf loc) (T.unpack doc)
 docHtml Nothing = pure mempty
 
-identifierLinks :: SrcLoc -> String -> DocM String
+identifierLinks :: Loc -> String -> DocM String
 identifierLinks _ [] = pure []
 identifierLinks loc s
   | Just ((name, namespace, file), s') <- identifierReference s = do
diff --git a/src/Futhark/IR/Aliases.hs b/src/Futhark/IR/Aliases.hs
--- a/src/Futhark/IR/Aliases.hs
+++ b/src/Futhark/IR/Aliases.hs
@@ -1,6 +1,5 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
-{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
 
 -- | A representation where all patterns are annotated with aliasing
 -- information.  It also records consumption of variables in bodies.
@@ -132,22 +131,28 @@
 
 instance
   ( ASTRep rep,
-    AliasedOp (OpC rep (Aliases rep)),
-    IsOp (OpC rep (Aliases rep))
+    AliasedOp (OpC rep),
+    ASTConstraints (OpC rep (Aliases rep))
   ) =>
   ASTRep (Aliases rep)
   where
   expTypesFromPat =
     withoutAliases . expTypesFromPat . removePatAliases
 
-instance (ASTRep rep, AliasedOp (OpC rep (Aliases rep))) => Aliased (Aliases rep) where
+instance
+  ( ASTRep rep,
+    AliasedOp (OpC rep),
+    ASTConstraints (OpC rep (Aliases rep))
+  ) =>
+  Aliased (Aliases rep)
+  where
   bodyAliases = map unAliases . fst . fst . bodyDec
   consumedInBody = unAliases . snd . fst . bodyDec
 
 instance
   ( ASTRep rep,
-    AliasedOp (OpC rep (Aliases rep)),
-    Pretty (OpC rep (Aliases rep))
+    AliasedOp (OpC rep),
+    ASTConstraints (OpC rep (Aliases rep))
   ) =>
   PrettyRep (Aliases rep)
   where
@@ -264,7 +269,7 @@
 -- | Augment a body decoration with aliasing information provided by
 -- the statements and result of that body.
 mkAliasedBody ::
-  (ASTRep rep, AliasedOp (OpC rep (Aliases rep))) =>
+  (ASTRep rep, AliasedOp (OpC rep), ASTConstraints (OpC rep (Aliases rep))) =>
   BodyDec rep ->
   Stms (Aliases rep) ->
   Result ->
@@ -370,7 +375,7 @@
     look k = M.findWithDefault mempty k aliasmap
 
 mkAliasedStm ::
-  (ASTRep rep, AliasedOp (OpC rep (Aliases rep))) =>
+  (ASTRep rep, AliasedOp (OpC rep), ASTConstraints (OpC rep (Aliases rep))) =>
   Pat (LetDec rep) ->
   StmAux (ExpDec rep) ->
   Exp (Aliases rep) ->
@@ -381,7 +386,13 @@
     (StmAux cs attrs (AliasDec $ consumedInExp e, dec))
     e
 
-instance (Buildable rep, AliasedOp (OpC rep (Aliases rep))) => Buildable (Aliases rep) where
+instance
+  ( Buildable rep,
+    AliasedOp (OpC rep),
+    ASTConstraints (OpC rep (Aliases rep))
+  ) =>
+  Buildable (Aliases rep)
+  where
   mkExpDec pat e =
     let dec = mkExpDec (removePatAliases pat) $ removeExpAliases e
      in (AliasDec $ consumedInExp e, dec)
@@ -401,7 +412,7 @@
 
 instance
   ( ASTRep rep,
-    AliasedOp (OpC rep (Aliases rep)),
+    AliasedOp (OpC rep),
     Buildable (Aliases rep)
   ) =>
   BuilderOps (Aliases rep)
@@ -411,7 +422,8 @@
   ( ASTRep rep,
     RephraseOp (OpC rep),
     CanBeAliased (OpC rep),
-    AliasedOp (OpC rep (Aliases rep))
+    AliasedOp (OpC rep),
+    ASTConstraints (OpC rep (Aliases rep))
   )
 
 -- | The class of operations that can be given aliasing information.
diff --git a/src/Futhark/IR/GPU/Op.hs b/src/Futhark/IR/GPU/Op.hs
--- a/src/Futhark/IR/GPU/Op.hs
+++ b/src/Futhark/IR/GPU/Op.hs
@@ -32,6 +32,7 @@
 import Futhark.IR
 import Futhark.IR.Aliases (Aliases, CanBeAliased (..))
 import Futhark.IR.GPU.Sizes
+import Futhark.IR.Mem (OpReturns (..), extReturns)
 import Futhark.IR.Prop.Aliases
 import Futhark.IR.SegOp
 import Futhark.IR.TypeCheck qualified as TC
@@ -196,21 +197,6 @@
     CalcNumBlocks <$> rename w <*> pure max_num_tblocks <*> rename tblock_size
   rename x = pure x
 
-instance IsOp SizeOp where
-  safeOp _ = True
-  cheapOp _ = True
-  opDependencies op = [freeIn op]
-
-instance TypedOp SizeOp where
-  opType (GetSize _ _) = pure [Prim int64]
-  opType (GetSizeMax _) = pure [Prim int64]
-  opType CmpSizeLe {} = pure [Prim Bool]
-  opType CalcNumBlocks {} = pure [Prim int64]
-
-instance AliasedOp SizeOp where
-  opAliases _ = [mempty]
-  consumedInOp _ = mempty
-
 instance FreeIn SizeOp where
   freeIn' (CmpSizeLe _ _ x) = freeIn' x
   freeIn' (CalcNumBlocks w _ tblock_size) = freeIn' w <> freeIn' tblock_size
@@ -282,15 +268,15 @@
   rename (SizeOp op) = SizeOp <$> rename op
   rename (GPUBody ts body) = GPUBody <$> rename ts <*> rename body
 
-instance (ASTRep rep, IsOp (op rep)) => IsOp (HostOp op rep) where
+instance (IsOp op) => IsOp (HostOp op) where
   safeOp (SegOp op) = safeOp op
   safeOp (OtherOp op) = safeOp op
-  safeOp (SizeOp op) = safeOp op
+  safeOp (SizeOp _) = True
   safeOp (GPUBody _ body) = all (safeExp . stmExp) $ bodyStms body
 
   cheapOp (SegOp op) = cheapOp op
   cheapOp (OtherOp op) = cheapOp op
-  cheapOp (SizeOp op) = cheapOp op
+  cheapOp (SizeOp _) = True
   cheapOp (GPUBody types body) =
     -- Current GPUBody usage only benefits from hoisting kernels that
     -- transfer scalars to device.
@@ -298,26 +284,29 @@
 
   opDependencies (SegOp op) = opDependencies op
   opDependencies (OtherOp op) = opDependencies op
-  opDependencies op@(SizeOp {}) = [freeIn op]
+  opDependencies (SizeOp op) = [freeIn op]
   opDependencies (GPUBody _ body) =
     replicate (length . bodyResult $ body) (freeIn body)
 
-instance (TypedOp (op rep)) => TypedOp (HostOp op rep) where
+instance (TypedOp op) => TypedOp (HostOp op) where
   opType (SegOp op) = opType op
   opType (OtherOp op) = opType op
-  opType (SizeOp op) = opType op
+  opType (SizeOp (GetSize _ _)) = pure [Prim int64]
+  opType (SizeOp (GetSizeMax _)) = pure [Prim int64]
+  opType (SizeOp CmpSizeLe {}) = pure [Prim Bool]
+  opType (SizeOp (CalcNumBlocks {})) = pure [Prim int64]
   opType (GPUBody ts _) =
     pure $ staticShapes $ map (`arrayOfRow` intConst Int64 1) ts
 
-instance (Aliased rep, AliasedOp (op rep)) => AliasedOp (HostOp op rep) where
+instance (AliasedOp op) => AliasedOp (HostOp op) where
   opAliases (SegOp op) = opAliases op
   opAliases (OtherOp op) = opAliases op
-  opAliases (SizeOp op) = opAliases op
+  opAliases (SizeOp _) = [mempty]
   opAliases (GPUBody ts _) = map (const mempty) ts
 
   consumedInOp (SegOp op) = consumedInOp op
   consumedInOp (OtherOp op) = consumedInOp op
-  consumedInOp (SizeOp op) = consumedInOp op
+  consumedInOp (SizeOp _) = mempty
   consumedInOp (GPUBody _ body) = consumedInBody body
 
 instance (ASTRep rep, FreeIn (op rep)) => FreeIn (HostOp op rep) where
@@ -337,6 +326,10 @@
   addOpWisdom (OtherOp op) = OtherOp $ addOpWisdom op
   addOpWisdom (SizeOp op) = SizeOp op
   addOpWisdom (GPUBody ts body) = GPUBody ts $ informBody body
+
+instance OpReturns (HostOp NoOp) where
+  opReturns (SegOp op) = segOpReturns op
+  opReturns k = extReturns <$> opType k
 
 instance (ASTRep rep, ST.IndexOp (op rep)) => ST.IndexOp (HostOp op rep) where
   indexOp vtable k (SegOp op) is = ST.indexOp vtable k op is
diff --git a/src/Futhark/IR/GPUMem.hs b/src/Futhark/IR/GPUMem.hs
--- a/src/Futhark/IR/GPUMem.hs
+++ b/src/Futhark/IR/GPUMem.hs
@@ -40,18 +40,6 @@
 instance ASTRep GPUMem where
   expTypesFromPat = pure . map snd . bodyReturnsFromPat
 
-instance OpReturns (HostOp NoOp GPUMem) where
-  opReturns (SegOp op) = segOpReturns op
-  opReturns k = extReturns <$> opType k
-
-instance OpReturns (HostOp NoOp (Aliases GPUMem)) where
-  opReturns (SegOp op) = segOpReturns op
-  opReturns k = extReturns <$> opType k
-
-instance OpReturns (HostOp NoOp (Engine.Wise GPUMem)) where
-  opReturns (SegOp op) = segOpReturns op
-  opReturns k = extReturns <$> opType k
-
 instance PrettyRep GPUMem
 
 instance TC.Checkable GPUMem where
diff --git a/src/Futhark/IR/MC/Op.hs b/src/Futhark/IR/MC/Op.hs
--- a/src/Futhark/IR/MC/Op.hs
+++ b/src/Futhark/IR/MC/Op.hs
@@ -19,6 +19,7 @@
 import Futhark.Analysis.SymbolTable qualified as ST
 import Futhark.IR
 import Futhark.IR.Aliases (Aliases, CanBeAliased (..))
+import Futhark.IR.Mem (OpReturns (..))
 import Futhark.IR.Prop.Aliases
 import Futhark.IR.SegOp
 import Futhark.IR.TypeCheck qualified as TC
@@ -71,7 +72,7 @@
   freeIn' (ParOp par_op op) = freeIn' par_op <> freeIn' op
   freeIn' (OtherOp op) = freeIn' op
 
-instance (ASTRep rep, IsOp (op rep)) => IsOp (MCOp op rep) where
+instance (IsOp op) => IsOp (MCOp op) where
   safeOp (ParOp _ op) = safeOp op
   safeOp (OtherOp op) = safeOp op
 
@@ -81,11 +82,11 @@
   opDependencies (ParOp _ op) = opDependencies op
   opDependencies (OtherOp op) = opDependencies op
 
-instance (TypedOp (op rep)) => TypedOp (MCOp op rep) where
+instance (TypedOp op) => TypedOp (MCOp op) where
   opType (ParOp _ op) = opType op
   opType (OtherOp op) = opType op
 
-instance (Aliased rep, AliasedOp (op rep)) => AliasedOp (MCOp op rep) where
+instance (AliasedOp op) => AliasedOp (MCOp op) where
   opAliases (ParOp _ op) = opAliases op
   opAliases (OtherOp op) = opAliases op
 
@@ -107,6 +108,10 @@
 instance (ASTRep rep, ST.IndexOp (op rep)) => ST.IndexOp (MCOp op rep) where
   indexOp vtable k (ParOp _ op) is = ST.indexOp vtable k op is
   indexOp vtable k (OtherOp op) is = ST.indexOp vtable k op is
+
+instance OpReturns (MCOp NoOp) where
+  opReturns (ParOp _ op) = segOpReturns op
+  opReturns (OtherOp NoOp) = pure []
 
 instance (PrettyRep rep, Pretty (op rep)) => Pretty (MCOp op rep) where
   pretty (ParOp Nothing op) = pretty op
diff --git a/src/Futhark/IR/MCMem.hs b/src/Futhark/IR/MCMem.hs
--- a/src/Futhark/IR/MCMem.hs
+++ b/src/Futhark/IR/MCMem.hs
@@ -14,7 +14,6 @@
 where
 
 import Futhark.Analysis.PrimExp.Convert
-import Futhark.IR.Aliases (Aliases)
 import Futhark.IR.MC.Op
 import Futhark.IR.Mem
 import Futhark.IR.Mem.Simplify
@@ -36,18 +35,6 @@
 
 instance ASTRep MCMem where
   expTypesFromPat = pure . map snd . bodyReturnsFromPat
-
-instance OpReturns (MCOp NoOp MCMem) where
-  opReturns (ParOp _ op) = segOpReturns op
-  opReturns (OtherOp NoOp) = pure []
-
-instance OpReturns (MCOp NoOp (Aliases MCMem)) where
-  opReturns (ParOp _ op) = segOpReturns op
-  opReturns (OtherOp NoOp) = pure []
-
-instance OpReturns (MCOp NoOp (Engine.Wise MCMem)) where
-  opReturns (ParOp _ op) = segOpReturns op
-  opReturns k = extReturns <$> opType k
 
 instance PrettyRep MCMem
 
diff --git a/src/Futhark/IR/Mem.hs b/src/Futhark/IR/Mem.hs
--- a/src/Futhark/IR/Mem.hs
+++ b/src/Futhark/IR/Mem.hs
@@ -76,6 +76,7 @@
     varReturns,
     expReturns,
     extReturns,
+    nameInfoToMemInfo,
     lookupMemInfo,
     subExpMemInfo,
     lookupArraySummary,
@@ -166,9 +167,11 @@
     RetType rep ~ RetTypeMem,
     BranchType rep ~ BranchTypeMem,
     ASTRep rep,
-    OpReturns (inner rep),
+    OpReturns inner,
     RephraseOp inner,
-    Op rep ~ MemOp inner rep
+    ASTConstraints (inner rep),
+    FreeIn (inner rep),
+    OpC rep ~ MemOp inner
   )
 
 instance IsRetType FunReturns where
@@ -200,11 +203,11 @@
   freeIn' (Alloc size _) = freeIn' size
   freeIn' (Inner k) = freeIn' k
 
-instance (TypedOp (inner rep)) => TypedOp (MemOp inner rep) where
+instance (TypedOp inner) => TypedOp (MemOp inner) where
   opType (Alloc _ space) = pure [Mem space]
   opType (Inner k) = opType k
 
-instance (AliasedOp (inner rep)) => AliasedOp (MemOp inner rep) where
+instance (AliasedOp inner) => AliasedOp (MemOp inner) where
   opAliases Alloc {} = [mempty]
   opAliases (Inner k) = opAliases k
 
@@ -232,13 +235,13 @@
   opMetrics Alloc {} = seen "Alloc"
   opMetrics (Inner k) = opMetrics k
 
-instance (IsOp (inner rep)) => IsOp (MemOp inner rep) where
+instance (IsOp inner) => IsOp (MemOp inner) where
   safeOp (Alloc (Constant (IntValue (Int64Value k))) _) = k >= 0
   safeOp Alloc {} = False
   safeOp (Inner k) = safeOp k
   cheapOp (Inner k) = cheapOp k
   cheapOp Alloc {} = True
-  opDependencies op@(Alloc {}) = [freeIn op]
+  opDependencies (Alloc _ e) = [freeIn e]
   opDependencies (Inner op) = opDependencies op
 
 instance (CanBeWise inner) => CanBeWise (MemOp inner) where
@@ -852,6 +855,7 @@
     LParamName summary -> pure summary
     IndexName it -> pure $ MemPrim $ IntType it
 
+-- | Turn info into memory information.
 nameInfoToMemInfo :: (Mem rep inner) => NameInfo rep -> MemBound NoUniqueness
 nameInfoToMemInfo info =
   case info of
@@ -860,6 +864,7 @@
     LetName summary -> letDecMem summary
     IndexName it -> MemPrim $ IntType it
 
+-- | Look up information about the memory block with this name.
 lookupMemInfo ::
   (HasScope rep m, Mem rep inner) =>
   VName ->
@@ -1149,14 +1154,14 @@
     & pure
 
 class (IsOp op) => OpReturns op where
-  opReturns :: (Mem rep inner, Monad m, HasScope rep m) => op -> m [ExpReturns]
+  opReturns :: (Mem rep inner, Monad m, HasScope rep m) => op rep -> m [ExpReturns]
   opReturns op = extReturns <$> opType op
 
-instance (OpReturns (inner rep)) => OpReturns (MemOp inner rep) where
+instance (OpReturns inner) => OpReturns (MemOp inner) where
   opReturns (Alloc _ space) = pure [MemMem space]
   opReturns (Inner op) = opReturns op
 
-instance OpReturns (NoOp rep) where
+instance OpReturns NoOp where
   opReturns NoOp = pure []
 
 applyFunReturns ::
diff --git a/src/Futhark/IR/Mem/Simplify.hs b/src/Futhark/IR/Mem/Simplify.hs
--- a/src/Futhark/IR/Mem/Simplify.hs
+++ b/src/Futhark/IR/Mem/Simplify.hs
@@ -30,12 +30,13 @@
     BodyDec rep ~ (),
     CanBeWise (OpC rep),
     BuilderOps (Wise rep),
-    OpReturns (inner (Wise rep)),
+    OpReturns inner,
     ST.IndexOp (inner (Wise rep)),
-    AliasedOp (inner (Wise rep)),
+    AliasedOp inner,
     Mem rep inner,
     CanBeWise inner,
-    RephraseOp inner
+    RephraseOp inner,
+    ASTConstraints (inner (Engine.Wise rep))
   )
 
 simpleGeneric ::
diff --git a/src/Futhark/IR/Prop.hs b/src/Futhark/IR/Prop.hs
--- a/src/Futhark/IR/Prop.hs
+++ b/src/Futhark/IR/Prop.hs
@@ -76,7 +76,7 @@
 -- any required certificates have been checked) in any context.  For
 -- example, array indexing is not safe, as the index may be out of
 -- bounds.  On the other hand, adding two numbers cannot fail.
-safeExp :: (IsOp (Op rep)) => Exp rep -> Bool
+safeExp :: (ASTRep rep) => Exp rep -> Bool
 safeExp (BasicOp op) = safeBasicOp op
   where
     safeBasicOp (BinOp (SDiv _ Safe) _ _) = True
@@ -128,7 +128,7 @@
 safeExp WithAcc {} = True -- Although unlikely to matter.
 safeExp (Op op) = safeOp op
 
-safeBody :: (IsOp (Op rep)) => Body rep -> Bool
+safeBody :: (ASTRep rep) => Body rep -> Bool
 safeBody = all (safeExp . stmExp) . bodyStms
 
 -- | Return the variable names used in 'Var' subexpressions.  May contain
@@ -184,17 +184,17 @@
   (Eq a, Ord a, Show a, Rename a, Substitute a, FreeIn a, Pretty a)
 
 -- | A type class for operations.
-class (ASTConstraints op, TypedOp op) => IsOp op where
+class (TypedOp op) => IsOp op where
   -- | Like 'safeExp', but for arbitrary ops.
-  safeOp :: op -> Bool
+  safeOp :: (ASTRep rep) => op rep -> Bool
 
   -- | Should we try to hoist this out of branches?
-  cheapOp :: op -> Bool
+  cheapOp :: (ASTRep rep) => op rep -> Bool
 
   -- | Compute the data dependencies of an operation.
-  opDependencies :: op -> [Names]
+  opDependencies :: (ASTRep rep) => op rep -> [Names]
 
-instance IsOp (NoOp rep) where
+instance IsOp NoOp where
   safeOp NoOp = True
   cheapOp NoOp = True
   opDependencies NoOp = []
@@ -213,7 +213,8 @@
     FreeIn (LParamInfo rep),
     FreeIn (RetType rep),
     FreeIn (BranchType rep),
-    IsOp (Op rep),
+    ASTConstraints (OpC rep rep),
+    IsOp (OpC rep),
     RephraseOp (OpC rep)
   ) =>
   ASTRep rep
diff --git a/src/Futhark/IR/Prop/Aliases.hs b/src/Futhark/IR/Prop/Aliases.hs
--- a/src/Futhark/IR/Prop/Aliases.hs
+++ b/src/Futhark/IR/Prop/Aliases.hs
@@ -38,7 +38,7 @@
 import Futhark.IR.Syntax
 
 -- | The class of representations that contain aliasing information.
-class (ASTRep rep, AliasedOp (Op rep), AliasesOf (LetDec rep)) => Aliased rep where
+class (ASTRep rep, AliasedOp (OpC rep), AliasesOf (LetDec rep)) => Aliased rep where
   -- | The aliases of the body results.  Note that this includes names
   -- bound in the body!
   bodyAliases :: Body rep -> [Names]
@@ -222,10 +222,10 @@
 -- | The class of operations that can produce aliasing and consumption
 -- information.
 class (IsOp op) => AliasedOp op where
-  opAliases :: op -> [Names]
-  consumedInOp :: op -> Names
+  opAliases :: (Aliased rep) => op rep -> [Names]
+  consumedInOp :: (Aliased rep) => op rep -> Names
 
-instance AliasedOp (NoOp rep) where
+instance AliasedOp NoOp where
   opAliases NoOp = []
   consumedInOp NoOp = mempty
 
diff --git a/src/Futhark/IR/Prop/TypeOf.hs b/src/Futhark/IR/Prop/TypeOf.hs
--- a/src/Futhark/IR/Prop/TypeOf.hs
+++ b/src/Futhark/IR/Prop/TypeOf.hs
@@ -122,7 +122,7 @@
 
 -- | The type of an expression.
 expExtType ::
-  (HasScope rep m, TypedOp (Op rep)) =>
+  (HasScope rep m, TypedOp (OpC rep)) =>
   Exp rep ->
   m [ExtType]
 expExtType (Apply _ _ rt _) = pure $ map (fromDecl . declExtTypeOf . fst) rt
@@ -150,7 +150,7 @@
 -- | Any operation must define an instance of this class, which
 -- describes the type of the operation (at the value level).
 class TypedOp op where
-  opType :: (HasScope t m) => op -> m [ExtType]
+  opType :: (HasScope rep m) => op rep -> m [ExtType]
 
-instance TypedOp (NoOp rep) where
+instance TypedOp NoOp where
   opType NoOp = pure []
diff --git a/src/Futhark/IR/Prop/Types.hs b/src/Futhark/IR/Prop/Types.hs
--- a/src/Futhark/IR/Prop/Types.hs
+++ b/src/Futhark/IR/Prop/Types.hs
@@ -61,7 +61,6 @@
     DeclTyped (..),
     ExtTyped (..),
     DeclExtTyped (..),
-    SetType (..),
     FixExt (..),
   )
 where
@@ -598,20 +597,6 @@
 
 instance DeclExtTyped DeclExtType where
   declExtTypeOf = id
-
--- | Typeclass for things whose type can be changed.
-class (Typed a) => SetType a where
-  setType :: a -> Type -> a
-
-instance SetType Type where
-  setType _ t = t
-
-instance (SetType b) => SetType (a, b) where
-  setType (a, b) t = (a, setType b t)
-
-instance (SetType dec) => SetType (PatElem dec) where
-  setType (PatElem name dec) t =
-    PatElem name $ setType dec t
 
 -- | Something with an existential context that can be (partially)
 -- fixed.
diff --git a/src/Futhark/IR/SOACS/SOAC.hs b/src/Futhark/IR/SOACS/SOAC.hs
--- a/src/Futhark/IR/SOACS/SOAC.hs
+++ b/src/Futhark/IR/SOACS/SOAC.hs
@@ -531,10 +531,10 @@
 soacType (Screma w _arrs form) =
   scremaType w form
 
-instance (ASTRep rep) => TypedOp (SOAC rep) where
+instance TypedOp SOAC where
   opType = pure . staticShapes . soacType
 
-instance (Aliased rep) => AliasedOp (SOAC rep) where
+instance AliasedOp SOAC where
   opAliases = map (const mempty) . soacType
 
   consumedInOp JVP {} = mempty
@@ -590,7 +590,7 @@
       onRed red = red {redLambda = Alias.analyseLambda aliases $ redLambda red}
       onScan scan = scan {scanLambda = Alias.analyseLambda aliases $ scanLambda scan}
 
-instance (ASTRep rep) => IsOp (SOAC rep) where
+instance IsOp SOAC where
   safeOp _ = False
   cheapOp _ = False
   opDependencies (Stream w arrs accs lam) =
diff --git a/src/Futhark/IR/SegOp.hs b/src/Futhark/IR/SegOp.hs
--- a/src/Futhark/IR/SegOp.hs
+++ b/src/Futhark/IR/SegOp.hs
@@ -523,10 +523,10 @@
     dims = segSpaceDims space
     segment_dims = init dims
 
-instance TypedOp (SegOp lvl rep) where
+instance TypedOp (SegOp lvl) where
   opType = pure . staticShapes . segOpType
 
-instance (ASTConstraints lvl, Aliased rep) => AliasedOp (SegOp lvl rep) where
+instance (ASTConstraints lvl) => AliasedOp (SegOp lvl) where
   opAliases = map (const mempty) . segOpType
 
   consumedInOp (SegMap _ _ _ kbody) =
@@ -993,10 +993,7 @@
         | otherwise = lift Nothing
   indexOp _ _ _ _ = Nothing
 
-instance
-  (ASTRep rep, ASTConstraints lvl) =>
-  IsOp (SegOp lvl rep)
-  where
+instance (ASTConstraints lvl) => IsOp (SegOp lvl) where
   cheapOp _ = False
   safeOp _ = True
   opDependencies op = replicate (length (segOpType op)) (freeIn op)
@@ -1428,7 +1425,7 @@
 -- | Like 'segOpType', but for memory representations.
 segOpReturns ::
   (Mem rep inner, Monad m, HasScope rep m) =>
-  SegOp lvl somerep ->
+  SegOp lvl rep ->
   m [ExpReturns]
 segOpReturns k@(SegMap _ _ _ kbody) =
   kernelBodyReturns kbody . extReturns =<< opType k
diff --git a/src/Futhark/IR/TypeCheck.hs b/src/Futhark/IR/TypeCheck.hs
--- a/src/Futhark/IR/TypeCheck.hs
+++ b/src/Futhark/IR/TypeCheck.hs
@@ -1439,7 +1439,7 @@
     prettyText e <> " must have type " <> prettyText t
 
 -- | The class of representations that can be type-checked.
-class (AliasableRep rep, TypedOp (OpC rep (Aliases rep))) => Checkable rep where
+class (AliasableRep rep, TypedOp (OpC rep)) => Checkable rep where
   checkExpDec :: ExpDec rep -> TypeM rep ()
   checkBodyDec :: BodyDec rep -> TypeM rep ()
   checkFParamDec :: VName -> FParamInfo rep -> TypeM rep ()
diff --git a/src/Futhark/Internalise.hs b/src/Futhark/Internalise.hs
--- a/src/Futhark/Internalise.hs
+++ b/src/Futhark/Internalise.hs
@@ -1,5 +1,3 @@
-{-# LANGUAGE Strict #-}
-
 -- |
 --
 -- This module implements a transformation from source to core
@@ -21,6 +19,15 @@
 -- * The core IR has no modules.  These are removed in
 --   "Futhark.Internalise.Defunctorise".
 --
+-- * The core IR has no type abbreviations.  These are removed in
+--   "Futhark.Internalise.ApplyTypeAbbrs".
+--
+-- * The core IR has little syntactic niceties. A lot of syntactic
+--   sugar is removed in "Futhark.Internalise.FullNormalise".
+--
+-- * Lambda lifting is performed by "Futhark.Internalise.LiftLambdas",
+-- * mostly to make the job of later passes simpler.
+--
 -- * The core IR is monomorphic.  Polymorphic functions are monomorphised in
 --   "Futhark.Internalise.Monomorphise"
 --
@@ -44,6 +51,7 @@
 import Data.Text qualified as T
 import Futhark.Compiler.Config
 import Futhark.IR.SOACS as I hiding (stmPat)
+import Futhark.Internalise.ApplyTypeAbbrs as ApplyTypeAbbrs
 import Futhark.Internalise.Defunctionalise as Defunctionalise
 import Futhark.Internalise.Defunctorise as Defunctorise
 import Futhark.Internalise.Entry (visibleTypes)
@@ -65,19 +73,19 @@
   m (I.Prog SOACS)
 internaliseProg config prog = do
   maybeLog "Defunctorising"
-  prog_decs <- Defunctorise.transformProg prog
+  prog_decs0 <- ApplyTypeAbbrs.transformProg =<< Defunctorise.transformProg prog
   maybeLog "Full Normalising"
-  prog_decs' <- FullNormalise.transformProg prog_decs
+  prog_decs1 <- FullNormalise.transformProg prog_decs0
+  maybeLog "Lifting lambdas"
+  prog_decs2 <- LiftLambdas.transformProg prog_decs1
   maybeLog "Monomorphising"
-  prog_decs'' <- Monomorphise.transformProg prog_decs'
+  prog_decs3 <- Monomorphise.transformProg prog_decs2
   maybeLog "Replacing records"
-  prog_decs''' <- ReplaceRecords.transformProg prog_decs''
-  maybeLog "Lifting lambdas"
-  prog_decs'''' <- LiftLambdas.transformProg prog_decs'''
+  prog_decs4 <- ReplaceRecords.transformProg prog_decs3
   maybeLog "Defunctionalising"
-  prog_decs''''' <- Defunctionalise.transformProg prog_decs''''
+  prog_decs5 <- Defunctionalise.transformProg prog_decs4
   maybeLog "Converting to core IR"
-  Exps.transformProg (futharkSafe config) (visibleTypes prog) prog_decs'''''
+  Exps.transformProg (futharkSafe config) (visibleTypes prog) prog_decs5
   where
     verbose = fst (futharkVerbose config) > NotVerbose
     maybeLog s
diff --git a/src/Futhark/Internalise/ApplyTypeAbbrs.hs b/src/Futhark/Internalise/ApplyTypeAbbrs.hs
new file mode 100644
--- /dev/null
+++ b/src/Futhark/Internalise/ApplyTypeAbbrs.hs
@@ -0,0 +1,85 @@
+-- | A minor cleanup pass that runs after defunctorisation and applies
+-- any type abbreviations. After this, the program consists entirely
+-- value bindings.
+module Futhark.Internalise.ApplyTypeAbbrs (transformProg) where
+
+import Control.Monad.Identity
+import Data.Map.Strict qualified as M
+import Data.Maybe (mapMaybe)
+import Language.Futhark
+import Language.Futhark.Semantic (TypeBinding (..))
+import Language.Futhark.Traversals
+import Language.Futhark.TypeChecker.Types
+
+type Types = M.Map VName (Subst StructRetType)
+
+getTypes :: Types -> [Dec] -> Types
+getTypes types [] = types
+getTypes types (TypeDec typebind : ds) = do
+  let (TypeBind name l tparams _ (Info (RetType dims t)) _ _) = typebind
+      tbinding = TypeAbbr l tparams $ RetType dims $ applySubst (`M.lookup` types) t
+      types' = M.insert name (substFromAbbr tbinding) types
+  getTypes types' ds
+getTypes types (_ : ds) =
+  getTypes types ds
+
+-- Perform a given substitution on the types in a pattern.
+substPat :: (t -> t) -> Pat t -> Pat t
+substPat f pat = case pat of
+  TuplePat pats loc -> TuplePat (map (substPat f) pats) loc
+  RecordPat fs loc -> RecordPat (map substField fs) loc
+    where
+      substField (n, p) = (n, substPat f p)
+  PatParens p loc -> PatParens (substPat f p) loc
+  PatAttr attr p loc -> PatAttr attr (substPat f p) loc
+  Id vn (Info tp) loc -> Id vn (Info $ f tp) loc
+  Wildcard (Info tp) loc -> Wildcard (Info $ f tp) loc
+  PatAscription p _ _ -> substPat f p
+  PatLit e (Info tp) loc -> PatLit e (Info $ f tp) loc
+  PatConstr n (Info tp) ps loc -> PatConstr n (Info $ f tp) ps loc
+
+removeTypeVariablesInType :: Types -> StructType -> StructType
+removeTypeVariablesInType types =
+  applySubst (`M.lookup` types)
+
+substEntry :: Types -> EntryPoint -> EntryPoint
+substEntry types (EntryPoint params ret) =
+  EntryPoint (map onEntryParam params) (onEntryType ret)
+  where
+    onEntryParam (EntryParam v t) =
+      EntryParam v $ onEntryType t
+    onEntryType (EntryType t te) =
+      EntryType (removeTypeVariablesInType types t) te
+
+-- Remove all type variables and type abbreviations from a value binding.
+removeTypeVariables :: Types -> ValBind -> ValBind
+removeTypeVariables types valbind = do
+  let (ValBind entry _ _ (Info (RetType dims rettype)) _ pats body _ _ _) = valbind
+      mapper =
+        ASTMapper
+          { mapOnExp = onExp,
+            mapOnName = pure,
+            mapOnStructType = pure . applySubst (`M.lookup` types),
+            mapOnParamType = pure . applySubst (`M.lookup` types),
+            mapOnResRetType = pure . applySubst (`M.lookup` types)
+          }
+      onExp = astMap mapper
+
+  let body' = runIdentity $ onExp body
+
+  valbind
+    { valBindRetType = Info (applySubst (`M.lookup` types) $ RetType dims rettype),
+      valBindParams = map (substPat $ applySubst (`M.lookup` types)) pats,
+      valBindEntryPoint = fmap (substEntry types) <$> entry,
+      valBindBody = body'
+    }
+
+-- | Apply type abbreviations from a list of top-level declarations. A
+-- module-free input program is expected, so only value declarations
+-- and type declaration are accepted.
+transformProg :: (Monad m) => [Dec] -> m [ValBind]
+transformProg decs =
+  let types = getTypes mempty decs
+      onDec (ValDec valbind) = Just $ removeTypeVariables types valbind
+      onDec _ = Nothing
+   in pure $ mapMaybe onDec decs
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
@@ -612,15 +612,8 @@
     Dynamic _ -> pure (Project vn e0' tp loc, Dynamic $ toParam Observe tp')
     HoleSV _ hloc -> pure (Project vn e0' tp loc, HoleSV tp' hloc)
     _ -> error $ "Projection of an expression with static value " ++ show sv0
-defuncExp (AppExp (LetWith id1 id2 idxs e1 body loc) res) = do
-  e1' <- defuncExp' e1
-  idxs' <- mapM defuncDimIndex idxs
-  let id1_binding =
-        Binding Nothing $ Dynamic $ toParam Observe $ unInfo $ identType id1
-  (body', sv) <-
-    localEnv (M.singleton (identName id1) id1_binding) $
-      defuncExp body
-  pure (AppExp (LetWith id1 id2 idxs' e1' body' loc) res, sv)
+defuncExp (AppExp LetWith {} _) =
+  error "defuncExp: unexpected LetWith"
 defuncExp expr@(AppExp (Index e0 idxs loc) res) = do
   e0' <- defuncExp' e0
   idxs' <- mapM defuncDimIndex idxs
@@ -752,11 +745,7 @@
         M.fromList . zip (retDims ret) $
           map (ExpSubst . flip sizeFromName mempty . qualName) ext'
       ret' = applySubst (`M.lookup` extsubst) ret
-      e' =
-        mkApply
-          e
-          (zip3 (map (fst . snd) ps) (repeat Nothing) vars)
-          (AppRes (toStruct $ retType ret') ext')
+      e' = mkApply e (map (Nothing,) vars) $ AppRes (toStruct $ retType ret') ext'
   pure (params, e', ret)
   where
     getType (RetType _ (Scalar (Arrow _ p d t1 t2))) =
@@ -914,9 +903,9 @@
 defuncApplyArg ::
   String ->
   (Exp, StaticVal) ->
-  (((Diet, Maybe VName), Exp), [ParamType]) ->
+  ((Maybe VName, Exp), [ParamType]) ->
   DefM (Exp, StaticVal)
-defuncApplyArg fname_s (f', LambdaSV pat lam_e_t lam_e closure_env) (((d, argext), arg), _) = do
+defuncApplyArg fname_s (f', LambdaSV pat lam_e_t lam_e closure_env) ((argext, arg), _) = do
   (arg', arg_sv) <- defuncExp arg
   let env' = alwaysMatchPatSV pat arg_sv
       dims = mempty
@@ -962,23 +951,23 @@
 
   let f_t = toStruct $ typeOf f'
       arg_t = toStruct $ typeOf arg'
-      fname_t = foldFunType [toParam Observe f_t, toParam d arg_t] lifted_rettype
+      fname_t = foldFunType [toParam Observe f_t, toParam (diet (patternType pat)) arg_t] lifted_rettype
       fname' = Var (qualName fname) (Info fname_t) (srclocOf arg)
   callret <- unRetType lifted_rettype
 
   pure
-    ( mkApply fname' [(Observe, Nothing, f'), (Observe, argext, arg')] callret,
+    ( mkApply fname' [(Nothing, f'), (argext, arg')] callret,
       sv
     )
 -- If 'f' is a dynamic function, we just leave the application in
 -- place, but we update the types since it may be partially
 -- applied or return a higher-order value.
-defuncApplyArg _ (f', DynamicFun _ sv) (((d, argext), arg), argtypes) = do
+defuncApplyArg _ (f', DynamicFun _ sv) ((argext, arg), argtypes) = do
   (arg', _) <- defuncExp arg
   let (argtypes', rettype) = dynamicFunType sv argtypes
       restype = foldFunType argtypes' (RetType [] rettype)
       callret = AppRes restype []
-      apply_e = mkApply f' [(d, argext, arg')] callret
+      apply_e = mkApply f' [(argext, arg')] callret
   pure (apply_e, sv)
 --
 defuncApplyArg fname_s (_, sv) ((_, arg), _) =
@@ -995,7 +984,7 @@
   AppExp apply $ Info $ AppRes (combineTypeShapes ret1 ret2) (ext1 <> ext2)
 updateReturn _ e = e
 
-defuncApply :: Exp -> NE.NonEmpty ((Diet, Maybe VName), Exp) -> AppRes -> SrcLoc -> DefM (Exp, StaticVal)
+defuncApply :: Exp -> NE.NonEmpty (Maybe VName, Exp) -> AppRes -> SrcLoc -> DefM (Exp, StaticVal)
 defuncApply f args appres loc = do
   (f', f_sv) <- defuncApplyFunction f (length args)
   case f_sv of
diff --git a/src/Futhark/Internalise/Defunctorise.hs b/src/Futhark/Internalise/Defunctorise.hs
--- a/src/Futhark/Internalise/Defunctorise.hs
+++ b/src/Futhark/Internalise/Defunctorise.hs
@@ -262,7 +262,7 @@
               astMap (substituter $ modScope mod <> scope) e'
         _ -> astMap (substituter scope) e
 
-transformTypeExp :: TypeExp Info VName -> TransformM (TypeExp Info VName)
+transformTypeExp :: TypeExp Exp VName -> TransformM (TypeExp Exp VName)
 transformTypeExp = transformNames
 
 transformStructType :: StructType -> TransformM StructType
diff --git a/src/Futhark/Internalise/Entry.hs b/src/Futhark/Internalise/Entry.hs
--- a/src/Futhark/Internalise/Entry.hs
+++ b/src/Futhark/Internalise/Entry.hs
@@ -32,7 +32,7 @@
     decTypes (E.TypeDec tb) = [tb]
     decTypes _ = []
 
-findType :: VName -> VisibleTypes -> Maybe (E.TypeExp E.Info VName)
+findType :: VName -> VisibleTypes -> Maybe (E.TypeExp E.Exp VName)
 findType v (VisibleTypes ts) = E.typeExp <$> find ((== v) . E.typeAlias) ts
 
 valueType :: I.TypeBase I.Rank Uniqueness -> I.ValueType
@@ -41,19 +41,19 @@
 valueType I.Acc {} = error "valueType Acc"
 valueType I.Mem {} = error "valueType Mem"
 
-withoutDims :: E.TypeExp E.Info VName -> (Int, E.TypeExp E.Info VName)
+withoutDims :: E.TypeExp E.Exp VName -> (Int, E.TypeExp E.Exp VName)
 withoutDims (E.TEArray _ te _) =
   let (d, te') = withoutDims te
    in (d + 1, te')
 withoutDims te = (0 :: Int, te)
 
-rootType :: E.TypeExp E.Info VName -> E.TypeExp E.Info VName
+rootType :: E.TypeExp E.Exp VName -> E.TypeExp E.Exp VName
 rootType (E.TEApply te E.TypeArgExpSize {} _) = rootType te
 rootType (E.TEUnique te _) = rootType te
 rootType (E.TEDim _ te _) = rootType te
 rootType te = te
 
-typeExpOpaqueName :: E.TypeExp E.Info VName -> Name
+typeExpOpaqueName :: E.TypeExp E.Exp VName -> Name
 typeExpOpaqueName = nameFromText . f
   where
     f = g . rootType
@@ -87,7 +87,10 @@
           error $ "Duplicate definition of entry point type " <> E.prettyString name
     _ -> I.OpaqueTypes ts <> I.OpaqueTypes [(name, t)]
 
-isRecord :: VisibleTypes -> E.TypeExp E.Info VName -> Maybe (M.Map Name (E.TypeExp E.Info VName))
+isRecord ::
+  VisibleTypes ->
+  E.TypeExp E.Exp VName ->
+  Maybe (M.Map Name (E.TypeExp E.Exp VName))
 isRecord _ (E.TERecord fs _) = Just $ M.fromList fs
 isRecord _ (E.TETuple fs _) = Just $ E.tupleFields fs
 isRecord types (E.TEVar v _) = isRecord types =<< findType (E.qualLeaf v) types
@@ -96,7 +99,7 @@
 recordFields ::
   VisibleTypes ->
   M.Map Name E.StructType ->
-  Maybe (E.TypeExp E.Info VName) ->
+  Maybe (E.TypeExp E.Exp VName) ->
   [(Name, E.EntryType)]
 recordFields types fs t =
   case isRecord types . rootType =<< t of
@@ -120,7 +123,10 @@
   where
     opaqueField e_t i_ts = snd <$> entryPointType types e_t i_ts
 
-isSum :: VisibleTypes -> E.TypeExp E.Info VName -> Maybe (M.Map Name [E.TypeExp E.Info VName])
+isSum ::
+  VisibleTypes ->
+  E.TypeExp E.Exp VName ->
+  Maybe (M.Map Name [E.TypeExp E.Exp VName])
 isSum _ (E.TESum cs _) = Just $ M.fromList cs
 isSum types (E.TEVar v _) = isSum types =<< findType (E.qualLeaf v) types
 isSum _ _ = Nothing
@@ -128,7 +134,7 @@
 sumConstrs ::
   VisibleTypes ->
   M.Map Name [E.StructType] ->
-  Maybe (E.TypeExp E.Info VName) ->
+  Maybe (E.TypeExp E.Exp VName) ->
   [(Name, [E.EntryType])]
 sumConstrs types cs t =
   case isSum types . rootType =<< t of
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
@@ -1484,7 +1484,7 @@
   | E.Hole (Info _) loc <- f =
       (FunctionHole loc, map onArg $ NE.toList args)
   where
-    onArg (Info (_, argext), e) = (e, argext)
+    onArg (Info argext, e) = (e, argext)
 findFuncall e =
   error $ "Invalid function expression in application:\n" ++ prettyString e
 
diff --git a/src/Futhark/Internalise/FullNormalise.hs b/src/Futhark/Internalise/FullNormalise.hs
--- a/src/Futhark/Internalise/FullNormalise.hs
+++ b/src/Futhark/Internalise/FullNormalise.hs
@@ -2,14 +2,20 @@
 -- module-free Futhark program into an equivalent with only simple expresssions.
 -- Notably, all non-trivial expression are converted into a list of
 -- let-bindings to make them simpler, with no nested apply, nested lets...
--- This module only performs synthatic operations.
+-- This module only performs syntactic operations.
 --
--- Also, it performs desugaring that is:
--- * Turn operator section into lambda
--- * turn BinOp into application (&& and || are converted to if structure)
--- * turn `let x [i] = e1` into `let x = x with [i] = e1`
--- * binds all implicit sizes
+-- Also, it performs various kinds of desugaring:
 --
+-- * Turns operator sections into explicit lambdas.
+--
+-- * Rewrites BinOp nodes to Apply nodes (&& and || are converted to conditionals).
+--
+-- * Turns `let x [i] = e1` into `let x = x with [i] = e1`.
+--
+-- * Binds all implicit sizes.
+--
+-- * Turns implicit record fields into explicit record fields.
+--
 -- This is currently not done for expressions inside sizes, this processing
 -- still needed in monomorphisation for now.
 module Futhark.Internalise.FullNormalise (transformProg) where
@@ -43,7 +49,7 @@
 -- A binding that occurs in the calculation flow
 data Binding
   = PatBind [SizeBinder VName] (Pat StructType) Exp
-  | FunBind VName ([TypeParam], [Pat ParamType], Maybe (TypeExp Info VName), Info ResRetType, Exp)
+  | FunBind VName ([TypeParam], [Pat ParamType], Maybe (TypeExp Exp VName), Info ResRetType, Exp)
 
 type NormState = (([Binding], [BindModifier]), VNameSource)
 
@@ -164,7 +170,8 @@
     f (RecordFieldExplicit n e floc) = do
       e' <- getOrdering False e
       pure $ RecordFieldExplicit n e' floc
-    f field@RecordFieldImplicit {} = pure field
+    f (RecordFieldImplicit v t _) =
+      f $ RecordFieldExplicit (baseName v) (Var (qualName v) t loc) loc
 getOrdering _ (ArrayLit es ty loc) = do
   es' <- mapM (getOrdering False) es
   pure $ ArrayLit es' ty loc
@@ -202,7 +209,7 @@
   let y = Var (qualName yn) (Info $ toStruct yty) mempty
       ret' = applySubst (pSubst x y) ret
       body =
-        mkApply (Var op ty mempty) [(Observe, xext, x), (Observe, Nothing, y)] $
+        mkApply (Var op ty mempty) [(xext, x), (Nothing, y)] $
           AppRes (toStruct ret') exts
   nameExp final $ Lambda [Id yn (Info yty) mempty] body Nothing (Info (RetType dims ret')) loc
   where
@@ -215,7 +222,7 @@
   y <- getOrdering False e
   let x = Var (qualName xn) (Info $ toStruct xty) mempty
       ret' = applySubst (pSubst x y) ret
-      body = mkApply (Var op ty mempty) [(Observe, Nothing, x), (Observe, yext, y)] $ AppRes (toStruct ret') []
+      body = mkApply (Var op ty mempty) [(Nothing, x), (yext, y)] $ AppRes (toStruct ret') []
   nameExp final $ Lambda [Id xn (Info xty) mempty] body Nothing (Info (RetType dims ret')) loc
   where
     pSubst x y vn
@@ -304,7 +311,7 @@
     (False, False) -> do
       el' <- naming (prettyString op <> "_lhs") $ getOrdering False el
       er' <- naming (prettyString op <> "_rhs") $ getOrdering False er
-      pure $ mkApply (Var op opT oloc) [(Observe, elp, el'), (Observe, erp, er')] resT
+      pure $ mkApply (Var op opT oloc) [(elp, el'), (erp, er')] resT
   nameExp final expr'
   where
     isOr = baseName (qualLeaf op) == "||"
@@ -349,11 +356,10 @@
     f body (FunBind vn infos) =
       AppExp (LetFun vn infos body mempty) appRes
 
-transformDec :: (MonadFreshNames m) => Dec -> m Dec
-transformDec (ValDec valbind) = do
+transformValBind :: (MonadFreshNames m) => ValBind -> m ValBind
+transformValBind valbind = do
   body' <- transformBody $ valBindBody valbind
-  pure $ ValDec (valbind {valBindBody = body'})
-transformDec d = pure d
+  pure $ valbind {valBindBody = body'}
 
-transformProg :: (MonadFreshNames m) => [Dec] -> m [Dec]
-transformProg = mapM transformDec
+transformProg :: (MonadFreshNames m) => [ValBind] -> m [ValBind]
+transformProg = mapM transformValBind
diff --git a/src/Futhark/Internalise/LiftLambdas.hs b/src/Futhark/Internalise/LiftLambdas.hs
--- a/src/Futhark/Internalise/LiftLambdas.hs
+++ b/src/Futhark/Internalise/LiftLambdas.hs
@@ -18,7 +18,7 @@
 import Language.Futhark.Traversals
 
 data Env = Env
-  { envReplace :: M.Map VName Exp,
+  { envReplace :: M.Map VName (StructType -> Exp),
     envVtable :: M.Map VName StructType
   }
 
@@ -53,7 +53,7 @@
       stateGlobal = foldl' (flip S.insert) (stateGlobal s) (valBindBound vb)
     }
 
-replacing :: VName -> Exp -> LiftM a -> LiftM a
+replacing :: VName -> (StructType -> Exp) -> LiftM a -> LiftM a
 replacing v e = local $ \env ->
   env {envReplace = M.insert v e $ envReplace env}
 
@@ -85,7 +85,7 @@
 toRet :: TypeBase Size u -> TypeBase Size Uniqueness
 toRet = second (const Nonunique)
 
-liftFunction :: VName -> [TypeParam] -> [Pat ParamType] -> ResRetType -> Exp -> LiftM Exp
+liftFunction :: VName -> [TypeParam] -> [Pat ParamType] -> ResRetType -> Exp -> LiftM (StructType -> Exp)
 liftFunction fname tparams params (RetType dims ret) funbody = do
   -- Find free variables
   vtable <- asks envVtable
@@ -124,22 +124,22 @@
         valBindEntryPoint = Nothing
       }
 
-  pure
-    $ apply
-      (Var (qualName fname) (Info (augType free_ts)) mempty)
-    $ free_dims ++ free_nondims
+  pure $ \orig_type ->
+    apply
+      orig_type
+      (Var (qualName fname) (Info (augType free_ts orig_type)) mempty)
+      $ free_dims ++ free_nondims
   where
-    orig_type = funType params $ RetType dims ret
     mkParam (v, t) = Id v (Info (toParam Observe t)) mempty
     freeVar (v, t) = Var (qualName v) (Info t) mempty
-    augType rem_free = funType (map mkParam rem_free) $ RetType [] $ toRet orig_type
+    augType rem_free orig_type = funType (map mkParam rem_free) $ RetType [] $ toRet orig_type
 
-    apply :: Exp -> [(VName, StructType)] -> Exp
-    apply f [] = f
-    apply f (p : rem_ps) =
-      let inner_ret = AppRes (augType rem_ps) mempty
-          inner = mkApply f [(Observe, Nothing, freeVar p)] inner_ret
-       in apply inner rem_ps
+    apply :: StructType -> Exp -> [(VName, StructType)] -> Exp
+    apply _ f [] = f
+    apply orig_type f (p : rem_ps) =
+      let inner_ret = AppRes (augType rem_ps orig_type) mempty
+          inner = mkApply f [(Nothing, freeVar p)] inner_ret
+       in apply orig_type inner rem_ps
 
 transformSubExps :: ASTMapper LiftM
 transformSubExps = identityMapper {mapOnExp = transformExp}
@@ -150,10 +150,10 @@
   fname' <- newVName $ "lifted_" ++ baseString fname
   lifted_call <- liftFunction fname' tparams params ret funbody'
   replacing fname lifted_call $ transformExp body
-transformExp (Lambda params body _ (Info ret) _) = do
+transformExp e@(Lambda params body _ (Info ret) _) = do
   body' <- bindingParams [] params $ transformExp body
   fname <- newVName "lifted_lambda"
-  liftFunction fname [] params ret body'
+  liftFunction fname [] params ret body' <*> pure (typeOf e)
 transformExp (AppExp (LetPat sizes pat e body loc) appres) = do
   e' <- transformExp e
   body' <- bindingLetPat (map sizeName sizes) pat $ transformExp body
@@ -173,10 +173,10 @@
     form' <- astMap transformSubExps form
     body' <- bindingForm form' $ transformExp body
     pure $ AppExp (Loop sizes pat args' form' body' loc) appres
-transformExp e@(Var v _ _) =
+transformExp e@(Var v (Info t) _) =
   -- Note that function-typed variables can only occur in expressions,
   -- not in other places where VNames/QualNames can occur.
-  asks (fromMaybe e . M.lookup (qualLeaf v) . envReplace)
+  asks $ maybe e ($ t) . M.lookup (qualLeaf v) . envReplace
 transformExp e = astMap transformSubExps e
 
 transformValBind :: ValBind -> LiftM ()
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
@@ -13,8 +13,6 @@
 --   is a side effect of the monomorphisation algorithm, which uses
 --   the entry points as roots).
 --
--- * Turns implicit record fields into explicit record fields.
---
 -- * Rewrite BinOp nodes to Apply nodes.
 --
 -- * Replace all size expressions by constants or variables,
@@ -36,14 +34,12 @@
 import Data.List (partition)
 import Data.List.NonEmpty qualified as NE
 import Data.Map.Strict qualified as M
-import Data.Maybe
 import Data.Sequence qualified as Seq
 import Data.Set qualified as S
 import Futhark.MonadFreshNames
 import Futhark.Util (nubOrd, topologicalSort)
 import Futhark.Util.Pretty
 import Language.Futhark
-import Language.Futhark.Semantic (TypeBinding (..))
 import Language.Futhark.Traversals
 import Language.Futhark.TypeChecker.Types
 
@@ -121,10 +117,10 @@
     andop = Var (qualName (intrinsicVar "&&")) (Info opt) mempty
     eqop = Var (qualName (intrinsicVar "==")) (Info opt) mempty
     logAnd x' y =
-      mkApply andop [(Observe, Nothing, x'), (Observe, Nothing, y)] $
+      mkApply andop [(Nothing, x'), (Nothing, y)] $
         AppRes bool []
     cmpExp (ReplacedExp x', y) =
-      mkApply eqop [(Observe, Nothing, x'), (Observe, Nothing, y')] $
+      mkApply eqop [(Nothing, x'), (Nothing, y')] $
         AppRes bool []
       where
         y' = Var (qualName y) (Info i64) mempty
@@ -133,26 +129,20 @@
 -- to a representation of their corresponding function bindings.
 data Env = Env
   { envPolyBindings :: M.Map VName PolyBinding,
-    envTypeBindings :: M.Map VName TypeBinding,
     envScope :: S.Set VName,
     envGlobalScope :: S.Set VName,
     envParametrized :: ExpReplacements
   }
 
 instance Semigroup Env where
-  Env tb1 pb1 sc1 gs1 pr1 <> Env tb2 pb2 sc2 gs2 pr2 = Env (tb1 <> tb2) (pb1 <> pb2) (sc1 <> sc2) (gs1 <> gs2) (pr1 <> pr2)
+  Env pb1 sc1 gs1 pr1 <> Env pb2 sc2 gs2 pr2 = Env (pb1 <> pb2) (sc1 <> sc2) (gs1 <> gs2) (pr1 <> pr2)
 
 instance Monoid Env where
-  mempty = Env mempty mempty mempty mempty mempty
+  mempty = Env mempty mempty mempty mempty
 
 localEnv :: Env -> MonoM a -> MonoM a
 localEnv env = local (env <>)
 
-extendEnv :: VName -> PolyBinding -> MonoM a -> MonoM a
-extendEnv vn binding =
-  localEnv
-    mempty {envPolyBindings = M.singleton vn binding}
-
 isolateNormalisation :: MonoM a -> MonoM a
 isolateNormalisation m = do
   prevRepl <- get
@@ -161,6 +151,15 @@
   put prevRepl
   pure ret
 
+-- | These now have monomorphic types in the given action. This is
+-- used to handle shadowing.
+withMono :: [VName] -> MonoM a -> MonoM a
+withMono [] = id
+withMono vs = local $ \env ->
+  env {envPolyBindings = M.filterWithKey keep (envPolyBindings env)}
+  where
+    keep v _ = v `notElem` vs
+
 withArgs :: S.Set VName -> MonoM a -> MonoM a
 withArgs args = localEnv $ mempty {envScope = args}
 
@@ -378,46 +377,45 @@
     maybeNormalisedSize _ = Nothing
 
 transformFName :: SrcLoc -> QualName VName -> StructType -> MonoM Exp
-transformFName loc fname t = do
-  t' <- removeTypeVariablesInType t
-  t'' <- transformType t'
-  let mono_t = monoType t'
+transformFName loc fname ft = do
+  t' <- transformType ft
+  let mono_t = monoType ft
   if baseTag (qualLeaf fname) <= maxIntrinsicTag
-    then pure $ var fname t''
+    then pure $ var fname t'
     else do
       maybe_fname <- lookupLifted (qualLeaf fname) mono_t
       maybe_funbind <- lookupFun $ qualLeaf fname
       case (maybe_fname, maybe_funbind) of
         -- The function has already been monomorphised.
         (Just (fname', infer), _) ->
-          applySizeArgs fname' (toRes Nonunique t'') <$> infer t''
+          applySizeArgs fname' (toRes Nonunique t') <$> infer t'
         -- An intrinsic function.
-        (Nothing, Nothing) -> pure $ var fname t''
+        (Nothing, Nothing) -> pure $ var fname t'
         -- A polymorphic function.
         (Nothing, Just funbind) -> do
           (fname', infer, funbind') <- monomorphiseBinding False funbind mono_t
           tell $ Seq.singleton (qualLeaf fname, funbind')
           addLifted (qualLeaf fname) mono_t (fname', infer)
-          applySizeArgs fname' (toRes Nonunique t'') <$> infer t''
+          applySizeArgs fname' (toRes Nonunique t') <$> infer t'
   where
-    var fname' t'' = Var fname' (Info t'') loc
+    var fname' t' = Var fname' (Info t') loc
 
-    applySizeArg t' (i, f) size_arg =
+    applySizeArg t (i, f) size_arg =
       ( i - 1,
         mkApply
           f
-          [(Observe, Nothing, size_arg)]
-          (AppRes (foldFunType (replicate i i64) (RetType [] t')) [])
+          [(Nothing, size_arg)]
+          (AppRes (foldFunType (replicate i i64) (RetType [] t)) [])
       )
 
-    applySizeArgs fname' t' size_args =
+    applySizeArgs fname' t size_args =
       snd $
         foldl'
-          (applySizeArg t')
+          (applySizeArg t)
           ( length size_args - 1,
             Var
               (qualName fname')
-              (Info (foldFunType (map (const i64) size_args) (RetType [] t')))
+              (Info (foldFunType (map (const i64) size_args) (RetType [] t)))
               loc
           )
           size_args
@@ -457,7 +455,7 @@
 
 transformRetTypeSizes :: S.Set VName -> RetTypeBase Size as -> MonoM (RetTypeBase Size as)
 transformRetTypeSizes argset (RetType dims ty) = do
-  ty' <- withArgs argset $ transformType ty
+  ty' <- withArgs argset $ withMono dims $ transformType ty
   rl <- parametrizing argset
   let dims' = dims <> map snd rl
   pure $ RetType dims' ty'
@@ -498,30 +496,8 @@
   body' <- withParams params $ scoping argset $ transformExp body
   res' <- transformAppRes res
   pure $ AppExp (LetPat sizes' pat' e' body' loc) (Info res')
-transformAppExp (LetFun fname (tparams, params, retdecl, Info ret, body) e loc) res
-  | not $ null tparams = do
-      -- Retrieve the lifted monomorphic function bindings that are
-      -- produced, filter those that are monomorphic versions of the
-      -- current let-bound function and insert them at this point, and
-      -- propagate the rest.
-      let funbind = PolyBinding (fname, tparams, params, ret, body, mempty, loc)
-      pass $ do
-        (e', bs) <- listen $ extendEnv fname funbind $ scoping (S.singleton fname) $ transformExp e
-        -- Do not remember this one for next time we monomorphise this
-        -- function.
-        modifyLifts $ filter ((/= fname) . fst . fst)
-        let (bs_local, bs_prop) = Seq.partition ((== fname) . fst) bs
-        pure (unfoldLetFuns (map snd $ toList bs_local) e', const bs_prop)
-  | otherwise = do
-      params' <- mapM transformPat params
-      body' <- scoping (S.fromList (foldMap patNames params')) $ transformExp body
-      ret' <- transformRetTypeSizes (S.fromList (foldMap patNames params')) ret
-      AppExp
-        <$> ( LetFun fname (tparams, params', retdecl, Info ret', body')
-                <$> scoping (S.singleton fname) (transformExp e)
-                <*> pure loc
-            )
-        <*> (Info <$> transformAppRes res)
+transformAppExp LetFun {} _ =
+  error "transformAppExp: LetFun is not supposed to occur"
 transformAppExp (If e1 e2 e3 loc) res =
   AppExp <$> (If <$> transformExp e1 <*> transformExp e2 <*> transformExp e3 <*> pure loc) <*> (Info <$> transformAppRes res)
 transformAppExp (Apply fe args _) res =
@@ -530,7 +506,7 @@
     <*> mapM onArg (NE.toList args)
     <*> transformAppRes res
   where
-    onArg (Info (d, ext), e) = (d,ext,) <$> transformExp e
+    onArg (Info ext, e) = (ext,) <$> transformExp e
 transformAppExp (Loop sparams pat e1 form body loc) res = do
   e1' <- transformExp e1
 
@@ -594,8 +570,8 @@
   where
     applyOp ret ext fname' x y =
       mkApply
-        (mkApply fname' [(Observe, unInfo d1, x)] (AppRes ret mempty))
-        [(Observe, unInfo d2, y)]
+        (mkApply fname' [(unInfo d1, x)] (AppRes ret mempty))
+        [(unInfo d2, y)]
         (AppRes ret ext)
 
     makeVarParam arg = do
@@ -605,17 +581,8 @@
         ( Var (qualName x) (Info argtype) mempty,
           Id x (Info argtype) mempty
         )
-transformAppExp (LetWith id1 id2 idxs e1 body loc) res = do
-  id1' <- transformIdent id1
-  id2' <- transformIdent id2
-  idxs' <- mapM transformDimIndex idxs
-  e1' <- transformExp e1
-  body' <- scoping (S.singleton $ identName id1') $ transformExp body
-  res' <- transformAppRes res
-  pure $ AppExp (LetWith id1' id2' idxs' e1' body' loc) (Info res')
-  where
-    transformIdent (Ident v t vloc) =
-      Ident v <$> traverse transformType t <*> pure vloc
+transformAppExp LetWith {} _ =
+  error "transformAppExp: LetWith is not supposed to occur"
 transformAppExp (Index e0 idxs loc) res =
   AppExp
     <$> (Index <$> transformExp e0 <*> mapM transformDimIndex idxs <*> pure loc)
@@ -683,17 +650,8 @@
   Negate <$> transformExp e <*> pure loc
 transformExp (Not e loc) =
   Not <$> transformExp e <*> pure loc
-transformExp (Lambda params e0 decl tp loc) = do
-  let patArgs = S.fromList $ foldMap patNames params
-  dimArgs <- withArgs patArgs $ askIntros (foldMap (fvVars . freeInPat) params)
-  let argset = dimArgs `S.union` patArgs
-  params' <- mapM transformPat params
-  paramed <- parametrizing argset
-  Lambda params'
-    <$> withParams paramed (scoping argset $ transformExp e0)
-    <*> pure decl
-    <*> traverse transformRetType tp
-    <*> pure loc
+transformExp (Lambda {}) =
+  error "transformExp: Lambda is not supposed to occur"
 transformExp (OpSection qn t loc) =
   transformExp $ Var qn t loc
 transformExp (OpSectionLeft fname (Info t) e arg (Info rettype, Info retext) loc) = do
@@ -781,7 +739,7 @@
   let apply_left =
         mkApply
           op
-          [(Observe, xext, e1)]
+          [(xext, e1)]
           (AppRes (Scalar $ Arrow mempty yp (diet ytype) (toStruct ytype) (RetType [] $ toRes Nonunique t')) [])
       onDim (Var d typ _)
         | Named p <- xp, qualLeaf d == p = Var (qualName v1) typ loc
@@ -790,7 +748,7 @@
       rettype' = first onDim rettype
   body <-
     scoping (S.fromList [v1, v2]) $
-      mkApply apply_left [(Observe, yext, e2)]
+      mkApply apply_left [(yext, e2)]
         <$> transformAppRes (AppRes (toStruct rettype') retext)
   rettype'' <- transformRetTypeSizes (S.fromList [v1, v2]) $ RetType dims rettype'
   pure . wrap_left . wrap_right $
@@ -853,16 +811,6 @@
       loc
 desugarIndexSection _ t _ = error $ "desugarIndexSection: not a function type: " ++ prettyString t
 
--- Convert a collection of 'ValBind's to a nested sequence of let-bound,
--- monomorphic functions with the given expression at the bottom.
-unfoldLetFuns :: [ValBind] -> Exp -> Exp
-unfoldLetFuns [] e = e
-unfoldLetFuns (ValBind _ fname _ (Info rettype) dim_params params body _ _ loc : rest) e =
-  AppExp (LetFun fname (dim_params, params, Nothing, Info rettype, body) e' loc) (Info $ AppRes e_t mempty)
-  where
-    e' = unfoldLetFuns rest e
-    e_t = typeOf e'
-
 transformPat :: Pat (TypeBase Size u) -> MonoM (Pat (TypeBase Size u))
 transformPat = traverse transformType
 
@@ -934,9 +882,6 @@
       Arrow u Unnamed d1 (f t1) (RetType dims (f t2))
     f' t = t
 
-transformRetType :: RetTypeBase Size u -> MonoM (RetTypeBase Size u)
-transformRetType (RetType ext t) = RetType ext <$> transformType t
-
 -- | arrowArg takes a return type and returns it
 -- with the existentials bound moved at the right of arrows.
 -- It also gives the new set of parameters to consider.
@@ -1036,15 +981,7 @@
   MonoType ->
   MonoM (VName, InferSizeArgs, ValBind)
 monomorphiseBinding entry (PolyBinding (name, tparams, params, rettype, body, attrs, loc)) inst_t = do
-  letFun <- asks $ S.member name . envScope
-  let paramGetClean argset =
-        if letFun
-          then parametrizing argset
-          else do
-            ret <- get
-            put mempty
-            pure ret
-  (if letFun then id else isolateNormalisation) $ do
+  isolateNormalisation $ do
     let bind_t = funType params rettype
     (substs, t_shape_params) <-
       typeSubstsM loc (noSizes bind_t) $ noNamedParams inst_t
@@ -1052,9 +989,9 @@
         substs' = M.map (Subst []) substs
         substStructType =
           substTypesAny (fmap (fmap (second (const mempty))) . (`M.lookup` substs'))
-        params' = map (substPat entry substStructType) params
+        params' = map (substPat substStructType) params
     params'' <- withArgs shape_names $ mapM transformPat params'
-    exp_naming <- paramGetClean shape_names
+    exp_naming <- paramGetClean
 
     let args = S.fromList $ foldMap patNames params
         arg_params = map snd exp_naming
@@ -1063,7 +1000,7 @@
       withParams exp_naming $
         withArgs (args <> shape_names) $
           hardTransformRetType (applySubst (`M.lookup` substs') rettype)
-    extNaming <- paramGetClean (args <> shape_names)
+    extNaming <- paramGetClean
     scope <- S.union shape_names <$> askScope'
     let (rettype'', new_params) = arrowArg scope args arg_params rettype'
         bind_t' = substTypesAny (`M.lookup` substs') bind_t
@@ -1078,9 +1015,7 @@
     body'' <- withParams exp_naming' $ withArgs (shape_names <> args) $ transformExp body'
     scope' <- S.union (shape_names <> args) <$> askScope'
     body''' <-
-      if letFun
-        then unscoping (shape_names <> args) body''
-        else expReplace exp_naming' <$> (calculateDims body'' . canCalculate scope' =<< get)
+      expReplace exp_naming' <$> (calculateDims body'' . canCalculate scope' =<< get)
 
     seen_before <- elem name . map (fst . fst) <$> getLifts
     name' <-
@@ -1114,6 +1049,11 @@
 
     updateExpTypes substs = astMap (mapper substs)
 
+    paramGetClean = do
+      ret <- get
+      put mempty
+      pure ret
+
     hardTransformRetType (RetType dims ty) = do
       ty' <- transformType ty
       unbounded <- askIntros $ fvVars $ freeInType ty'
@@ -1184,7 +1124,6 @@
     sub t1@(Scalar Sum {}) t2 = sub t1 t2
     sub t1 t2@(Scalar Sum {}) = sub t1 t2
     sub t1 t2 = error $ unlines ["typeSubstsM: mismatched types:", prettyString t1, prettyString t2]
-
     addSubst (QualName _ v) (RetType ext t) = do
       (ts, sizes) <- get
       unless (v `M.member` ts) $ do
@@ -1204,19 +1143,17 @@
     onDim MonoAnon = pure anySize
 
 -- Perform a given substitution on the types in a pattern.
-substPat :: Bool -> (t -> t) -> Pat t -> Pat t
-substPat entry f pat = case pat of
-  TuplePat pats loc -> TuplePat (map (substPat entry f) pats) loc
+substPat :: (t -> t) -> Pat t -> Pat t
+substPat f pat = case pat of
+  TuplePat pats loc -> TuplePat (map (substPat f) pats) loc
   RecordPat fs loc -> RecordPat (map substField fs) loc
     where
-      substField (n, p) = (n, substPat entry f p)
-  PatParens p loc -> PatParens (substPat entry f p) loc
-  PatAttr attr p loc -> PatAttr attr (substPat entry f p) loc
+      substField (n, p) = (n, substPat f p)
+  PatParens p loc -> PatParens (substPat f p) loc
+  PatAttr attr p loc -> PatAttr attr (substPat f p) loc
   Id vn (Info tp) loc -> Id vn (Info $ f tp) loc
   Wildcard (Info tp) loc -> Wildcard (Info $ f tp) loc
-  PatAscription p td loc
-    | entry -> PatAscription (substPat False f p) td loc
-    | otherwise -> substPat False f p
+  PatAscription p _ _ -> substPat f p
   PatLit e (Info tp) loc -> PatLit e (Info $ f tp) loc
   PatConstr n (Info tp) ps loc -> PatConstr n (Info $ f tp) ps loc
 
@@ -1224,62 +1161,19 @@
 toPolyBinding (ValBind _ name _ (Info rettype) tparams params body _ attrs loc) =
   PolyBinding (name, tparams, params, rettype, body, attrs, loc)
 
--- Remove all type variables and type abbreviations from a value binding.
-removeTypeVariables :: Bool -> ValBind -> MonoM ValBind
-removeTypeVariables entry valbind = do
-  let (ValBind _ _ _ (Info (RetType dims rettype)) _ pats body _ _ _) = valbind
-  subs <- asks $ M.map substFromAbbr . envTypeBindings
-  let mapper =
-        ASTMapper
-          { mapOnExp = onExp,
-            mapOnName = pure,
-            mapOnStructType = pure . applySubst (`M.lookup` subs),
-            mapOnParamType = pure . applySubst (`M.lookup` subs),
-            mapOnResRetType = pure . applySubst (`M.lookup` subs)
-          }
-
-      onExp = astMap mapper
-
-  body' <- onExp body
-
-  pure
-    valbind
-      { valBindRetType = Info (applySubst (`M.lookup` subs) $ RetType dims rettype),
-        valBindParams = map (substPat entry $ applySubst (`M.lookup` subs)) pats,
-        valBindBody = body'
-      }
-
-removeTypeVariablesInType :: StructType -> MonoM StructType
-removeTypeVariablesInType t = do
-  subs <- asks $ M.map substFromAbbr . envTypeBindings
-  pure $ applySubst (`M.lookup` subs) t
-
-transformEntryPoint :: EntryPoint -> MonoM EntryPoint
-transformEntryPoint (EntryPoint params ret) =
-  EntryPoint <$> mapM onEntryParam params <*> onEntryType ret
-  where
-    onEntryParam (EntryParam v t) =
-      EntryParam v <$> onEntryType t
-    onEntryType (EntryType t te) =
-      EntryType <$> removeTypeVariablesInType t <*> pure te
-
 transformValBind :: ValBind -> MonoM Env
 transformValBind valbind = do
-  valbind' <-
-    toPolyBinding
-      <$> removeTypeVariables (isJust (valBindEntryPoint valbind)) valbind
+  let valbind' = toPolyBinding valbind
 
   case valBindEntryPoint valbind of
     Nothing -> pure ()
-    Just (Info entry) -> do
-      t <-
-        removeTypeVariablesInType $
-          funType (valBindParams valbind) $
-            unInfo $
-              valBindRetType valbind
+    Just entry -> do
+      let t =
+            funType (valBindParams valbind) $
+              unInfo $
+                valBindRetType valbind
       (name, infer, valbind'') <- monomorphiseBinding True valbind' $ monoType t
-      entry' <- transformEntryPoint entry
-      tell $ Seq.singleton (name, valbind'' {valBindEntryPoint = Just $ Info entry'})
+      tell $ Seq.singleton (name, valbind'' {valBindEntryPoint = Just entry})
       addLifted (valBindName valbind) (monoType t) (name, infer)
 
   pure
@@ -1291,30 +1185,15 @@
             else mempty
       }
 
-transformTypeBind :: TypeBind -> MonoM Env
-transformTypeBind (TypeBind name l tparams _ (Info (RetType dims t)) _ _) = do
-  subs <- asks $ M.map substFromAbbr . envTypeBindings
-  let tbinding = TypeAbbr l tparams $ RetType dims $ applySubst (`M.lookup` subs) t
-  pure mempty {envTypeBindings = M.singleton name tbinding}
-
-transformDecs :: [Dec] -> MonoM ()
-transformDecs [] = pure ()
-transformDecs (ValDec valbind : ds) = do
+transformValBinds :: [ValBind] -> MonoM ()
+transformValBinds [] = pure ()
+transformValBinds (valbind : ds) = do
   env <- transformValBind valbind
-  localEnv env $ transformDecs ds
-transformDecs (TypeDec typebind : ds) = do
-  env <- transformTypeBind typebind
-  localEnv env $ transformDecs ds
-transformDecs (dec : _) =
-  error $
-    "The monomorphization module expects a module-free "
-      ++ "input program, but received: "
-      ++ prettyString dec
+  localEnv env $ transformValBinds ds
 
--- | Monomorphise a list of top-level declarations. A module-free input program
--- is expected, so only value declarations and type declaration are accepted.
-transformProg :: (MonadFreshNames m) => [Dec] -> m [ValBind]
+-- | Monomorphise a list of top-level value bindings.
+transformProg :: (MonadFreshNames m) => [ValBind] -> m [ValBind]
 transformProg decs =
   fmap (toList . fmap snd . snd) $
     modifyNameSource $ \namesrc ->
-      runMonoM namesrc $ transformDecs decs
+      runMonoM namesrc $ transformValBinds decs
diff --git a/src/Futhark/Internalise/ReplaceRecords.hs b/src/Futhark/Internalise/ReplaceRecords.hs
--- a/src/Futhark/Internalise/ReplaceRecords.hs
+++ b/src/Futhark/Internalise/ReplaceRecords.hs
@@ -117,18 +117,10 @@
   (pat', rr) <- transformPat pat
   body' <- withRecordReplacements rr $ transformExp body
   pure $ AppExp (LetPat sizes pat' e' body' loc) res
-transformExp (AppExp (LetFun fname (tparams, params, retdecl, Info ret, funbody) letbody loc) res) = do
-  (params', rr) <- mapAndUnzipM transformPat params
-  funbody' <- withRecordReplacements (mconcat rr) $ transformExp funbody
-  letbody' <- transformExp letbody
-  pure $ AppExp (LetFun fname (tparams, params', retdecl, Info ret, funbody') letbody' loc) res
-transformExp (Lambda params e decl tp loc) = do
-  (params', rrs) <- mapAndUnzipM transformPat params
-  Lambda params'
-    <$> withRecordReplacements (mconcat rrs) (transformExp e)
-    <*> pure decl
-    <*> pure tp
-    <*> pure loc
+transformExp (AppExp (LetFun {}) _) = do
+  error "transformExp: LetFun is not supposed to occur"
+transformExp (Lambda {}) =
+  error "transformExp: Lambda is not supposed to occur"
 transformExp e = astMap m e
   where
     m = identityMapper {mapOnExp = transformExp}
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
@@ -15,8 +15,8 @@
 import Data.Map qualified as M
 import Data.Text qualified as T
 import Futhark.Compiler.Program (ProgError (..))
-import Futhark.LSP.Tool (posToUri, rangeFromLoc, rangeFromSrcLoc)
-import Futhark.Util.Loc (Loc (..), SrcLoc, locOf)
+import Futhark.LSP.Tool (posToUri, rangeFromLoc)
+import Futhark.Util.Loc (Loc (..))
 import Futhark.Util.Pretty (Doc, docText)
 import Language.LSP.Diagnostics (partitionBySource)
 import Language.LSP.Protocol.Lens (HasVersion (version))
@@ -49,21 +49,19 @@
     (partitionBySource diags)
 
 -- | Send warning diagnostics to the client.
-publishWarningDiagnostics :: [(SrcLoc, Doc a)] -> LspT () IO ()
+publishWarningDiagnostics :: [(Loc, Doc a)] -> LspT () IO ()
 publishWarningDiagnostics warnings = do
   publish $ M.assocs $ M.unionsWith (++) $ map onWarn warnings
   where
-    onWarn (srcloc, msg) =
-      case locOf srcloc of
-        NoLoc -> mempty
-        Loc pos _ ->
-          M.singleton
-            (posToUri pos)
-            [ mkDiagnostic
-                (rangeFromSrcLoc srcloc)
-                DiagnosticSeverity_Warning
-                (docText msg)
-            ]
+    onWarn (NoLoc, _) = mempty
+    onWarn (loc@(Loc pos _), msg) =
+      M.singleton
+        (posToUri pos)
+        [ mkDiagnostic
+            (rangeFromLoc loc)
+            DiagnosticSeverity_Warning
+            (docText msg)
+        ]
 
 -- | Send error diagnostics to the client.
 publishErrorDiagnostics :: NE.NonEmpty ProgError -> LspT () IO ()
diff --git a/src/Futhark/LSP/Tool.hs b/src/Futhark/LSP/Tool.hs
--- a/src/Futhark/LSP/Tool.hs
+++ b/src/Futhark/LSP/Tool.hs
@@ -3,7 +3,6 @@
 module Futhark.LSP.Tool
   ( getHoverInfoFromState,
     findDefinitionRange,
-    rangeFromSrcLoc,
     rangeFromLoc,
     posToUri,
     computeMapping,
@@ -19,7 +18,7 @@
     toStalePos,
   )
 import Futhark.LSP.State (State (..), getStaleContent, getStaleMapping)
-import Futhark.Util.Loc (Loc (Loc, NoLoc), Pos (Pos), SrcLoc, locOf)
+import Futhark.Util.Loc (Loc (Loc, NoLoc), Pos (Pos))
 import Futhark.Util.Pretty (prettyText)
 import Language.Futhark.Prop (isBuiltinLoc)
 import Language.Futhark.Query
@@ -127,7 +126,3 @@
 rangeFromLoc :: Loc -> Range
 rangeFromLoc (Loc start end) = Range (getStartPos start) (getEndPos end)
 rangeFromLoc NoLoc = Range (Position 0 0) (Position 0 5) -- only when file not found, throw error after moving to vfs
-
--- | Create an LSP 'Range' from a Futhark 'SrcLoc'.
-rangeFromSrcLoc :: SrcLoc -> Range
-rangeFromSrcLoc = rangeFromLoc . locOf
diff --git a/src/Futhark/Optimise/ArrayShortCircuiting/ArrayCoalescing.hs b/src/Futhark/Optimise/ArrayShortCircuiting/ArrayCoalescing.hs
--- a/src/Futhark/Optimise/ArrayShortCircuiting/ArrayCoalescing.hs
+++ b/src/Futhark/Optimise/ArrayShortCircuiting/ArrayCoalescing.hs
@@ -1594,10 +1594,12 @@
 
 sameSpace :: (Coalesceable rep inner) => TopdownEnv rep -> VName -> VName -> Bool
 sameSpace td_env m_x m_b
-  | MemMem pat_space <- runReader (lookupMemInfo m_x) $ removeScopeAliases $ scope td_env,
-    MemMem return_space <- runReader (lookupMemInfo m_b) $ removeScopeAliases $ scope td_env =
+  | Just (MemMem pat_space) <- nameInfoToMemInfo <$> M.lookup m_x scope',
+    Just (MemMem return_space) <- nameInfoToMemInfo <$> M.lookup m_b scope' =
       pat_space == return_space
   | otherwise = False
+  where
+    scope' = removeScopeAliases $ scope td_env
 
 data MemBodyResult = MemBodyResult
   { patMem :: VName,
diff --git a/src/Futhark/Optimise/Simplify/Engine.hs b/src/Futhark/Optimise/Simplify/Engine.hs
--- a/src/Futhark/Optimise/Simplify/Engine.hs
+++ b/src/Futhark/Optimise/Simplify/Engine.hs
@@ -959,10 +959,12 @@
     TraverseOpStms (Wise rep),
     CanBeWise (OpC rep),
     ST.IndexOp (Op (Wise rep)),
-    AliasedOp (Op (Wise rep)),
+    IsOp (OpC rep),
+    ASTConstraints (OpC rep (Wise rep)),
+    AliasedOp (OpC (Wise rep)),
     RephraseOp (OpC rep),
     BuilderOps (Wise rep),
-    IsOp (Op rep)
+    IsOp (OpC rep)
   )
 
 class Simplifiable e where
diff --git a/src/Futhark/Optimise/Simplify/Rep.hs b/src/Futhark/Optimise/Simplify/Rep.hs
--- a/src/Futhark/Optimise/Simplify/Rep.hs
+++ b/src/Futhark/Optimise/Simplify/Rep.hs
@@ -122,7 +122,7 @@
     Ord (OpC rep (Wise rep)),
     Eq (OpC rep (Wise rep)),
     Show (OpC rep (Wise rep)),
-    IsOp (OpC rep (Wise rep)),
+    IsOp (OpC rep),
     Pretty (OpC rep (Wise rep))
   ) =>
   RepTypes (Wise rep)
@@ -144,7 +144,7 @@
   scope <- asksScope removeScopeWisdom
   runReaderT m scope
 
-instance (Informing rep, IsOp (OpC rep (Wise rep))) => ASTRep (Wise rep) where
+instance (Informing rep, IsOp (OpC rep)) => ASTRep (Wise rep) where
   expTypesFromPat =
     withoutWisdom . expTypesFromPat . removePatWisdom
 
@@ -291,10 +291,11 @@
 -- representation.
 type Informing rep =
   ( ASTRep rep,
-    AliasedOp (OpC rep (Wise rep)),
+    AliasedOp (OpC rep),
     RephraseOp (OpC rep),
     CanBeWise (OpC rep),
-    FreeIn (OpC rep (Wise rep))
+    FreeIn (OpC rep (Wise rep)),
+    ASTConstraints (OpC rep (Wise rep))
   )
 
 -- | A type class for indicating that this operation can be lifted into the simplifier representation.
diff --git a/src/Futhark/Optimise/Simplify/Rules/BasicOp.hs b/src/Futhark/Optimise/Simplify/Rules/BasicOp.hs
--- a/src/Futhark/Optimise/Simplify/Rules/BasicOp.hs
+++ b/src/Futhark/Optimise/Simplify/Rules/BasicOp.hs
@@ -96,9 +96,11 @@
 
 -- Removing a concatenation that involves only a single array.  This
 -- may be produced as a result of other simplification rules.
-simplifyConcat _ pat aux (Concat _ (x :| []) _) =
-  -- Still need a copy because Concat produces a fresh array.
-  Simplify $ auxing aux $ letBind pat $ BasicOp $ Replicate mempty $ Var x
+simplifyConcat (vtable, _) pat aux (Concat _ (x :| []) w)
+  | Just x_t <- ST.lookupType x vtable,
+    arraySize 0 x_t == w =
+      -- Still need a copy because Concat produces a fresh array.
+      Simplify $ auxing aux $ letBind pat $ BasicOp $ Replicate mempty $ Var x
 -- concat xs (concat ys zs) == concat xs ys zs
 simplifyConcat (vtable, _) pat (StmAux cs attrs _) (Concat i (x :| xs) new_d)
   | x' /= x || concat xs' /= xs =
diff --git a/src/Futhark/Pass/ExplicitAllocations.hs b/src/Futhark/Pass/ExplicitAllocations.hs
--- a/src/Futhark/Pass/ExplicitAllocations.hs
+++ b/src/Futhark/Pass/ExplicitAllocations.hs
@@ -1040,14 +1040,15 @@
 mkLetNamesB'' ::
   ( Mem rep inner,
     LetDec rep ~ LetDecMem,
-    OpReturns (inner (Engine.Wise rep)),
+    OpReturns inner,
     ExpDec rep ~ (),
     Rep m ~ Engine.Wise rep,
     HasScope (Engine.Wise rep) m,
     MonadBuilder m,
-    AliasedOp (inner (Engine.Wise rep)),
+    AliasedOp inner,
     RephraseOp (MemOp inner),
-    Engine.CanBeWise inner
+    Engine.CanBeWise inner,
+    ASTConstraints (inner (Engine.Wise rep))
   ) =>
   Space ->
   [VName] ->
@@ -1082,9 +1083,9 @@
     Mem (Engine.Wise rep) inner,
     Engine.CanBeWise inner,
     RephraseOp inner,
-    IsOp (inner rep),
-    OpReturns (inner (Engine.Wise rep)),
-    AliasedOp (inner (Engine.Wise rep)),
+    IsOp inner,
+    OpReturns inner,
+    AliasedOp inner,
     IndexOp (inner (Engine.Wise rep))
   ) =>
   (inner (Engine.Wise rep) -> UT.UsageTable) ->
diff --git a/src/Futhark/Pass/LiftAllocations.hs b/src/Futhark/Pass/LiftAllocations.hs
--- a/src/Futhark/Pass/LiftAllocations.hs
+++ b/src/Futhark/Pass/LiftAllocations.hs
@@ -22,7 +22,7 @@
 import Futhark.Pass (Pass (..))
 
 liftInProg ::
-  (AliasableRep rep, Mem rep inner, OpReturns (inner (Aliases rep))) =>
+  (AliasableRep rep, Mem rep inner, ASTConstraints (inner (Aliases rep))) =>
   (inner (Aliases rep) -> LiftM (inner (Aliases rep)) (inner (Aliases rep))) ->
   Prog rep ->
   Prog rep
diff --git a/src/Futhark/Test.hs b/src/Futhark/Test.hs
--- a/src/Futhark/Test.hs
+++ b/src/Futhark/Test.hs
@@ -27,7 +27,6 @@
 where
 
 import Codec.Compression.GZip
-import Codec.Compression.Zlib.Internal (DecompressError)
 import Control.Applicative
 import Control.Exception (catch)
 import Control.Exception.Base qualified as E
diff --git a/src/Futhark/Util/Pretty.hs b/src/Futhark/Util/Pretty.hs
--- a/src/Futhark/Util/Pretty.hs
+++ b/src/Futhark/Util/Pretty.hs
@@ -12,6 +12,7 @@
     prettyTextOneLine,
     docText,
     docTextForHandle,
+    docString,
 
     -- * Rendering to terminal
     putDoc,
@@ -111,6 +112,11 @@
   where
     layouter =
       layoutSmart defaultLayoutOptions {layoutPageWidth = Unbounded}
+
+-- | Convert a 'Doc' to a 'String', through 'docText'. Intended for
+-- debugging.
+docString :: Doc a -> String
+docString = T.unpack . docText
 
 -- | Prettyprint a value to a 'Text' on a single line.
 prettyTextOneLine :: (Pretty a) => a -> Text
diff --git a/src/Futhark/Version.hs b/src/Futhark/Version.hs
--- a/src/Futhark/Version.hs
+++ b/src/Futhark/Version.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE TemplateHaskell #-}
 
 -- | This module exports version information about the Futhark
@@ -12,7 +13,7 @@
 import Data.FileEmbed
 import Data.Text qualified as T
 import Data.Version
-import Futhark.Util (trim)
+import Futhark.Util (showText, trim)
 import GitHash
 import Paths_futhark qualified
 
@@ -28,7 +29,7 @@
 -- | The version of Futhark that we are using, in human-readable form.
 versionString :: T.Text
 versionString =
-  T.pack (showVersion version) <> unreleased <> gitversion $$tGitInfoCwdTry
+  T.pack (showVersion version) <> unreleased <> gitversion $$tGitInfoCwdTry <> ghcversion
   where
     unreleased =
       if last (versionBranch version) == 0
@@ -47,13 +48,21 @@
           " (",
           T.pack (giCommitDate gi),
           ")",
-          dirty
+          dirty,
+          "\n"
         ]
       where
         branch
           | giBranch gi == "master" = ""
           | otherwise = T.pack (giBranch gi) <> " @ "
         dirty = if giDirty gi then " [modified]" else ""
+
+    ghcversion = "Compiled with GHC " <> showText a <> "." <> showText b <> "." <> showText c <> ".\n"
+      where
+        a, b, c :: Int
+        a = __GLASGOW_HASKELL__ `div` 100
+        b = __GLASGOW_HASKELL__ `mod` 100
+        c = __GLASGOW_HASKELL_PATCHLEVEL1__
 
 commitIdFromFile :: Maybe String
 commitIdFromFile = trim . BS.unpack <$> $(embedFileIfExists "./commit-id")
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
@@ -855,7 +855,7 @@
   f' <- eval env f
   foldM (apply loc env) f' args'
   where
-    evalArg' (Info (_, ext), x) = evalArg env x ext
+    evalArg' (Info ext, x) = evalArg env x ext
 evalAppExp env (Index e is loc) = do
   is' <- mapM (evalDimIndex env) is
   arr <- eval env e
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
@@ -502,7 +502,7 @@
 Constr :: { (Name, Loc) }
         : constructor { let L _ (CONSTRUCTOR c) = $1 in (c, locOf $1) }
 
-TypeArg :: { TypeArgExp NoInfo Name }
+TypeArg :: { TypeArgExp UncheckedExp Name }
          : SizeExp %prec top
            { TypeArgExpSize $1 }
          | TypeExpAtom
@@ -522,7 +522,7 @@
             | TypeExp ',' TupleTypes { $1 : $3 }
 
 
-SizeExp :: { SizeExp NoInfo Name }
+SizeExp :: { SizeExp UncheckedExp }
          : '[' Exp ']'    { SizeExp $2 (srcspan $1 $>) }
          | '['     ']'    { SizeExpAny (srcspan $1 $>) }
          | '...[' Exp ']' { SizeExp $2 (srcspan $1 $>) }
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
@@ -86,7 +86,7 @@
   pretty (BoolValue False) = "false"
   pretty (FloatValue v) = pretty v
 
-instance (Eq vn, IsName vn, Annot f) => Pretty (SizeExp f vn) where
+instance (Pretty d) => Pretty (SizeExp d) where
   pretty SizeExpAny {} = brackets mempty
   pretty (SizeExp e _) = brackets $ pretty e
 
@@ -167,7 +167,7 @@
 instance Pretty (TypeArg Size) where
   pretty = prettyTypeArg 0
 
-instance (Eq vn, IsName vn, Annot f) => Pretty (TypeExp f vn) where
+instance (IsName vn, Pretty d) => Pretty (TypeExp d vn) where
   pretty (TEUnique t _) = "*" <> pretty t
   pretty (TEArray d at _) = pretty d <> pretty at
   pretty (TETuple ts _) = parens $ commasep $ map pretty ts
@@ -188,7 +188,7 @@
   pretty (TEDim dims te _) =
     "?" <> mconcat (map (brackets . prettyName) dims) <> "." <> pretty te
 
-instance (Eq vn, IsName vn, Annot f) => Pretty (TypeArgExp f vn) where
+instance (Pretty d, IsName vn) => Pretty (TypeArgExp d vn) where
   pretty (TypeArgExpSize d) = pretty d
   pretty (TypeArgExpType t) = pretty t
 
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
@@ -153,7 +153,7 @@
 -- | Return the dimensionality of a type.  For non-arrays, this is
 -- zero.  For a one-dimensional array it is one, for a two-dimensional
 -- it is two, and so forth.
-arrayRank :: TypeBase dim as -> Int
+arrayRank :: TypeBase () u -> Int
 arrayRank = shapeRank . arrayShape
 
 -- | Return the shape of a type - for non-arrays, this is 'mempty'.
@@ -310,7 +310,7 @@
 arrayOfWithAliases ::
   u ->
   Shape dim ->
-  TypeBase dim u ->
+  TypeBase dim u' ->
   TypeBase dim u
 arrayOfWithAliases u shape2 (Array _ shape1 et) =
   Array u (shape2 <> shape1) et
@@ -567,7 +567,7 @@
 patternOrderZero = orderZero . patternType
 
 -- | The set of identifiers bound in a pattern.
-patIdents :: Pat t -> [Ident t]
+patIdents :: PatBase f vn t -> [IdentBase f vn t]
 patIdents (Id v t loc) = [Ident v t loc]
 patIdents (PatParens p _) = patIdents p
 patIdents (TuplePat pats _) = foldMap patIdents pats
@@ -1499,7 +1499,7 @@
 type UncheckedType = TypeBase (Shape Name) ()
 
 -- | An unchecked type expression.
-type UncheckedTypeExp = TypeExp NoInfo Name
+type UncheckedTypeExp = TypeExp UncheckedExp 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
@@ -204,7 +204,7 @@
     Loc start end -> pos >= start && pos <= end
     NoLoc -> False
 
-atPosInTypeExp :: TypeExp Info VName -> Pos -> Maybe RawAtPos
+atPosInTypeExp :: TypeExp Exp VName -> Pos -> Maybe RawAtPos
 atPosInTypeExp te pos =
   case te of
     TEVar qn loc -> do
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
@@ -402,56 +402,110 @@
 
 -- | A dimension declaration expression for use in a 'TypeExp'.
 -- Syntactically includes the brackets.
-data SizeExp f vn
-  = -- | The size of the dimension is this expression, all of which
-    -- free variables must be in scope.
-    SizeExp (ExpBase f vn) SrcLoc
+data SizeExp d
+  = -- | The size of the dimension is this expression (or whatever),
+    -- all of which free variables must be in scope.
+    SizeExp d SrcLoc
   | -- | No dimension declaration.
     SizeExpAny SrcLoc
+  deriving (Eq, Ord, Show)
 
-instance Located (SizeExp f vn) where
+instance Functor SizeExp where
+  fmap = fmapDefault
+
+instance Foldable SizeExp where
+  foldMap = foldMapDefault
+
+instance Traversable SizeExp where
+  traverse _ (SizeExpAny loc) = pure (SizeExpAny loc)
+  traverse f (SizeExp d loc) = SizeExp <$> f d <*> pure loc
+
+instance Located (SizeExp d) where
   locOf (SizeExp _ loc) = locOf loc
   locOf (SizeExpAny loc) = locOf loc
 
-deriving instance Show (SizeExp Info VName)
+-- | A type argument expression passed to a type constructor.
+data TypeArgExp d vn
+  = TypeArgExpSize (SizeExp d)
+  | TypeArgExpType (TypeExp d vn)
+  deriving (Eq, Ord, Show)
 
-deriving instance (Show vn) => Show (SizeExp NoInfo vn)
+instance Functor (TypeArgExp d) where
+  fmap = fmapDefault
 
-deriving instance Eq (SizeExp NoInfo VName)
+instance Foldable (TypeArgExp d) where
+  foldMap = foldMapDefault
 
-deriving instance Eq (SizeExp Info VName)
+instance Traversable (TypeArgExp d) where
+  traverse = bitraverse pure
 
-deriving instance Ord (SizeExp NoInfo VName)
+instance Bifunctor TypeArgExp where
+  bimap = bimapDefault
 
-deriving instance Ord (SizeExp Info VName)
+instance Bifoldable TypeArgExp where
+  bifoldMap = bifoldMapDefault
 
+instance Bitraversable TypeArgExp where
+  bitraverse f _ (TypeArgExpSize d) = TypeArgExpSize <$> traverse f d
+  bitraverse f g (TypeArgExpType te) = TypeArgExpType <$> bitraverse f g te
+
+instance Located (TypeArgExp f vn) where
+  locOf (TypeArgExpSize e) = locOf e
+  locOf (TypeArgExpType t) = locOf t
+
 -- | 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
+data TypeExp d 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
-  | TEUnique (TypeExp f vn) SrcLoc
-  | TEApply (TypeExp f vn) (TypeArgExp f vn) SrcLoc
-  | TEArrow (Maybe vn) (TypeExp f vn) (TypeExp f vn) SrcLoc
-  | TESum [(Name, [TypeExp f vn])] SrcLoc
-  | TEDim [vn] (TypeExp f vn) SrcLoc
+  | TEParens (TypeExp d vn) SrcLoc
+  | TETuple [TypeExp d vn] SrcLoc
+  | TERecord [(Name, TypeExp d vn)] SrcLoc
+  | TEArray (SizeExp d) (TypeExp d vn) SrcLoc
+  | TEUnique (TypeExp d vn) SrcLoc
+  | TEApply (TypeExp d vn) (TypeArgExp d vn) SrcLoc
+  | TEArrow (Maybe vn) (TypeExp d vn) (TypeExp d vn) SrcLoc
+  | TESum [(Name, [TypeExp d vn])] SrcLoc
+  | TEDim [vn] (TypeExp d vn) SrcLoc
+  deriving (Eq, Ord, Show)
 
-deriving instance Show (TypeExp Info VName)
+instance Bitraversable TypeExp where
+  bitraverse _ g (TEVar v loc) =
+    TEVar <$> traverse g v <*> pure loc
+  bitraverse f g (TEParens te loc) =
+    TEParens <$> bitraverse f g te <*> pure loc
+  bitraverse f g (TETuple tes loc) =
+    TETuple <$> traverse (bitraverse f g) tes <*> pure loc
+  bitraverse f g (TERecord fs loc) =
+    TERecord <$> traverse (traverse (bitraverse f g)) fs <*> pure loc
+  bitraverse f g (TESum cs loc) =
+    TESum <$> traverse (traverse (traverse (bitraverse f g))) cs <*> pure loc
+  bitraverse f g (TEArray d te loc) =
+    TEArray <$> traverse f d <*> bitraverse f g te <*> pure loc
+  bitraverse f g (TEUnique te loc) =
+    TEUnique <$> bitraverse f g te <*> pure loc
+  bitraverse f g (TEApply te arg loc) =
+    TEApply <$> bitraverse f g te <*> bitraverse f g arg <*> pure loc
+  bitraverse f g (TEArrow pn te1 te2 loc) =
+    TEArrow <$> traverse g pn <*> bitraverse f g te1 <*> bitraverse f g te2 <*> pure loc
+  bitraverse f g (TEDim dims te loc) =
+    TEDim <$> traverse g dims <*> bitraverse f g te <*> pure loc
 
-deriving instance (Show vn) => Show (TypeExp NoInfo vn)
+instance Functor (TypeExp d) where
+  fmap = fmapDefault
 
-deriving instance Eq (TypeExp NoInfo VName)
+instance Foldable (TypeExp dim) where
+  foldMap = foldMapDefault
 
-deriving instance Eq (TypeExp Info VName)
+instance Traversable (TypeExp dim) where
+  traverse = bitraverse pure
 
-deriving instance Ord (TypeExp NoInfo VName)
+instance Bifunctor TypeExp where
+  bimap = bimapDefault
 
-deriving instance Ord (TypeExp Info VName)
+instance Bifoldable TypeExp where
+  bifoldMap = bifoldMapDefault
 
 instance Located (TypeExp f vn) where
   locOf (TEArray _ _ loc) = locOf loc
@@ -465,27 +519,6 @@
   locOf (TESum _ loc) = locOf loc
   locOf (TEDim _ _ loc) = locOf loc
 
--- | A type argument expression passed to a type constructor.
-data TypeArgExp f vn
-  = TypeArgExpSize (SizeExp f vn)
-  | TypeArgExpType (TypeExp f vn)
-
-deriving instance Show (TypeArgExp Info VName)
-
-deriving instance (Show vn) => Show (TypeArgExp NoInfo vn)
-
-deriving instance Eq (TypeArgExp NoInfo VName)
-
-deriving instance Eq (TypeArgExp Info VName)
-
-deriving instance Ord (TypeArgExp NoInfo VName)
-
-deriving instance Ord (TypeArgExp Info VName)
-
-instance Located (TypeArgExp f vn) where
-  locOf (TypeArgExpSize e) = locOf e
-  locOf (TypeArgExpType t) = locOf t
-
 -- | Information about which parts of a parameter are consumed.  This
 -- can be considered kind of an effect on the function.
 data Diet
@@ -620,16 +653,10 @@
   }
   deriving (Show)
 
-instance Eq (QualName Name) where
-  QualName qs1 v1 == QualName qs2 v2 = qs1 == qs2 && v1 == v2
-
-instance Eq (QualName VName) where
+instance (Eq v) => Eq (QualName v) where
   QualName _ v1 == QualName _ v2 = v1 == v2
 
-instance Ord (QualName Name) where
-  QualName qs1 v1 `compare` QualName qs2 v2 = compare (qs1, v1) (qs2, v2)
-
-instance Ord (QualName VName) where
+instance (Ord v) => Ord (QualName v) where
   QualName _ v1 `compare` QualName _ v2 = compare v1 v2
 
 instance Functor QualName where
@@ -669,7 +696,7 @@
     -- identical).
     Apply
       (ExpBase f vn)
-      (NE.NonEmpty (f (Diet, Maybe VName), ExpBase f vn))
+      (NE.NonEmpty (f (Maybe VName), ExpBase f vn))
       SrcLoc
   | Range
       (ExpBase f vn)
@@ -686,7 +713,7 @@
       vn
       ( [TypeParamBase vn],
         [PatBase f vn ParamType],
-        Maybe (TypeExp f vn),
+        Maybe (TypeExp (ExpBase f vn) vn),
         f ResRetType,
         ExpBase f vn
       )
@@ -797,7 +824,7 @@
   | Lambda
       [PatBase f vn ParamType]
       (ExpBase f vn)
-      (Maybe (TypeExp f vn))
+      (Maybe (TypeExp (ExpBase f vn) vn))
       (f ResRetType)
       SrcLoc
   | -- | @+@; first two types are operands, third is result.
@@ -823,9 +850,9 @@
   | -- | Array indexing as a section: @(.[i,j])@.
     IndexSection (SliceBase f vn) (f StructType) SrcLoc
   | -- | Type ascription: @e : t@.
-    Ascript (ExpBase f vn) (TypeExp f vn) SrcLoc
+    Ascript (ExpBase f vn) (TypeExp (ExpBase f vn) vn) SrcLoc
   | -- | Size coercion: @e :> t@.
-    Coerce (ExpBase f vn) (TypeExp f vn) (f StructType) SrcLoc
+    Coerce (ExpBase f vn) (TypeExp (ExpBase f vn) vn) (f StructType) SrcLoc
   | AppExp (AppExpBase f vn) (f AppRes)
 
 deriving instance Show (ExpBase Info VName)
@@ -942,7 +969,7 @@
   | PatParens (PatBase f vn t) SrcLoc
   | Id vn (f t) SrcLoc
   | Wildcard (f t) SrcLoc -- Nothing, i.e. underscore.
-  | PatAscription (PatBase f vn t) (TypeExp f vn) SrcLoc
+  | PatAscription (PatBase f vn t) (TypeExp (ExpBase f vn) vn) SrcLoc
   | PatLit PatLit (f t) SrcLoc
   | PatConstr Name (f t) [PatBase f vn t] SrcLoc
   | PatAttr (AttrInfo vn) (PatBase f vn t) SrcLoc
@@ -1003,7 +1030,7 @@
 -- classes.
 data EntryType = EntryType
   { entryType :: StructType,
-    entryAscribed :: Maybe (TypeExp Info VName)
+    entryAscribed :: Maybe (TypeExp (ExpBase Info VName) VName)
   }
   deriving (Show)
 
@@ -1033,7 +1060,7 @@
     -- may refer to abstract types that are no longer in scope.
     valBindEntryPoint :: Maybe (f EntryPoint),
     valBindName :: vn,
-    valBindRetDecl :: Maybe (TypeExp f vn),
+    valBindRetDecl :: Maybe (TypeExp (ExpBase f vn) vn),
     -- | If 'valBindParams' is null, then the 'retDims' are brought
     -- into scope at this point.
     valBindRetType :: f ResRetType,
@@ -1057,7 +1084,7 @@
   { typeAlias :: vn,
     typeLiftedness :: Liftedness,
     typeParams :: [TypeParamBase vn],
-    typeExp :: TypeExp f vn,
+    typeExp :: TypeExp (ExpBase f vn) vn,
     typeElab :: f StructRetType,
     typeDoc :: Maybe DocComment,
     typeBindLocation :: SrcLoc
@@ -1115,7 +1142,7 @@
   = ValSpec
       { specName :: vn,
         specTypeParams :: [TypeParamBase vn],
-        specTypeExp :: TypeExp f vn,
+        specTypeExp :: TypeExp (ExpBase f vn) vn,
         specType :: f StructType,
         specDoc :: Maybe DocComment,
         specLocation :: SrcLoc
@@ -1150,7 +1177,12 @@
 deriving instance Show (ModTypeExpBase NoInfo Name)
 
 -- | A type refinement.
-data TypeRefBase f vn = TypeRef (QualName vn) [TypeParamBase vn] (TypeExp f vn) SrcLoc
+data TypeRefBase f vn
+  = TypeRef
+      (QualName vn)
+      [TypeParamBase vn]
+      (TypeExp (ExpBase f vn) vn)
+      SrcLoc
 
 deriving instance Show (TypeRefBase Info VName)
 
@@ -1292,7 +1324,7 @@
 deriving instance Show (ProgBase NoInfo Name)
 
 -- | Construct an 'Apply' node, with type information.
-mkApply :: ExpBase Info vn -> [(Diet, Maybe VName, ExpBase Info vn)] -> AppRes -> ExpBase Info vn
+mkApply :: ExpBase Info vn -> [(Maybe VName, ExpBase Info vn)] -> AppRes -> ExpBase Info vn
 mkApply f args (AppRes t ext)
   | Just args' <- NE.nonEmpty $ map onArg args =
       case f of
@@ -1304,7 +1336,7 @@
           AppExp (Apply f args' (srcspan f $ snd $ NE.last args')) (Info (AppRes t ext))
   | otherwise = f
   where
-    onArg (d, v, x) = (Info (d, v), x)
+    onArg (v, x) = (Info v, x)
 
 -- | Construct an 'Apply' node, without type information.
 mkApplyUT :: ExpBase NoInfo vn -> ExpBase NoInfo vn -> ExpBase NoInfo vn
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
@@ -27,6 +27,7 @@
 where
 
 import Data.Bifunctor
+import Data.Bitraversable
 import Data.List.NonEmpty qualified as NE
 import Language.Futhark.Syntax
 
@@ -225,7 +226,7 @@
   astMap tv (ForIn pat e) = ForIn <$> astMap tv pat <*> mapOnExp tv e
   astMap tv (While e) = While <$> mapOnExp tv e
 
-instance ASTMappable (TypeExp Info VName) where
+instance ASTMappable (TypeExp (ExpBase Info VName) VName) where
   astMap tv (TEVar qn loc) =
     TEVar <$> mapOnName tv qn <*> pure loc
   astMap tv (TEParens te loc) =
@@ -247,11 +248,11 @@
   astMap tv (TEDim dims t loc) =
     TEDim dims <$> astMap tv t <*> pure loc
 
-instance ASTMappable (TypeArgExp Info VName) where
+instance ASTMappable (TypeArgExp (ExpBase Info VName) VName) where
   astMap tv (TypeArgExpSize dim) = TypeArgExpSize <$> astMap tv dim
   astMap tv (TypeArgExpType te) = TypeArgExpType <$> astMap tv te
 
-instance ASTMappable (SizeExp Info VName) where
+instance ASTMappable (SizeExp (ExpBase Info VName)) where
   astMap tv (SizeExp e loc) = SizeExp <$> mapOnExp tv e <*> pure loc
   astMap _ (SizeExpAny loc) = pure $ SizeExpAny loc
 
@@ -324,31 +325,36 @@
   astMap tv (Ident name (Info t) loc) =
     Ident name <$> (Info <$> mapOnStructType tv t) <*> pure loc
 
-traversePat :: (Monad m) => (t1 -> m t2) -> PatBase Info VName t1 -> m (PatBase Info VName t2)
-traversePat f (Id name (Info t) loc) =
+traversePat ::
+  (Monad m) =>
+  (t1 -> m t2) ->
+  (ExpBase Info VName -> m (ExpBase Info VName)) ->
+  PatBase Info VName t1 ->
+  m (PatBase Info VName t2)
+traversePat f _ (Id name (Info t) loc) =
   Id name <$> (Info <$> f t) <*> pure loc
-traversePat f (TuplePat pats loc) =
-  TuplePat <$> mapM (traversePat f) pats <*> pure loc
-traversePat f (RecordPat fields loc) =
-  RecordPat <$> mapM (traverse $ traversePat f) fields <*> pure loc
-traversePat f (PatParens pat loc) =
-  PatParens <$> traversePat f pat <*> pure loc
-traversePat f (PatAscription pat t loc) =
-  PatAscription <$> traversePat f pat <*> pure t <*> pure loc
-traversePat f (Wildcard (Info t) loc) =
+traversePat f g (TuplePat pats loc) =
+  TuplePat <$> mapM (traversePat f g) pats <*> pure loc
+traversePat f g (RecordPat fields loc) =
+  RecordPat <$> mapM (traverse $ traversePat f g) fields <*> pure loc
+traversePat f g (PatParens pat loc) =
+  PatParens <$> traversePat f g pat <*> pure loc
+traversePat f g (PatAscription pat t loc) =
+  PatAscription <$> traversePat f g pat <*> bitraverse g pure t <*> pure loc
+traversePat f _ (Wildcard (Info t) loc) =
   Wildcard <$> (Info <$> f t) <*> pure loc
-traversePat f (PatLit v (Info t) loc) =
+traversePat f _ (PatLit v (Info t) loc) =
   PatLit v <$> (Info <$> f t) <*> pure loc
-traversePat f (PatConstr n (Info t) ps loc) =
-  PatConstr n <$> (Info <$> f t) <*> mapM (traversePat f) ps <*> pure loc
-traversePat f (PatAttr attr p loc) =
-  PatAttr attr <$> traversePat f p <*> pure loc
+traversePat f g (PatConstr n (Info t) ps loc) =
+  PatConstr n <$> (Info <$> f t) <*> mapM (traversePat f g) ps <*> pure loc
+traversePat f g (PatAttr attr p loc) =
+  PatAttr attr <$> traversePat f g p <*> pure loc
 
 instance ASTMappable (PatBase Info VName StructType) where
-  astMap tv = traversePat $ mapOnStructType tv
+  astMap tv = traversePat (mapOnStructType tv) (mapOnExp tv)
 
 instance ASTMappable (PatBase Info VName ParamType) where
-  astMap tv = traversePat $ mapOnParamType tv
+  astMap tv = traversePat (mapOnParamType tv) (mapOnExp tv)
 
 instance ASTMappable (FieldBase Info VName) where
   astMap tv (RecordFieldExplicit name e loc) =
@@ -416,11 +422,11 @@
 bareCase :: CaseBase Info VName -> CaseBase NoInfo VName
 bareCase (CasePat pat e loc) = CasePat (barePat pat) (bareExp e) loc
 
-bareSizeExp :: SizeExp Info VName -> SizeExp NoInfo VName
+bareSizeExp :: SizeExp (ExpBase Info VName) -> SizeExp (ExpBase NoInfo VName)
 bareSizeExp (SizeExp e loc) = SizeExp (bareExp e) loc
 bareSizeExp (SizeExpAny loc) = SizeExpAny loc
 
-bareTypeExp :: TypeExp Info VName -> TypeExp NoInfo VName
+bareTypeExp :: TypeExp (ExpBase Info VName) VName -> TypeExp (ExpBase NoInfo VName) VName
 bareTypeExp (TEVar qn loc) = TEVar qn loc
 bareTypeExp (TEParens te loc) = TEParens (bareTypeExp te) loc
 bareTypeExp (TETuple tys loc) = TETuple (map bareTypeExp tys) loc
diff --git a/src/Language/Futhark/Tuple.hs b/src/Language/Futhark/Tuple.hs
--- a/src/Language/Futhark/Tuple.hs
+++ b/src/Language/Futhark/Tuple.hs
@@ -17,7 +17,8 @@
 areTupleFields :: M.Map Name a -> Maybe [a]
 areTupleFields fs =
   let fs' = sortFields fs
-   in if and $ zipWith (==) (map fst fs') tupleFieldNames
+   in if (null fs || length fs' > 1)
+        && and (zipWith (==) (map fst fs') tupleFieldNames)
         then Just $ map snd fs'
         else Nothing
 
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
@@ -19,7 +19,6 @@
 where
 
 import Control.Monad
-import Control.Monad.Except
 import Data.Bifunctor
 import Data.Either
 import Data.List qualified as L
@@ -33,6 +32,7 @@
 import Language.Futhark.Semantic
 import Language.Futhark.TypeChecker.Modules
 import Language.Futhark.TypeChecker.Monad
+import Language.Futhark.TypeChecker.Names
 import Language.Futhark.TypeChecker.Terms
 import Language.Futhark.TypeChecker.Types
 import Prelude hiding (abs, mod)
@@ -51,7 +51,7 @@
   UncheckedProg ->
   (Warnings, Either TypeError (FileModule, VNameSource))
 checkProg files src name prog =
-  runTypeM initialEnv files' name src checkSizeExp $ checkProgM prog
+  runTypeM initialEnv files' name src $ checkProgM prog
   where
     files' = M.map fileEnv $ M.fromList files
 
@@ -67,7 +67,13 @@
   UncheckedExp ->
   (Warnings, Either TypeError ([TypeParam], Exp))
 checkExp files src env e =
-  second (fmap fst) $ runTypeM env files' (mkInitialImport "") src checkSizeExp $ checkOneExp e
+  second (fmap fst) $
+    runTypeM
+      env
+      files'
+      (mkInitialImport "")
+      src
+      (checkOneExp =<< resolveExp e)
   where
     files' = M.map fileEnv $ M.fromList files
 
@@ -84,7 +90,7 @@
   (Warnings, Either TypeError (Env, Dec, VNameSource))
 checkDec files src env name d =
   second (fmap massage) $
-    runTypeM env files' name src checkSizeExp $ do
+    runTypeM env files' name src $ do
       (_, env', d') <- checkOneDec d
       pure (env' <> env, d')
   where
@@ -103,7 +109,7 @@
   ModExpBase NoInfo Name ->
   (Warnings, Either TypeError (MTy, ModExpBase Info VName))
 checkModExp files src env me =
-  second (fmap fst) . runTypeM env files' (mkInitialImport "") src checkSizeExp $ do
+  second (fmap fst) . runTypeM env files' (mkInitialImport "") src $ do
     (_abs, mty, me') <- checkOneModExp me
     pure (mty, me')
   where
@@ -206,9 +212,9 @@
 
 checkTypeDecl ::
   UncheckedTypeExp ->
-  TypeM ([VName], TypeExp Info VName, StructType, Liftedness)
+  TypeM ([VName], TypeExp Exp VName, StructType, Liftedness)
 checkTypeDecl te = do
-  (te', svars, RetType dims st, l) <- checkTypeExp te
+  (te', svars, RetType dims st, l) <- checkTypeExp checkSizeExp =<< resolveTypeExp te
   pure (svars ++ dims, te', toStruct st, l)
 
 -- In this function, after the recursion, we add the Env of the
@@ -219,67 +225,67 @@
 -- redundantly imported multiple times).
 checkSpecs :: [SpecBase NoInfo Name] -> TypeM (TySet, Env, [SpecBase Info VName])
 checkSpecs [] = pure (mempty, mempty, [])
-checkSpecs (ValSpec name tparams vtype NoInfo doc loc : specs) =
-  bindSpaced [(Term, name)] $ do
-    name' <- checkName Term name loc
-    (tparams', vtype', vtype_t) <-
-      checkTypeParams tparams $ \tparams' -> bindingTypeParams tparams' $ do
-        (ext, vtype', vtype_t, _) <- checkTypeDecl vtype
+checkSpecs (ValSpec name tparams vtype NoInfo doc loc : specs) = do
+  (tparams', vtype', vtype_t) <-
+    resolveTypeParams tparams $ \tparams' -> bindingTypeParams tparams' $ do
+      (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"
-              <+> dquotes (prettyName name')
-              <> "."
+      unless (null ext) $
+        typeError loc mempty $
+          "All function parameters must have non-anonymous sizes."
+            </> "Hint: add size parameters to"
+            <+> dquotes (pretty name)
+            <> "."
 
-        pure (tparams', vtype', vtype_t)
+      pure (tparams', vtype', vtype_t)
 
-    let binding = BoundV tparams' vtype_t
-        valenv =
+  bindSpaced1 Term name loc $ \name' -> do
+    let valenv =
           mempty
-            { envVtable = M.singleton name' binding,
+            { envVtable = M.singleton name' $ BoundV tparams' vtype_t,
               envNameMap = M.singleton (Term, name) $ qualName name'
             }
+    usedName name'
     (abstypes, env, specs') <- localEnv valenv $ checkSpecs specs
     pure
       ( abstypes,
         env <> valenv,
         ValSpec name' tparams' vtype' (Info vtype_t) doc loc : specs'
       )
-checkSpecs (TypeAbbrSpec tdec : specs) =
-  bindSpaced [(Type, typeAlias tdec)] $ do
-    (tenv, tdec') <- checkTypeBind tdec
+checkSpecs (TypeAbbrSpec tdec : specs) = do
+  (tenv, tdec') <- checkTypeBind tdec
+  bindSpaced1 Type (typeAlias tdec) (srclocOf tdec) $ \name' -> do
+    usedName name'
     (abstypes, env, specs') <- localEnv tenv $ checkSpecs specs
     pure
       ( abstypes,
         env <> tenv,
         TypeAbbrSpec tdec' : specs'
       )
-checkSpecs (TypeSpec l name ps doc loc : specs) =
-  checkTypeParams ps $ \ps' ->
-    bindSpaced [(Type, name)] $ do
-      name' <- checkName Type name loc
-      let tenv =
-            mempty
-              { envNameMap =
-                  M.singleton (Type, name) $ qualName name',
-                envTypeTable =
-                  M.singleton name' $
-                    TypeAbbr l ps' . RetType [] . Scalar $
-                      TypeVar mempty (qualName name') $
-                        map typeParamToArg ps'
-              }
-      (abstypes, env, specs') <- localEnv tenv $ checkSpecs specs
-      pure
-        ( M.insert (qualName name') l abstypes,
-          env <> tenv,
-          TypeSpec l name' ps' doc loc : specs'
-        )
-checkSpecs (ModSpec name sig doc loc : specs) =
-  bindSpaced [(Term, name)] $ do
-    name' <- checkName Term name loc
-    (_sig_abs, mty, sig') <- checkModTypeExp sig
+checkSpecs (TypeSpec l name ps doc loc : specs) = do
+  ps' <- resolveTypeParams ps pure
+  bindSpaced1 Type name loc $ \name' -> do
+    usedName name'
+    let tenv =
+          mempty
+            { envNameMap =
+                M.singleton (Type, name) $ qualName name',
+              envTypeTable =
+                M.singleton name' $
+                  TypeAbbr l ps' . RetType [] . Scalar $
+                    TypeVar mempty (qualName name') $
+                      map typeParamToArg ps'
+            }
+    (abstypes, env, specs') <- localEnv tenv $ checkSpecs specs
+    pure
+      ( M.insert (qualName name') l abstypes,
+        env <> tenv,
+        TypeSpec l name' ps' doc loc : specs'
+      )
+checkSpecs (ModSpec name sig doc loc : specs) = do
+  (_sig_abs, mty, sig') <- checkModTypeExp sig
+  bindSpaced1 Term name loc $ \name' -> do
+    usedName name'
     let senv =
           mempty
             { envNameMap = M.singleton (Term, name) $ qualName name',
@@ -294,7 +300,7 @@
 checkSpecs (IncludeSpec e loc : specs) = do
   (e_abs, env_abs, e_env, e') <- checkModTypeExpToEnv e
 
-  mapM_ (warnIfShadowing . fmap baseName) $ M.keys env_abs
+  mapM_ warnIfShadowing $ M.keys env_abs
 
   (abstypes, env, specs') <- localEnv e_env $ checkSpecs specs
   pure
@@ -303,11 +309,11 @@
       IncludeSpec e' loc : specs'
     )
   where
-    warnIfShadowing qn =
-      (lookupType loc qn >> warnAbout qn)
-        `catchError` \_ -> pure ()
+    warnIfShadowing qn = do
+      known <- isKnownType qn
+      when known $ warnAbout qn
     warnAbout qn =
-      warn loc $ "Inclusion shadows type" <+> dquotes (pretty qn) <+> "."
+      warn loc $ "Inclusion shadows type" <+> dquotes (pretty qn) <> "."
 
 checkModTypeExp :: ModTypeExpBase NoInfo Name -> TypeM (TySet, MTy, ModTypeExpBase Info VName)
 checkModTypeExp (ModTypeParens e loc) = do
@@ -323,7 +329,7 @@
   pure (abstypes, MTy abstypes $ ModEnv env, ModTypeSpecs specs' loc)
 checkModTypeExp (ModTypeWith s (TypeRef tname ps te trloc) loc) = do
   (abs, s_abs, s_env, s') <- checkModTypeExpToEnv s
-  checkTypeParams ps $ \ps' -> do
+  resolveTypeParams ps $ \ps' -> do
     (ext, te', te_t, _) <- bindingTypeParams ps' $ checkTypeDecl te
     unless (null ext) $
       typeError te' mempty "Anonymous dimensions are not allowed here."
@@ -333,8 +339,7 @@
   (e1_abs, MTy s_abs e1_mod, e1') <- checkModTypeExp e1
   (env_for_e2, maybe_pname') <-
     case maybe_pname of
-      Just pname -> bindSpaced [(Term, pname)] $ do
-        pname' <- checkName Term pname loc
+      Just pname -> bindSpaced1 Term pname loc $ \pname' ->
         pure
           ( mempty
               { envNameMap = M.singleton (Term, pname) $ qualName pname',
@@ -363,8 +368,8 @@
 checkModTypeBind :: ModTypeBindBase NoInfo Name -> TypeM (TySet, Env, ModTypeBindBase Info VName)
 checkModTypeBind (ModTypeBind name e doc loc) = do
   (abs, env, e') <- checkModTypeExp e
-  bindSpaced [(Signature, name)] $ do
-    name' <- checkName Signature name loc
+  bindSpaced1 Signature name loc $ \name' -> do
+    usedName name'
     pure
       ( abs,
         mempty
@@ -444,8 +449,7 @@
   TypeM a
 withModParam (ModParam pname psig_e NoInfo loc) m = do
   (_abs, MTy p_abs p_mod, psig_e') <- checkModTypeExp psig_e
-  bindSpaced [(Term, pname)] $ do
-    pname' <- checkName Term pname loc
+  bindSpaced1 Term pname loc $ \pname' -> do
     let in_body_env = mempty {envModTable = M.singleton pname' p_mod}
     localEnv in_body_env $
       m (ModParam pname' psig_e' (Info $ map qualLeaf $ M.keys p_abs) loc) p_abs p_mod
@@ -492,8 +496,8 @@
 checkModBind :: ModBindBase NoInfo Name -> TypeM (TySet, Env, ModBindBase Info VName)
 checkModBind (ModBind name [] maybe_fsig_e e doc loc) = do
   (e_abs, maybe_fsig_e', e', mty) <- checkModBody (fst <$> maybe_fsig_e) e loc
-  bindSpaced [(Term, name)] $ do
-    name' <- checkName Term name loc
+  bindSpaced1 Term name loc $ \name' -> do
+    usedName name'
     pure
       ( e_abs,
         mempty
@@ -516,8 +520,8 @@
             body_e',
             FunModType p_abs p_mod $ foldr addParam mty $ zip ps_abs ps_mod
           )
-  bindSpaced [(Term, name)] $ do
-    name' <- checkName Term name loc
+  bindSpaced1 Term name loc $ \name' -> do
+    usedName name'
     pure
       ( abs,
         mempty
@@ -554,8 +558,9 @@
   TypeBindBase NoInfo Name ->
   TypeM (Env, TypeBindBase Info VName)
 checkTypeBind (TypeBind name l tps te NoInfo doc loc) =
-  checkTypeParams tps $ \tps' -> do
-    (te', svars, RetType dims t, l') <- bindingTypeParams tps' $ checkTypeExp te
+  resolveTypeParams tps $ \tps' -> do
+    (te', svars, RetType dims t, l') <-
+      bindingTypeParams tps' $ checkTypeExp checkSizeExp =<< resolveTypeExp te
 
     let (witnessed, _) = determineSizeWitnesses $ toStruct t
     case L.find (`S.notMember` witnessed) svars of
@@ -595,8 +600,8 @@
                 <> "."
       _ -> pure ()
 
-    bindSpaced [(Type, name)] $ do
-      name' <- checkName Type name loc
+    bindSpaced1 Type name loc $ \name' -> do
+      usedName name'
       pure
         ( mempty
             { envTypeTable =
@@ -607,7 +612,7 @@
           TypeBind name' l tps' te' (Info elab_t) doc loc
         )
 
-entryPoint :: [Pat ParamType] -> Maybe (TypeExp Info VName) -> ResRetType -> EntryPoint
+entryPoint :: [Pat ParamType] -> Maybe (TypeExp Exp VName) -> ResRetType -> EntryPoint
 entryPoint params orig_ret_te (RetType _ret orig_ret) =
   EntryPoint (map patternEntry params ++ more_params) rettype'
   where
@@ -639,7 +644,7 @@
   SrcLoc ->
   [TypeParam] ->
   [Pat ParamType] ->
-  Maybe (TypeExp Info VName) ->
+  Maybe (TypeExp Exp VName) ->
   ResRetType ->
   TypeM ()
 checkEntryPoint loc tparams params maybe_tdecl rettype
@@ -687,31 +692,34 @@
     param_ts = map patternType params ++ rettype_params
 
 checkValBind :: ValBindBase NoInfo Name -> TypeM (Env, ValBind)
-checkValBind (ValBind entry fname maybe_tdecl NoInfo tparams params body doc attrs loc) = do
+checkValBind vb = do
+  (ValBind entry fname maybe_tdecl NoInfo tparams params body doc attrs loc) <-
+    resolveValBind vb
+
   top_level <- atTopLevel
   when (not top_level && isJust entry) $
     typeError loc mempty $
       withIndexLink "nested-entry" "Entry points may not be declared inside modules."
 
-  (fname', tparams', params', maybe_tdecl', rettype, body') <-
+  attrs' <- mapM checkAttr attrs
+
+  (tparams', params', maybe_tdecl', rettype, body') <-
     checkFunDef (fname, maybe_tdecl, tparams, params, body, loc)
 
   let entry' = Info (entryPoint params' maybe_tdecl' rettype) <$ entry
-
   case entry' of
     Just _ -> checkEntryPoint loc tparams' params' maybe_tdecl' rettype
     _ -> pure ()
 
-  attrs' <- mapM checkAttr attrs
-  let vb = ValBind entry' fname' maybe_tdecl' (Info rettype) tparams' params' body' doc attrs' loc
+  let vb' = ValBind entry' fname maybe_tdecl' (Info rettype) tparams' params' body' doc attrs' loc
   pure
     ( mempty
         { envVtable =
-            M.singleton fname' $ uncurry BoundV $ valBindTypeScheme vb,
+            M.singleton fname $ uncurry BoundV $ valBindTypeScheme vb',
           envNameMap =
-            M.singleton (Term, fname) $ qualName fname'
+            M.singleton (Term, baseName fname) $ qualName fname
         },
-      vb
+      vb'
     )
 
 nastyType :: (Monoid als) => TypeBase dim als -> Bool
@@ -719,7 +727,7 @@
 nastyType t@Array {} = nastyType $ stripArray 1 t
 nastyType _ = True
 
-nastyReturnType :: (Monoid als) => Maybe (TypeExp Info VName) -> TypeBase dim als -> Bool
+nastyReturnType :: (Monoid als) => Maybe (TypeExp Exp VName) -> TypeBase dim als -> Bool
 nastyReturnType Nothing (Scalar (Arrow _ _ _ t1 (RetType _ t2))) =
   nastyType t1 || nastyReturnType Nothing t2
 nastyReturnType (Just (TEArrow _ te1 te2 _)) (Scalar (Arrow _ _ _ t1 (RetType _ t2))) =
@@ -744,7 +752,7 @@
     ascripted (PatParens p' _) = ascripted p'
     ascripted _ = False
 
-niceTypeExp :: TypeExp Info VName -> Bool
+niceTypeExp :: TypeExp Exp VName -> Bool
 niceTypeExp (TEVar (QualName [] _) _) = True
 niceTypeExp (TEApply te TypeArgExpSize {} _) = niceTypeExp te
 niceTypeExp (TEArray _ te _) = niceTypeExp te
diff --git a/src/Language/Futhark/TypeChecker/Consumption.hs b/src/Language/Futhark/TypeChecker/Consumption.hs
--- a/src/Language/Futhark/TypeChecker/Consumption.hs
+++ b/src/Language/Futhark/TypeChecker/Consumption.hs
@@ -705,23 +705,25 @@
 
 --
 checkExp (AppExp (Apply f args loc) appres) = do
-  (args', args_als) <- NE.unzip <$> checkArgs args
   (f', f_als) <- checkExp f
+  (args', args_als) <- NE.unzip <$> checkArgs (toRes Nonunique f_als) args
   res_als <- checkFuncall loc (fname f) f_als args_als
   pure (AppExp (Apply f' args' loc) appres, res_als)
   where
     fname (Var v _ _) = Just v
     fname (AppExp (Apply e _ _) _) = fname e
     fname _ = Nothing
-    checkArg' prev (Info (d, p), e) = do
+    checkArg' prev d (Info p, e) = do
       (e', e_als) <- checkArg prev (second (const d) (typeOf e)) e
-      pure ((Info (d, p), e'), e_als)
+      pure ((Info p, e'), e_als)
 
-    checkArgs (x NE.:| args') = do
+    checkArgs (Scalar (Arrow _ _ d _ (RetType _ rt))) (x NE.:| args') = do
       -- Note Futhark uses right-to-left evaluation of applications.
-      args'' <- maybe (pure []) (fmap NE.toList . checkArgs) $ NE.nonEmpty args'
-      (x', x_als) <- checkArg' (map (first snd) args'') x
+      args'' <- maybe (pure []) (fmap NE.toList . checkArgs rt) $ NE.nonEmpty args'
+      (x', x_als) <- checkArg' (map (first snd) args'') d x
       pure $ (x', x_als) NE.:| args''
+    checkArgs t _ =
+      error $ "checkArgs: " <> prettyString t
 
 --
 checkExp (AppExp (Loop sparams pat args form body loc) appres) = do
@@ -973,7 +975,7 @@
 -- | Type-check a value definition.  This also infers a new return
 -- type that may be more unique than previously.
 checkValDef ::
-  (VName, [Pat ParamType], Exp, ResRetType, Maybe (TypeExp Info VName), SrcLoc) ->
+  (VName, [Pat ParamType], Exp, ResRetType, Maybe (TypeExp Exp VName), SrcLoc) ->
   ((Exp, ResRetType), [TypeError])
 checkValDef (_fname, params, body, RetType ext ret, retdecl, loc) = runCheckM (locOf loc) $ do
   fmap fst . bindingParams params $ do
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
@@ -8,9 +8,12 @@
     atTopLevel,
     enteringModule,
     bindSpaced,
+    bindSpaced1,
+    bindIdents,
     qualifyTypeVars,
     lookupMTy,
     lookupImport,
+    lookupMod,
     localEnv,
     TypeError (..),
     prettyTypeError,
@@ -18,15 +21,18 @@
     withIndexLink,
     unappliedFunctor,
     unknownVariable,
-    unknownType,
     underscoreUse,
     Notes,
     aNote,
     MonadTypeChecker (..),
     TypeState (stateNameSource),
+    usedName,
     checkName,
     checkAttr,
+    checkQualName,
+    checkValName,
     badOnLeft,
+    isKnownType,
     module Language.Futhark.Warnings,
     Env (..),
     TySet,
@@ -56,10 +62,11 @@
 import Control.Monad.Reader
 import Control.Monad.State.Strict
 import Data.Either
-import Data.List (find, isPrefixOf)
+import Data.List (find)
 import Data.Map.Strict qualified as M
 import Data.Maybe
 import Data.Set qualified as S
+import Data.Text qualified as T
 import Data.Version qualified as Version
 import Futhark.FreshNames hiding (newName)
 import Futhark.FreshNames qualified
@@ -138,11 +145,6 @@
   typeError loc mempty $
     "Unknown" <+> pretty space <+> dquotes (pretty name)
 
--- | An unknown type was referenced.
-unknownType :: (MonadTypeChecker m) => SrcLoc -> QualName Name -> m a
-unknownType loc name =
-  typeError loc mempty $ "Unknown type" <+> pretty name <> "."
-
 -- | A name prefixed with an underscore was used.
 underscoreUse ::
   (MonadTypeChecker m) =>
@@ -165,13 +167,14 @@
     contextImportName :: ImportName,
     -- | Currently type-checking at the top level?  If false, we are
     -- inside a module.
-    contextAtTopLevel :: Bool,
-    contextCheckExp :: UncheckedExp -> TypeM Exp
+    contextAtTopLevel :: Bool
   }
 
 data TypeState = TypeState
   { stateNameSource :: VNameSource,
     stateWarnings :: Warnings,
+    -- | Which names have been used.
+    stateUsed :: S.Set VName,
     stateCounter :: Int
   }
 
@@ -209,15 +212,14 @@
   ImportTable ->
   ImportName ->
   VNameSource ->
-  (UncheckedExp -> TypeM Exp) ->
   TypeM a ->
   (Warnings, Either TypeError (a, VNameSource))
-runTypeM env imports fpath src checker (TypeM m) = do
-  let ctx = Context env imports fpath True checker
-      s = TypeState src mempty 0
+runTypeM env imports fpath src (TypeM m) = do
+  let ctx = Context env imports fpath True
+      s = TypeState src mempty mempty 0
   case runExcept $ runStateT (runReaderT m ctx) s of
     Left (ws, e) -> (ws, Left e)
-    Right (x, TypeState src' ws _) -> (ws, Right (x, src'))
+    Right (x, s') -> (stateWarnings s', Right (x, stateNameSource s'))
 
 -- | Retrieve the current 'Env'.
 askEnv :: TypeM Env
@@ -272,6 +274,11 @@
   put s {stateCounter = stateCounter s + 1}
   pure $ stateCounter s
 
+bindNameMap :: NameMap -> TypeM a -> TypeM a
+bindNameMap m = local $ \ctx ->
+  let env = contextEnv ctx
+   in ctx {contextEnv = env {envNameMap = m <> envNameMap env}}
+
 -- | Monads that support type checking.  The reason we have this
 -- internal interface is because we use distinct monads for checking
 -- expressions and declarations.
@@ -281,40 +288,63 @@
 
   newName :: VName -> m VName
   newID :: Name -> m VName
+  newID s = newName $ VName s 0
   newTypeName :: Name -> m VName
 
-  bindNameMap :: NameMap -> m a -> m a
   bindVal :: VName -> BoundV -> m a -> m a
 
-  checkQualName :: Namespace -> QualName Name -> SrcLoc -> m (QualName VName)
-
-  lookupType :: SrcLoc -> QualName Name -> m (QualName VName, [TypeParam], StructRetType, Liftedness)
-  lookupMod :: SrcLoc -> QualName Name -> m (QualName VName, Mod)
-  lookupVar :: SrcLoc -> QualName Name -> m (QualName VName, StructType)
-
-  checkExpForSize :: UncheckedExp -> m Exp
+  lookupType :: QualName VName -> m ([TypeParam], StructRetType, Liftedness)
 
   typeError :: (Located loc) => loc -> Notes -> Doc () -> m a
 
--- | Elaborate the given name in the given namespace at the given
--- location, producing the corresponding unique 'VName'.
-checkName :: (MonadTypeChecker m) => Namespace -> Name -> SrcLoc -> m VName
-checkName space name loc = qualLeaf <$> checkQualName space (qualName name) loc
+warnIfUnused :: (Namespace, VName, SrcLoc) -> TypeM ()
+warnIfUnused (ns, name, loc) = do
+  used <- gets stateUsed
+  unless (name `S.member` used || "_" `T.isPrefixOf` nameToText (baseName name)) $
+    warn loc $
+      "Unused" <+> pretty ns <+> dquotes (prettyName name) <> "."
 
--- | Map source-level names do fresh unique internal names, and
+-- | Map source-level names to fresh unique internal names, and
 -- evaluate a type checker context with the mapping active.
-bindSpaced :: (MonadTypeChecker m) => [(Namespace, Name)] -> m a -> m a
+bindSpaced :: [(Namespace, Name, SrcLoc)] -> ([VName] -> TypeM a) -> TypeM a
 bindSpaced names body = do
-  names' <- mapM (newID . snd) names
-  let mapping = M.fromList (zip names $ map qualName names')
-  bindNameMap mapping body
+  names' <- mapM (\(_, v, _) -> newID v) names
+  let mapping = M.fromList $ zip (map (\(ns, v, _) -> (ns, v)) names) $ map qualName names'
+  bindNameMap mapping (body names')
+    <* mapM_ warnIfUnused [(ns, v, loc) | ((ns, _, loc), v) <- zip names names']
 
+-- | Map single source-level name to fresh unique internal names, and
+-- evaluate a type checker context with the mapping active.
+bindSpaced1 :: Namespace -> Name -> SrcLoc -> (VName -> TypeM a) -> TypeM a
+bindSpaced1 ns name loc body = do
+  name' <- newID name
+  let mapping = M.singleton (ns, name) $ qualName name'
+  bindNameMap mapping (body name') <* warnIfUnused (ns, name', loc)
+
+-- | Bind these identifiers in the name map and also check whether
+-- they have been used.
+bindIdents :: [IdentBase NoInfo VName t] -> TypeM a -> TypeM a
+bindIdents idents body = do
+  let mapping =
+        M.fromList $
+          zip
+            (map ((Term,) . (baseName . identName)) idents)
+            (map (qualName . identName) idents)
+  bindNameMap mapping body <* mapM_ warnIfUnused [(Term, v, loc) | Ident v _ loc <- idents]
+
+-- | Indicate that this name has been used. This is usually done
+-- implicitly by other operations, but sometimes we want to make a
+-- "fake" use to avoid things like top level functions being
+-- considered unused.
+usedName :: VName -> TypeM ()
+usedName name = modify $ \s -> s {stateUsed = S.insert name $ stateUsed s}
+
 instance MonadTypeChecker TypeM where
   warnings ws =
     modify $ \s -> s {stateWarnings = stateWarnings s <> ws}
 
   warn loc problem =
-    warnings $ singleWarning (srclocOf loc) problem
+    warnings $ singleWarning (locOf loc) problem
 
   newName v = do
     s <- get
@@ -322,16 +352,10 @@
     put $ s {stateNameSource = src'}
     pure v'
 
-  newID s = newName $ VName s 0
-
   newTypeName name = do
     i <- incCounter
     newID $ mkTypeVarName name i
 
-  bindNameMap m = local $ \ctx ->
-    let env = contextEnv ctx
-     in ctx {contextEnv = env {envNameMap = m <> envNameMap env}}
-
   bindVal v t = local $ \ctx ->
     ctx
       { contextEnv =
@@ -340,50 +364,27 @@
             }
       }
 
-  checkQualName space name loc = snd <$> checkQualNameWithEnv space name loc
-
-  lookupType loc qn = do
+  lookupType qn = do
     outer_env <- askEnv
-    (scope, qn'@(QualName qs name)) <- checkQualNameWithEnv Type qn loc
-    case M.lookup name $ envTypeTable scope of
-      Nothing -> unknownType loc qn
+    scope <- lookupQualNameEnv qn
+    case M.lookup (qualLeaf qn) $ envTypeTable scope of
+      Nothing -> error $ "lookupType: " <> show qn
       Just (TypeAbbr l ps (RetType dims def)) ->
-        pure (qn', ps, RetType dims $ qualifyTypeVars outer_env mempty qs def, l)
-
-  lookupMod loc qn = do
-    (scope, qn'@(QualName _ name)) <- checkQualNameWithEnv Term qn loc
-    case M.lookup name $ envModTable scope of
-      Nothing -> unknownVariable Term qn loc
-      Just m -> pure (qn', m)
-
-  lookupVar loc qn = do
-    outer_env <- askEnv
-    (env, qn'@(QualName qs name)) <- checkQualNameWithEnv Term qn loc
-    case M.lookup name $ envVtable env of
-      Nothing -> unknownVariable Term qn loc
-      Just (BoundV _ t)
-        | "_" `isPrefixOf` baseString name -> underscoreUse loc qn
-        | otherwise ->
-            case getType t of
-              Nothing ->
-                typeError loc mempty $
-                  "Attempt to use function" <+> prettyName name <+> "as value."
-              Just t' ->
-                pure
-                  ( qn',
-                    qualifyTypeVars outer_env mempty qs t'
-                  )
-
-  checkExpForSize e = do
-    checker <- asks contextCheckExp
-    checker e
+        pure (ps, RetType dims $ qualifyTypeVars outer_env mempty (qualQuals qn) def, l)
 
   typeError loc notes s = throwError $ TypeError (locOf loc) notes s
 
--- | Extract from a type a first-order type.
-getType :: TypeBase dim as -> Maybe (TypeBase dim as)
-getType (Scalar Arrow {}) = Nothing
-getType t = Just t
+lookupQualNameEnv :: QualName VName -> TypeM Env
+lookupQualNameEnv qn@(QualName quals _) = do
+  env <- askEnv
+  descend env quals
+  where
+    descend scope [] = pure scope
+    descend scope (q : qs)
+      | Just (ModEnv q_scope) <- M.lookup q $ envModTable scope =
+          descend q_scope qs
+      | otherwise =
+          error $ "lookupQualNameEnv: " ++ show qn
 
 checkQualNameWithEnv :: Namespace -> QualName Name -> SrcLoc -> TypeM (Env, QualName VName)
 checkQualNameWithEnv space qn@(QualName quals name) loc = do
@@ -391,13 +392,15 @@
   descend env quals
   where
     descend scope []
-      | Just name' <- M.lookup (space, name) $ envNameMap scope =
+      | Just name' <- M.lookup (space, name) $ envNameMap scope = do
+          usedName $ qualLeaf name'
           pure (scope, name')
       | otherwise =
           unknownVariable space qn loc
     descend scope (q : qs)
       | Just (QualName _ q') <- M.lookup (Term, q) $ envNameMap scope,
-        Just res <- M.lookup q' $ envModTable scope =
+        Just res <- M.lookup q' $ envModTable scope = do
+          usedName q'
           case res of
             ModEnv q_scope -> do
               (scope', QualName qs' name') <- descend q_scope qs
@@ -406,6 +409,49 @@
       | otherwise =
           unknownVariable space qn loc
 
+-- | Elaborate the given qualified name in the given namespace at the
+-- given location, producing the corresponding unique 'QualName'.
+-- Fails if the name is a module.
+checkValName :: QualName Name -> SrcLoc -> TypeM (QualName VName)
+checkValName name loc = do
+  (env, name') <- checkQualNameWithEnv Term name loc
+  case M.lookup (qualLeaf name') $ envModTable env of
+    Just _ -> unknownVariable Term name loc
+    Nothing -> pure name'
+
+-- | Elaborate the given qualified name in the given namespace at the
+-- given location, producing the corresponding unique 'QualName'.
+checkQualName :: Namespace -> QualName Name -> SrcLoc -> TypeM (QualName VName)
+checkQualName space name loc = snd <$> checkQualNameWithEnv space name loc
+
+-- | Elaborate the given name in the given namespace at the given
+-- location, producing the corresponding unique 'VName'.
+checkName :: Namespace -> Name -> SrcLoc -> TypeM VName
+checkName space name loc = qualLeaf <$> checkQualName space (qualName name) loc
+
+-- | Does a type with this name already exist? This is used for
+-- warnings, so it is OK it's a little unprincipled.
+isKnownType :: QualName VName -> TypeM Bool
+isKnownType qn = do
+  env <- askEnv
+  descend env (qualQuals qn) (qualLeaf qn)
+  where
+    descend env [] v
+      | Just v' <- M.lookup (Type, baseName v) $ envNameMap env =
+          pure $ M.member (qualLeaf v') $ envTypeTable env
+    descend env (q : qs) v
+      | Just q' <- M.lookup (Term, baseName q) $ envNameMap env,
+        Just (ModEnv env') <- M.lookup (qualLeaf q') $ envModTable env =
+          descend env' qs v
+    descend _ _ _ = pure False
+
+lookupMod :: SrcLoc -> QualName Name -> TypeM (QualName VName, Mod)
+lookupMod loc qn = do
+  (scope, qn'@(QualName _ name)) <- checkQualNameWithEnv Term qn loc
+  case M.lookup name $ envModTable scope of
+    Nothing -> unknownVariable Term qn loc
+    Just m -> pure (qn', m)
+
 -- | Try to prepend qualifiers to the type names such that they
 -- represent how to access the type in some scope.
 qualifyTypeVars ::
@@ -537,7 +583,7 @@
     subscript = flip lookup $ zip "0123456789" "₀₁₂₃₄₅₆₇₈₉"
 
 -- | Type-check an attribute.
-checkAttr :: (MonadTypeChecker m) => AttrInfo Name -> m (AttrInfo VName)
+checkAttr :: (MonadTypeChecker m) => AttrInfo VName -> m (AttrInfo VName)
 checkAttr (AttrComp f attrs loc) =
   AttrComp f <$> mapM checkAttr attrs <*> pure loc
 checkAttr (AttrAtom (AtomName v) loc) =
diff --git a/src/Language/Futhark/TypeChecker/Names.hs b/src/Language/Futhark/TypeChecker/Names.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Futhark/TypeChecker/Names.hs
@@ -0,0 +1,475 @@
+-- | Resolve names.
+--
+-- This also performs a small amount of rewriting; specifically
+-- turning 'Var's with qualified names into 'Project's, based on
+-- whether they are referencing a module or not.
+--
+-- Also checks for other name-related problems, such as duplicate
+-- names.
+module Language.Futhark.TypeChecker.Names
+  ( resolveValBind,
+    resolveTypeParams,
+    resolveTypeExp,
+    resolveExp,
+  )
+where
+
+import Control.Monad
+import Control.Monad.Except
+import Control.Monad.State
+import Data.List qualified as L
+import Data.Map qualified as M
+import Data.Text qualified as T
+import Futhark.Util.Pretty
+import Language.Futhark
+import Language.Futhark.Semantic (includeToFilePath)
+import Language.Futhark.TypeChecker.Monad
+import Prelude hiding (mod)
+
+-- | Names that may not be shadowed.
+doNotShadow :: [Name]
+doNotShadow = ["&&", "||"]
+
+checkDoNotShadow :: (Located a) => a -> Name -> TypeM ()
+checkDoNotShadow loc v =
+  when (v `elem` doNotShadow) $
+    typeError loc mempty . withIndexLink "may-not-be-redefined" $
+      "The" <+> prettyName v <+> "operator may not be redefined."
+
+-- | Check whether the type contains arrow types that define the same
+-- parameter.  These might also exist further down, but that's not
+-- really a problem - we mostly do this checking to help the user,
+-- since it is likely an error, but it's easy to assign a semantics to
+-- it (normal name shadowing).
+checkForDuplicateNamesInType :: TypeExp (ExpBase NoInfo Name) Name -> TypeM ()
+checkForDuplicateNamesInType = check mempty
+  where
+    bad v loc prev_loc =
+      typeError loc mempty $
+        "Name"
+          <+> dquotes (pretty v)
+          <+> "also bound at"
+          <+> pretty (locStr prev_loc)
+          <> "."
+
+    check seen (TEArrow (Just v) t1 t2 loc)
+      | Just prev_loc <- M.lookup v seen =
+          bad v loc prev_loc
+      | otherwise =
+          check seen' t1 >> check seen' t2
+      where
+        seen' = M.insert v loc seen
+    check seen (TEArrow Nothing t1 t2 _) =
+      check seen t1 >> check seen t2
+    check seen (TETuple ts _) = mapM_ (check seen) ts
+    check seen (TERecord fs _) = mapM_ (check seen . snd) fs
+    check seen (TEUnique t _) = check seen t
+    check seen (TESum cs _) = mapM_ (mapM (check seen) . snd) cs
+    check seen (TEApply t1 (TypeArgExpType t2) _) =
+      check seen t1 >> check seen t2
+    check seen (TEApply t1 TypeArgExpSize {} _) =
+      check seen t1
+    check seen (TEDim (v : vs) t loc)
+      | Just prev_loc <- M.lookup v seen =
+          bad v loc prev_loc
+      | otherwise =
+          check (M.insert v loc seen) (TEDim vs t loc)
+    check seen (TEDim [] t _) =
+      check seen t
+    check _ TEArray {} = pure ()
+    check _ TEVar {} = pure ()
+    check seen (TEParens te _) = check seen te
+
+-- | Check for duplication of names inside a binding group.
+checkForDuplicateNames ::
+  (MonadTypeChecker m) => [UncheckedTypeParam] -> [UncheckedPat t] -> m ()
+checkForDuplicateNames tps pats = (`evalStateT` mempty) $ do
+  mapM_ checkTypeParam tps
+  mapM_ checkPat pats
+  where
+    checkTypeParam (TypeParamType _ v loc) = seen Type v loc
+    checkTypeParam (TypeParamDim v loc) = seen Term v loc
+
+    checkPat (Id v _ loc) = seen Term v loc
+    checkPat (PatParens p _) = checkPat p
+    checkPat (PatAttr _ p _) = checkPat p
+    checkPat Wildcard {} = pure ()
+    checkPat (TuplePat ps _) = mapM_ checkPat ps
+    checkPat (RecordPat fs _) = mapM_ (checkPat . snd) fs
+    checkPat (PatAscription p _ _) = checkPat p
+    checkPat PatLit {} = pure ()
+    checkPat (PatConstr _ _ ps _) = mapM_ checkPat ps
+
+    seen ns v loc = do
+      already <- gets $ M.lookup (ns, v)
+      case already of
+        Just prev_loc ->
+          lift $
+            typeError loc mempty $
+              "Name"
+                <+> dquotes (pretty v)
+                <+> "also bound at"
+                <+> pretty (locStr prev_loc)
+                <> "."
+        Nothing ->
+          modify $ M.insert (ns, v) loc
+
+resolveQualName :: QualName Name -> SrcLoc -> TypeM (QualName VName)
+resolveQualName v loc = do
+  v' <- checkValName v loc
+  case v' of
+    QualName (q : _) _
+      | baseTag q <= maxIntrinsicTag -> do
+          me <- askImportName
+          unless (isBuiltin (includeToFilePath me)) $
+            warn loc "Using intrinsic functions directly can easily crash the compiler or result in wrong code generation."
+    _ -> pure ()
+  pure v'
+
+resolveName :: Name -> SrcLoc -> TypeM VName
+resolveName v loc = qualLeaf <$> resolveQualName (qualName v) loc
+
+resolveAttrAtom :: AttrAtom Name -> TypeM (AttrAtom VName)
+resolveAttrAtom (AtomName v) = pure $ AtomName v
+resolveAttrAtom (AtomInt x) = pure $ AtomInt x
+
+resolveAttrInfo :: AttrInfo Name -> TypeM (AttrInfo VName)
+resolveAttrInfo (AttrAtom atom loc) =
+  AttrAtom <$> resolveAttrAtom atom <*> pure loc
+resolveAttrInfo (AttrComp name infos loc) =
+  AttrComp name <$> mapM resolveAttrInfo infos <*> pure loc
+
+resolveSizeExp :: SizeExp (ExpBase NoInfo Name) -> TypeM (SizeExp (ExpBase NoInfo VName))
+resolveSizeExp (SizeExpAny loc) = pure $ SizeExpAny loc
+resolveSizeExp (SizeExp e loc) = SizeExp <$> resolveExp e <*> pure loc
+
+-- | Resolve names in a single type expression.
+resolveTypeExp ::
+  TypeExp (ExpBase NoInfo Name) Name ->
+  TypeM (TypeExp (ExpBase NoInfo VName) VName)
+resolveTypeExp orig = checkForDuplicateNamesInType orig >> f orig
+  where
+    f (TEVar v loc) =
+      TEVar <$> checkQualName Type v loc <*> pure loc
+    f (TEParens te loc) =
+      TEParens <$> f te <*> pure loc
+    f (TETuple tes loc) =
+      TETuple <$> mapM f tes <*> pure loc
+    f (TERecord fs loc) =
+      TERecord <$> mapM (traverse f) fs <*> pure loc
+    f (TEUnique te loc) =
+      TEUnique <$> f te <*> pure loc
+    f (TEApply te1 args loc) =
+      TEApply <$> f te1 <*> onArg args <*> pure loc
+      where
+        onArg (TypeArgExpSize size) = TypeArgExpSize <$> resolveSizeExp size
+        onArg (TypeArgExpType te) = TypeArgExpType <$> f te
+    f (TEArrow Nothing te1 te2 loc) =
+      TEArrow Nothing <$> f te1 <*> f te2 <*> pure loc
+    f (TEArrow (Just v) te1 te2 loc) =
+      bindSpaced1 Term v loc $ \v' -> do
+        usedName v'
+        TEArrow (Just v') <$> f te1 <*> f te2 <*> pure loc
+    f (TESum cs loc) =
+      TESum <$> mapM (traverse $ mapM f) cs <*> pure loc
+    f (TEDim vs te loc) =
+      bindSpaced (map (Term,,loc) vs) $ \vs' ->
+        TEDim vs' <$> f te <*> pure loc
+    f (TEArray size te loc) =
+      TEArray <$> resolveSizeExp size <*> f te <*> pure loc
+
+-- | Resolve names in a single expression.
+resolveExp :: ExpBase NoInfo Name -> TypeM (ExpBase NoInfo VName)
+--
+-- First all the trivial cases.
+resolveExp (Literal x loc) = pure $ Literal x loc
+resolveExp (IntLit x NoInfo loc) = pure $ IntLit x NoInfo loc
+resolveExp (FloatLit x NoInfo loc) = pure $ FloatLit x NoInfo loc
+resolveExp (StringLit x loc) = pure $ StringLit x loc
+resolveExp (Hole NoInfo loc) = pure $ Hole NoInfo loc
+--
+-- The main interesting cases (except for the ones in AppExp).
+resolveExp (Var qn NoInfo loc) = do
+  -- The qualifiers of a variable is divided into two parts: first a
+  -- possibly-empty sequence of module qualifiers, followed by a
+  -- possible-empty sequence of record field accesses.  We use scope
+  -- information to perform the split, by taking qualifiers off the
+  -- end until we find something that is not a module.
+  (qn', fields) <- findRootVar (qualQuals qn) (qualLeaf qn)
+  when ("_" `T.isPrefixOf` nameToText (qualLeaf qn)) $
+    underscoreUse loc qn
+  pure $ L.foldl' project (Var qn' NoInfo loc) fields
+  where
+    findRootVar qs name =
+      (whenFound <$> resolveQualName (QualName qs name) loc)
+        `catchError` notFound qs name
+
+    whenFound qn' = (qn', [])
+
+    notFound qs name err
+      | null qs = throwError err
+      | otherwise = do
+          (qn', fields) <-
+            findRootVar (init qs) (last qs) `catchError` const (throwError err)
+          pure (qn', fields ++ [name])
+
+    project e k = Project k e NoInfo loc
+--
+resolveExp (Lambda params body ret NoInfo loc) = do
+  checkForDuplicateNames [] params
+  resolveParams params $ \params' -> do
+    body' <- resolveExp body
+    ret' <- traverse resolveTypeExp ret
+    pure $ Lambda params' body' ret' NoInfo loc
+--
+resolveExp (QualParens (modname, modnameloc) e loc) = do
+  (modname', mod) <- lookupMod loc modname
+  case mod of
+    ModEnv env -> localEnv (qualifyEnv modname' env) $ do
+      e' <- resolveExp e
+      pure $ QualParens (modname', modnameloc) e' loc
+    ModFun {} ->
+      typeError loc mempty . withIndexLink "module-is-parametric" $
+        "Module" <+> pretty modname <+> " is a parametric module."
+  where
+    qualifyEnv modname' env =
+      env {envNameMap = qualify' modname' <$> envNameMap env}
+    qualify' modname' (QualName qs name) =
+      QualName (qualQuals modname' ++ [qualLeaf modname'] ++ qs) name
+
+--
+-- The tedious recursive cases.
+resolveExp (Parens e loc) =
+  Parens <$> resolveExp e <*> pure loc
+resolveExp (Attr attr e loc) =
+  Attr <$> resolveAttrInfo attr <*> resolveExp e <*> pure loc
+resolveExp (TupLit es loc) =
+  TupLit <$> mapM resolveExp es <*> pure loc
+resolveExp (ArrayLit es NoInfo loc) =
+  ArrayLit <$> mapM resolveExp es <*> pure NoInfo <*> pure loc
+resolveExp (Negate e loc) =
+  Negate <$> resolveExp e <*> pure loc
+resolveExp (Not e loc) =
+  Not <$> resolveExp e <*> pure loc
+resolveExp (Assert e1 e2 NoInfo loc) =
+  Assert <$> resolveExp e1 <*> resolveExp e2 <*> pure NoInfo <*> pure loc
+resolveExp (RecordLit fs loc) =
+  RecordLit <$> mapM resolveField fs <*> pure loc
+  where
+    resolveField (RecordFieldExplicit k e floc) =
+      RecordFieldExplicit k <$> resolveExp e <*> pure floc
+    resolveField (RecordFieldImplicit vn NoInfo floc) =
+      RecordFieldImplicit <$> resolveName vn floc <*> pure NoInfo <*> pure floc
+resolveExp (Project k e NoInfo loc) =
+  Project k <$> resolveExp e <*> pure NoInfo <*> pure loc
+resolveExp (Constr k es NoInfo loc) =
+  Constr k <$> mapM resolveExp es <*> pure NoInfo <*> pure loc
+resolveExp (Update e1 slice e2 loc) =
+  Update <$> resolveExp e1 <*> resolveSlice slice <*> resolveExp e2 <*> pure loc
+resolveExp (RecordUpdate e1 fs e2 NoInfo loc) =
+  RecordUpdate <$> resolveExp e1 <*> pure fs <*> resolveExp e2 <*> pure NoInfo <*> pure loc
+resolveExp (OpSection v NoInfo loc) =
+  OpSection <$> resolveQualName v loc <*> pure NoInfo <*> pure loc
+resolveExp (OpSectionLeft v info1 e info2 info3 loc) =
+  OpSectionLeft
+    <$> resolveQualName v loc
+    <*> pure info1
+    <*> resolveExp e
+    <*> pure info2
+    <*> pure info3
+    <*> pure loc
+resolveExp (OpSectionRight v info1 e info2 info3 loc) =
+  OpSectionRight
+    <$> resolveQualName v loc
+    <*> pure info1
+    <*> resolveExp e
+    <*> pure info2
+    <*> pure info3
+    <*> pure loc
+resolveExp (ProjectSection ks info loc) =
+  pure $ ProjectSection ks info loc
+resolveExp (IndexSection slice info loc) =
+  IndexSection <$> resolveSlice slice <*> pure info <*> pure loc
+resolveExp (Ascript e te loc) =
+  Ascript <$> resolveExp e <*> resolveTypeExp te <*> pure loc
+resolveExp (Coerce e te info loc) =
+  Coerce <$> resolveExp e <*> resolveTypeExp te <*> pure info <*> pure loc
+resolveExp (AppExp e NoInfo) =
+  AppExp <$> resolveAppExp e <*> pure NoInfo
+
+sizeBinderToParam :: SizeBinder Name -> UncheckedTypeParam
+sizeBinderToParam (SizeBinder v loc) = TypeParamDim v loc
+
+resolveAppExp :: AppExpBase NoInfo Name -> TypeM (AppExpBase NoInfo VName)
+resolveAppExp (Apply f args loc) =
+  Apply <$> resolveExp f <*> traverse (traverse resolveExp) args <*> pure loc
+resolveAppExp (Range e1 e2 e3 loc) =
+  Range
+    <$> resolveExp e1
+    <*> traverse resolveExp e2
+    <*> traverse resolveExp e3
+    <*> pure loc
+resolveAppExp (If e1 e2 e3 loc) =
+  If <$> resolveExp e1 <*> resolveExp e2 <*> resolveExp e3 <*> pure loc
+resolveAppExp (Match e cases loc) =
+  Match <$> resolveExp e <*> mapM resolveCase cases <*> pure loc
+  where
+    resolveCase (CasePat p body cloc) =
+      resolvePat p $ \p' -> CasePat p' <$> resolveExp body <*> pure cloc
+resolveAppExp (LetPat sizes p e1 e2 loc) = do
+  checkForDuplicateNames (map sizeBinderToParam sizes) [p]
+  resolveSizes sizes $ \sizes' -> do
+    e1' <- resolveExp e1
+    resolvePat p $ \p' -> do
+      e2' <- resolveExp e2
+      pure $ LetPat sizes' p' e1' e2' loc
+resolveAppExp (LetFun fname (tparams, params, ret, NoInfo, fbody) body loc) = do
+  checkForDuplicateNames tparams params
+  checkDoNotShadow loc fname
+  (tparams', params', ret', fbody') <-
+    resolveTypeParams tparams $ \tparams' ->
+      resolveParams params $ \params' -> do
+        ret' <- traverse resolveTypeExp ret
+        (tparams',params',ret',) <$> resolveExp fbody
+  bindSpaced1 Term fname loc $ \fname' -> do
+    body' <- resolveExp body
+    pure $ LetFun fname' (tparams', params', ret', NoInfo, fbody') body' loc
+resolveAppExp (LetWith (Ident dst _ dstloc) (Ident src _ srcloc) slice e1 e2 loc) = do
+  src' <- Ident <$> resolveName src srcloc <*> pure NoInfo <*> pure srcloc
+  e1' <- resolveExp e1
+  slice' <- resolveSlice slice
+  bindSpaced1 Term dst loc $ \dstv -> do
+    let dst' = Ident dstv NoInfo dstloc
+    e2' <- resolveExp e2
+    pure $ LetWith dst' src' slice' e1' e2' loc
+resolveAppExp (BinOp (f, floc) finfo (e1, info1) (e2, info2) loc) = do
+  f' <- resolveQualName f floc
+  e1' <- resolveExp e1
+  e2' <- resolveExp e2
+  pure $ BinOp (f', floc) finfo (e1', info1) (e2', info2) loc
+resolveAppExp (Index e1 slice loc) =
+  Index <$> resolveExp e1 <*> resolveSlice slice <*> pure loc
+resolveAppExp (Loop sizes pat e form body loc) = do
+  e' <- resolveExp e
+  case form of
+    For (Ident i _ iloc) bound -> do
+      bound' <- resolveExp bound
+      bindSpaced1 Term i iloc $ \iv -> do
+        let i' = Ident iv NoInfo iloc
+        resolvePat pat $ \pat' -> do
+          body' <- resolveExp body
+          pure $ Loop sizes pat' e' (For i' bound') body' loc
+    ForIn elemp arr -> do
+      arr' <- resolveExp arr
+      resolvePat elemp $ \elemp' -> resolvePat pat $ \pat' -> do
+        body' <- resolveExp body
+        pure $ Loop sizes pat' e' (ForIn elemp' arr') body' loc
+    While cond -> resolvePat pat $ \pat' -> do
+      cond' <- resolveExp cond
+      body' <- resolveExp body
+      pure $ Loop sizes pat' e' (While cond') body' loc
+
+resolveSlice :: SliceBase NoInfo Name -> TypeM (SliceBase NoInfo VName)
+resolveSlice = mapM onDimIndex
+  where
+    onDimIndex (DimFix e) = DimFix <$> resolveExp e
+    onDimIndex (DimSlice e1 e2 e3) =
+      DimSlice
+        <$> traverse resolveExp e1
+        <*> traverse resolveExp e2
+        <*> traverse resolveExp e3
+
+resolvePat :: PatBase NoInfo Name t -> (PatBase NoInfo VName t -> TypeM a) -> TypeM a
+resolvePat outer m = do
+  outer' <- resolve outer
+  bindIdents (patIdents outer') $ m outer'
+  where
+    resolve (Id v NoInfo loc) = do
+      checkDoNotShadow loc v
+      Id <$> newID v <*> pure NoInfo <*> pure loc
+    resolve (Wildcard NoInfo loc) =
+      pure $ Wildcard NoInfo loc
+    resolve (PatParens p loc) =
+      PatParens <$> resolve p <*> pure loc
+    resolve (TuplePat ps loc) =
+      TuplePat <$> mapM resolve ps <*> pure loc
+    resolve (RecordPat ps loc) =
+      RecordPat <$> mapM (traverse resolve) ps <*> pure loc
+    resolve (PatAscription p t loc) =
+      PatAscription <$> resolve p <*> resolveTypeExp t <*> pure loc
+    resolve (PatLit l NoInfo loc) =
+      pure $ PatLit l NoInfo loc
+    resolve (PatConstr k NoInfo ps loc) =
+      PatConstr k NoInfo <$> mapM resolve ps <*> pure loc
+    resolve (PatAttr attr p loc) =
+      PatAttr <$> resolveAttrInfo attr <*> resolve p <*> pure loc
+
+resolveParams :: [PatBase NoInfo Name ParamType] -> ([PatBase NoInfo VName ParamType] -> TypeM a) -> TypeM a
+resolveParams [] m = m []
+resolveParams (p : ps) m = resolvePat p $ \p' -> resolveParams ps (m . (p' :))
+
+-- | @resolveTypeParams ps m@ resolves the type parameters @ps@, then
+-- invokes the continuation @m@ with the resolveed parameters, while
+-- extending the monadic name map with @ps@.
+resolveTypeParams ::
+  [TypeParamBase Name] -> ([TypeParamBase VName] -> TypeM a) -> TypeM a
+resolveTypeParams ps m =
+  bindSpaced (map typeParamSpace ps) $ \_ ->
+    m =<< evalStateT (mapM checkTypeParam ps) mempty
+  where
+    typeParamSpace (TypeParamDim pv loc) = (Term, pv, loc)
+    typeParamSpace (TypeParamType _ pv loc) = (Type, pv, loc)
+
+    checkParamName ns v loc = do
+      seen <- gets $ M.lookup (ns, v)
+      case seen of
+        Just prev ->
+          lift $
+            typeError loc mempty $
+              "Type parameter"
+                <+> dquotes (pretty v)
+                <+> "previously defined at"
+                <+> pretty (locStr prev)
+                <> "."
+        Nothing -> do
+          modify $ M.insert (ns, v) loc
+          lift $ checkName ns v loc
+
+    checkTypeParam (TypeParamDim pv loc) =
+      TypeParamDim <$> checkParamName Term pv loc <*> pure loc
+    checkTypeParam (TypeParamType l pv loc) =
+      TypeParamType l <$> checkParamName Type pv loc <*> pure loc
+
+resolveSizes :: [SizeBinder Name] -> ([SizeBinder VName] -> TypeM a) -> TypeM a
+resolveSizes [] m = m [] -- Minor optimisation.
+resolveSizes sizes m = do
+  foldM_ lookForDuplicates mempty sizes
+  bindSpaced (map sizeWithSpace sizes) $ \sizes' ->
+    m $ zipWith SizeBinder sizes' $ map srclocOf sizes
+  where
+    lookForDuplicates prev size
+      | Just (_, prevloc) <- L.find ((== sizeName size) . fst) prev =
+          typeError size mempty $
+            "Size name also bound at "
+              <> pretty (locStrRel (srclocOf size) prevloc)
+              <> "."
+      | otherwise =
+          pure $ (sizeName size, srclocOf size) : prev
+
+    sizeWithSpace size =
+      (Term, sizeName size, srclocOf size)
+
+-- | Resolve names in a value binding. If this succeeds, then it is
+-- guaranteed that all names references things that are in scope.
+resolveValBind :: ValBindBase NoInfo Name -> TypeM (ValBindBase NoInfo VName)
+resolveValBind (ValBind entry fname ret NoInfo tparams params body doc attrs loc) = do
+  attrs' <- mapM resolveAttrInfo attrs
+  checkForDuplicateNames tparams params
+  checkDoNotShadow loc fname
+  resolveTypeParams tparams $ \tparams' ->
+    resolveParams params $ \params' -> do
+      ret' <- traverse resolveTypeExp ret
+      body' <- resolveExp body
+      bindSpaced1 Term fname loc $ \fname' -> do
+        usedName fname'
+        pure $ ValBind entry fname' ret' NoInfo tparams' params' body' doc attrs' loc
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
@@ -34,7 +34,7 @@
 import Language.Futhark.Traversals
 import Language.Futhark.TypeChecker.Consumption qualified as Consumption
 import Language.Futhark.TypeChecker.Match
-import Language.Futhark.TypeChecker.Monad hiding (BoundV)
+import Language.Futhark.TypeChecker.Monad hiding (BoundV, lookupMod)
 import Language.Futhark.TypeChecker.Terms.Loop
 import Language.Futhark.TypeChecker.Terms.Monad
 import Language.Futhark.TypeChecker.Terms.Pat
@@ -182,9 +182,9 @@
 
 checkAscript ::
   SrcLoc ->
-  UncheckedTypeExp ->
-  UncheckedExp ->
-  TermTypeM (TypeExp Info VName, Exp)
+  TypeExp (ExpBase NoInfo VName) VName ->
+  ExpBase NoInfo VName ->
+  TermTypeM (TypeExp Exp VName, Exp)
 checkAscript loc te e = do
   (te', decl_t, _) <- checkTypeExpNonrigid te
   e' <- checkExp e
@@ -197,9 +197,9 @@
 
 checkCoerce ::
   SrcLoc ->
-  UncheckedTypeExp ->
-  UncheckedExp ->
-  TermTypeM (TypeExp Info VName, StructType, Exp)
+  TypeExp (ExpBase NoInfo VName) VName ->
+  ExpBase NoInfo VName ->
+  TermTypeM (TypeExp Exp VName, StructType, Exp)
 checkCoerce loc te e = do
   (te', te_t, ext) <- checkTypeExpNonrigid te
   e' <- checkExp e
@@ -280,7 +280,7 @@
       case expKiller e' of
         Nothing -> pure e'
         Just cause -> do
-          vn <- lift $ lift $ newRigidDim tloc (RigidOutOfScope (srclocOf e) cause) "d"
+          vn <- lift $ lift $ newRigidDim tloc (RigidOutOfScope (locOf e) cause) "d"
           modify (vn :)
           pure $ sizeFromName (qualName vn) (srclocOf e)
 
@@ -347,7 +347,7 @@
 unscopeType tloc unscoped =
   sizeFree tloc $ find (`elem` unscoped) . fvVars . freeInExp
 
-checkExp :: UncheckedExp -> TermTypeM Exp
+checkExp :: ExpBase NoInfo VName -> TermTypeM Exp
 checkExp (Literal val loc) =
   pure $ Literal val loc
 checkExp (Hole _ loc) = do
@@ -365,20 +365,18 @@
   pure $ FloatLit val (Info t) loc
 checkExp (TupLit es loc) =
   TupLit <$> mapM checkExp es <*> pure loc
-checkExp (RecordLit fs loc) = do
-  fs' <- evalStateT (mapM checkField fs) mempty
-
-  pure $ RecordLit fs' loc
+checkExp (RecordLit fs loc) =
+  RecordLit <$> evalStateT (mapM checkField fs) mempty <*> pure loc
   where
     checkField (RecordFieldExplicit f e rloc) = do
       errIfAlreadySet f rloc
       modify $ M.insert f rloc
       RecordFieldExplicit f <$> lift (checkExp e) <*> pure rloc
     checkField (RecordFieldImplicit name NoInfo rloc) = do
-      errIfAlreadySet name rloc
-      (QualName _ name', t) <- lift $ lookupVar rloc $ qualName name
-      modify $ M.insert name rloc
-      pure $ RecordFieldImplicit name' (Info t) rloc
+      errIfAlreadySet (baseName name) rloc
+      t <- lift $ lookupVar rloc $ qualName name
+      modify $ M.insert (baseName name) rloc
+      pure $ RecordFieldImplicit name (Info t) rloc
 
     errIfAlreadySet f rloc = do
       maybe_sloc <- gets $ M.lookup f
@@ -492,19 +490,19 @@
   t' <- matchDims (const . const pure) t te_t
   pure $ Coerce e' te' (Info t') loc
 checkExp (AppExp (BinOp (op, oploc) NoInfo (e1, _) (e2, _) loc) NoInfo) = do
-  (op', ftype) <- lookupVar oploc op
+  ftype <- lookupVar oploc op
   e1' <- checkExp e1
   e2' <- checkExp e2
 
   -- Note that the application to the first operand cannot fix any
   -- existential sizes, because it must by necessity be a function.
-  (_, _, rt, p1_ext, _) <- checkApply loc (Just op', 0) ftype e1'
-  (_, _, rt', p2_ext, retext) <- checkApply loc (Just op', 1) rt e2'
+  (_, rt, p1_ext, _) <- checkApply loc (Just op, 0) ftype e1'
+  (_, rt', p2_ext, retext) <- checkApply loc (Just op, 1) rt e2'
 
   pure $
     AppExp
       ( BinOp
-          (op', oploc)
+          (op, oploc)
           (Info ftype)
           (e1', Info p1_ext)
           (e2', Info p2_ext)
@@ -537,52 +535,17 @@
 checkExp (Parens e loc) =
   Parens <$> checkExp e <*> pure loc
 checkExp (QualParens (modname, modnameloc) e loc) = do
-  (modname', mod) <- lookupMod loc modname
+  mod <- lookupMod modname
   case mod of
-    ModEnv env -> local (`withEnv` qualifyEnv modname' env) $ do
+    ModEnv env -> local (`withEnv` env) $ do
       e' <- checkExp e
-      pure $ QualParens (modname', modnameloc) e' loc
+      pure $ QualParens (modname, modnameloc) e' loc
     ModFun {} ->
       typeError loc mempty . withIndexLink "module-is-parametric" $
         "Module" <+> pretty modname <+> " is a parametric module."
-  where
-    qualifyEnv modname' env =
-      env {envNameMap = M.map (qualify' modname') $ envNameMap env}
-    qualify' modname' (QualName qs name) =
-      QualName (qualQuals modname' ++ [qualLeaf modname'] ++ qs) name
--- Handle common case specially for efficiency.
-checkExp (Var qn@(QualName [] _) NoInfo loc) = do
-  (qn', t) <- lookupVar loc qn
-  pure $ Var qn' (Info t) loc
 checkExp (Var qn NoInfo loc) = do
-  -- The qualifiers of a variable is divided into two parts: first a
-  -- possibly-empty sequence of module qualifiers, followed by a
-  -- possible-empty sequence of record field accesses.  We use scope
-  -- information to perform the split, by taking qualifiers off the
-  -- end until we find a module.
-
-  (qn', t, fields) <- findRootVar (qualQuals qn) (qualLeaf qn)
-
-  foldM checkField (Var qn' (Info t) loc) fields
-  where
-    findRootVar qs name =
-      (whenFound <$> lookupVar loc (QualName qs name)) `catchError` notFound qs name
-
-    whenFound (qn', t) = (qn', t, [])
-
-    notFound qs name err
-      | null qs = throwError err
-      | otherwise = do
-          (qn', t, fields) <-
-            findRootVar (init qs) (last qs)
-              `catchError` const (throwError err)
-          pure (qn', t, fields ++ [name])
-
-    checkField e k = do
-      t <- expType e
-      let usage = mkUsage loc $ docText $ "projection of field " <> dquotes (pretty k)
-      kt <- mustHaveField usage k t
-      pure $ Project k e (Info kt) loc
+  t <- lookupVar loc qn
+  pure $ Var qn (Info t) loc
 checkExp (Negate arg loc) = do
   arg' <- require "numeric negation" anyNumberType =<< checkExp arg
   pure $ Negate arg' loc
@@ -602,10 +565,10 @@
   pure $ AppExp (Apply fe' args'' loc) $ Info $ AppRes rt exts
   where
     onArg fname (i, all_exts, t) arg' = do
-      (d1, _, rt, argext, exts) <- checkApply loc (fname, i) t arg'
+      (_, rt, argext, exts) <- checkApply loc (fname, i) t arg'
       pure
         ( (i + 1, all_exts <> exts, rt),
-          (Info (d1, argext), arg')
+          (Info argext, arg')
         )
 checkExp (AppExp (LetPat sizes pat e body loc) _) = do
   e' <- checkExp e
@@ -613,58 +576,50 @@
   -- Not technically an ascription, but we want the pattern to have
   -- exactly the type of 'e'.
   t <- expType e'
-  bindingSizes sizes $ \sizes' ->
-    incLevel . bindingPat sizes' pat t $ \pat' -> do
-      body' <- incLevel $ checkExp body
-      body_t <- expTypeFully body'
+  bindingSizes sizes . incLevel . bindingPat sizes pat t $ \pat' -> do
+    body' <- incLevel $ checkExp body
+    body_t <- expTypeFully body'
 
-      -- If the bound expression is of type i64, then we replace the
-      -- pattern name with the expression in the type of the body.
-      -- Otherwise, we need to come up with unknown sizes for the
-      -- sizes going out of scope.
-      t' <- normType t -- Might be overloaded integer until now.
-      (body_t', retext) <-
-        case (t', patNames pat') of
-          (Scalar (Prim (Signed Int64)), [v])
-            | not $ hasBinding e' -> do
-                let f x = if x == v then Just (ExpSubst e') else Nothing
-                pure (applySubst f body_t, [])
-          _ ->
-            unscopeType loc (map sizeName sizes' <> patNames pat') body_t
+    -- If the bound expression is of type i64, then we replace the
+    -- pattern name with the expression in the type of the body.
+    -- Otherwise, we need to come up with unknown sizes for the
+    -- sizes going out of scope.
+    t' <- normType t -- Might be overloaded integer until now.
+    (body_t', retext) <-
+      case (t', patNames pat') of
+        (Scalar (Prim (Signed Int64)), [v])
+          | not $ hasBinding e' -> do
+              let f x = if x == v then Just (ExpSubst e') else Nothing
+              pure (applySubst f body_t, [])
+        _ ->
+          unscopeType loc (map sizeName sizes <> patNames pat') body_t
 
-      pure $
-        AppExp
-          (LetPat sizes' (fmap toStruct pat') e' body' loc)
-          (Info $ AppRes body_t' retext)
+    pure $
+      AppExp
+        (LetPat sizes (fmap toStruct pat') e' body' loc)
+        (Info $ AppRes body_t' retext)
 checkExp (AppExp (LetFun name (tparams, params, maybe_retdecl, NoInfo, e) body loc) _) = do
   (tparams', params', maybe_retdecl', rettype, e') <-
     checkBinding (name, maybe_retdecl, tparams, params, e, loc)
 
-  bindSpaced [(Term, name)] $ do
-    name' <- checkName Term name loc
-
-    let entry = BoundV tparams' $ funType params' rettype
-        bindF scope =
-          scope
-            { scopeVtable =
-                M.insert name' entry $ scopeVtable scope,
-              scopeNameMap =
-                M.insert (Term, name) (qualName name') $
-                  scopeNameMap scope
-            }
-    body' <- localScope bindF $ checkExp body
+  let entry = BoundV tparams' $ funType params' rettype
+      bindF scope =
+        scope
+          { scopeVtable = M.insert name entry $ scopeVtable scope
+          }
+  body' <- localScope bindF $ checkExp body
 
-    (body_t, ext) <- unscopeType loc [name'] =<< expTypeFully body'
+  (body_t, ext) <- unscopeType loc [name] =<< expTypeFully body'
 
-    pure $
-      AppExp
-        ( LetFun
-            name'
-            (tparams', params', maybe_retdecl', Info rettype, e')
-            body'
-            loc
-        )
-        (Info $ AppRes body_t ext)
+  pure $
+    AppExp
+      ( LetFun
+          name
+          (tparams', params', maybe_retdecl', Info rettype, e')
+          body'
+          loc
+      )
+      (Info $ AppRes body_t ext)
 checkExp (AppExp (LetWith dest src slice ve body loc) _) = do
   src' <- checkIdent src
   slice' <- checkSlice slice
@@ -732,7 +687,7 @@
   pure $ Assert e1' e2' (Info (prettyText e1)) loc
 checkExp (Lambda params body rettype_te NoInfo loc) = do
   (params', body', rettype', RetType dims ty) <-
-    incLevel . bindingParams [] params $ \_ params' -> do
+    incLevel . bindingParams [] params $ \params' -> do
       rettype_checked <- traverse checkTypeExpNonrigid rettype_te
       let declared_rettype =
             case rettype_checked of
@@ -783,17 +738,17 @@
 
       pure $ RetType (S.toList $ foldMap onDim $ fvVars $ freeInType ret) ret
 checkExp (OpSection op _ loc) = do
-  (op', ftype) <- lookupVar loc op
-  pure $ OpSection op' (Info ftype) loc
+  ftype <- lookupVar loc op
+  pure $ OpSection op (Info ftype) loc
 checkExp (OpSectionLeft op _ e _ _ loc) = do
-  (op', ftype) <- lookupVar loc op
+  ftype <- lookupVar loc op
   e' <- checkExp e
-  (_, t1, rt, argext, retext) <- checkApply loc (Just op', 0) ftype e'
+  (t1, rt, argext, retext) <- checkApply loc (Just op, 0) ftype e'
   case (ftype, rt) of
     (Scalar (Arrow _ m1 d1 _ _), Scalar (Arrow _ m2 d2 t2 rettype)) ->
       pure $
         OpSectionLeft
-          op'
+          op
           (Info ftype)
           e'
           (Info (m1, toParam d1 t1, argext), Info (m2, toParam d2 t2))
@@ -803,21 +758,21 @@
       typeError loc mempty $
         "Operator section with invalid operator of type" <+> pretty ftype
 checkExp (OpSectionRight op _ e _ NoInfo loc) = do
-  (op', ftype) <- lookupVar loc op
+  ftype <- lookupVar loc op
   e' <- checkExp e
   case ftype of
     Scalar (Arrow _ m1 d1 t1 (RetType [] (Scalar (Arrow _ m2 d2 t2 (RetType dims2 ret))))) -> do
-      (_, t2', arrow', argext, _) <-
+      (t2', arrow', argext, _) <-
         checkApply
           loc
-          (Just op', 1)
+          (Just op, 1)
           (Scalar $ Arrow mempty m2 d2 t2 $ RetType [] $ Scalar $ Arrow Nonunique m1 d1 t1 $ RetType dims2 ret)
           e'
       case arrow' of
         Scalar (Arrow _ _ _ t1' (RetType dims2' ret')) ->
           pure $
             OpSectionRight
-              op'
+              op
               (Info ftype)
               e'
               (Info (m1, toParam d1 t1'), Info (m2, toParam d2 t2', argext))
@@ -866,7 +821,7 @@
 
 checkCases ::
   StructType ->
-  NE.NonEmpty (CaseBase NoInfo Name) ->
+  NE.NonEmpty (CaseBase NoInfo VName) ->
   TermTypeM (NE.NonEmpty (CaseBase Info VName), StructType, [VName])
 checkCases mt rest_cs =
   case NE.uncons rest_cs of
@@ -881,7 +836,7 @@
 
 checkCase ::
   StructType ->
-  CaseBase NoInfo Name ->
+  CaseBase NoInfo VName ->
   TermTypeM (CaseBase Info VName, StructType, [VName])
 checkCase mt (CasePat p e loc) =
   bindingPat [] p mt $ \p' -> do
@@ -918,12 +873,12 @@
       pretty' (PatLit e _ _) = pretty e
       pretty' (PatConstr n _ ps _) = "#" <> pretty n <+> sep (map pretty' ps)
 
-checkIdent :: IdentBase NoInfo Name StructType -> TermTypeM (Ident StructType)
+checkIdent :: IdentBase NoInfo VName StructType -> TermTypeM (Ident StructType)
 checkIdent (Ident name _ loc) = do
-  (QualName _ name', vt) <- lookupVar loc (qualName name)
-  pure $ Ident name' (Info vt) loc
+  vt <- lookupVar loc $ qualName name
+  pure $ Ident name (Info vt) loc
 
-checkSlice :: UncheckedSlice -> TermTypeM [DimIndex]
+checkSlice :: SliceBase NoInfo VName -> TermTypeM [DimIndex]
 checkSlice = mapM checkDimIndex
   where
     checkDimIndex (DimFix i) = do
@@ -1001,8 +956,8 @@
   ApplyOp ->
   StructType ->
   Exp ->
-  TermTypeM (Diet, StructType, StructType, Maybe VName, [VName])
-checkApply loc (fname, _) (Scalar (Arrow _ pname d1 tp1 tp2)) argexp = do
+  TermTypeM (StructType, StructType, Maybe VName, [VName])
+checkApply loc (fname, _) (Scalar (Arrow _ pname _ tp1 tp2)) argexp = do
   let argtype = typeOf argexp
   onFailure (CheckingApply fname argexp tp1 argtype) $ do
     unify (mkUsage argexp "use as function argument") tp1 argtype
@@ -1045,7 +1000,7 @@
                    in pure (Nothing, applySubst parsubst $ toStruct tp2')
         _ -> pure (Nothing, toStruct tp2')
 
-    pure (d1, tp1, tp2'', argext, ext)
+    pure (tp1, tp2'', argext, ext)
 checkApply loc fname tfun@(Scalar TypeVar {}) arg = do
   tv <- newTypeVar loc "b"
   unify (mkUsage loc "use as function") tfun $
@@ -1083,21 +1038,21 @@
 -- | Type-check a single expression in isolation.  This expression may
 -- turn out to be polymorphic, in which case the list of type
 -- parameters will be non-empty.
-checkOneExp :: UncheckedExp -> TypeM ([TypeParam], Exp)
+checkOneExp :: ExpBase NoInfo VName -> TypeM ([TypeParam], Exp)
 checkOneExp e = runTermTypeM checkExp $ do
   e' <- checkExp e
   let t = typeOf e'
   (tparams, _, _) <-
     letGeneralise (nameFromString "<exp>") (srclocOf e) [] [] $ toRes Nonunique t
   fixOverloadedTypes $ typeVars t
-  e'' <- updateTypes e'
+  e'' <- normTypeFully e'
   localChecks e''
   causalityCheck e''
   pure (tparams, e'')
 
 -- | Type-check a single size expression in isolation.  This expression may
 -- turn out to be polymorphic, in which case it is unified with i64.
-checkSizeExp :: UncheckedExp -> TypeM Exp
+checkSizeExp :: ExpBase NoInfo VName -> TypeM Exp
 checkSizeExp e = runTermTypeM checkExp $ do
   e' <- checkExp e
   let t = typeOf e'
@@ -1105,7 +1060,7 @@
     typeError (srclocOf e') mempty . withIndexLink "size-expression-bind" $
       "Size expression with binding is forbidden."
   unify (mkUsage e' "Size expression") t (Scalar (Prim (Signed Int64)))
-  updateTypes e'
+  normTypeFully e'
 
 -- Verify that all sum type constructors and empty array literals have
 -- a size that is known (rigid or a type parameter).  This is to
@@ -1175,7 +1130,7 @@
           seqArgs known' [] = do
             void $ onExp known' f
             modify (S.fromList (appResExt res) <>)
-          seqArgs known' ((Info (_, p), x) : xs) = do
+          seqArgs known' ((Info p, x) : xs) = do
             new_known <- collectingNewKnown $ onExp known' x
             void $ seqArgs (new_known <> known') xs
             modify ((new_known <> S.fromList (maybeToList p)) <>)
@@ -1335,18 +1290,17 @@
 -- Despite the name, this is also used for checking constant
 -- definitions, by treating them as 0-ary functions.
 checkFunDef ::
-  ( Name,
-    Maybe UncheckedTypeExp,
-    [UncheckedTypeParam],
-    [UncheckedPat ParamType],
-    UncheckedExp,
+  ( VName,
+    Maybe (TypeExp (ExpBase NoInfo VName) VName),
+    [TypeParam],
+    [PatBase NoInfo VName ParamType],
+    ExpBase NoInfo VName,
     SrcLoc
   ) ->
   TypeM
-    ( VName,
-      [TypeParam],
+    ( [TypeParam],
       [Pat ParamType],
-      Maybe (TypeExp Info VName),
+      Maybe (TypeExp Exp VName),
       ResRetType,
       Exp
     )
@@ -1361,8 +1315,8 @@
       typeVars rettype' <> foldMap (typeVars . patternType) params'
 
     -- Then replace all inferred types in the body and parameters.
-    body'' <- updateTypes body'
-    params'' <- updateTypes params'
+    body'' <- normTypeFully body'
+    params'' <- mapM normTypeFully params'
     maybe_retdecl'' <- traverse updateTypes maybe_retdecl'
     rettype'' <- normTypeFully rettype'
 
@@ -1373,25 +1327,19 @@
     mapM_ (mustBeIrrefutable . fmap toStruct) params'
     localChecks body''
 
-    bindSpaced [(Term, fname)] $ do
-      fname' <- checkName Term fname loc
-      when (fname `elem` doNotShadow) $
-        typeError loc mempty . withIndexLink "may-not-be-redefined" $
-          "The" <+> prettyName fname <+> "operator may not be redefined."
-
-      let ((body''', updated_ret), errors) =
-            Consumption.checkValDef
-              ( fname',
-                params'',
-                body'',
-                RetType dims rettype'',
-                maybe_retdecl'',
-                loc
-              )
+    let ((body''', updated_ret), errors) =
+          Consumption.checkValDef
+            ( fname,
+              params'',
+              body'',
+              RetType dims rettype'',
+              maybe_retdecl'',
+              loc
+            )
 
-      mapM_ throwError errors
+    mapM_ throwError errors
 
-      pure (fname', tparams', params'', maybe_retdecl'', updated_ret, body''')
+    pure (tparams', params'', maybe_retdecl'', updated_ret, body''')
 
 -- | This is "fixing" as in "setting them", not "correcting them".  We
 -- only make very conservative fixing.
@@ -1469,22 +1417,22 @@
     hidden = hiddenParamNames params
 
 checkBinding ::
-  ( Name,
-    Maybe UncheckedTypeExp,
-    [UncheckedTypeParam],
-    [UncheckedPat ParamType],
-    UncheckedExp,
+  ( VName,
+    Maybe (TypeExp (ExpBase NoInfo VName) VName),
+    [TypeParam],
+    [PatBase NoInfo VName ParamType],
+    ExpBase NoInfo VName,
     SrcLoc
   ) ->
   TermTypeM
     ( [TypeParam],
       [Pat ParamType],
-      Maybe (TypeExp Info VName),
+      Maybe (TypeExp Exp VName),
       ResRetType,
       Exp
     )
 checkBinding (fname, maybe_retdecl, tparams, params, body, loc) =
-  incLevel . bindingParams tparams params $ \tparams' params' -> do
+  incLevel . bindingParams tparams params $ \params' -> do
     maybe_retdecl' <- traverse checkTypeExpNonrigid maybe_retdecl
 
     body' <-
@@ -1510,13 +1458,12 @@
 
     verifyFunctionParams (Just fname) params''
 
-    (tparams'', params''', rettype') <-
-      letGeneralise fname loc tparams' params''
-        =<< unscopeUnknown rettype
+    (tparams', params''', rettype') <-
+      letGeneralise (baseName fname) loc tparams params'' =<< unscopeUnknown rettype
 
     when
       ( null params
-          && any isSizeParam tparams''
+          && any isSizeParam tparams'
           && not (null (retDims rettype'))
       )
       $ typeError loc mempty
@@ -1524,9 +1471,9 @@
         </> "Type of this binding is:"
         </> indent 2 (pretty rettype')
         </> "with the following type parameters:"
-        </> indent 2 (sep $ map pretty $ filter isSizeParam tparams'')
+        </> indent 2 (sep $ map pretty $ filter isSizeParam tparams')
 
-    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.
@@ -1549,9 +1496,9 @@
 -- These restrictions apply to all functions (anonymous or otherwise).
 -- Top-level functions have further restrictions that are checked
 -- during let-generalisation.
-verifyFunctionParams :: Maybe Name -> [Pat ParamType] -> TermTypeM ()
+verifyFunctionParams :: Maybe VName -> [Pat ParamType] -> TermTypeM ()
 verifyFunctionParams fname params =
-  onFailure (CheckingParams fname) $
+  onFailure (CheckingParams (baseName <$> fname)) $
     verifyParams (foldMap patNames params) =<< mapM updateTypes params
   where
     verifyParams forbidden (p : ps)
@@ -1647,7 +1594,7 @@
     closeOver (k, NoConstraint l usage) =
       pure $ Just $ Left $ TypeParamType l k $ srclocOf usage
     closeOver (k, ParamType l loc) =
-      pure $ Just $ Left $ TypeParamType l k loc
+      pure $ Just $ Left $ TypeParamType l k $ srclocOf loc
     closeOver (k, Size Nothing usage) =
       pure $ Just $ Left $ TypeParamDim k $ srclocOf usage
     closeOver (k, UnknownSize _ _)
@@ -1723,7 +1670,7 @@
 
 checkFunBody ::
   [Pat ParamType] ->
-  UncheckedExp ->
+  ExpBase NoInfo VName ->
   Maybe ResType ->
   SrcLoc ->
   TermTypeM Exp
diff --git a/src/Language/Futhark/TypeChecker/Terms/Loop.hs b/src/Language/Futhark/TypeChecker/Terms/Loop.hs
--- a/src/Language/Futhark/TypeChecker/Terms/Loop.hs
+++ b/src/Language/Futhark/TypeChecker/Terms/Loop.hs
@@ -102,7 +102,7 @@
 
 -- | An un-checked loop.
 type UncheckedLoop =
-  (UncheckedPat ParamType, UncheckedExp, LoopFormBase NoInfo Name, UncheckedExp)
+  (PatBase NoInfo VName ParamType, ExpBase NoInfo VName, LoopFormBase NoInfo VName, ExpBase NoInfo VName)
 
 -- | A loop that has been type-checked.
 type CheckedLoop =
@@ -111,7 +111,7 @@
 -- | Type-check a @loop@ expression, passing in a function for
 -- type-checking subexpressions.
 checkLoop ::
-  (UncheckedExp -> TermTypeM Exp) ->
+  (ExpBase NoInfo VName -> TermTypeM Exp) ->
   UncheckedLoop ->
   SrcLoc ->
   TermTypeM (CheckedLoop, AppRes)
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
@@ -32,6 +32,8 @@
     unifies,
     require,
     checkTypeExpNonrigid,
+    lookupVar,
+    lookupMod,
 
     -- * Sizes
     isInt64,
@@ -58,9 +60,8 @@
 import Futhark.FreshNames qualified
 import Futhark.Util.Pretty hiding (space)
 import Language.Futhark
-import Language.Futhark.Semantic (includeToFilePath)
 import Language.Futhark.Traversals
-import Language.Futhark.TypeChecker.Monad hiding (BoundV, stateNameSource)
+import Language.Futhark.TypeChecker.Monad hiding (BoundV, lookupMod, stateNameSource)
 import Language.Futhark.TypeChecker.Monad qualified as TypeM
 import Language.Futhark.TypeChecker.Types
 import Language.Futhark.TypeChecker.Unify
@@ -93,7 +94,7 @@
   | CheckingAscription StructType StructType
   | CheckingLetGeneralise Name
   | CheckingParams (Maybe Name)
-  | CheckingPat (UncheckedPat StructType) (Inferred StructType)
+  | CheckingPat (PatBase NoInfo VName StructType) (Inferred StructType)
   | CheckingLoopBody StructType StructType
   | CheckingLoopInitial StructType StructType
   | CheckingRecordUpdate [Name] StructType StructType
@@ -195,7 +196,7 @@
   { termScope :: TermScope,
     termChecking :: Maybe Checking,
     termLevel :: Level,
-    termChecker :: UncheckedExp -> TermTypeM Exp,
+    termChecker :: ExpBase NoInfo VName -> TermTypeM Exp,
     termOuterEnv :: Env,
     termImportName :: ImportName
   }
@@ -203,21 +204,19 @@
 data TermScope = TermScope
   { scopeVtable :: M.Map VName ValBinding,
     scopeTypeTable :: M.Map VName TypeBinding,
-    scopeModTable :: M.Map VName Mod,
-    scopeNameMap :: NameMap
+    scopeModTable :: M.Map VName Mod
   }
   deriving (Show)
 
 instance Semigroup TermScope where
-  TermScope vt1 tt1 mt1 nt1 <> TermScope vt2 tt2 mt2 nt2 =
-    TermScope (vt2 `M.union` vt1) (tt2 `M.union` tt1) (mt1 `M.union` mt2) (nt2 `M.union` nt1)
+  TermScope vt1 tt1 mt1 <> TermScope vt2 tt2 mt2 =
+    TermScope (vt2 `M.union` vt1) (tt2 `M.union` tt1) (mt1 `M.union` mt2)
 
 envToTermScope :: Env -> TermScope
 envToTermScope env =
   TermScope
     { scopeVtable = vtable,
       scopeTypeTable = envTypeTable env,
-      scopeNameMap = envNameMap env,
       scopeModTable = envModTable env
     }
   where
@@ -256,7 +255,6 @@
 data TermTypeState = TermTypeState
   { stateConstraints :: Constraints,
     stateCounter :: !Int,
-    stateUsed :: S.Set VName,
     stateWarnings :: Warnings,
     stateNameSource :: VNameSource
   }
@@ -312,7 +310,7 @@
   newDimVar usage rigidity name = do
     dim <- newTypeName name
     case rigidity of
-      Rigid rsrc -> constrain dim $ UnknownSize (srclocOf usage) rsrc
+      Rigid rsrc -> constrain dim $ UnknownSize (locOf usage) rsrc
       Nonrigid -> constrain dim $ Size Nothing usage
     pure dim
 
@@ -386,58 +384,35 @@
         "instantiated size parameter of " <> dquotes (pretty qn)
       pure (v, ExpSubst $ sizeFromName (qualName v) loc)
 
-checkQualNameWithEnv :: Namespace -> QualName Name -> SrcLoc -> TermTypeM (TermScope, QualName VName)
-checkQualNameWithEnv space qn@(QualName quals name) loc = do
+lookupQualNameEnv :: QualName VName -> TermTypeM TermScope
+lookupQualNameEnv (QualName [q] _)
+  | baseTag q <= maxIntrinsicTag = asks termScope -- Magical intrinsic module.
+lookupQualNameEnv qn@(QualName quals _) = do
   scope <- asks termScope
   descend scope quals
   where
-    descend scope []
-      | Just name' <- M.lookup (space, name) $ scopeNameMap scope =
-          pure (scope, name')
-      | otherwise =
-          unknownVariable space qn loc
+    descend scope [] = pure scope
     descend scope (q : qs)
-      | Just (QualName _ q') <- M.lookup (Term, q) $ scopeNameMap scope,
-        Just res <- M.lookup q' $ scopeModTable scope =
-          case res of
-            -- Check if we are referring to the magical intrinsics
-            -- module.
-            _
-              | baseTag q' <= maxIntrinsicTag ->
-                  checkIntrinsic space qn loc
-            ModEnv q_scope -> do
-              (scope', QualName qs' name') <- descend (envToTermScope q_scope) qs
-              pure (scope', QualName (q' : qs') name')
-            ModFun {} -> unappliedFunctor loc
+      | Just (ModEnv q_scope) <- M.lookup q $ scopeModTable scope =
+          descend (envToTermScope q_scope) qs
       | otherwise =
-          unknownVariable space qn loc
+          error $ "lookupQualNameEnv " <> show qn
 
-checkIntrinsic :: Namespace -> QualName Name -> SrcLoc -> TermTypeM (TermScope, QualName VName)
-checkIntrinsic space qn@(QualName _ name) loc
-  | Just v <- M.lookup (space, name) intrinsicsNameMap = do
-      me <- asks termImportName
-      unless (isBuiltin (includeToFilePath me)) $
-        warn loc "Using intrinsic functions directly can easily crash the compiler or result in wrong code generation."
-      scope <- asks termScope
-      pure (scope, v)
-  | otherwise =
-      unknownVariable space qn loc
+lookupMod :: QualName VName -> TermTypeM Mod
+lookupMod qn@(QualName _ name) = do
+  scope <- lookupQualNameEnv qn
+  case M.lookup name $ scopeModTable scope of
+    Nothing -> error $ "lookupMod: " <> show qn
+    Just m -> pure m
 
 localScope :: (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
 localScope f = local $ \tenv -> tenv {termScope = f $ termScope tenv}
 
 instance MonadTypeChecker TermTypeM where
-  checkExpForSize e = do
-    checker <- asks termChecker
-    e' <- checker e
-    let t = toStruct $ typeOf e'
-    unify (mkUsage (srclocOf e') "Size expression") t (Scalar (Prim (Signed Int64)))
-    updateTypes e'
-
   warnings ws =
     modify $ \s -> s {stateWarnings = stateWarnings s <> ws}
 
-  warn loc problem = warnings $ singleWarning (srclocOf loc) problem
+  warn loc problem = warnings $ singleWarning (locOf loc) problem
 
   newName v = do
     s <- get
@@ -445,81 +420,25 @@
     put $ s {stateNameSource = src'}
     pure v'
 
-  newID s = newName $ VName s 0
-
   newTypeName name = do
     i <- incCounter
     newID $ mkTypeVarName name i
 
-  checkQualName space name loc = snd <$> checkQualNameWithEnv space name loc
-
-  bindNameMap m = localScope $ \scope ->
-    scope {scopeNameMap = m <> scopeNameMap scope}
-
   bindVal v (TypeM.BoundV tps t) = localScope $ \scope ->
     scope {scopeVtable = M.insert v (BoundV tps t) $ scopeVtable scope}
 
-  lookupType loc qn = do
+  lookupType qn = do
     outer_env <- asks termOuterEnv
-    (scope, qn'@(QualName qs name)) <- checkQualNameWithEnv Type qn loc
-    case M.lookup name $ scopeTypeTable scope of
-      Nothing -> unknownType loc qn
+    scope <- lookupQualNameEnv qn
+    case M.lookup (qualLeaf qn) $ scopeTypeTable scope of
+      Nothing -> error $ "lookupType: " <> show qn
       Just (TypeAbbr l ps (RetType dims def)) ->
         pure
-          ( qn',
-            ps,
-            RetType dims $ qualifyTypeVars outer_env (map typeParamName ps) qs def,
+          ( ps,
+            RetType dims $ qualifyTypeVars outer_env (map typeParamName ps) (qualQuals qn) def,
             l
           )
 
-  lookupMod loc qn = do
-    (scope, qn'@(QualName _ name)) <- checkQualNameWithEnv Term qn loc
-    case M.lookup name $ scopeModTable scope of
-      Nothing -> unknownVariable Term qn loc
-      Just m -> pure (qn', m)
-
-  lookupVar loc qn = do
-    (scope, qn'@(QualName qs name)) <- checkQualNameWithEnv Term qn loc
-    let usage = mkUsage loc $ docText $ "use of " <> dquotes (pretty qn)
-
-    t <- case M.lookup name $ scopeVtable scope of
-      Nothing ->
-        typeError loc mempty $
-          "Unknown variable" <+> dquotes (pretty qn) <> "."
-      Just (BoundV tparams t) -> do
-        when (null qs) . modify $ \s ->
-          s {stateUsed = S.insert (qualLeaf qn') $ stateUsed s}
-        when (T.head (nameToText (baseName name)) == '_') $
-          underscoreUse loc qn
-        if null tparams && null qs
-          then pure t
-          else do
-            (tnames, t') <- instantiateTypeScheme qn' loc tparams t
-            outer_env <- asks termOuterEnv
-            pure $ qualifyTypeVars outer_env tnames qs t'
-      Just EqualityF -> do
-        argtype <- newTypeVar loc "t"
-        equalityType usage argtype
-        pure $
-          Scalar . Arrow mempty Unnamed Observe argtype . RetType [] $
-            Scalar $
-              Arrow mempty Unnamed Observe argtype $
-                RetType [] $
-                  Scalar $
-                    Prim Bool
-      Just (OverloadedF ts pts rt) -> do
-        argtype <- newTypeVar loc "t"
-        mustBeOneOf ts usage argtype
-        let (pts', rt') = instOverloaded argtype pts rt
-        pure $ foldFunType (map (toParam Observe) pts') $ RetType [] $ toRes Nonunique rt'
-
-    pure (qn', t)
-    where
-      instOverloaded argtype pts rt =
-        ( map (maybe (toStruct argtype) (Scalar . Prim)) pts,
-          maybe (toStruct argtype) (Scalar . Prim) rt
-        )
-
   typeError loc notes s = do
     checking <- asks termChecking
     case checking of
@@ -528,6 +447,42 @@
       Nothing ->
         throwError $ TypeError (locOf loc) notes s
 
+lookupVar :: SrcLoc -> QualName VName -> TermTypeM StructType
+lookupVar loc qn@(QualName qs name) = do
+  scope <- lookupQualNameEnv qn
+  let usage = mkUsage loc $ docText $ "use of " <> dquotes (pretty qn)
+
+  case M.lookup name $ scopeVtable scope of
+    Nothing ->
+      error $ "lookupVar: " <> show qn
+    Just (BoundV tparams t) -> do
+      if null tparams && null qs
+        then pure t
+        else do
+          (tnames, t') <- instantiateTypeScheme qn loc tparams t
+          outer_env <- asks termOuterEnv
+          pure $ qualifyTypeVars outer_env tnames qs t'
+    Just EqualityF -> do
+      argtype <- newTypeVar loc "t"
+      equalityType usage argtype
+      pure $
+        Scalar . Arrow mempty Unnamed Observe argtype . RetType [] $
+          Scalar $
+            Arrow mempty Unnamed Observe argtype $
+              RetType [] $
+                Scalar $
+                  Prim Bool
+    Just (OverloadedF ts pts rt) -> do
+      argtype <- newTypeVar loc "t"
+      mustBeOneOf ts usage argtype
+      let (pts', rt') = instOverloaded argtype pts rt
+      pure $ foldFunType (map (toParam Observe) pts') $ RetType [] $ toRes Nonunique rt'
+  where
+    instOverloaded argtype pts rt =
+      ( map (maybe (toStruct argtype) (Scalar . Prim)) pts,
+        maybe (toStruct argtype) (Scalar . Prim) rt
+      )
+
 onFailure :: Checking -> TermTypeM a -> TermTypeM a
 onFailure c = local $ \env -> env {termChecking = Just c}
 
@@ -616,23 +571,25 @@
   mustBeOneOf ts (mkUsage (srclocOf e) why) . toStruct =<< expType e
   pure e
 
-termCheckTypeExp ::
-  TypeExp NoInfo Name ->
-  TermTypeM (TypeExp Info VName, [VName], ResRetType)
-termCheckTypeExp te = do
-  (te', svars, rettype, _l) <- checkTypeExp te
+checkExpForSize :: ExpBase NoInfo VName -> TermTypeM Exp
+checkExpForSize e = do
+  checker <- asks termChecker
+  e' <- checker e
+  let t = toStruct $ typeOf e'
+  unify (mkUsage (locOf e') "Size expression") t (Scalar (Prim (Signed Int64)))
+  updateTypes e'
 
+checkTypeExpNonrigid ::
+  TypeExp (ExpBase NoInfo VName) VName ->
+  TermTypeM (TypeExp Exp VName, ResType, [VName])
+checkTypeExpNonrigid te = do
+  (te', svars, rettype, _l) <- checkTypeExp checkExpForSize te
+
   -- No guarantee that the locally bound sizes in rettype are globally
   -- unique, but we want to turn them into size variables, so let's
-  -- give them some unique names.  Maybe this should be done below,
-  -- where we actually turn these into size variables?
+  -- give them some unique names.
   RetType dims st <- renameRetType rettype
 
-  pure (te', svars, RetType dims st)
-
-checkTypeExpNonrigid :: TypeExp NoInfo Name -> TermTypeM (TypeExp Info VName, ResType, [VName])
-checkTypeExpNonrigid te = do
-  (te', svars, RetType dims st) <- termCheckTypeExp te
   forM_ (svars ++ dims) $ \v ->
     constrain v $ Size Nothing $ mkUsage (srclocOf te) "anonymous size in type expression"
   pure (te', st, svars ++ dims)
@@ -653,7 +610,6 @@
   TermScope
     { scopeVtable = initialVtable,
       scopeTypeTable = mempty,
-      scopeNameMap = mempty,
       scopeModTable = mempty
     }
   where
@@ -679,7 +635,7 @@
       Just (name, EqualityF)
     addIntrinsicF _ = Nothing
 
-runTermTypeM :: (UncheckedExp -> TermTypeM Exp) -> TermTypeM a -> TypeM a
+runTermTypeM :: (ExpBase NoInfo VName -> TermTypeM Exp) -> TermTypeM a -> TypeM a
 runTermTypeM checker (TermTypeM m) = do
   initial_scope <- (initialTermScope <>) . envToTermScope <$> askEnv
   name <- askImportName
@@ -698,7 +654,6 @@
         TermTypeState
           { stateConstraints = mempty,
             stateCounter = 0,
-            stateUsed = mempty,
             stateWarnings = mempty,
             stateNameSource = src
           }
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
@@ -5,19 +5,16 @@
     bindingPat,
     bindingIdent,
     bindingSizes,
-    doNotShadow,
   )
 where
 
 import Control.Monad
-import Control.Monad.State
-import Data.Bitraversable
+import Data.Bifunctor
 import Data.Either
 import Data.List (find, isPrefixOf, sort)
 import Data.Map.Strict qualified as M
 import Data.Maybe
 import Data.Set qualified as S
-import Data.Text qualified as T
 import Futhark.Util.Pretty hiding (group, space)
 import Language.Futhark
 import Language.Futhark.TypeChecker.Monad hiding (BoundV)
@@ -26,27 +23,14 @@
 import Language.Futhark.TypeChecker.Unify hiding (Usage)
 import Prelude hiding (mod)
 
--- | Names that may not be shadowed.
-doNotShadow :: [Name]
-doNotShadow = ["&&", "||"]
-
-nonrigidFor :: [SizeBinder VName] -> StructType -> TermTypeM StructType
-nonrigidFor [] t = pure t -- Minor optimisation.
-nonrigidFor sizes t = evalStateT (bitraverse onDim pure t) mempty
+nonrigidFor :: [(SizeBinder VName, QualName VName)] -> StructType -> StructType
+nonrigidFor [] = id -- Minor optimisation.
+nonrigidFor sizes = first onDim
   where
-    onDim (Var (QualName _ v) typ loc)
-      | Just size <- find ((== v) . sizeName) sizes = do
-          prev <- gets $ lookup v
-          case prev of
-            Nothing -> do
-              v' <- lift $ newID $ baseName v
-              lift . constrain v' . Size Nothing $
-                mkUsage size "ambiguous size of bound expression"
-              modify ((v, v') :)
-              pure $ Var (qualName v') typ loc
-            Just v' ->
-              pure $ Var (qualName v') typ loc
-    onDim d = pure d
+    onDim (Var (QualName _ v) info loc)
+      | Just (_, v') <- find ((== v) . sizeName . fst) sizes =
+          Var v' info loc
+    onDim d = d
 
 -- | Bind these identifiers locally while running the provided action.
 binding ::
@@ -62,8 +46,8 @@
     -- integers, because they may become integers later due to
     -- inference...
     forM_ idents $ \ident ->
-      constrain (identName ident) $ ParamSize $ srclocOf ident
-    m <* checkIfUsed
+      constrain (identName ident) $ ParamSize $ locOf ident
+    m
   where
     bindVars = foldl bindVar
 
@@ -73,15 +57,6 @@
             M.insert name (BoundV [] tp) $ scopeVtable scope
         }
 
-    checkIfUsed = do
-      used <- gets stateUsed
-      forM_ (filter ((`S.notMember` used) . identName) idents) $ \ident ->
-        unless ("_" `T.isPrefixOf` nameToText (baseName (identName ident))) $
-          warn ident $
-            "Unused variable "
-              <> dquotes (prettyName (identName ident))
-              <> "."
-
 bindingTypes ::
   [Either (VName, TypeBinding) (VName, Constraint)] ->
   TermTypeM a ->
@@ -104,57 +79,34 @@
   where
     typeParamType (TypeParamType l v loc) =
       [ Left (v, TypeAbbr l [] $ RetType [] $ Scalar (TypeVar mempty (qualName v) [])),
-        Right (v, ParamType l loc)
+        Right (v, ParamType l $ locOf loc)
       ]
     typeParamType (TypeParamDim v loc) =
-      [Right (v, ParamSize loc)]
+      [Right (v, ParamSize $ locOf loc)]
 
 typeParamIdent :: TypeParam -> Maybe (Ident StructType)
 typeParamIdent (TypeParamDim v loc) =
   Just $ Ident v (Info $ Scalar $ Prim $ Signed Int64) loc
 typeParamIdent _ = Nothing
 
--- | Bind a single term-level identifier.
-bindingIdent ::
-  IdentBase NoInfo Name StructType ->
-  StructType ->
-  (Ident StructType -> TermTypeM a) ->
-  TermTypeM a
-bindingIdent (Ident v NoInfo vloc) t m =
-  bindSpaced [(Term, v)] $ do
-    v' <- checkName Term v vloc
-    let ident = Ident v' (Info t) vloc
-    binding [ident] $ m ident
-
 -- | Bind @let@-bound sizes.  This is usually followed by 'bindingPat'
 -- immediately afterwards.
-bindingSizes :: [SizeBinder Name] -> ([SizeBinder VName] -> TermTypeM a) -> TermTypeM a
-bindingSizes [] m = m [] -- Minor optimisation.
-bindingSizes sizes m = do
-  foldM_ lookForDuplicates mempty sizes
-  bindSpaced (map sizeWithSpace sizes) $ do
-    sizes' <- mapM check sizes
-    binding (map sizeWithType sizes') $ m sizes'
+bindingSizes :: [SizeBinder VName] -> TermTypeM a -> TermTypeM a
+bindingSizes [] m = m -- Minor optimisation.
+bindingSizes sizes m = binding (map sizeWithType sizes) m
   where
-    lookForDuplicates prev size
-      | Just prevloc <- M.lookup (sizeName size) prev =
-          typeError size mempty $
-            "Size name also bound at "
-              <> pretty (locStrRel (srclocOf size) prevloc)
-              <> "."
-      | otherwise =
-          pure $ M.insert (sizeName size) (srclocOf size) prev
-
-    sizeWithSpace size =
-      (Term, sizeName size)
     sizeWithType size =
       Ident (sizeName size) (Info (Scalar (Prim (Signed Int64)))) (srclocOf size)
 
-    check (SizeBinder v loc) =
-      SizeBinder <$> checkName Term v loc <*> pure loc
-
-sizeBinderToParam :: SizeBinder VName -> UncheckedTypeParam
-sizeBinderToParam (SizeBinder v loc) = TypeParamDim (baseName v) loc
+-- | Bind a single term-level identifier.
+bindingIdent ::
+  IdentBase NoInfo VName StructType ->
+  StructType ->
+  (Ident StructType -> TermTypeM a) ->
+  TermTypeM a
+bindingIdent (Ident v NoInfo vloc) t m = do
+  let ident = Ident v (Info t) vloc
+  binding [ident] $ m ident
 
 -- All this complexity is just so we can handle un-suffixed numeric
 -- literals in patterns.
@@ -171,24 +123,19 @@
   pure $ Scalar $ Prim $ primValueType v
 
 checkPat' ::
-  [SizeBinder VName] ->
-  UncheckedPat ParamType ->
+  [(SizeBinder VName, QualName VName)] ->
+  PatBase NoInfo VName ParamType ->
   Inferred ParamType ->
   TermTypeM (Pat ParamType)
 checkPat' sizes (PatParens p loc) t =
   PatParens <$> checkPat' sizes p t <*> pure loc
 checkPat' sizes (PatAttr attr p loc) t =
   PatAttr <$> checkAttr attr <*> checkPat' sizes p t <*> pure loc
-checkPat' _ (Id name _ loc) _
-  | name `elem` doNotShadow =
-      typeError loc mempty $ "The" <+> pretty name <+> "operator may not be redefined."
-checkPat' _ (Id name NoInfo loc) (Ascribed t) = do
-  name' <- newID name
-  pure $ Id name' (Info t) loc
+checkPat' _ (Id name NoInfo loc) (Ascribed t) =
+  pure $ Id name (Info t) loc
 checkPat' _ (Id name NoInfo loc) NoneInferred = do
-  name' <- newID name
   t <- newTypeVar loc "t"
-  pure $ Id name' (Info t) loc
+  pure $ Id name (Info t) loc
 checkPat' _ (Wildcard _ loc) (Ascribed t) =
   pure $ Wildcard (Info t) loc
 checkPat' _ (Wildcard NoInfo loc) NoneInferred = do
@@ -239,7 +186,7 @@
 
   case maybe_outer_t of
     Ascribed outer_t -> do
-      st_forunify <- nonrigidFor sizes $ toStruct st
+      let st_forunify = nonrigidFor sizes $ toStruct st
       unify (mkUsage loc "explicit type ascription") st_forunify (toStruct outer_t)
 
       PatAscription
@@ -290,58 +237,57 @@
     usage = mkUsage loc "matching against constructor"
 
 checkPat ::
-  [SizeBinder VName] ->
-  UncheckedPat (TypeBase Size u) ->
+  [(SizeBinder VName, QualName VName)] ->
+  PatBase NoInfo VName (TypeBase Size u) ->
   Inferred StructType ->
   (Pat ParamType -> TermTypeM a) ->
   TermTypeM a
 checkPat sizes p t m = do
-  checkForDuplicateNames (map sizeBinderToParam sizes) [p]
   p' <-
     onFailure (CheckingPat (fmap toStruct p) t) $
       checkPat' sizes (fmap (toParam Observe) p) (fmap (toParam Observe) t)
 
   let explicit = mustBeExplicitInType $ patternStructType p'
 
-  case filter ((`S.member` explicit) . sizeName) sizes of
-    size : _ ->
+  case filter ((`S.member` explicit) . sizeName . fst) sizes of
+    (size, _) : _ ->
       typeError size mempty $
         "Cannot bind"
           <+> pretty size
           <+> "as it is never used as the size of a concrete (non-function) value."
     [] ->
-      bindNameMap (patNameMap p') $ m p'
+      m p'
 
 -- | Check and bind a @let@-pattern.
 bindingPat ::
   [SizeBinder VName] ->
-  UncheckedPat (TypeBase Size u) ->
+  PatBase NoInfo VName (TypeBase Size u) ->
   StructType ->
   (Pat ParamType -> TermTypeM a) ->
   TermTypeM a
 bindingPat sizes p t m = do
-  checkPat sizes p (Ascribed t) $ \p' -> binding (patIdents (fmap toStruct p')) $
+  substs <- mapM mkSizeSubst sizes
+  checkPat substs p (Ascribed t) $ \p' -> binding (patIdents (fmap toStruct p')) $
     case filter ((`S.notMember` fvVars (freeInPat p')) . sizeName) sizes of
       [] -> m p'
       size : _ -> unusedSize size
-
-patNameMap :: Pat t -> NameMap
-patNameMap = M.fromList . map asTerm . patNames
   where
-    asTerm v = ((Term, baseName v), qualName v)
+    mkSizeSubst v = do
+      v' <- newID $ baseName $ sizeName v
+      constrain v' . Size Nothing $
+        mkUsage v "ambiguous size of bound expression"
+      pure (v, qualName v')
 
 -- | Check and bind type and value parameters.
 bindingParams ::
-  [UncheckedTypeParam] ->
-  [UncheckedPat ParamType] ->
-  ([TypeParam] -> [Pat ParamType] -> TermTypeM a) ->
+  [TypeParam] ->
+  [PatBase NoInfo VName ParamType] ->
+  ([Pat ParamType] -> TermTypeM a) ->
   TermTypeM a
-bindingParams tps orig_ps m = do
-  checkForDuplicateNames tps orig_ps
-  checkTypeParams tps $ \tps' -> bindingTypeParams tps' $ do
-    let descend ps' (p : ps) =
-          checkPat [] p NoneInferred $ \p' ->
-            binding (patIdents $ fmap toStruct p') $ incLevel $ descend (p' : ps') ps
-        descend ps' [] = m tps' $ reverse ps'
+bindingParams tps orig_ps m = bindingTypeParams tps $ do
+  let descend ps' (p : ps) =
+        checkPat [] p NoneInferred $ \p' ->
+          binding (patIdents $ fmap toStruct p') $ incLevel $ descend (p' : ps') ps
+      descend ps' [] = m $ reverse ps'
 
-    incLevel $ descend [] orig_ps
+  incLevel $ descend [] orig_ps
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
@@ -2,8 +2,6 @@
 module Language.Futhark.TypeChecker.Types
   ( checkTypeExp,
     renameRetType,
-    checkForDuplicateNames,
-    checkTypeParams,
     typeParamToArg,
     Subst (..),
     substFromAbbr,
@@ -20,7 +18,6 @@
 
 import Control.Monad
 import Control.Monad.Identity
-import Control.Monad.Reader
 import Control.Monad.State
 import Data.Bifunctor
 import Data.List (find, foldl', sort, unzip4, (\\))
@@ -86,26 +83,27 @@
       pure $ RetType dims st
 
 evalTypeExp ::
-  (MonadTypeChecker m) =>
-  TypeExp NoInfo Name ->
-  m (TypeExp Info VName, [VName], ResRetType, Liftedness)
-evalTypeExp (TEVar name loc) = do
-  (name', ps, t, l) <- lookupType loc name
+  (MonadTypeChecker m, Pretty df) =>
+  (df -> m Exp) ->
+  TypeExp df VName ->
+  m (TypeExp Exp VName, [VName], ResRetType, Liftedness)
+evalTypeExp _ (TEVar name loc) = do
+  (ps, t, l) <- lookupType name
   t' <- renameRetType $ toResRet Nonunique t
   case ps of
-    [] -> pure (TEVar name' loc, [], t', l)
+    [] -> pure (TEVar name loc, [], t', l)
     _ ->
       typeError loc mempty $
         "Type constructor"
           <+> dquotes (hsep (pretty name : map pretty ps))
           <+> "used without any arguments."
 --
-evalTypeExp (TEParens te loc) = do
-  (te', svars, ts, ls) <- evalTypeExp te
+evalTypeExp df (TEParens te loc) = do
+  (te', svars, ts, ls) <- evalTypeExp df te
   pure (TEParens te' loc, svars, ts, ls)
 --
-evalTypeExp (TETuple ts loc) = do
-  (ts', svars, ts_s, ls) <- unzip4 <$> mapM evalTypeExp ts
+evalTypeExp df (TETuple ts loc) = do
+  (ts', svars, ts_s, ls) <- unzip4 <$> mapM (evalTypeExp df) ts
   pure
     ( TETuple ts' loc,
       mconcat svars,
@@ -113,14 +111,14 @@
       foldl' max Unlifted ls
     )
 --
-evalTypeExp t@(TERecord fs loc) = do
+evalTypeExp df t@(TERecord fs loc) = do
   -- Check for duplicate field names.
   let field_names = map fst fs
   unless (sort field_names == sort (nubOrd field_names)) $
     typeError loc mempty $
       "Duplicate record fields in" <+> pretty t <> "."
 
-  checked <- traverse evalTypeExp $ M.fromList fs
+  checked <- traverse (evalTypeExp df) $ M.fromList fs
   let fs' = fmap (\(x, _, _, _) -> x) checked
       fs_svars = foldMap (\(_, y, _, _) -> y) checked
       ts_s = fmap (\(_, _, z, _) -> z) checked
@@ -132,9 +130,9 @@
       foldl' max Unlifted ls
     )
 --
-evalTypeExp (TEArray d t loc) = do
+evalTypeExp df (TEArray d t loc) = do
   (d_svars, d', d'') <- checkSizeExp d
-  (t', svars, RetType dims st, l) <- evalTypeExp t
+  (t', svars, RetType dims st, l) <- evalTypeExp df t
   case (l, arrayOfWithAliases Nonunique (Shape [d'']) st) of
     (Unlifted, st') ->
       pure
@@ -158,11 +156,11 @@
       dv <- newTypeName "d"
       pure ([dv], SizeExpAny dloc, sizeFromName (qualName dv) dloc)
     checkSizeExp (SizeExp e dloc) = do
-      e' <- checkExpForSize e
+      e' <- df e
       pure ([], SizeExp e' dloc, e')
 --
-evalTypeExp (TEUnique t loc) = do
-  (t', svars, RetType dims st, l) <- evalTypeExp t
+evalTypeExp df (TEUnique t loc) = do
+  (t', svars, RetType dims st, l) <- evalTypeExp df t
   unless (mayContainArray st) $
     warn loc $
       "Declaring" <+> dquotes (pretty st) <+> "as unique has no effect."
@@ -175,22 +173,20 @@
     mayContainArray (Scalar Arrow {}) = False
     mayContainArray (Scalar (Sum cs)) = (any . any) mayContainArray cs
 --
-evalTypeExp (TEArrow (Just v) t1 t2 loc) = do
-  (t1', svars1, RetType dims1 st1, _) <- evalTypeExp t1
-  bindSpaced [(Term, v)] $ do
-    v' <- checkName Term v loc
-    bindVal v' (BoundV [] $ toStruct st1) $ do
-      (t2', svars2, RetType dims2 st2, _) <- evalTypeExp t2
-      pure
-        ( TEArrow (Just v') t1' t2' loc,
-          svars1 ++ dims1 ++ svars2,
-          RetType [] $ Scalar $ Arrow Nonunique (Named v') (diet $ resToParam st1) (toStruct st1) (RetType dims2 st2),
-          Lifted
-        )
+evalTypeExp df (TEArrow (Just v) t1 t2 loc) = do
+  (t1', svars1, RetType dims1 st1, _) <- evalTypeExp df t1
+  bindVal v (BoundV [] $ toStruct st1) $ do
+    (t2', svars2, RetType dims2 st2, _) <- evalTypeExp df t2
+    pure
+      ( TEArrow (Just v) t1' t2' loc,
+        svars1 ++ dims1 ++ svars2,
+        RetType [] $ Scalar $ Arrow Nonunique (Named v) (diet $ resToParam st1) (toStruct st1) (RetType dims2 st2),
+        Lifted
+      )
 --
-evalTypeExp (TEArrow Nothing t1 t2 loc) = do
-  (t1', svars1, RetType dims1 st1, _) <- evalTypeExp t1
-  (t2', svars2, RetType dims2 st2, _) <- evalTypeExp t2
+evalTypeExp df (TEArrow Nothing t1 t2 loc) = do
+  (t1', svars1, RetType dims1 st1, _) <- evalTypeExp df t1
+  (t2', svars2, RetType dims2 st2, _) <- evalTypeExp df t2
   pure
     ( TEArrow Nothing t1' t2' loc,
       svars1 ++ dims1 ++ svars2,
@@ -200,31 +196,29 @@
       Lifted
     )
 --
-evalTypeExp (TEDim dims t loc) = do
-  bindSpaced (map (Term,) dims) $ do
-    dims' <- mapM (flip (checkName Term) loc) dims
-    bindDims dims' $ do
-      (t', svars, RetType t_dims st, l) <- evalTypeExp t
-      let (witnessed, _) = determineSizeWitnesses $ toStruct st
-      case find (`S.notMember` witnessed) dims' of
-        Just d ->
-          typeError loc mempty . withIndexLink "unused-existential" $
-            "Existential size "
-              <> dquotes (prettyName d)
-              <> " not used as array size."
-        Nothing ->
-          pure
-            ( TEDim dims' t' loc,
-              svars,
-              RetType (dims' ++ t_dims) st,
-              max l SizeLifted
-            )
+evalTypeExp df (TEDim dims t loc) = do
+  bindDims dims $ do
+    (t', svars, RetType t_dims st, l) <- evalTypeExp df t
+    let (witnessed, _) = determineSizeWitnesses $ toStruct st
+    case find (`S.notMember` witnessed) dims of
+      Just d ->
+        typeError loc mempty . withIndexLink "unused-existential" $
+          "Existential size "
+            <> dquotes (prettyName d)
+            <> " not used as array size."
+      Nothing ->
+        pure
+          ( TEDim dims t' loc,
+            svars,
+            RetType (dims ++ t_dims) st,
+            max l SizeLifted
+          )
   where
     bindDims [] m = m
     bindDims (d : ds) m =
       bindVal d (BoundV [] $ Scalar $ Prim $ Signed Int64) $ bindDims ds m
 --
-evalTypeExp t@(TESum cs loc) = do
+evalTypeExp df t@(TESum cs loc) = do
   let constructors = map fst cs
   unless (sort constructors == sort (nubOrd constructors)) $
     typeError loc mempty $
@@ -233,7 +227,7 @@
   unless (length constructors < 256) $
     typeError loc mempty "Sum types must have less than 256 constructors."
 
-  checked <- (traverse . traverse) evalTypeExp $ M.fromList cs
+  checked <- (traverse . traverse) (evalTypeExp df) $ M.fromList cs
   let cs' = (fmap . fmap) (\(x, _, _, _) -> x) checked
       cs_svars = (foldMap . foldMap) (\(_, y, _, _) -> y) checked
       ts_s = (fmap . fmap) (\(_, _, z, _) -> z) checked
@@ -247,9 +241,9 @@
             M.map (map retType) ts_s,
       foldl' max Unlifted ls
     )
-evalTypeExp ote@TEApply {} = do
+evalTypeExp df ote@TEApply {} = do
   (tname, tname_loc, targs) <- rootAndArgs ote
-  (tname', ps, tname_t, l) <- lookupType tloc tname
+  (ps, tname_t, l) <- lookupType tname
   RetType t_dims t <- renameRetType $ toResRet Nonunique tname_t
   if length ps /= length targs
     then
@@ -264,7 +258,7 @@
     else do
       (targs', dims, substs) <- unzip3 <$> zipWithM checkArgApply ps targs
       pure
-        ( foldl (\x y -> TEApply x y tloc) (TEVar tname' tname_loc) targs',
+        ( foldl (\x y -> TEApply x y tloc) (TEVar tname tname_loc) targs',
           [],
           RetType (t_dims ++ mconcat dims) $
             applySubst (`M.lookup` mconcat substs) t,
@@ -273,10 +267,6 @@
   where
     tloc = srclocOf ote
 
-    rootAndArgs ::
-      (MonadTypeChecker m) =>
-      TypeExp NoInfo Name ->
-      m (QualName Name, SrcLoc, [TypeArgExp NoInfo Name])
     rootAndArgs (TEVar qn loc) = pure (qn, loc, [])
     rootAndArgs (TEApply op arg _) = do
       (op', loc, args) <- rootAndArgs op
@@ -286,7 +276,7 @@
         "Type" <+> dquotes (pretty te') <+> "is not a type constructor."
 
     checkSizeExp (SizeExp e dloc) = do
-      e' <- checkExpForSize e
+      e' <- df e
       pure
         ( TypeArgExpSize (SizeExp e' dloc),
           [],
@@ -304,7 +294,7 @@
       (d', svars, subst) <- checkSizeExp d
       pure (d', svars, M.singleton pv subst)
     checkArgApply (TypeParamType _ pv _) (TypeArgExpType te) = do
-      (te', svars, RetType dims st, _) <- evalTypeExp te
+      (te', svars, RetType dims st, _) <- evalTypeExp df te
       pure
         ( TypeArgExpType te',
           svars ++ dims,
@@ -325,128 +315,11 @@
 -- * The elaborated type.
 -- * The liftedness of the type.
 checkTypeExp ::
-  (MonadTypeChecker m) =>
-  TypeExp NoInfo Name ->
-  m (TypeExp Info VName, [VName], ResRetType, Liftedness)
-checkTypeExp te = do
-  checkForDuplicateNamesInType te
-  evalTypeExp te
-
--- | Check for duplication of names inside a binding group.
-checkForDuplicateNames ::
-  (MonadTypeChecker m) => [UncheckedTypeParam] -> [UncheckedPat t] -> m ()
-checkForDuplicateNames tps pats = (`evalStateT` mempty) $ do
-  mapM_ checkTypeParam tps
-  mapM_ checkPat pats
-  where
-    checkTypeParam (TypeParamType _ v loc) = seen Type v loc
-    checkTypeParam (TypeParamDim v loc) = seen Term v loc
-
-    checkPat (Id v _ loc) = seen Term v loc
-    checkPat (PatParens p _) = checkPat p
-    checkPat (PatAttr _ p _) = checkPat p
-    checkPat Wildcard {} = pure ()
-    checkPat (TuplePat ps _) = mapM_ checkPat ps
-    checkPat (RecordPat fs _) = mapM_ (checkPat . snd) fs
-    checkPat (PatAscription p _ _) = checkPat p
-    checkPat PatLit {} = pure ()
-    checkPat (PatConstr _ _ ps _) = mapM_ checkPat ps
-
-    seen ns v loc = do
-      already <- gets $ M.lookup (ns, v)
-      case already of
-        Just prev_loc ->
-          lift $
-            typeError loc mempty $
-              "Name"
-                <+> dquotes (pretty v)
-                <+> "also bound at"
-                <+> pretty (locStr prev_loc)
-                <> "."
-        Nothing ->
-          modify $ M.insert (ns, v) loc
-
--- | Check whether the type contains arrow types that define the same
--- parameter.  These might also exist further down, but that's not
--- really a problem - we mostly do this checking to help the user,
--- since it is likely an error, but it's easy to assign a semantics to
--- it (normal name shadowing).
-checkForDuplicateNamesInType ::
-  (MonadTypeChecker m) =>
-  TypeExp NoInfo Name ->
-  m ()
-checkForDuplicateNamesInType = check mempty
-  where
-    bad v loc prev_loc =
-      typeError loc mempty $
-        "Name"
-          <+> dquotes (pretty v)
-          <+> "also bound at"
-          <+> pretty (locStr prev_loc)
-          <> "."
-
-    check seen (TEArrow (Just v) t1 t2 loc)
-      | Just prev_loc <- M.lookup v seen =
-          bad v loc prev_loc
-      | otherwise =
-          check seen' t1 >> check seen' t2
-      where
-        seen' = M.insert v loc seen
-    check seen (TEArrow Nothing t1 t2 _) =
-      check seen t1 >> check seen t2
-    check seen (TETuple ts _) = mapM_ (check seen) ts
-    check seen (TERecord fs _) = mapM_ (check seen . snd) fs
-    check seen (TEUnique t _) = check seen t
-    check seen (TESum cs _) = mapM_ (mapM (check seen) . snd) cs
-    check seen (TEApply t1 (TypeArgExpType t2) _) =
-      check seen t1 >> check seen t2
-    check seen (TEApply t1 TypeArgExpSize {} _) =
-      check seen t1
-    check seen (TEDim (v : vs) t loc)
-      | Just prev_loc <- M.lookup v seen =
-          bad v loc prev_loc
-      | otherwise =
-          check (M.insert v loc seen) (TEDim vs t loc)
-    check seen (TEDim [] t _) =
-      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
--- extending the monadic name map with @ps@.
-checkTypeParams ::
-  (MonadTypeChecker m) =>
-  [TypeParamBase Name] ->
-  ([TypeParamBase VName] -> m a) ->
-  m a
-checkTypeParams ps m =
-  bindSpaced (map typeParamSpace ps) $
-    m =<< evalStateT (mapM checkTypeParam ps) mempty
-  where
-    typeParamSpace (TypeParamDim pv _) = (Term, pv)
-    typeParamSpace (TypeParamType _ pv _) = (Type, pv)
-
-    checkParamName ns v loc = do
-      seen <- gets $ M.lookup (ns, v)
-      case seen of
-        Just prev ->
-          lift $
-            typeError loc mempty $
-              "Type parameter"
-                <+> dquotes (pretty v)
-                <+> "previously defined at"
-                <+> pretty (locStr prev)
-                <> "."
-        Nothing -> do
-          modify $ M.insert (ns, v) loc
-          lift $ checkName ns v loc
-
-    checkTypeParam (TypeParamDim pv loc) =
-      TypeParamDim <$> checkParamName Term pv loc <*> pure loc
-    checkTypeParam (TypeParamType l pv loc) =
-      TypeParamType l <$> checkParamName Type pv loc <*> pure loc
+  (MonadTypeChecker m, Pretty df) =>
+  (df -> m Exp) ->
+  TypeExp df VName ->
+  m (TypeExp Exp VName, [VName], ResRetType, Liftedness)
+checkTypeExp = evalTypeExp
 
 -- | Construct a type argument corresponding to a type parameter.
 typeParamToArg :: TypeParam -> StructTypeArg
@@ -579,7 +452,7 @@
     -- XXX: the size names we invent here not globally unique.  This
     -- is _probably_ not a problem, since substituting types with
     -- outermost non-null existential sizes is done only when type
-    -- checking modules.
+    -- checking modules and monomorphising.
     freshDims (RetType [] t) = pure $ RetType [] t
     freshDims (RetType ext t) = do
       seen_ext <- get
@@ -601,7 +474,7 @@
 
     onType (Array u shape et) =
       arrayOfWithAliases u (applySubst lookupSubst' shape)
-        <$> onType (second (const mempty) $ Scalar et)
+        <$> onType (Scalar et)
     onType (Scalar (Prim t)) = pure $ Scalar $ Prim t
     onType (Scalar (TypeVar u v targs)) = do
       targs' <- mapM subsTypeArg targs
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
@@ -90,17 +90,17 @@
   pretty (BreadCrumbs bcs) = line <> stack (map pretty bcs)
 
 -- | A usage that caused a type constraint.
-data Usage = Usage (Maybe T.Text) SrcLoc
+data Usage = Usage (Maybe T.Text) Loc
   deriving (Show)
 
 -- | Construct a 'Usage' from a location and a description.
 mkUsage :: (Located a) => a -> T.Text -> Usage
-mkUsage = flip (Usage . Just) . srclocOf
+mkUsage = flip (Usage . Just) . locOf
 
 -- | Construct a 'Usage' that has just a location, but no particular
 -- description.
 mkUsage' :: (Located a) => a -> Usage
-mkUsage' = Usage Nothing . srclocOf
+mkUsage' = Usage Nothing . locOf
 
 instance Pretty Usage where
   pretty (Usage Nothing loc) = "use at " <> textwrap (locText loc)
@@ -117,13 +117,13 @@
 -- | A constraint on a yet-ambiguous type variable.
 data Constraint
   = NoConstraint Liftedness Usage
-  | ParamType Liftedness SrcLoc
+  | ParamType Liftedness Loc
   | Constraint StructRetType Usage
   | Overloaded [PrimType] Usage
   | HasFields Liftedness (M.Map Name StructType) Usage
   | Equality Usage
   | HasConstrs Liftedness (M.Map Name [StructType]) Usage
-  | ParamSize SrcLoc
+  | ParamSize Loc
   | -- | Is not actually a type, but a term-level size,
     -- possibly already set to something specific.
     Size (Maybe Exp) Usage
@@ -131,7 +131,7 @@
     -- created from the result of applying a function
     -- whose return size is existential, or otherwise
     -- hiding a size.
-    UnknownSize SrcLoc RigidSource
+    UnknownSize Loc RigidSource
   deriving (Show)
 
 instance Located Constraint where
@@ -176,7 +176,7 @@
     RigidCond StructType StructType
   | -- | Invented during unification.
     RigidUnify
-  | RigidOutOfScope SrcLoc VName
+  | RigidOutOfScope Loc VName
   | -- | Blank dimension in coercion.
     RigidCoerce
   deriving (Eq, Ord, Show)
@@ -186,7 +186,7 @@
 data Rigidity = Rigid RigidSource | Nonrigid
   deriving (Eq, Ord, Show)
 
-prettySource :: SrcLoc -> SrcLoc -> RigidSource -> Doc ()
+prettySource :: Loc -> Loc -> RigidSource -> Doc ()
 prettySource ctx loc (RigidRet Nothing) =
   "is unknown size returned by function at"
     <+> pretty (locStrRel ctx loc)
@@ -261,7 +261,7 @@
   case c of
     Just (_, UnknownSize loc rsrc) ->
       pure . aNote $
-        dquotes (pretty d) <+> prettySource (srclocOf ctx) loc rsrc
+        dquotes (pretty d) <+> prettySource (locOf ctx) loc rsrc
     _ -> pure mempty
 dimNotes _ _ = pure mempty
 
@@ -304,7 +304,7 @@
     x <- getConstraints
     putConstraints $ f x
 
-  newTypeVar :: (Monoid als) => SrcLoc -> Name -> m (TypeBase dim als)
+  newTypeVar :: (Monoid als, Located a) => a -> Name -> m (TypeBase dim als)
   newDimVar :: Usage -> Rigidity -> Name -> m VName
   newRigidDim :: (Located a) => a -> RigidSource -> Name -> m VName
   newRigidDim loc = newDimVar (mkUsage' loc) . Rigid
@@ -1101,7 +1101,7 @@
   m StructType
 mustHaveFieldWith onDims usage bound bcs l t = do
   constraints <- getConstraints
-  l_type <- newTypeVar (srclocOf usage) "t"
+  l_type <- newTypeVar (locOf usage) "t"
   case t of
     Scalar (TypeVar _ (QualName _ tn) [])
       | Just (lvl, NoConstraint {}) <- M.lookup tn constraints -> do
@@ -1143,7 +1143,7 @@
 
 newDimOnMismatch ::
   (MonadUnify m) =>
-  SrcLoc ->
+  Loc ->
   StructType ->
   StructType ->
   m (StructType, [VName])
@@ -1159,11 +1159,11 @@
           -- same new size.
           maybe_d <- gets $ M.lookup (d1, d2)
           case maybe_d of
-            Just d -> pure $ sizeFromName (qualName d) loc
+            Just d -> pure $ sizeFromName (qualName d) $ srclocOf loc
             Nothing -> do
               d <- lift $ newRigidDim loc r "differ"
               modify $ M.insert (d1, d2) d
-              pure $ sizeFromName (qualName d) loc
+              pure $ sizeFromName (qualName d) $ srclocOf loc
 
 -- | Like unification, but creates new size variables where mismatches
 -- occur.  Returns the new dimensions thus created.
@@ -1180,7 +1180,7 @@
   unifyWith allOK usage mempty noBreadCrumbs t1 t2
   t1' <- normTypeFully t1
   t2' <- normTypeFully t2
-  newDimOnMismatch (srclocOf usage) t1' t2'
+  newDimOnMismatch (locOf usage) t1' t2'
 
 -- Simple MonadUnify implementation.
 
@@ -1207,7 +1207,7 @@
 
   newTypeVar loc name = do
     v <- newVar name
-    modifyConstraints $ M.insert v (0, NoConstraint Lifted $ Usage Nothing loc)
+    modifyConstraints $ M.insert v (0, NoConstraint Lifted $ Usage Nothing $ locOf loc)
     pure $ Scalar $ TypeVar mempty (qualName v) []
 
   newDimVar usage rigidity name = do
@@ -1215,7 +1215,7 @@
     case rigidity of
       Rigid src ->
         modifyConstraints $
-          M.insert dim (0, UnknownSize (srclocOf usage) src)
+          M.insert dim (0, UnknownSize (locOf usage) src)
       Nonrigid ->
         modifyConstraints $
           M.insert dim (0, Size Nothing usage)
@@ -1243,10 +1243,10 @@
     constraints =
       M.fromList $
         map nonrigid nonrigid_tparams <> map rigid rigid_tparams
-    nonrigid (TypeParamDim p loc) = (p, (1, Size Nothing $ Usage Nothing loc))
-    nonrigid (TypeParamType l p loc) = (p, (1, NoConstraint l $ Usage Nothing loc))
-    rigid (TypeParamDim p loc) = (p, (0, ParamSize loc))
-    rigid (TypeParamType l p loc) = (p, (0, ParamType l loc))
+    nonrigid (TypeParamDim p loc) = (p, (1, Size Nothing $ Usage Nothing $ locOf loc))
+    nonrigid (TypeParamType l p loc) = (p, (1, NoConstraint l $ Usage Nothing $ locOf loc))
+    rigid (TypeParamDim p loc) = (p, (0, ParamSize $ locOf loc))
+    rigid (TypeParamType l p loc) = (p, (0, ParamType l $ locOf loc))
 
 -- | Perform a unification of two types outside a monadic context.
 -- The first list of type parameters are rigid but may have liftedness
@@ -1262,7 +1262,7 @@
   Either TypeError StructType
 doUnification loc rigid_tparams nonrigid_tparams t1 t2 =
   runUnifyM rigid_tparams nonrigid_tparams $ do
-    unify (Usage Nothing (srclocOf loc)) t1 t2
+    unify (Usage Nothing (locOf loc)) t1 t2
     normTypeFully t2
 
 -- Note [Linking variables to sum types]
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
@@ -20,7 +20,7 @@
 
 -- | The warnings produced by the compiler.  The 'Show' instance
 -- produces a human-readable description.
-newtype Warnings = Warnings [(SrcLoc, [SrcLoc], Doc ())]
+newtype Warnings = Warnings [(Loc, [Loc], Doc ())]
 
 instance Semigroup Warnings where
   Warnings ws1 <> Warnings ws2 = Warnings $ ws1 <> ws2
@@ -53,14 +53,14 @@
 anyWarnings (Warnings ws) = not $ null ws
 
 -- | A single warning at the given location.
-singleWarning :: SrcLoc -> Doc () -> Warnings
+singleWarning :: Loc -> Doc () -> Warnings
 singleWarning loc = singleWarning' loc []
 
 -- | A single warning at the given location, but also with a stack
 -- trace (sort of) to the location.
-singleWarning' :: SrcLoc -> [SrcLoc] -> Doc () -> Warnings
+singleWarning' :: Loc -> [Loc] -> Doc () -> Warnings
 singleWarning' loc locs problem = Warnings [(loc, locs, problem)]
 
 -- | Exports Warnings into a list of (location, problem).
-listWarnings :: Warnings -> [(SrcLoc, Doc ())]
+listWarnings :: Warnings -> [(Loc, Doc ())]
 listWarnings (Warnings ws) = map (\(loc, _, doc) -> (loc, doc)) ws
diff --git a/unittests/Language/Futhark/TypeChecker/TypesTests.hs b/unittests/Language/Futhark/TypeChecker/TypesTests.hs
--- a/unittests/Language/Futhark/TypeChecker/TypesTests.hs
+++ b/unittests/Language/Futhark/TypeChecker/TypesTests.hs
@@ -11,15 +11,16 @@
 import Language.Futhark.SyntaxTests ()
 import Language.Futhark.TypeChecker (initialEnv)
 import Language.Futhark.TypeChecker.Monad
+import Language.Futhark.TypeChecker.Names (resolveTypeExp)
 import Language.Futhark.TypeChecker.Terms
 import Language.Futhark.TypeChecker.Types
 import Test.Tasty
 import Test.Tasty.HUnit
 
-evalTest :: TypeExp NoInfo Name -> Either String ([VName], ResRetType) -> TestTree
+evalTest :: TypeExp (ExpBase NoInfo Name) Name -> Either String ([VName], ResRetType) -> TestTree
 evalTest te expected =
   testCase (prettyString te) $
-    case (fmap (extract . fst) (run (checkTypeExp te)), expected) of
+    case (fmap (extract . fst) (run (checkTypeExp checkSizeExp =<< resolveTypeExp te)), expected) of
       (Left got_e, Left expected_e) ->
         let got_e_s = T.unpack $ docText $ prettyTypeError got_e
          in (expected_e `isInfixOf` got_e_s) @? got_e_s
@@ -32,7 +33,7 @@
         assertFailure $ "Expected error, got: " <> show actual_t
   where
     extract (_, svars, t, _) = (svars, t)
-    run = snd . runTypeM env mempty (mkInitialImport "") blankNameSource checkSizeExp
+    run = snd . runTypeM env mempty (mkInitialImport "") (newNameSource 100)
     -- We hack up an environment with some predefined type
     -- abbreviations for testing.  This is all pretty sensitive to the
     -- specific unique names, so we have to be careful!
@@ -83,64 +84,64 @@
     mkNeg (x, y) = evalTest x (Left y)
     pos =
       [ ( "[]i32",
-          ([], "?[d_0].[d_0]i32")
+          ([], "?[d_100].[d_100]i32")
         ),
         ( "[][]i32",
-          ([], "?[d_0][d_1].[d_0][d_1]i32")
+          ([], "?[d_100][d_101].[d_100][d_101]i32")
         ),
         ( "bool -> []i32",
-          ([], "bool -> ?[d_0].[d_0]i32")
+          ([], "bool -> ?[d_100].[d_100]i32")
         ),
         ( "bool -> []f32 -> []i32",
-          (["d_0"], "bool -> [d_0]f32 -> ?[d_1].[d_1]i32")
+          (["d_100"], "bool -> [d_100]f32 -> ?[d_101].[d_101]i32")
         ),
         ( "([]i32,[]i32)",
-          ([], "?[d_0][d_1].([d_0]i32, [d_1]i32)")
+          ([], "?[d_100][d_101].([d_100]i32, [d_101]i32)")
         ),
         ( "{a:[]i32,b:[]i32}",
-          ([], "?[d_0][d_1].{a:[d_0]i32, b:[d_1]i32}")
+          ([], "?[d_100][d_101].{a:[d_100]i32, b:[d_101]i32}")
         ),
         ( "?[n].[n][n]bool",
-          ([], "?[n_0].[n_0][n_0]bool")
+          ([], "?[n_100].[n_100][n_100]bool")
         ),
         ( "([]i32 -> []i32) -> bool -> []i32",
-          (["d_0"], "([d_0]i32 -> ?[d_1].[d_1]i32) -> bool -> ?[d_2].[d_2]i32")
+          (["d_100"], "([d_100]i32 -> ?[d_101].[d_101]i32) -> bool -> ?[d_102].[d_102]i32")
         ),
         ( "((k: i64) -> [k]i32 -> [k]i32) -> []i32 -> bool",
-          (["d_1"], "((k_0: i64) -> [k_0]i32 -> [k_0]i32) -> [d_1]i32 -> bool")
+          (["d_101"], "((k_100: i64) -> [k_100]i32 -> [k_100]i32) -> [d_101]i32 -> bool")
         ),
         ( "square [10]",
           ([], "[10][10]i32")
         ),
         ( "square []",
-          ([], "?[d_0].[d_0][d_0]i32")
+          ([], "?[d_100].[d_100][d_100]i32")
         ),
         ( "bool -> square []",
-          ([], "bool -> ?[d_0].[d_0][d_0]i32")
+          ([], "bool -> ?[d_100].[d_100][d_100]i32")
         ),
         ( "(k: i64) -> square [k]",
-          ([], "(k_0: i64) -> [k_0][k_0]i32")
+          ([], "(k_100: i64) -> [k_100][k_100]i32")
         ),
         ( "fun i32 bool",
           ([], "i32 -> bool")
         ),
         ( "fun ([]i32) bool",
-          ([], "?[d_0].[d_0]i32 -> bool")
+          ([], "?[d_100].[d_100]i32 -> bool")
         ),
         ( "fun bool ([]i32)",
-          ([], "?[d_0].bool -> [d_0]i32")
+          ([], "?[d_100].bool -> [d_100]i32")
         ),
         ( "bool -> fun ([]i32) bool",
-          ([], "bool -> ?[d_0].[d_0]i32 -> bool")
+          ([], "bool -> ?[d_100].[d_100]i32 -> bool")
         ),
         ( "bool -> fun bool ([]i32)",
-          ([], "bool -> ?[d_0].bool -> [d_0]i32")
+          ([], "bool -> ?[d_100].bool -> [d_100]i32")
         ),
         ( "pair",
-          ([], "?[n_0][m_1].([n_0]i64, [m_1]i64)")
+          ([], "?[n_100][m_101].([n_100]i64, [m_101]i64)")
         ),
         ( "(pair,pair)",
-          ([], "?[n_0][m_1][n_2][m_3].(([n_0]i64, [m_1]i64), ([n_2]i64, [m_3]i64))")
+          ([], "?[n_100][m_101][n_102][m_103].(([n_100]i64, [m_101]i64), ([n_102]i64, [m_103]i64))")
         )
       ]
     neg =