diff --git a/futhark.cabal b/futhark.cabal
--- a/futhark.cabal
+++ b/futhark.cabal
@@ -2,10 +2,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: ca599dc882c25837255ce48c8e6ab8c5a9f1ff05234e05f6d73705f5cf9fe1c6
+-- hash: befc35fd82c38f76939296d95942a59561978305f93fb1599eb91ea20a6af5fe
 
 name:           futhark
-version:        0.10.1
+version:        0.10.2
 synopsis:       An optimising compiler for a functional, array-oriented language.
 description:    Futhark is a small programming language designed to be compiled to
                 efficient parallel code. It is a statically typed, data-parallel,
@@ -98,6 +98,7 @@
     , srcloc >=0.4
     , template-haskell >=2.11.1
     , temporary
+    , terminal-size >=0.3
     , text >=1.2.2.2
     , time >=1.6.0.1
     , transformers >=0.3
diff --git a/futlib/array.fut b/futlib/array.fut
--- a/futlib/array.fut
+++ b/futlib/array.fut
@@ -50,7 +50,7 @@
 -- | Rotate an array some number of elements to the left.  A negative
 -- rotation amount is also supported.
 --
--- For example, if `b==rotate 1 i a`, then `b[x,y+1] = a[x,y]`.
+-- For example, if `b==rotate r a`, then `b[x+r] = a[x]`.
 let rotate 't (r: i32) (xs: []t) = intrinsics.rotate (r, xs)
 
 -- | Replace an element of the array with a new value.
diff --git a/rts/c/opencl.h b/rts/c/opencl.h
--- a/rts/c/opencl.h
+++ b/rts/c/opencl.h
@@ -27,6 +27,7 @@
   int preferred_device_num;
   const char *preferred_platform;
   const char *preferred_device;
+  int ignore_blacklist;
 
   const char* dump_program_to;
   const char* load_program_from;
@@ -59,6 +60,7 @@
   cfg->preferred_device_num = 0;
   cfg->preferred_platform = "";
   cfg->preferred_device = "";
+  cfg->ignore_blacklist = 0;
   cfg->dump_program_to = NULL;
   cfg->load_program_from = NULL;
   cfg->dump_binary_to = NULL;
@@ -225,6 +227,7 @@
 
 void set_preferred_platform(struct opencl_config *cfg, const char *s) {
   cfg->preferred_platform = s;
+  cfg->ignore_blacklist = 1;
 }
 
 void set_preferred_device(struct opencl_config *cfg, const char *s) {
@@ -241,6 +244,7 @@
   }
   cfg->preferred_device = s;
   cfg->preferred_device_num = x;
+  cfg->ignore_blacklist = 1;
 }
 
 static char* opencl_platform_info(cl_platform_id platform,
@@ -347,6 +351,45 @@
   *num_devices_out = num_devices;
 }
 
+// Returns 0 on success.
+static int select_device_interactively(struct opencl_config *cfg) {
+  struct opencl_device_option *devices;
+  size_t num_devices;
+  int ret = 1;
+
+  opencl_all_device_options(&devices, &num_devices);
+
+  printf("Choose OpenCL device:\n");
+  const char *cur_platform = "";
+  for (size_t i = 0; i < num_devices; i++) {
+    struct opencl_device_option device = devices[i];
+    if (strcmp(cur_platform, device.platform_name) != 0) {
+      printf("Platform: %s\n", device.platform_name);
+      cur_platform = device.platform_name;
+    }
+    printf("[%d] %s\n", (int)i, device.device_name);
+  }
+
+  int selection;
+  printf("Choice: ");
+  if (scanf("%d", &selection) == 1) {
+    ret = 0;
+    cfg->preferred_platform = "";
+    cfg->preferred_device = "";
+    cfg->preferred_device_num = selection;
+    cfg->ignore_blacklist = 1;
+  }
+
+  // Free all the platform and device names.
+  for (size_t j = 0; j < num_devices; j++) {
+    free(devices[j].platform_name);
+    free(devices[j].device_name);
+  }
+  free(devices);
+
+  return ret;
+}
+
 static int is_blacklisted(const char *platform_name, const char *device_name,
                           const struct opencl_config *cfg) {
   if (strcmp(cfg->preferred_platform, "") != 0 ||
@@ -370,9 +413,10 @@
 
   for (size_t i = 0; i < num_devices; i++) {
     struct opencl_device_option device = devices[i];
-    if (!is_blacklisted(device.platform_name, device.device_name, cfg) &&
-        strstr(device.platform_name, cfg->preferred_platform) != NULL &&
+    if (strstr(device.platform_name, cfg->preferred_platform) != NULL &&
         strstr(device.device_name, cfg->preferred_device) != NULL &&
+        (cfg->ignore_blacklist ||
+         !is_blacklisted(device.platform_name, device.device_name, cfg)) &&
         num_device_matches++ == cfg->preferred_device_num) {
       // Free all the platform and device names, except the ones we have chosen.
       for (size_t j = 0; j < num_devices; j++) {
diff --git a/rts/c/values.h b/rts/c/values.h
--- a/rts/c/values.h
+++ b/rts/c/values.h
@@ -434,6 +434,20 @@
 #define BINARY_FORMAT_VERSION 2
 #define IS_BIG_ENDIAN (!*(unsigned char *)&(uint16_t){1})
 
+// On Windows we need to explicitly set the file mode to not mangle
+// newline characters.  On *nix there is no difference.
+#ifdef _WIN32
+#include <io.h>
+#include <fcntl.h>
+static void set_binary_mode(FILE *f) {
+  setmode(fileno(f), O_BINARY);
+}
+#else
+static void set_binary_mode(FILE *f) {
+  (void)f;
+}
+#endif
+
 // Reading little-endian byte sequences.  On big-endian hosts, we flip
 // the resulting bytes.
 
diff --git a/src/Futhark/CLI/REPL.hs b/src/Futhark/CLI/REPL.hs
--- a/src/Futhark/CLI/REPL.hs
+++ b/src/Futhark/CLI/REPL.hs
@@ -84,10 +84,10 @@
 
   maybe_init_state <- liftIO $ newFutharkiState 0 Nothing
   case maybe_init_state of
-    Left err -> error $ "Failed to initialise intepreter state: " ++ err
+    Left err -> error $ "Failed to initialise interpreter state: " ++ err
     Right init_state -> Haskeline.runInputT Haskeline.defaultSettings $ toploop init_state
 
-  putStrLn "Leaving futharki."
+  putStrLn "Leaving 'futhark repl'."
 
 confirmQuit :: Haskeline.InputT IO Bool
 confirmQuit = do
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
@@ -22,6 +22,7 @@
 import System.Exit
 import System.FilePath
 import System.Console.GetOpt
+import qualified System.Console.Terminal.Size as Terminal
 import System.IO
 import Text.Regex.TDFA
 
@@ -348,9 +349,10 @@
   moveCursorToTableTop
   putStrLn $ statusTable ts
   clearLine
-  putStrLn $ atMostChars 60 running
-  where running    = "Now testing: " ++
-                     (unwords . reverse . map testCaseProgram . testStatusRun) ts
+  w <- maybe 80 Terminal.width <$> Terminal.size
+  putStrLn $ atMostChars (w-length labelstr) running
+  where running = labelstr ++ (unwords . reverse . map testCaseProgram . testStatusRun) ts
+        labelstr = "Now testing: "
 
 moveCursorToTableTop :: IO ()
 moveCursorToTableTop = cursorUpLine tableLines
diff --git a/src/Futhark/CodeGen/Backends/COpenCL/Boilerplate.hs b/src/Futhark/CodeGen/Backends/COpenCL/Boilerplate.hs
--- a/src/Futhark/CodeGen/Backends/COpenCL/Boilerplate.hs
+++ b/src/Futhark/CodeGen/Backends/COpenCL/Boilerplate.hs
@@ -124,6 +124,12 @@
                          set_preferred_platform(&cfg->opencl, s);
                        }|])
 
+  GC.publicDef_ "context_config_select_device_interactively" GC.InitDecl $ \s ->
+    ([C.cedecl|void $id:s(struct $id:cfg* cfg);|],
+     [C.cedecl|void $id:s(struct $id:cfg* cfg) {
+                         select_device_interactively(&cfg->opencl);
+                       }|])
+
   GC.publicDef_ "context_config_dump_program_to" GC.InitDecl $ \s ->
     ([C.cedecl|void $id:s(struct $id:cfg* cfg, const char *path);|],
      [C.cedecl|void $id:s(struct $id:cfg* cfg, const char *path) {
diff --git a/src/Futhark/CodeGen/Backends/GenericC.hs b/src/Futhark/CodeGen/Backends/GenericC.hs
--- a/src/Futhark/CodeGen/Backends/GenericC.hs
+++ b/src/Futhark/CodeGen/Backends/GenericC.hs
@@ -1186,6 +1186,7 @@
     int time_runs;
 
     /* Declare and read input. */
+    set_binary_mode(stdin);
     $items:input_items
     $items:output_decls
 
@@ -1208,6 +1209,9 @@
     $stms:free_parsed
 
     /* Print the final result. */
+    if (binary_output) {
+      set_binary_mode(stdout);
+    }
     $stms:printstms
 
     $stms:free_outputs
diff --git a/src/Futhark/CodeGen/ImpGen/Kernels.hs b/src/Futhark/CodeGen/ImpGen/Kernels.hs
--- a/src/Futhark/CodeGen/ImpGen/Kernels.hs
+++ b/src/Futhark/CodeGen/ImpGen/Kernels.hs
@@ -48,8 +48,22 @@
            -> CallKernelGen ()
 opCompiler dest (Alloc e space) =
   ImpGen.compileAlloc dest e space
-opCompiler dest (Inner kernel) =
+opCompiler (Pattern _ [pe]) (Inner (GetSize key size_class)) = do
+  fname <- asks ImpGen.envFunction
+  sOp $ Imp.GetSize (patElemName pe) (keyWithEntryPoint fname key) $
+    sizeClassWithEntryPoint fname size_class
+opCompiler (Pattern _ [pe]) (Inner (CmpSizeLe key size_class x)) = do
+  fname <- asks ImpGen.envFunction
+  let size_class' = sizeClassWithEntryPoint fname size_class
+  sOp . Imp.CmpSizeLe (patElemName pe) (keyWithEntryPoint fname key) size_class'
+    =<< ImpGen.compileSubExp x
+opCompiler (Pattern _ [pe]) (Inner (GetSizeMax size_class)) =
+  sOp $ Imp.GetSizeMax (patElemName pe) size_class
+opCompiler dest (Inner (HostOp kernel)) =
   kernelCompiler dest kernel
+opCompiler pat e =
+  compilerBugS $ "ImpGen.opCompiler: Invalid pattern\n  " ++
+  pretty pat ++ "\nfor expression\n  " ++ pretty e
 
 sizeClassWithEntryPoint :: Name -> Imp.SizeClass -> Imp.SizeClass
 sizeClassWithEntryPoint fname (Imp.SizeThreshold path) =
@@ -60,20 +74,6 @@
 kernelCompiler :: Pattern ExplicitMemory -> Kernel InKernel
                -> CallKernelGen ()
 
-kernelCompiler (Pattern _ [pe]) (GetSize key size_class) = do
-  fname <- asks ImpGen.envFunction
-  sOp $ Imp.GetSize (patElemName pe) (keyWithEntryPoint fname key) $
-    sizeClassWithEntryPoint fname size_class
-
-kernelCompiler (Pattern _ [pe]) (CmpSizeLe key size_class x) = do
-  fname <- asks ImpGen.envFunction
-  let size_class' = sizeClassWithEntryPoint fname size_class
-  sOp . Imp.CmpSizeLe (patElemName pe) (keyWithEntryPoint fname key) size_class'
-    =<< ImpGen.compileSubExp x
-
-kernelCompiler (Pattern _ [pe]) (GetSizeMax size_class) =
-  sOp $ Imp.GetSizeMax (patElemName pe) size_class
-
 kernelCompiler pat (Kernel desc space _ kernel_body) = do
   (constants, init_constants) <- kernelInitialisation space
 
@@ -113,10 +113,6 @@
 
 kernelCompiler pat (SegGenRed space ops _ body) =
   compileSegGenRed pat space ops body
-
-kernelCompiler pat e =
-  compilerBugS $ "ImpGen.kernelCompiler: Invalid pattern\n  " ++
-  pretty pat ++ "\nfor expression\n  " ++ pretty e
 
 expCompiler :: ImpGen.ExpCompiler ExplicitMemory Imp.HostOp
 
diff --git a/src/Futhark/CodeGen/ImpGen/Kernels/Base.hs b/src/Futhark/CodeGen/ImpGen/Kernels/Base.hs
--- a/src/Futhark/CodeGen/ImpGen/Kernels/Base.hs
+++ b/src/Futhark/CodeGen/ImpGen/Kernels/Base.hs
@@ -339,13 +339,13 @@
 
 atomicUpdateLocking lam
   | Just ops_and_ts <- splitOp lam,
-    all (\(_, t, _) -> primBitSize t == 32) ops_and_ts = Left $ \arrs bucket ->
+    all (\(_, t, _, _) -> primBitSize t == 32) ops_and_ts = Left $ \arrs bucket ->
   -- If the operator is a vectorised binary operator on 32-bit values,
   -- we can use a particularly efficient implementation. If the
   -- operator has an atomic implementation we use that, otherwise it
   -- is still a binary operator which can be implemented by atomic
   -- compare-and-swap if 32 bits.
-  forM_ (zip arrs ops_and_ts) $ \(a, (op, t, val)) -> do
+  forM_ (zip arrs ops_and_ts) $ \(a, (op, t, x, y)) -> do
 
   -- Common variables.
   old <- dPrim "old" t
@@ -353,47 +353,26 @@
   (arr', _a_space, bucket_offset) <- ImpGen.fullyIndexArray a bucket
 
   case opHasAtomicSupport old arr' bucket_offset op of
-    Just f -> sOp $ f val
-
-    Nothing -> do
-      -- Code generation target:
-      --
-      -- old = d_his[idx];
-      -- do {
-      --   assumed = old;
-      --   tmp = OP::apply(val, assumed);
-      --   old = atomicCAS(&d_his[idx], assumed, tmp);
-      -- } while(assumed != old);
-      assumed <- dPrim "assumed" t
-      run_loop <- dPrimV "run_loop" 1
-      ImpGen.copyDWIM old [] (Var a) bucket
-
-      -- Critical section
-      x <- dPrim "x" t
-      y <- dPrim "y" t
+    Just f -> sOp $ f $ Imp.var y t
 
-      -- While-loop: Try to insert your value
-      let (toBits, fromBits) =
-            case t of FloatType Float32 -> (\v -> Imp.FunExp "to_bits32" [v] int32,
-                                            \v -> Imp.FunExp "from_bits32" [v] t)
-                      _                 -> (id, id)
-      sWhile (Imp.var run_loop int32) $ do
-        assumed <-- Imp.var old t
-        x <-- val
-        y <-- Imp.var assumed t
-        x <-- Imp.BinOpExp op (Imp.var x t) (Imp.var y t)
-        old_bits <- dPrim "old_bits" int32
-        sOp $ Imp.Atomic $
-          Imp.AtomicCmpXchg old_bits arr' bucket_offset
-          (toBits (Imp.var assumed t)) (toBits (Imp.var x t))
-        old <-- fromBits (Imp.var old_bits int32)
-        sWhen (toBits (Imp.var assumed t) .==. Imp.var old_bits int32)
-          (run_loop <-- 0)
+    Nothing -> atomicUpdateCAS t a old bucket x $
+      x <-- Imp.BinOpExp op (Imp.var x t) (Imp.var y t)
 
   where opHasAtomicSupport old arr' bucket' bop = do
           let atomic f = Imp.Atomic . f old arr' bucket'
           atomic <$> Imp.atomicBinOp bop
 
+-- If the operator functions purely on single 32-bit values, we can
+-- use an implementation based on CAS, no matter what the operator
+-- does.
+atomicUpdateLocking op
+  | [Prim t] <- lambdaReturnType op,
+    [xp, _] <- lambdaParams op,
+    primBitSize t == 32 = Left $ \[arr] bucket -> do
+      old <- dPrim "old" t
+      atomicUpdateCAS t arr old bucket (paramName xp) $
+        ImpGen.compileBody' [xp] $ lambdaBody op
+
 atomicUpdateLocking op = Right $ \locking arrs bucket -> do
   old <- dPrim "old" int32
   continue <- dPrimV "continue" true
@@ -453,8 +432,45 @@
     sOp Imp.MemFence
   where writeArray bucket arr val = ImpGen.copyDWIM arr bucket val []
 
+atomicUpdateCAS :: PrimType
+                -> VName -> VName
+                -> [Imp.Exp] -> VName
+                -> ImpGen.ImpM lore Imp.KernelOp ()
+                -> ImpGen.ImpM lore Imp.KernelOp ()
+atomicUpdateCAS t arr old bucket x do_op = do
+  -- Code generation target:
+  --
+  -- old = d_his[idx];
+  -- do {
+  --   assumed = old;
+  --   x = do_op(assumed, y);
+  --   old = atomicCAS(&d_his[idx], assumed, tmp);
+  -- } while(assumed != old);
+  assumed <- dPrim "assumed" t
+  run_loop <- dPrimV "run_loop" 1
+  ImpGen.copyDWIM old [] (Var arr) bucket
+
+  (arr', _a_space, bucket_offset) <- ImpGen.fullyIndexArray arr bucket
+
+  -- While-loop: Try to insert your value
+  let (toBits, fromBits) =
+        case t of FloatType Float32 -> (\v -> Imp.FunExp "to_bits32" [v] int32,
+                                        \v -> Imp.FunExp "from_bits32" [v] t)
+                  _                 -> (id, id)
+  sWhile (Imp.var run_loop int32) $ do
+    assumed <-- Imp.var old t
+    x <-- Imp.var assumed t
+    do_op
+    old_bits <- dPrim "old_bits" int32
+    sOp $ Imp.Atomic $
+      Imp.AtomicCmpXchg old_bits arr' bucket_offset
+      (toBits (Imp.var assumed t)) (toBits (Imp.var x t))
+    old <-- fromBits (Imp.var old_bits int32)
+    sWhen (toBits (Imp.var assumed t) .==. Imp.var old_bits int32)
+      (run_loop <-- 0)
+
 -- | Horizontally fission a lambda that models a binary operator.
-splitOp :: Attributes lore => Lambda lore -> Maybe [(BinOp, PrimType, Imp.Exp)]
+splitOp :: Attributes lore => Lambda lore -> Maybe [(BinOp, PrimType, VName, VName)]
 splitOp lam = mapM splitStm $ bodyResult $ lambdaBody lam
   where n = length $ lambdaReturnType lam
         splitStm (Var res) = do
@@ -467,7 +483,7 @@
           guard $ paramName xp == x
           guard $ paramName yp == y
           Prim t <- Just $ patElemType pe
-          return (op, t, Imp.var (paramName yp) t)
+          return (op, t, paramName xp, paramName yp)
         splitStm _ = Nothing
 
 computeKernelUses :: FreeIn a =>
diff --git a/src/Futhark/CodeGen/ImpGen/Kernels/SegGenRed.hs b/src/Futhark/CodeGen/ImpGen/Kernels/SegGenRed.hs
--- a/src/Futhark/CodeGen/ImpGen/Kernels/SegGenRed.hs
+++ b/src/Futhark/CodeGen/ImpGen/Kernels/SegGenRed.hs
@@ -202,7 +202,7 @@
                 vs_params = takeLast (length vs') $ lambdaParams lam
 
             sWhen bucket_in_bounds $ do
-              ImpGen.dLParams vs_params
+              ImpGen.dLParams $ lambdaParams lam
               vectorLoops [] (shapeDims shape) $ \is -> do
                 forM_ (zip vs_params vs') $ \(p, v) ->
                   ImpGen.copyDWIM (paramName p) [] v is
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
@@ -311,7 +311,7 @@
 valBindHtml name (ValBind _ _ retdecl (Info rettype) tparams params _ _ _) = do
   let tparams' = mconcat $ map ((" "<>) . typeParamHtml) tparams
       noLink' = noLink $ map typeParamName tparams ++
-                map identName (S.toList $ mconcat $ map patIdentSet params)
+                map identName (S.toList $ mconcat $ map patternIdents params)
   rettype' <- noLink' $ maybe (typeHtml rettype) typeExpHtml retdecl
   params' <- noLink' $ mapM patternHtml params
   return (keyword "val " <> (H.span ! A.class_ "decl_name") name,
diff --git a/src/Futhark/Internalise.hs b/src/Futhark/Internalise.hs
--- a/src/Futhark/Internalise.hs
+++ b/src/Futhark/Internalise.hs
@@ -2,7 +2,7 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE OverloadedStrings #-}
-{-# OPTIONS_GHC -fmax-pmcheck-iterations=2500000#-}
+{-# OPTIONS_GHC -fmax-pmcheck-iterations=25000000#-}
 -- |
 --
 -- This module implements a transformation from source to core
@@ -128,7 +128,7 @@
   -- parameters here.
   bindingParams [] (map E.patternNoShapeAnnotations params) $
   \_ shapeparams params' -> do
-    (entry_rettype, _) <- internaliseEntryReturnType $ E.vacuousShapeAnnotations rettype
+    (entry_rettype, _) <- internaliseEntryReturnType $ anyDimShapeAnnotations rettype
     let entry' = entryPoint (zip params params') (retdecl, rettype, entry_rettype)
         args = map (I.Var . I.paramName) $ concat params'
 
@@ -232,8 +232,7 @@
       is_const <- lookupConstant loc name
       case is_const of
         Just ses -> return ses
-        Nothing -> (:[]) . I.Var <$> internaliseIdent (E.Ident name (Info t') loc)
-  where t' = removeShapeAnnotations t
+        Nothing -> (:[]) . I.Var <$> internaliseIdent (E.Ident name (Info t) loc)
 
 internaliseExp desc (E.Index e idxs _ loc) = do
   vs <- internaliseExpToVars "indexed" e
@@ -253,7 +252,7 @@
           M.singleton name <$> internaliseExp desc e
         internaliseField (E.RecordFieldImplicit name t loc) =
           internaliseField $ E.RecordFieldExplicit (baseName name)
-          (E.Var (E.qualName name) (vacuousShapeAnnotations <$> t) loc) loc
+          (E.Var (E.qualName name) t loc) loc
 
 internaliseExp desc (E.ArrayLit es (Info arr_t) loc)
   -- If this is a multidimensional array literal of primitives, we
@@ -278,7 +277,7 @@
   es' <- mapM (internaliseExp "arr_elem") es
   case es' of
     [] -> do
-      rowtypes <- internaliseType (rowtype `setAliases` ())
+      rowtypes <- internaliseType $ toStructural rowtype
       let arraylit rt = I.BasicOp $ I.ArrayLit [] rt
       letSubExps desc $ map (arraylit . zeroDim . fromDecl) rowtypes
     e' : _ -> do
@@ -391,7 +390,7 @@
                (eBody [eDivRoundingUp Int32 (eSubExp distance) (eSubExp pos_step)])
   pure <$> letSubExp desc (I.BasicOp $ I.Iota num_elems start' step it)
 
-internaliseExp desc (E.Ascript e (TypeDecl dt (Info et)) loc) = do
+internaliseExp desc (E.Ascript e (TypeDecl dt (Info et)) _ loc) = do
   es <- internaliseExp desc e
   (ts, cm) <- internaliseReturnType et
   mapM_ (uncurry (internaliseDimConstant loc)) cm
@@ -432,7 +431,7 @@
            args' <- concat <$> mapM (internaliseExp "arg") args
            fst <$> funcall desc qfname args' loc
 
-internaliseExp desc (E.LetPat tparams pat e body loc) =
+internaliseExp desc (E.LetPat tparams pat e body _ loc) =
   internalisePat desc tparams pat e body loc (internaliseExp desc)
 
 internaliseExp desc (E.LetFun ofname (tparams, params, retdecl, Info rettype, body) letbody loc) = do
@@ -581,11 +580,11 @@
                    loop_initial_cond : mergeinit,
                    init_loop_cond_bnds))
 
-internaliseExp desc (E.LetWith name src idxs ve body loc) = do
-  let pat = E.Id (E.identName name) (E.vacuousShapeAnnotations <$> E.identType name) loc
-      src_t = E.fromStruct . E.vacuousShapeAnnotations <$> E.identType src
+internaliseExp desc (E.LetWith name src idxs ve body t loc) = do
+  let pat = E.Id (E.identName name) (E.identType name) loc
+      src_t = E.fromStruct <$> E.identType src
       e = E.Update (E.Var (E.qualName $ E.identName src) src_t loc) idxs ve loc
-  internaliseExp desc $ E.LetPat [] pat e body loc
+  internaliseExp desc $ E.LetPat [] pat e body t loc
 
 internaliseExp desc (E.Update src slice ve loc) = do
   ves <- internaliseExp "lw_val" ve
@@ -633,143 +632,6 @@
           letBindNames_ [v'] $ I.BasicOp $ I.SubExp v
           return $ I.Var v'
 
-internaliseExp desc (E.Map lam arr _ _) = do
-  arr' <- internaliseExpToVars "map_arr" arr
-  lam' <- internaliseMapLambda internaliseLambda lam $ map I.Var arr'
-  w <- arraysSize 0 <$> mapM lookupType arr'
-  letTupExp' desc $ I.Op $
-    I.Screma w (I.mapSOAC lam') arr'
-
-internaliseExp desc (E.Reduce comm lam ne arr loc) =
-  internaliseScanOrReduce desc "reduce" reduce (lam, ne, arr, loc)
-  where reduce w red_lam nes arrs =
-          I.Screma w <$> I.reduceSOAC comm red_lam nes <*> pure arrs
-
-internaliseExp desc (E.GenReduce hist op ne buckets img loc) = do
-  ne' <- internaliseExp "gen_reduce_ne" ne
-  hist' <- internaliseExpToVars "gen_reduce_hist" hist
-  buckets' <- letExp "gen_reduce_buckets" . BasicOp . SubExp =<<
-              internaliseExp1 "gen_reduce_buckets" buckets
-  img' <- internaliseExpToVars "gen_reduce_img" img
-
-  -- reshape neutral element to have same size as the destination array
-  ne_shp <- forM (zip ne' hist') $ \(n, h) -> do
-    rowtype <- I.stripArray 1 <$> lookupType h
-    ensureShape asserting
-      "Row shape of destination array does not match shape of neutral element"
-      loc rowtype "gen_reduce_ne_right_shape" n
-  ne_ts <- mapM I.subExpType ne_shp
-  his_ts <- mapM lookupType hist'
-  op' <- internaliseFoldLambda internaliseLambda op ne_ts his_ts
-
-  -- reshape return type of bucket function to have same size as neutral element
-  -- (modulo the index)
-  bucket_param <- newParam "bucket_p" $ I.Prim int32
-  img_params <- mapM (newParam "img_p" . rowType) =<< mapM lookupType img'
-  let params = bucket_param : img_params
-      rettype = I.Prim int32 : ne_ts
-      body = mkBody mempty $ map (I.Var . paramName) params
-  body' <- localScope (scopeOfLParams params) $
-           ensureResultShape asserting
-           "Row shape of value array does not match row shape of gen_reduce target"
-           (srclocOf img) rettype body
-
-  -- get sizes of histogram and image arrays
-  w_hist <- arraysSize 0 <$> mapM lookupType hist'
-  w_img <- arraysSize 0 <$> mapM lookupType img'
-
-  -- Generate an assertion and reshapes to ensure that buckets' and
-  -- img' are the same size.
-  b_shape <- arrayShape <$> lookupType buckets'
-  let b_w = shapeSize 0 b_shape
-  cmp <- letSubExp "bucket_cmp" $ I.BasicOp $ I.CmpOp (I.CmpEq I.int32) b_w w_img
-  c <- assertingOne $
-    letExp "bucket_cert" $ I.BasicOp $
-    I.Assert cmp "length of index and value array does not match" (loc, mempty)
-  buckets'' <- certifying c $ letExp (baseString buckets') $
-    I.BasicOp $ I.Reshape (reshapeOuter [DimCoercion w_img] 1 b_shape) buckets'
-
-  letTupExp' desc $ I.Op $
-    I.GenReduce w_img [GenReduceOp w_hist hist' ne_shp op'] (I.Lambda params body' rettype) $ buckets'' : img'
-
-internaliseExp desc (E.Scan lam ne arr loc) =
-  internaliseScanOrReduce desc "scan" scan (lam, ne, arr, loc)
-  where scan w scan_lam nes arrs =
-          I.Screma w <$> I.scanSOAC scan_lam nes <*> pure arrs
-
-internaliseExp _ (E.Filter lam arr _) = do
-  arrs <- internaliseExpToVars "filter_input" arr
-  lam' <- internalisePartitionLambda internaliseLambda 1 lam $ map I.Var arrs
-  uncurry (++) <$> partitionWithSOACS 1 lam' arrs
-
-internaliseExp _ (E.Partition k lam arr _) = do
-  arrs <- internaliseExpToVars "partition_input" arr
-  lam' <- internalisePartitionLambda internaliseLambda k lam $ map I.Var arrs
-  uncurry (++) <$> partitionWithSOACS k lam' arrs
-
-internaliseExp desc (E.Stream (E.MapLike o) lam arr _) = do
-  arrs <- internaliseExpToVars "stream_input" arr
-  lam' <- internaliseStreamMapLambda internaliseLambda lam $ map I.Var arrs
-  w <- arraysSize 0 <$> mapM lookupType arrs
-  let form = I.Parallel o Commutative (I.Lambda [] (mkBody mempty []) []) []
-  letTupExp' desc $ I.Op $ I.Stream w form lam' arrs
-
--- If the stream form is a reduce, we also have to fiddle with the
--- lambda to incorporate the reduce function.  FIXME: can't we just
--- modify the internal representation of reduction streams?
-internaliseExp desc (E.Stream (E.RedLike o comm lam0) lam arr _) = do
-  arrs <- internaliseExpToVars "stream_input" arr
-  rowts <- mapM (fmap I.rowType . lookupType) arrs
-  (lam_params, lam_body) <-
-    internaliseStreamLambda internaliseLambda lam rowts
-  let (chunk_param, _, lam_val_params) =
-        partitionChunkedFoldParameters 0 lam_params
-
-  -- Synthesize neutral elements by applying the fold function
-  -- to an empty chunk.
-  letBindNames_ [I.paramName chunk_param] $
-    I.BasicOp $ I.SubExp $ constant (0::Int32)
-  forM_ lam_val_params $ \p ->
-    letBindNames_ [I.paramName p] $
-    I.BasicOp $ I.Scratch (I.elemType $ I.paramType p) $
-    I.arrayDims $ I.paramType p
-  accs <- bodyBind =<< renameBody lam_body
-
-  acctps <- mapM I.subExpType accs
-  outsz  <- arraysSize 0 <$> mapM lookupType arrs
-  let acc_arr_tps = [ I.arrayOf t (I.Shape [outsz]) NoUniqueness | t <- acctps ]
-  lam0'  <- internaliseFoldLambda internaliseLambda lam0 acctps acc_arr_tps
-  let lam0_acc_params = fst $ splitAt (length accs) $ I.lambdaParams lam0'
-  acc_params <- forM lam0_acc_params $ \p -> do
-    name <- newVName $ baseString $ I.paramName p
-    return p { I.paramName = name }
-
-  body_with_lam0 <-
-    ensureResultShape asserting "shape of result does not match shape of initial value"
-    (srclocOf lam0) acctps <=< insertStmsM $ do
-      lam_res <- bodyBind lam_body
-
-      let consumed = consumedByLambda $ Alias.analyseLambda lam0'
-          copyIfConsumed p (I.Var v)
-            | I.paramName p `S.member` consumed =
-                letSubExp "acc_copy" $ I.BasicOp $ I.Copy v
-          copyIfConsumed _ x = return x
-
-      accs' <- zipWithM copyIfConsumed (I.lambdaParams lam0') accs
-      lam_res' <- ensureArgShapes asserting
-                  "shape of chunk function result does not match shape of initial value"
-                  (srclocOf lam) [] (map I.typeOf $ I.lambdaParams lam0') lam_res
-      new_lam_res <- eLambda lam0' $ map eSubExp $ accs' ++ lam_res'
-      return $ resultBody new_lam_res
-
-  -- Make sure the chunk size parameter comes first.
-  let form = I.Parallel o comm lam0' accs
-      lam' = I.Lambda { lambdaParams = chunk_param : acc_params ++ lam_val_params
-                      , lambdaBody = body_with_lam0
-                      , lambdaReturnType = acctps }
-  w <- arraysSize 0 <$> mapM lookupType arrs
-  letTupExp' desc $ I.Op $ I.Stream w form lam' arrs
-
 internaliseExp _ (E.VConstr0 c (Info t) loc) =
   case t of
     Enum cs ->
@@ -860,9 +722,9 @@
 andExp l r = E.If l r (E.Literal (E.BoolValue False) noLoc) (Info (E.Prim E.Bool)) noLoc
 
 eqExp :: E.Exp -> E.Exp -> E.Exp
-eqExp l r = E.BinOp eq (Info $ vacuousShapeAnnotations ft)
+eqExp l r = E.BinOp eq (Info ft)
             (l, sType l) (r, sType r) (Info (E.Prim E.Bool)) noLoc
-  where sType e = Info $ toStruct $ vacuousShapeAnnotations $ E.typeOf e
+  where sType e = Info $ toStruct $ E.typeOf e
         arrow   = Arrow S.empty Nothing
         ft      = E.typeOf l `arrow` E.typeOf r `arrow` E.Prim E.Bool
         eq      = qualName $ VName "==" (-1)
@@ -871,7 +733,7 @@
 generateCond p e = foldr andExp (E.Literal (E.BoolValue True) noLoc) conds
   where conds = mapMaybe ((<*> pure e) . fst) $ generateCond' p
 
-        generateCond' :: E.Pattern -> [(Maybe (E.Exp -> E.Exp), CompType)]
+        generateCond' :: E.Pattern -> [(Maybe (E.Exp -> E.Exp), PatternType)]
         generateCond' (E.TuplePattern ps loc) = generateCond' (E.RecordPattern fs loc)
           where fs = zipWith (\i p' -> (nameFromString (show i), p')) ([1..] :: [Integer]) ps
         generateCond' (E.RecordPattern fs _) = concatMap instCond holes
@@ -885,12 +747,12 @@
                 instCond (condHoles, f) = map (projectHole f) condHoles
         generateCond' (E.PatternParens p' _) = generateCond' p'
         generateCond' (E.Id _ (Info t) _) =
-          [(Nothing, removeShapeAnnotations t)]
+          [(Nothing, t)]
         generateCond' (E.Wildcard (Info t) _)=
-          [(Nothing, removeShapeAnnotations t)]
+          [(Nothing, t)]
         generateCond' (E.PatternAscription p' _ _) = generateCond' p'
         generateCond' (E.PatternLit ePat (Info t) _) =
-          [(Just (eqExp ePat), removeShapeAnnotations t)]
+          [(Just (eqExp ePat), t)]
 
 
 generateCaseIf :: String -> E.Exp -> Case -> I.Body -> InternaliseM I.Exp
@@ -1024,6 +886,121 @@
   w <- arraysSize 0 <$> mapM lookupType arrs
   letTupExp' desc . I.Op =<< f w lam' nes' arrs
 
+internaliseGenReduce :: String
+                     -> E.Exp -> E.Exp -> E.Exp -> E.Exp -> E.Exp -> SrcLoc
+                     -> InternaliseM [SubExp]
+internaliseGenReduce desc hist op ne buckets img loc = do
+  ne' <- internaliseExp "gen_reduce_ne" ne
+  hist' <- internaliseExpToVars "gen_reduce_hist" hist
+  buckets' <- letExp "gen_reduce_buckets" . BasicOp . SubExp =<<
+              internaliseExp1 "gen_reduce_buckets" buckets
+  img' <- internaliseExpToVars "gen_reduce_img" img
+
+  -- reshape neutral element to have same size as the destination array
+  ne_shp <- forM (zip ne' hist') $ \(n, h) -> do
+    rowtype <- I.stripArray 1 <$> lookupType h
+    ensureShape asserting
+      "Row shape of destination array does not match shape of neutral element"
+      loc rowtype "gen_reduce_ne_right_shape" n
+  ne_ts <- mapM I.subExpType ne_shp
+  his_ts <- mapM lookupType hist'
+  op' <- internaliseFoldLambda internaliseLambda op ne_ts his_ts
+
+  -- reshape return type of bucket function to have same size as neutral element
+  -- (modulo the index)
+  bucket_param <- newParam "bucket_p" $ I.Prim int32
+  img_params <- mapM (newParam "img_p" . rowType) =<< mapM lookupType img'
+  let params = bucket_param : img_params
+      rettype = I.Prim int32 : ne_ts
+      body = mkBody mempty $ map (I.Var . paramName) params
+  body' <- localScope (scopeOfLParams params) $
+           ensureResultShape asserting
+           "Row shape of value array does not match row shape of gen_reduce target"
+           (srclocOf img) rettype body
+
+  -- get sizes of histogram and image arrays
+  w_hist <- arraysSize 0 <$> mapM lookupType hist'
+  w_img <- arraysSize 0 <$> mapM lookupType img'
+
+  -- Generate an assertion and reshapes to ensure that buckets' and
+  -- img' are the same size.
+  b_shape <- arrayShape <$> lookupType buckets'
+  let b_w = shapeSize 0 b_shape
+  cmp <- letSubExp "bucket_cmp" $ I.BasicOp $ I.CmpOp (I.CmpEq I.int32) b_w w_img
+  c <- assertingOne $
+    letExp "bucket_cert" $ I.BasicOp $
+    I.Assert cmp "length of index and value array does not match" (loc, mempty)
+  buckets'' <- certifying c $ letExp (baseString buckets') $
+    I.BasicOp $ I.Reshape (reshapeOuter [DimCoercion w_img] 1 b_shape) buckets'
+
+  letTupExp' desc $ I.Op $
+    I.GenReduce w_img [GenReduceOp w_hist hist' ne_shp op'] (I.Lambda params body' rettype) $ buckets'' : img'
+
+internaliseStreamMap :: String -> StreamOrd -> E.Exp -> E.Exp
+                     -> InternaliseM [SubExp]
+internaliseStreamMap desc o lam arr = do
+  arrs <- internaliseExpToVars "stream_input" arr
+  lam' <- internaliseStreamMapLambda internaliseLambda lam $ map I.Var arrs
+  w <- arraysSize 0 <$> mapM lookupType arrs
+  let form = I.Parallel o Commutative (I.Lambda [] (mkBody mempty []) []) []
+  letTupExp' desc $ I.Op $ I.Stream w form lam' arrs
+
+internaliseStreamRed :: String -> StreamOrd -> Commutativity
+                     -> E.Exp -> E.Exp -> E.Exp
+                     -> InternaliseM [SubExp]
+internaliseStreamRed desc o comm lam0 lam arr = do
+  arrs <- internaliseExpToVars "stream_input" arr
+  rowts <- mapM (fmap I.rowType . lookupType) arrs
+  (lam_params, lam_body) <-
+    internaliseStreamLambda internaliseLambda lam rowts
+  let (chunk_param, _, lam_val_params) =
+        partitionChunkedFoldParameters 0 lam_params
+
+  -- Synthesize neutral elements by applying the fold function
+  -- to an empty chunk.
+  letBindNames_ [I.paramName chunk_param] $
+    I.BasicOp $ I.SubExp $ constant (0::Int32)
+  forM_ lam_val_params $ \p ->
+    letBindNames_ [I.paramName p] $
+    I.BasicOp $ I.Scratch (I.elemType $ I.paramType p) $
+    I.arrayDims $ I.paramType p
+  accs <- bodyBind =<< renameBody lam_body
+
+  acctps <- mapM I.subExpType accs
+  outsz  <- arraysSize 0 <$> mapM lookupType arrs
+  let acc_arr_tps = [ I.arrayOf t (I.Shape [outsz]) NoUniqueness | t <- acctps ]
+  lam0'  <- internaliseFoldLambda internaliseLambda lam0 acctps acc_arr_tps
+  let lam0_acc_params = fst $ splitAt (length accs) $ I.lambdaParams lam0'
+  acc_params <- forM lam0_acc_params $ \p -> do
+    name <- newVName $ baseString $ I.paramName p
+    return p { I.paramName = name }
+
+  body_with_lam0 <-
+    ensureResultShape asserting "shape of result does not match shape of initial value"
+    (srclocOf lam0) acctps <=< insertStmsM $ do
+      lam_res <- bodyBind lam_body
+
+      let consumed = consumedByLambda $ Alias.analyseLambda lam0'
+          copyIfConsumed p (I.Var v)
+            | I.paramName p `S.member` consumed =
+                letSubExp "acc_copy" $ I.BasicOp $ I.Copy v
+          copyIfConsumed _ x = return x
+
+      accs' <- zipWithM copyIfConsumed (I.lambdaParams lam0') accs
+      lam_res' <- ensureArgShapes asserting
+                  "shape of chunk function result does not match shape of initial value"
+                  (srclocOf lam) [] (map I.typeOf $ I.lambdaParams lam0') lam_res
+      new_lam_res <- eLambda lam0' $ map eSubExp $ accs' ++ lam_res'
+      return $ resultBody new_lam_res
+
+  -- Make sure the chunk size parameter comes first.
+  let form = I.Parallel o comm lam0' accs
+      lam' = I.Lambda { lambdaParams = chunk_param : acc_params ++ lam_val_params
+                      , lambdaBody = body_with_lam0
+                      , lambdaReturnType = acctps }
+  w <- arraysSize 0 <$> mapM lookupType arrs
+  letTupExp' desc $ I.Op $ I.Stream w form lam' arrs
+
 internaliseExp1 :: String -> E.Exp -> InternaliseM I.SubExp
 internaliseExp1 desc e = do
   vs <- internaliseExp desc e
@@ -1204,27 +1181,7 @@
     mapM_ (uncurry (internaliseDimConstant loc)) $ pcm<>rcm
     return (params', body', map I.fromDecl rettype')
 
-internaliseLambda E.OpSection{} _ = fail "internaliseLambda: unexpected OpSection"
-
-internaliseLambda E.OpSectionLeft{} _ = fail "internaliseLambda: unexpected OpSectionLeft"
-
-internaliseLambda E.OpSectionRight{} _ = fail "internaliseLambda: unexpected OpSectionRight"
-
-internaliseLambda e rowtypes = do
-  (_, _, remaining_params_ts) <- findFuncall e
-  (params, param_args) <- fmap unzip $ forM remaining_params_ts $ \et -> do
-    name <- newVName "not_curried"
-    return (E.Id name (Info $ E.vacuousShapeAnnotations $ et `setAliases` mempty) loc,
-            E.Var (E.qualName name)
-             (Info (et `setAliases` mempty)) loc)
-  let rettype = E.typeOf e
-      body = foldl (\f arg -> E.Apply f arg (Info E.Observe)
-                              (Info $ E.vacuousShapeAnnotations rettype) loc)
-                   e
-                   param_args
-      rettype' = E.vacuousShapeAnnotations $ rettype `E.setAliases` ()
-  internaliseLambda (E.Lambda [] params body Nothing (Info (mempty, rettype')) loc) rowtypes
-  where loc = srclocOf e
+internaliseLambda e _ = fail $ "internaliseLambda: unexpected expression:\n" ++ pretty e
 
 internaliseDimConstant :: SrcLoc -> Name -> VName -> InternaliseM ()
 internaliseDimConstant loc fname name =
@@ -1411,6 +1368,60 @@
       (++) <$> internaliseExp (desc ++ "_zip_x") x
            <*> internaliseExp (desc ++ "_zip_y") y
 
+    handle [TupLit [lam, arr] _] "map" = Just $ \desc -> do
+      arr' <- internaliseExpToVars "map_arr" arr
+      lam' <- internaliseMapLambda internaliseLambda lam $ map I.Var arr'
+      w <- arraysSize 0 <$> mapM lookupType arr'
+      letTupExp' desc $ I.Op $
+        I.Screma w (I.mapSOAC lam') arr'
+
+    handle [TupLit [lam, arr] _] "filter" = Just $ \_desc -> do
+      arrs <- internaliseExpToVars "filter_input" arr
+      lam' <- internalisePartitionLambda internaliseLambda 1 lam $ map I.Var arrs
+      uncurry (++) <$> partitionWithSOACS 1 lam' arrs
+
+    handle [TupLit [k, lam, arr] _] "partition" = do
+      k' <- fromIntegral <$> isInt32 k
+      Just $ \_desc -> do
+        arrs <- internaliseExpToVars "partition_input" arr
+        lam' <- internalisePartitionLambda internaliseLambda k' lam $ map I.Var arrs
+        uncurry (++) <$> partitionWithSOACS k' lam' arrs
+        where isInt32 (Literal (SignedValue (Int32Value k')) _) = Just k'
+              isInt32 (IntLit k' (Info (E.Prim (Signed Int32))) _) = Just $ fromInteger k'
+              isInt32 _ = Nothing
+
+    handle [TupLit [lam, ne, arr] _] "reduce" = Just $ \desc ->
+      internaliseScanOrReduce desc "reduce" reduce (lam, ne, arr, loc)
+      where reduce w red_lam nes arrs =
+              I.Screma w <$>
+              I.reduceSOAC Noncommutative red_lam nes <*> pure arrs
+
+    handle [TupLit [lam, ne, arr] _] "reduce_comm" = Just $ \desc ->
+      internaliseScanOrReduce desc "reduce" reduce (lam, ne, arr, loc)
+      where reduce w red_lam nes arrs =
+              I.Screma w <$>
+              I.reduceSOAC Commutative red_lam nes <*> pure arrs
+
+    handle [TupLit [lam, ne, arr] _] "scan" = Just $ \desc ->
+      internaliseScanOrReduce desc "scan" reduce (lam, ne, arr, loc)
+      where reduce w scan_lam nes arrs =
+              I.Screma w <$> I.scanSOAC scan_lam nes <*> pure arrs
+
+    handle [TupLit [op, f, arr] _] "stream_red" = Just $ \desc ->
+      internaliseStreamRed desc InOrder Noncommutative op f arr
+
+    handle [TupLit [op, f, arr] _] "stream_red_per" = Just $ \desc ->
+      internaliseStreamRed desc Disorder Commutative op f arr
+
+    handle [TupLit [f, arr] _] "stream_map" = Just $ \desc ->
+      internaliseStreamMap desc InOrder f arr
+
+    handle [TupLit [f, arr] _] "stream_map_per" = Just $ \desc ->
+      internaliseStreamMap desc Disorder f arr
+
+    handle [TupLit [dest, op, ne, buckets, img] _] "gen_reduce" = Just $ \desc ->
+      internaliseGenReduce desc dest op ne buckets img loc
+
     handle [x] "unzip" = Just $ flip internaliseExp x
     handle [x] "trace" = Just $ flip internaliseExp x
     handle [x] "break" = Just $ flip internaliseExp x
@@ -1556,7 +1567,7 @@
           safety <- askSafety
           se <- letSubExp (baseString name ++ "_arg") $
                 I.Apply fname [] [I.Prim I.int32] (safety, loc, [])
-          return (se, I.Observe, I.Prim I.int32)
+          return (se, I.ObservePrim, I.Prim I.int32)
 
 funcall :: String -> QualName VName -> [SubExp] -> SrcLoc
         -> InternaliseM ([SubExp], [I.ExtType])
@@ -1567,7 +1578,7 @@
   argts <- mapM subExpType args
   closure_ts <- mapM lookupType closure
   shapeargs <- argShapes shapes value_paramts argts
-  let diets = const_ds ++ replicate (length closure + length shapeargs) I.Observe ++
+  let diets = const_ds ++ replicate (length closure + length shapeargs) I.ObservePrim ++
               map I.diet value_paramts
       constOrShape = const $ I.Prim int32
       paramts = map constOrShape constargs ++ closure_ts ++
diff --git a/src/Futhark/Internalise/Bindings.hs b/src/Futhark/Internalise/Bindings.hs
--- a/src/Futhark/Internalise/Bindings.hs
+++ b/src/Futhark/Internalise/Bindings.hs
@@ -101,8 +101,7 @@
       -- XXX: we gotta be screwing up somehow by ignoring the extra
       -- return values.  If not, why not?
       (tss, _) <- internaliseParamTypes nothing_bound mempty
-                  [flip E.setAliases () $ E.vacuousShapeAnnotations $
-                   E.unInfo $ E.identType bindee]
+                  [flip E.setAliases () $ E.unInfo $ E.identType bindee]
       case concat tss of
         [t] -> return [(name, t)]
         tss' -> forM tss' $ \t -> do
@@ -131,8 +130,7 @@
           flattenPattern' $ E.Id name t loc
         flattenPattern' (E.Id v (Info t) loc) = do
           new_name <- newVName $ baseString v
-          return [((E.Ident v (Info (E.removeShapeAnnotations t)) loc,
-                    new_name),
+          return [((E.Ident v (Info t) loc, new_name),
                    t `E.setAliases` ())]
         flattenPattern' (E.TuplePattern pats _) =
           concat <$> mapM flattenPattern' pats
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
@@ -19,7 +19,7 @@
 
 -- | A static value stores additional information about the result of
 -- defunctionalization of an expression, aside from the residual expression.
-data StaticVal = Dynamic CompType
+data StaticVal = Dynamic PatternType
                | LambdaSV [VName] Pattern StructType Exp Env
                  -- ^ The 'VName's are shape parameters that are bound
                  -- by the 'Pattern'.
@@ -171,31 +171,29 @@
       (pats, body, tp) <- etaExpand e
       defuncExp $ Lambda [] pats body Nothing (Info (mempty, tp)) noLoc
     _ -> let tp = typeFromSV sv
-         in return (Var qn (Info (vacuousShapeAnnotations tp)) loc, sv)
+         in return (Var qn (Info tp) loc, sv)
 
-defuncExp (Ascript e0 tydecl loc)
+defuncExp (Ascript e0 tydecl t loc)
   | orderZero (typeOf e0) = do (e0', sv) <- defuncExp e0
-                               return (Ascript e0' tydecl loc, sv)
+                               return (Ascript e0' tydecl t loc, sv)
   | otherwise = defuncExp e0
 
-defuncExp (LetPat tparams pat e1 e2 loc) = do
+defuncExp (LetPat tparams pat e1 e2 _ loc) = do
   let env_dim = envFromShapeParams tparams
   (e1', sv1) <- localEnv env_dim $ defuncExp e1
   let env  = matchPatternSV pat sv1
       pat' = updatePattern pat sv1
   (e2', sv2) <- localEnv (env <> env_dim) $ defuncExp e2
-  return (LetPat tparams pat' e1' e2' loc, sv2)
+  return (LetPat tparams pat' e1' e2' (Info $ typeOf e2') loc, sv2)
 
 defuncExp (LetFun vn (dims, pats, _, rettype@(Info ret), e1) e2 loc) = do
   let env_dim = envFromShapeParams dims
   (pats', e1', sv1) <- localEnv env_dim $ defuncLet dims pats e1 rettype
   (e2', sv2) <- extendEnv vn sv1 $ defuncExp e2
   case pats' of
-    []  -> let t1 = combineTypeShapes (fromStruct ret) $
-                    vacuousShapeAnnotations $ typeOf e1'
-           in return (LetPat dims (Id vn (Info t1) noLoc) e1' e2' loc, sv2)
-    _:_ -> let t1 = combineTypeShapes ret $
-                    vacuousShapeAnnotations . toStruct $ typeOf e1'
+    []  -> let t1 = combineTypeShapes (fromStruct ret) $ typeOf e1'
+           in return (LetPat dims (Id vn (Info t1) noLoc) e1' e2' (Info $ typeOf e2') loc, sv2)
+    _:_ -> let t1 = combineTypeShapes ret $ toStruct $ typeOf e1'
            in return (LetFun vn (dims, pats', Nothing, Info t1, e1') e2' loc, sv2)
 
 defuncExp (If e1 e2 e3 tp loc) = do
@@ -204,6 +202,14 @@
   (e3', _ ) <- defuncExp e3
   return (If e1' e2' e3' tp loc, sv)
 
+defuncExp e@(Apply f@(Var f' _ _) arg d t loc)
+  | baseTag (qualLeaf f') <= maxIntrinsicTag,
+    TupLit es tuploc <- arg = do
+      -- defuncSoacExp also works fine for non-SOACs.
+      es' <- mapM defuncSoacExp es
+      return (Apply f (TupLit es' tuploc) d t loc,
+              Dynamic $ typeOf e)
+
 defuncExp e@Apply{} = defuncApply 0 e
 
 defuncExp (Negate e0 loc) = do
@@ -242,7 +248,7 @@
 
         closureFromDynamicFun (vn, sv) =
           let name = nameFromString $ pretty vn
-              tp' = vacuousShapeAnnotations $ typeFromSV sv
+              tp' = typeFromSV sv
           in (RecordFieldExplicit name
                (Var (qualName vn) (Info tp') noLoc) noLoc, (vn, sv))
 
@@ -267,7 +273,8 @@
                         return (While e2', mempty)
   (e3', sv) <- localEnv (env1 <> env2 <> env_dim) $ defuncExp e3
   return (DoLoop tparams pat e1' form' e3' loc, sv)
-  where envFromIdent (Ident vn (Info tp) _) = M.singleton vn $ Dynamic tp
+  where envFromIdent (Ident vn (Info tp) _) =
+          M.singleton vn $ Dynamic tp
 
 -- We handle BinOps by turning them into ordinary function applications.
 defuncExp (BinOp qn (Info t) (e1, Info pt1) (e2, Info pt2) (Info ret) loc) =
@@ -284,12 +291,12 @@
     Dynamic _ -> return (Project vn e0' tp loc, Dynamic tp')
     _ -> error $ "Projection of an expression with static value " ++ show sv0
 
-defuncExp (LetWith id1 id2 idxs e1 body loc) = do
+defuncExp (LetWith id1 id2 idxs e1 body t loc) = do
   e1' <- defuncExp' e1
   sv1 <- lookupVar (identSrcLoc id2) $ identName id2
   idxs' <- mapM defuncDimIndex idxs
   (body', sv) <- extendEnv (identName id1) sv1 $ defuncExp body
-  return (LetWith id1 id2 idxs' e1' body' loc, sv)
+  return (LetWith id1 id2 idxs' e1' body' t loc, sv)
 
 defuncExp expr@(Index e0 idxs info loc) = do
   e0' <- defuncExp' e0
@@ -309,8 +316,7 @@
   (e1', sv1) <- defuncExp e1
   (e2', sv2) <- defuncExp e2
   let sv = staticField sv1 sv2 fs
-  return (RecordUpdate e1' fs e2'
-           (Info $ vacuousShapeAnnotations $ typeFromSV sv1) loc,
+  return (RecordUpdate e1' fs e2' (Info $ typeFromSV sv1) loc,
           sv)
   where staticField (RecordSV svs) sv2 (f:fs') =
           case lookup f svs of
@@ -321,48 +327,6 @@
           staticField (svFromType t) sv2 fs'
         staticField _ sv2 _ = sv2
 
-defuncExp e@(Map fun arr t loc) = do
-  fun' <- defuncSoacExp fun
-  arr' <- defuncExp' arr
-  return (Map fun' arr' t loc, Dynamic $ typeOf e)
-
-defuncExp e@(Reduce comm fun ne arr loc) = do
-  fun' <- defuncSoacExp fun
-  ne' <- defuncExp' ne
-  arr' <- defuncExp' arr
-  return (Reduce comm fun' ne' arr' loc, Dynamic $ typeOf e)
-
-defuncExp e@(GenReduce hist op ne bfun img loc) = do
-  hist' <- defuncExp' hist
-  op' <- defuncSoacExp op
-  ne' <- defuncExp' ne
-  bfun' <- defuncSoacExp bfun
-  img' <- defuncExp' img
-  return (GenReduce hist' op' ne' bfun' img' loc, Dynamic $ typeOf e)
-
-defuncExp e@(Scan fun ne arr loc) =
-  (,) <$> (Scan <$> defuncSoacExp fun <*> defuncExp' ne <*> defuncExp' arr
-                <*> pure loc)
-      <*> pure (Dynamic $ typeOf e)
-
-defuncExp e@(Filter fun arr loc) = do
-  fun' <- defuncSoacExp fun
-  arr' <- defuncExp' arr
-  return (Filter fun' arr' loc, Dynamic $ typeOf e)
-
-defuncExp e@(Partition k fun arr loc) = do
-  fun' <- defuncSoacExp fun
-  arr' <- defuncExp' arr
-  return (Partition k fun' arr' loc, Dynamic $ typeOf e)
-
-defuncExp e@(Stream form lam arr loc) = do
-  form' <- case form of
-             MapLike _          -> return form
-             RedLike so comm e' -> RedLike so comm <$> defuncSoacExp e'
-  lam' <- defuncSoacExp lam
-  arr' <- defuncExp' arr
-  return (Stream form' lam' arr' loc, Dynamic $ typeOf e)
-
 defuncExp (Unsafe e1 loc) = do
   (e1', sv) <- defuncExp e1
   return (Unsafe e1' loc, sv)
@@ -424,15 +388,13 @@
   let (ps, ret) = getType $ typeOf e
   (pats, vars) <- fmap unzip . forM ps $ \t -> do
     x <- newNameFromString "x"
-    let t' = vacuousShapeAnnotations t
-    return (Id x (Info t') noLoc,
-            Var (qualName x) (Info t') noLoc)
-  let ps_st = map vacuousShapeAnnotations ps
-      e' = foldl' (\e1 (e2, t2, argtypes) ->
+    return (Id x (Info t) noLoc,
+            Var (qualName x) (Info t) noLoc)
+  let e' = foldl' (\e1 (e2, t2, argtypes) ->
                      Apply e1 e2 (Info $ diet t2)
-                     (Info (foldFunType argtypes (vacuousShapeAnnotations ret))) noLoc)
-           e $ zip3 vars ps (drop 1 $ tails ps_st)
-  return (pats, e', vacuousShapeAnnotations $ toStruct ret)
+                     (Info (foldFunType argtypes ret)) noLoc)
+           e $ zip3 vars ps (drop 1 $ tails ps)
+  return (pats, e', toStruct ret)
 
   where getType (Arrow _ _ t1 t2) =
           let (ps, r) = getType t2 in (t1 : ps, r)
@@ -464,7 +426,7 @@
   (body', sv) <- defuncExp body
   return ([], body', imposeType sv rettype )
   where imposeType Dynamic{} t =
-          Dynamic $ fromStruct $ removeShapeAnnotations t
+          Dynamic $ fromStruct t
         imposeType (RecordSV fs1) (Record fs2) =
           RecordSV $ M.toList $ M.intersectionWith imposeType (M.fromList fs1) fs2
         imposeType sv _ = sv
@@ -496,7 +458,8 @@
           params_for_rettype = params ++ svParams sv1 ++ svParams sv2
           svParams (LambdaSV _ sv_pat _ _ _) = [sv_pat]
           svParams _                         = []
-          rettype = buildRetType closure_env params_for_rettype e0_t $ typeOf e0'
+          rettype = buildRetType closure_env params_for_rettype e0_t $
+                    anyDimShapeAnnotations $ typeOf e0'
 
           -- Embed some information about the original function
           -- into the name of the lifted function, to make the
@@ -509,8 +472,8 @@
       fname <- newNameFromString $ liftedName (0::Int) e1
       liftValDec fname rettype dims params e0'
 
-      let t1 = vacuousShapeAnnotations . toStruct $ typeOf e1'
-          t2 = vacuousShapeAnnotations . toStruct $ typeOf e2'
+      let t1 = toStruct $ typeOf e1'
+          t2 = toStruct $ typeOf e2'
           fname' = qualName fname
       return (Parens (Apply (Apply (Var fname' (Info (Arrow mempty Nothing (fromStruct t1) $
                                                       Arrow mempty Nothing (fromStruct t2) rettype)) loc)
@@ -556,7 +519,7 @@
 
       IntrinsicSV -> return (e, IntrinsicSV)
 
-      _ -> return (Var qn (Info (vacuousShapeAnnotations $ typeFromSV sv)) loc, sv)
+      _ -> return (Var qn (Info (typeFromSV sv)) loc, sv)
 
 defuncApply _ expr = defuncExp expr
 
@@ -587,7 +550,7 @@
   TuplePattern ps _       -> foldMap envFromPattern ps
   RecordPattern fs _      -> foldMap (envFromPattern . snd) fs
   PatternParens p _       -> envFromPattern p
-  Id vn (Info t) _        -> M.singleton vn $ Dynamic $ removeShapeAnnotations t
+  Id vn (Info t) _        -> M.singleton vn $ Dynamic t
   Wildcard _ _            -> mempty
   PatternAscription p _ _ -> envFromPattern p
   PatternLit{}            -> mempty
@@ -609,7 +572,7 @@
 liftValDec :: VName -> PatternType -> [VName] -> [Pattern] -> Exp -> DefM ()
 liftValDec fname rettype dims pats body = tell $ Seq.singleton dec
   where dims' = map (flip TypeParamDim noLoc) dims
-        rettype_st = vacuousShapeAnnotations $ toStruct rettype
+        rettype_st = anyDimShapeAnnotations $ toStruct rettype
         dec = ValBind
           { valBindEntryPoint = False
           , valBindName       = fname
@@ -626,9 +589,8 @@
 -- binds the closed over variables.
 buildEnvPattern :: Env -> Pattern
 buildEnvPattern env = RecordPattern (map buildField $ M.toList env) noLoc
-  where buildField (vn, sv) = let tp = vacuousShapeAnnotations (typeFromSV sv)
-                              in (nameFromString (pretty vn),
-                                  Id vn (Info tp) noLoc)
+  where buildField (vn, sv) = (nameFromString (pretty vn),
+                               Id vn (Info $ anyDimShapeAnnotations $ typeFromSV sv) noLoc)
 
 -- | Given a closure environment pattern and the type of a term,
 -- construct the type of that term, where uniqueness is set to
@@ -637,16 +599,16 @@
 -- lifted function can create unique arrays as long as they do not
 -- alias any of its parameters.  XXX: it is not clear that this is a
 -- sufficient property, unfortunately.
-buildRetType :: Env -> [Pattern] -> StructType -> CompType -> PatternType
+buildRetType :: Env -> [Pattern] -> StructType -> PatternType -> PatternType
 buildRetType env pats = comb
   where bound = foldMap oneName (M.keys env) <> foldMap patternVars pats
         boundAsUnique v =
           maybe False (unique . unInfo . identType) $
-          find ((==v) . identName) $ S.toList $ foldMap patIdentSet pats
+          find ((==v) . identName) $ S.toList $ foldMap patternIdents pats
         problematic v = (v `member` bound) && not (boundAsUnique v)
         comb (Record fs_annot) (Record fs_got) =
           Record $ M.intersectionWith comb fs_annot fs_got
-        comb Arrow{} t = vacuousShapeAnnotations $ descend t
+        comb Arrow{} t = descend t
         comb got et = descend $ fromStruct got `setUniqueness` uniqueness et `setAliases` aliases et
 
         descend t@Array{}
@@ -655,15 +617,15 @@
         descend t = t
 
 -- | Compute the corresponding type for a given static value.
-typeFromSV :: StaticVal -> CompType
-typeFromSV (Dynamic tp)           = tp
+typeFromSV :: StaticVal -> PatternType
+typeFromSV (Dynamic tp)           = anyDimShapeAnnotations tp
 typeFromSV (LambdaSV _ _ _ _ env) = typeFromEnv env
 typeFromSV (RecordSV ls)          = Record $ M.fromList $ map (fmap typeFromSV) ls
 typeFromSV (DynamicFun (_, sv) _) = typeFromSV sv
 typeFromSV IntrinsicSV            = error $ "Tried to get the type from the "
                                          ++ "static value of an intrinsic."
 
-typeFromEnv :: Env -> CompType
+typeFromEnv :: Env -> PatternType
 typeFromEnv = Record . M.fromList .
               map (bimap (nameFromString . pretty) typeFromSV) . M.toList
 
@@ -672,7 +634,7 @@
 dynamicFunType :: StaticVal -> [PatternType] -> ([PatternType], PatternType)
 dynamicFunType (DynamicFun _ sv) (p:ps) =
   let (ps', ret) = dynamicFunType sv ps in (p : ps', ret)
-dynamicFunType sv _ = ([], vacuousShapeAnnotations $ typeFromSV sv)
+dynamicFunType sv _ = ([], typeFromSV sv)
 
 -- | Match a pattern with its static value. Returns an environment with
 -- the identifier components of the pattern mapped to the corresponding
@@ -690,7 +652,7 @@
   -- the pattern wins out.  This is important when matching a
   -- nonunique pattern with a unique value.
   if orderZeroSV sv
-  then M.singleton vn $ Dynamic $ removeShapeAnnotations t
+  then M.singleton vn $ Dynamic t
   else M.singleton vn sv
 matchPatternSV (Wildcard _ _) _ = mempty
 matchPatternSV (PatternAscription pat _ _) sv = matchPatternSV pat sv
@@ -717,11 +679,10 @@
   PatternParens (updatePattern pat sv) loc
 updatePattern pat@(Id vn (Info tp) loc) sv
   | orderZero tp = pat
-  | otherwise = Id vn (Info . vacuousShapeAnnotations $
-                       typeFromSV sv `setUniqueness` Nonunique) loc
+  | otherwise = Id vn (Info $ typeFromSV sv `setUniqueness` Nonunique) loc
 updatePattern pat@(Wildcard (Info tp) loc) sv
   | orderZero tp = pat
-  | otherwise = Wildcard (Info . vacuousShapeAnnotations $ typeFromSV sv) loc
+  | otherwise = Wildcard (Info $ typeFromSV sv) loc
 updatePattern (PatternAscription pat tydecl loc) sv
   | orderZero . unInfo $ expandedType tydecl =
       PatternAscription (updatePattern pat sv) tydecl loc
@@ -734,7 +695,7 @@
 
 -- | Convert a record (or tuple) type to a record static value. This is used for
 -- "unwrapping" tuples and records that are nested in 'Dynamic' static values.
-svFromType :: CompType -> StaticVal
+svFromType :: PatternType -> StaticVal
 svFromType (Record fs) = RecordSV . M.toList $ M.map svFromType fs
 svFromType t           = Dynamic t
 
@@ -780,9 +741,9 @@
   Range e me incl _ _  -> freeVars e <> foldMap freeVars me <>
                           foldMap freeVars incl
   Var qn (Info t) _    -> NameSet $ M.singleton (qualLeaf qn) $ uniqueness t
-  Ascript e t _        -> freeVars e <> names (typeDimNames $ unInfo $ expandedType t)
-  LetPat _ pat e1 e2 _ -> freeVars e1 <> ((names (patternDimNames pat) <> freeVars e2)
-                                          `without` patternVars pat)
+  Ascript e t _ _      -> freeVars e <> names (typeDimNames $ unInfo $ expandedType t)
+  LetPat _ pat e1 e2 _ _ -> freeVars e1 <> ((names (patternDimNames pat) <> freeVars e2)
+                                            `without` patternVars pat)
 
   LetFun vn (_, pats, _, _, e1) e2 _ ->
     ((freeVars e1 <> names (foldMap patternDimNames pats))
@@ -812,7 +773,7 @@
                                     freeVars e1 <> freeVars e2
   Project _ e _ _                -> freeVars e
 
-  LetWith id1 id2 idxs e1 e2 _ ->
+  LetWith id1 id2 idxs e1 e2 _ _ ->
     ident id2 <> foldMap freeDimIndex idxs <> freeVars e1 <>
     (freeVars e2 `without` ident id1)
 
@@ -820,17 +781,6 @@
   Update e1 idxs e2 _ -> freeVars e1 <> foldMap freeDimIndex idxs <> freeVars e2
   RecordUpdate e1 _ e2 _ _ -> freeVars e1 <> freeVars e2
 
-  Map e1 e2 _ _       -> freeVars e1 <> freeVars e2
-  Reduce _ e1 e2 e3 _ -> freeVars e1 <> freeVars e2 <> freeVars e3
-  GenReduce e1 e2 e3 e4 e5 _ -> freeVars e1 <> freeVars e2 <> freeVars e3 <>
-                                freeVars e4 <> freeVars e5
-  Scan e1 e2 e3 _     -> freeVars e1 <> freeVars e2 <> freeVars e3
-  Filter e1 e2 _      -> freeVars e1 <> freeVars e2
-  Partition _ e1 e2 _ -> freeVars e1 <> freeVars e2
-  Stream form e1 e2 _ -> freeInForm form <> freeVars e1 <> freeVars e2
-    where freeInForm (RedLike _ _ e) = freeVars e
-          freeInForm _ = mempty
-
   Unsafe e _          -> freeVars e
   Assert e1 e2 _ _    -> freeVars e1 <> freeVars e2
   VConstr0{}          -> mempty
@@ -845,41 +795,7 @@
 
 -- | Extract all the variable names bound in a pattern.
 patternVars :: Pattern -> NameSet
-patternVars = mconcat . map ident . S.toList . patIdentSet
-
--- | Combine the shape information of types as much as possible. The first
--- argument is the orignal type and the second is the type of the transformed
--- expression. This is necessary since the original type may contain additional
--- information (e.g., shape restrictions) from the user given annotation.
-combineTypeShapes :: (Monoid as, ArrayDim dim) =>
-                     TypeBase dim as -> TypeBase dim as -> TypeBase dim as
-combineTypeShapes (Record ts1) (Record ts2)
-  | M.keys ts1 == M.keys ts2 =
-      Record $ M.map (uncurry combineTypeShapes) (M.intersectionWith (,) ts1 ts2)
-combineTypeShapes (Array als1 u1 et1 shape1) (Array als2 _u2 et2 shape2)
-  | Just new_shape <- unifyShapes shape1 shape2 =
-      Array (als1<>als2) u1 (combineElemTypeInfo et1 et2) new_shape
-combineTypeShapes _ new_tp = new_tp
-
-combineElemTypeInfo :: ArrayDim dim =>
-                       ArrayElemTypeBase dim
-                    -> ArrayElemTypeBase dim -> ArrayElemTypeBase dim
-combineElemTypeInfo (ArrayRecordElem et1) (ArrayRecordElem et2) =
-  ArrayRecordElem $ M.map (uncurry combineRecordArrayTypeInfo)
-                          (M.intersectionWith (,) et1 et2)
-combineElemTypeInfo _ new_tp = new_tp
-
-combineRecordArrayTypeInfo :: ArrayDim dim =>
-                              RecordArrayElemTypeBase dim
-                           -> RecordArrayElemTypeBase dim
-                           -> RecordArrayElemTypeBase dim
-combineRecordArrayTypeInfo (RecordArrayElem et1) (RecordArrayElem et2) =
-  RecordArrayElem $ combineElemTypeInfo et1 et2
-combineRecordArrayTypeInfo (RecordArrayArrayElem et1 shape1)
-                           (RecordArrayArrayElem et2 shape2)
-  | Just new_shape <- unifyShapes shape1 shape2 =
-      RecordArrayArrayElem (combineElemTypeInfo et1 et2) new_shape
-combineRecordArrayTypeInfo _ new_tp = new_tp
+patternVars = mconcat . map ident . S.toList . patternIdents
 
 -- | Defunctionalize a top-level value binding. Returns the
 -- transformed result as well as an environment that binds the name of
@@ -908,7 +824,7 @@
   let dim_names = foldMap patternDimNames params'
       tparams' = filter ((`S.member` dim_names) . typeParamName) tparams
 
-  let rettype' = vacuousShapeAnnotations . toStruct $ typeOf body'
+  let rettype' = anyDimShapeAnnotations $ toStruct $ typeOf body'
   return ( valbind { valBindRetDecl    = retdecl
                    , valBindRetType    = Info $ combineTypeShapes
                                          (unInfo rettype) rettype'
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
@@ -144,12 +144,23 @@
   where forward v = lookupSubst v mod_substs
         substs' = M.map forward substs
 
+extendAbsTypes :: Substitutions -> TransformM a -> TransformM a
+extendAbsTypes ascript_substs m = do
+  abs <- asks envAbs
+  -- Some abstract types may have a different name on the inside, and
+  -- we need to make them visible, because substitutions involving
+  -- abstract types must be lifted out in transformModBind.
+  let subst_abs = S.fromList $ map snd $ filter ((`S.member` abs) . fst) $
+                  M.toList ascript_substs
+  bindingAbs subst_abs m
+
 evalModExp :: ModExp -> TransformM Mod
 evalModExp (ModVar qn _) = lookupMod qn
 evalModExp (ModParens e _) = evalModExp e
 evalModExp (ModDecs decs _) = ModMod <$> transformDecs decs
 evalModExp (ModImport _ (Info fpath) _) = ModMod <$> lookupImport fpath
 evalModExp (ModAscript me _ (Info ascript_substs) _) =
+  extendAbsTypes ascript_substs $
   substituteInMod ascript_substs <$> evalModExp me
 evalModExp (ModApply f arg (Info p_substs) (Info b_substs) loc) = do
   f_mod <- evalModExp f
@@ -159,7 +170,7 @@
       fail $ "Cannot apply non-parametric module at " ++ locStr loc
     ModFun f_abs f_closure f_p f_body ->
       bindingAbs (f_abs <> S.fromList (unInfo (modParamAbs f_p))) $
-      extendScope f_closure $ generating $ do
+      extendAbsTypes b_substs $ extendScope f_closure $ generating $ do
         outer_substs <- scopeSubsts <$> askScope
         abs <- asks envAbs
         let forward (k,v) = (lookupSubst k outer_substs, v)
@@ -196,8 +207,6 @@
                         return $ qualLeaf $ fst $ lookupSubstInScope (qualName v) scope
                     , mapOnQualName = \v ->
                         return $ fst $ lookupSubstInScope v scope
-                    , mapOnType = astMap (substituter scope)
-                    , mapOnCompType = astMap (substituter scope)
                     , mapOnStructType = astMap (substituter scope)
                     , mapOnPatternType = astMap (substituter scope)
                     }
@@ -247,7 +256,12 @@
          (maybeAscript (srclocOf mb) (modSignature mb) $ modExp mb) $
          modParams mb
   mname <- transformName $ modName mb
-  return $ Scope mempty $ M.singleton mname mod
+  abs <- asks envAbs
+  -- Copy substitutions involving abstract types out, because they are
+  -- always resolved at the outermost level.
+  let abs_substs = M.filterWithKey (const . flip S.member abs) $
+                   scopeSubsts $ modScope mod
+  return $ Scope abs_substs $ M.singleton mname mod
 
 transformDecs :: [Dec] -> TransformM Scope
 transformDecs ds =
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
@@ -180,7 +180,7 @@
         transformField (RecordFieldImplicit v t _) = do
           t' <- traverse transformType t
           transformField $ RecordFieldExplicit (baseName v)
-            (Var (qualName v) (vacuousShapeAnnotations <$> t') loc) loc
+            (Var (qualName v) t' loc) loc
 
 transformExp (ArrayLit es tp loc) =
   ArrayLit <$> mapM transformExp es <*> pure tp <*> pure loc
@@ -197,7 +197,7 @@
     Just fs -> do
       let toField (f, (f_v, f_t)) = do
             f_t' <- transformType f_t
-            let f_v' = Var (qualName f_v) (Info $ vacuousShapeAnnotations f_t') loc
+            let f_v' = Var (qualName f_v) (Info f_t') loc
             return $ RecordFieldExplicit f f_v' loc
       RecordLit <$> mapM toField (M.toList fs) <*> pure loc
     Nothing -> do
@@ -205,13 +205,15 @@
       t' <- transformType t
       return $ Var (QualName qs fname') (Info t') loc
 
-transformExp (Ascript e tp loc) =
-  Ascript <$> transformExp e <*> pure tp <*> pure loc
+transformExp (Ascript e tp t loc) =
+  Ascript <$> transformExp e <*> pure tp <*> pure t <*> pure loc
 
-transformExp (LetPat tparams pat e1 e2 loc) = do
+transformExp (LetPat tparams pat e1 e2 (Info t) loc) = do
   (pat', rr) <- expandRecordPattern pat
+  t' <- transformType t
   LetPat tparams pat' <$> transformExp e1 <*>
-    withRecordReplacements rr (transformExp e2) <*> pure loc
+    withRecordReplacements rr (transformExp e2) <*>
+    pure (Info t') <*> pure loc
 
 transformExp (LetFun fname (tparams, params, retdecl, Info ret, body) e loc)
   | any isTypeParam tparams = do
@@ -226,9 +228,9 @@
         return (unfoldLetFuns (map snd $ toList bs_local) e', const bs_prop)
 
   | otherwise =
-      transformExp $ LetPat [] (Id fname (Info ft) loc) lam e loc
+      transformExp $ LetPat [] (Id fname (Info ft) loc) lam e (Info $ fromStruct ret) loc
         where lam = Lambda tparams params body Nothing (Info (mempty, ret)) loc
-              ft = foldFunType (map (vacuousShapeAnnotations . patternType) params) $ fromStruct ret
+              ft = foldFunType (map patternType params) $ fromStruct ret
 
 transformExp (If e1 e2 e3 tp loc) = do
   e1' <- transformExp e1
@@ -237,53 +239,11 @@
   tp' <- traverse transformType tp
   return $ If e1' e2' e3' tp' loc
 
-transformExp (Apply e1 e2 d tp loc) =
-  -- We handle on an ad-hoc basis certain polymorphic higher-order
-  -- intrinsics here.  They can only be used in very particular ways,
-  -- or the compiler will fail.  In practice they will only be used
-  -- once, in the basis library, to define normal functions.
-  case (e1, e2) of
-    (Var v _ _, TupLit [op, ne, arr] _)
-      | intrinsic "reduce" v ->
-          transformExp $ Reduce Noncommutative op ne arr loc
-      | intrinsic "reduce_comm" v ->
-          transformExp $ Reduce Commutative op ne arr loc
-      | intrinsic "scan" v ->
-          transformExp $ Scan op ne arr loc
-    (Var v _ _, TupLit [f, arr] _)
-      | intrinsic "map" v ->
-          transformExp $ Map f arr (removeShapeAnnotations <$> tp) loc
-      | intrinsic "filter" v ->
-          transformExp $ Filter f arr loc
-    (Var v _ _, TupLit [k, f, arr] _)
-      | intrinsic "partition" v,
-        Just k' <- isInt32 k ->
-          transformExp $ Partition (fromIntegral k') f arr loc
-    (Var v _ _, TupLit [op, f, arr] _)
-      | intrinsic "stream_red" v ->
-          transformExp $ Stream (RedLike InOrder Noncommutative op) f arr loc
-      | intrinsic "stream_red_per" v ->
-          transformExp $ Stream (RedLike Disorder Commutative op) f arr loc
-    (Var v _ _, TupLit [f, arr] _)
-      | intrinsic "stream_map" v ->
-          transformExp $ Stream (MapLike InOrder) f arr loc
-      | intrinsic "stream_map_per" v ->
-          transformExp $ Stream (MapLike Disorder) f arr loc
-    (Var v _ _, TupLit [dest, op, ne, buckets, img] _)
-      | intrinsic "gen_reduce" v ->
-          transformExp $ GenReduce dest op ne buckets img loc
-
-    _ -> do
-      e1' <- transformExp e1
-      e2' <- transformExp e2
-      tp' <- traverse transformType tp
-      return $ Apply e1' e2' d tp' loc
-  where intrinsic s (QualName _ v) =
-          baseTag v <= maxIntrinsicTag && baseName v == nameFromString s
-
-        isInt32 (Literal (SignedValue (Int32Value k)) _) = Just k
-        isInt32 (IntLit k (Info (Prim (Signed Int32))) _) = Just $ fromInteger k
-        isInt32 _ = Nothing
+transformExp (Apply e1 e2 d tp loc) = do
+  e1' <- transformExp e1
+  e2' <- transformExp e2
+  tp' <- traverse transformType tp
+  return $ Apply e1' e2' d tp' loc
 
 transformExp (Negate e loc) =
   Negate <$> transformExp e <*> pure loc
@@ -334,16 +294,17 @@
     _          -> return Nothing
   case maybe_fs of
     Just m | Just (v, _) <- M.lookup n m ->
-               return $ Var (qualName v) (vacuousShapeAnnotations <$> tp) loc
+               return $ Var (qualName v) tp loc
     _ -> do
       e' <- transformExp e
       return $ Project n e' tp loc
 
-transformExp (LetWith id1 id2 idxs e1 body loc) = do
+transformExp (LetWith id1 id2 idxs e1 body (Info t) loc) = do
   idxs' <- mapM transformDimIndex idxs
   e1' <- transformExp e1
   body' <- transformExp body
-  return $ LetWith id1 id2 idxs' e1' body' loc
+  t' <- transformType t
+  return $ LetWith id1 id2 idxs' e1' body' (Info t') loc
 
 transformExp (Index e0 idxs info loc) =
   Index <$> transformExp e0 <*> mapM transformDimIndex idxs <*> pure info <*> pure loc
@@ -356,37 +317,6 @@
   RecordUpdate <$> transformExp e1 <*> pure fs
                <*> transformExp e2 <*> pure t <*> pure loc
 
-transformExp (Map e1 es t loc) =
-  Map <$> transformExp e1 <*> transformExp es <*> pure t <*> pure loc
-
-transformExp (Reduce comm e1 e2 e3 loc) =
-  Reduce comm <$> transformExp e1 <*> transformExp e2
-              <*> transformExp e3 <*> pure loc
-
-transformExp (Scan e1 e2 e3 loc) =
-  Scan <$> transformExp e1 <*> transformExp e2 <*> transformExp e3 <*> pure loc
-
-transformExp (Filter e1 e2 loc) =
-  Filter <$> transformExp e1 <*> transformExp e2 <*> pure loc
-
-transformExp (Partition k f e0 loc) =
-  Partition k <$> transformExp f <*> transformExp e0 <*> pure loc
-
-transformExp (Stream form e1 e2 loc) = do
-  form' <- case form of
-             MapLike _         -> return form
-             RedLike so comm e -> RedLike so comm <$> transformExp e
-  Stream form' <$> transformExp e1 <*> transformExp e2 <*> pure loc
-
-transformExp (GenReduce e1 e2 e3 e4 e5 loc) =
-  GenReduce
-    <$> transformExp e1 -- hist
-    <*> transformExp e2 -- operator
-    <*> transformExp e3 -- neutral element
-    <*> transformExp e4 -- buckets
-    <*> transformExp e5 -- input image
-    <*> pure loc
-
 transformExp (Unsafe e1 loc) =
   Unsafe <$> transformExp e1 <*> pure loc
 
@@ -415,7 +345,7 @@
   (e1, p1) <- makeVarParam e_left $ fromStruct xtype
   (e2, p2) <- makeVarParam e_right $ fromStruct ytype
   let body = BinOp qn (Info t) (e1, Info xtype) (e2, Info ytype) (Info rettype) loc
-      rettype' = vacuousShapeAnnotations $ toStruct rettype
+      rettype' = toStruct rettype
   return $ Lambda [] (p1 ++ p2) body Nothing (Info (mempty, rettype')) loc
 
   where makeVarParam (Just e) _ = return (e, [])
@@ -440,9 +370,8 @@
 desugarIndexSection :: [DimIndex] -> PatternType -> SrcLoc -> MonoM Exp
 desugarIndexSection idxs (Arrow _ _ t1 t2) loc = do
   p <- newVName "index_i"
-  let body = Index (Var (qualName p) (Info t1) loc) idxs (Info t2') loc
+  let body = Index (Var (qualName p) (Info t1) loc) idxs (Info t2) loc
   return $ Lambda [] [Id p (Info t1) noLoc] body Nothing (Info (mempty, toStruct t2)) loc
-  where t2' = removeShapeAnnotations t2
 desugarIndexSection  _ t _ = error $ "desugarIndexSection: not a function type: " ++ pretty t
 
 noticeDims :: TypeBase (DimDecl VName) as -> MonoM ()
@@ -517,8 +446,6 @@
         mapper substs = ASTMapper { mapOnExp         = astMap $ mapper substs
                                   , mapOnName        = pure
                                   , mapOnQualName    = pure
-                                  , mapOnType        = pure . applySubst substs
-                                  , mapOnCompType    = pure . applySubst substs
                                   , mapOnStructType  = pure . applySubst substs
                                   , mapOnPatternType = pure . applySubst substs
                                   }
@@ -557,9 +484,9 @@
           | Just t1' <- peelArray (arrayRank t1) t1,
             Just t2' <- peelArray (arrayRank t1) t2 =
               sub pos t1' t2'
-        sub pos (Arrow _ _ t1a t1b) (Arrow _ _ t2a t2b) = do
+        sub _ (Arrow _ _ t1a t1b) (Arrow _ _ t2a t2b) = do
           sub False t1a t2a
-          sub pos t1b t2b
+          sub False t1b t2b
 
         sub _ t1 t2 = error $ unlines ["typeSubstsM: mismatched types:", pretty t1, pretty t2]
 
@@ -600,11 +527,6 @@
           mapOnExp         = astMap mapper
         , mapOnName        = pure
         , mapOnQualName    = pure
-        , mapOnType        = pure . removeShapeAnnotations .
-                             substituteTypes subs . vacuousShapeAnnotations
-        , mapOnCompType    = pure . removeShapeAnnotations .
-                             substituteTypes subs .
-                             vacuousShapeAnnotations
         , mapOnStructType  = pure . substituteTypes subs
         , mapOnPatternType = pure . substituteTypes subs
         }
@@ -616,7 +538,7 @@
                  , valBindBody    = body'
                  }
 
-removeTypeVariablesInType :: TypeBase dim () -> MonoM (TypeBase () ())
+removeTypeVariablesInType :: TypeBase () () -> MonoM (TypeBase () ())
 removeTypeVariablesInType t = do
   subs <- asks $ M.map TypeSub . envTypeBindings
   return $ removeShapeAnnotations $ substituteTypes subs $ vacuousShapeAnnotations t
diff --git a/src/Futhark/Internalise/TypesValues.hs b/src/Futhark/Internalise/TypesValues.hs
--- a/src/Futhark/Internalise/TypesValues.hs
+++ b/src/Futhark/Internalise/TypesValues.hs
@@ -139,7 +139,7 @@
 -- | How many core language values are needed to represent one source
 -- language value of the given type?
 internalisedTypeSize :: E.TypeBase dim () -> InternaliseM Int
-internalisedTypeSize = fmap length . internaliseType . E.removeShapeAnnotations
+internalisedTypeSize = fmap length . internaliseType . E.toStructural
 
 -- | Convert an external primitive to an internal primitive.
 internalisePrimType :: E.PrimType -> I.PrimType
diff --git a/src/Futhark/Optimise/CSE.hs b/src/Futhark/Optimise/CSE.hs
--- a/src/Futhark/Optimise/CSE.hs
+++ b/src/Futhark/Optimise/CSE.hs
@@ -177,6 +177,10 @@
   CSEState _ cse_arrays <- ask
   return $ runReader m $ newCSEState cse_arrays
 
+instance CSEInOp op => CSEInOp (Kernel.HostOp lore op) where
+  cseInOp (Kernel.HostOp op) = Kernel.HostOp <$> cseInOp op
+  cseInOp x = return x
+
 instance (Attributes lore, Aliased lore, CSEInOp (Op lore)) => CSEInOp (Kernel.Kernel lore) where
   cseInOp = subCSE .
             Kernel.mapKernelM
diff --git a/src/Futhark/Optimise/DoubleBuffer.hs b/src/Futhark/Optimise/DoubleBuffer.hs
--- a/src/Futhark/Optimise/DoubleBuffer.hs
+++ b/src/Futhark/Optimise/DoubleBuffer.hs
@@ -60,10 +60,10 @@
   in (fundec { funDefBody = body' }, src')
   where env = Env mempty optimiseKernelOp doNotTouchLoop
 
-        optimiseKernelOp (Inner k) = do
+        optimiseKernelOp (Inner (HostOp k)) = do
           scope <- castScope <$> askScope
           modifyNameSource $
-            runState (runReaderT (runDoubleBufferM $ Inner <$> optimiseKernel k) $
+            runState (runReaderT (runDoubleBufferM $ Inner . HostOp <$> optimiseKernel k) $
                       Env scope optimiseInKernelOp optimiseLoop)
           where optimiseKernel =
                   mapKernelM identityKernelMapper
diff --git a/src/Futhark/Optimise/InPlaceLowering.hs b/src/Futhark/Optimise/InPlaceLowering.hs
--- a/src/Futhark/Optimise/InPlaceLowering.hs
+++ b/src/Futhark/Optimise/InPlaceLowering.hs
@@ -156,13 +156,13 @@
   where optimise = identityMapper { mapOnBody = const optimiseBody
                                   }
 onKernelOp :: OnOp Kernels
-onKernelOp (Kernel debug kspace ts kbody) = do
+onKernelOp (HostOp (Kernel debug kspace ts kbody)) = do
   old_scope <- askScope
   modifyNameSource $ runForwardingM lowerUpdateInKernel onKernelExp $
     bindingScope (castScope old_scope <> scopeOfKernelSpace kspace) $ do
     stms <- deepen $ optimiseStms (stmsToList (kernelBodyStms kbody)) $
             mapM_ seenVar $ freeIn $ kernelBodyResult kbody
-    return $ Kernel debug kspace ts $ kbody { kernelBodyStms = stmsFromList stms }
+    return $ HostOp $ Kernel debug kspace ts $ kbody { kernelBodyStms = stmsFromList stms }
 onKernelOp op = return op
 
 onKernelExp :: OnOp InKernel
diff --git a/src/Futhark/Optimise/InPlaceLowering/LowerIntoStm.hs b/src/Futhark/Optimise/InPlaceLowering/LowerIntoStm.hs
--- a/src/Futhark/Optimise/InPlaceLowering/LowerIntoStm.hs
+++ b/src/Futhark/Optimise/InPlaceLowering/LowerIntoStm.hs
@@ -65,14 +65,14 @@
 
 lowerUpdateKernels :: MonadFreshNames m => LowerUpdate Kernels m
 lowerUpdateKernels
-  (Let (Pattern [] [PatElem v v_attr]) aux (Op (Kernel debug kspace ts kbody)))
+  (Let (Pattern [] [PatElem v v_attr]) aux (Op (HostOp (Kernel debug kspace ts kbody))))
   [update@(DesiredUpdate bindee_nm bindee_attr cs _src is val)]
   | v == val = do
     kbody' <- lowerUpdateIntoKernel update kspace kbody
     let is' = fullSlice (typeOf bindee_attr) is
     Just $ return [certify (stmAuxCerts aux <> cs) $
                     mkLet [] [Ident bindee_nm $ typeOf bindee_attr] $
-                    Op $ Kernel debug kspace ts kbody',
+                    Op $ HostOp $ Kernel debug kspace ts kbody',
                    mkLet [] [Ident v $ typeOf v_attr] $ BasicOp $ Index bindee_nm is']
 lowerUpdateKernels stm updates = lowerUpdate stm updates
 
diff --git a/src/Futhark/Optimise/TileLoops.hs b/src/Futhark/Optimise/TileLoops.hs
--- a/src/Futhark/Optimise/TileLoops.hs
+++ b/src/Futhark/Optimise/TileLoops.hs
@@ -40,7 +40,7 @@
   Body () <$> (mconcat <$> mapM optimiseStm (stmsToList bnds)) <*> pure res
 
 optimiseStm :: Stm Kernels -> TileM (Stms Kernels)
-optimiseStm stmt@(Let pat aux (Op old_kernel@(Kernel desc space ts body))) = do
+optimiseStm stmt@(Let pat aux (Op (HostOp old_kernel@(Kernel desc space ts body)))) = do
   res3dtiling <- doRegTiling3D stmt
   case res3dtiling of
     Just (extra_bnds, stmt') -> return $ extra_bnds <> oneStm stmt'
@@ -51,8 +51,8 @@
           -- changing the number of groups being used for a kernel that
           -- returns a result-per-group).
           if kernelType old_kernel == kernelType new_kernel
-            then return $ extra_bnds <> oneStm (Let pat aux $ Op new_kernel)
-            else return $ oneStm $ Let pat aux $ Op old_kernel
+            then return $ extra_bnds <> oneStm (Let pat aux $ Op $ HostOp new_kernel)
+            else return $ oneStm $ Let pat aux $ Op $ HostOp old_kernel
   where initial_variance = M.map mempty $ scopeOfKernelSpace space
 optimiseStm (Let pat aux e) =
   pure <$> (Let pat aux <$> mapExpM optimise e)
diff --git a/src/Futhark/Optimise/TileLoops/RegTiling3D.hs b/src/Futhark/Optimise/TileLoops/RegTiling3D.hs
--- a/src/Futhark/Optimise/TileLoops/RegTiling3D.hs
+++ b/src/Futhark/Optimise/TileLoops/RegTiling3D.hs
@@ -102,7 +102,7 @@
 --     }
 --
 doRegTiling3D :: Stm Kernels -> TileM (Maybe (Stms Kernels, Stm Kernels))
-doRegTiling3D (Let pat aux (Op old_kernel))
+doRegTiling3D (Let pat aux (Op (HostOp old_kernel)))
   | Kernel kerhint space kertp (KernelBody () kstms kres) <- old_kernel,
     FlatThreadSpace gspace <- spaceStructure space,
     initial_variance <- M.map mempty $ scopeOfKernelSpace space,
@@ -211,7 +211,7 @@
       -- finally, put everything together
           kstms' = stmsFromList $ mask_stm : mm_stmt : stm_loop : (code2_inv ++ unrolled_code)
           ker_body = KernelBody () kstms' kres'
-          new_ker = Op $ Kernel kerhint kspace' kertp' ker_body
+          new_ker = Op $ HostOp $ Kernel kerhint kspace' kertp' ker_body
           extra_stms = space_stms <> stmsFromList (scratch_stms ++ manif_stms)
       return $ Just (extra_stms, Let pat aux new_ker)
 
diff --git a/src/Futhark/Optimise/Unstream.hs b/src/Futhark/Optimise/Unstream.hs
--- a/src/Futhark/Optimise/Unstream.hs
+++ b/src/Futhark/Optimise/Unstream.hs
@@ -39,11 +39,12 @@
   Body () <$> (stmsFromList . concat <$> mapM optimiseStm (stmsToList stms)) <*> pure res
 
 optimiseStm :: Stm Kernels -> UnstreamM [Stm Kernels]
-optimiseStm (Let pat aux (Op (Kernel desc space ts body))) = do
+optimiseStm (Let pat aux (Op (HostOp (Kernel desc space ts body)))) = do
   inv <- S.fromList . M.keys <$> askScope
   stms' <- localScope (scopeOfKernelSpace space) $
            runBinder_ $ optimiseInKernelStms inv $ kernelBodyStms body
-  return [Let pat aux $ Op $ Kernel desc space ts $ body { kernelBodyStms = stms' }]
+  return [Let pat aux $ Op $ HostOp $
+          Kernel desc space ts $ body { kernelBodyStms = stms' }]
 optimiseStm (Let pat aux e) =
   pure <$> (Let pat aux <$> mapExpM optimise e)
   where optimise = identityMapper { mapOnBody = \scope -> localScope scope . optimiseBody }
diff --git a/src/Futhark/Pass/ExpandAllocations.hs b/src/Futhark/Pass/ExpandAllocations.hs
--- a/src/Futhark/Pass/ExpandAllocations.hs
+++ b/src/Futhark/Pass/ExpandAllocations.hs
@@ -72,7 +72,7 @@
 
 transformExp :: Exp ExplicitMemory -> ExpandM (Stms ExplicitMemory, Exp ExplicitMemory)
 
-transformExp (Op (Inner (Kernel desc kspace ts kbody))) = do
+transformExp (Op (Inner (HostOp (Kernel desc kspace ts kbody)))) = do
   let (kbody', allocs) = extractKernelBodyAllocations kbody
       variantAlloc (Var v) = v `S.member` bound_in_kernel
       variantAlloc _ = False
@@ -87,13 +87,13 @@
              runOffsetM scope' alloc_offsets $ offsetMemoryInKernelBody kbody'
 
   return (alloc_stms,
-          Op $ Inner $ Kernel desc kspace ts kbody'')
+          Op $ Inner $ HostOp $ Kernel desc kspace ts kbody'')
 
   where bound_in_kernel =
           S.fromList $ M.keys $ scopeOfKernelSpace kspace <>
           scopeOf (kernelBodyStms kbody)
 
-transformExp (Op (Inner (SegRed kspace comm red_op nes ts kbody))) = do
+transformExp (Op (Inner (HostOp (SegRed kspace comm red_op nes ts kbody)))) = do
   let (kbody', kbody_allocs) = extractBodyAllocations kbody
       (red_op', red_op_allocs) = extractLambdaAllocations red_op
       variantAlloc (Var v) = v `S.member` bound_in_kernel
@@ -111,14 +111,14 @@
     red_op'' <- localScope (scopeOf red_op') $ offsetMemoryInLambda red_op'
 
     return (alloc_stms,
-            Op $ Inner $ SegRed kspace comm red_op'' nes ts kbody'')
+            Op $ Inner $ HostOp $ SegRed kspace comm red_op'' nes ts kbody'')
 
   where bound_in_kernel =
           S.fromList $ map fst (spaceDimensions kspace) ++
           M.keys (scopeOfKernelSpace kspace <>
                   scopeOf (bodyStms kbody))
 
-transformExp (Op (Inner (SegGenRed kspace ops ts kbody))) = do
+transformExp (Op (Inner (HostOp (SegGenRed kspace ops ts kbody)))) = do
   let (kbody', kbody_allocs) = extractBodyAllocations kbody
       (ops', ops_allocs) = unzip $ map extractGenRedOpAllocations ops
       variantAlloc (Var v) = v `S.member` bound_in_kernel
@@ -130,7 +130,7 @@
     ops'' <- mapM offsetMemoryInGenRedOp ops'
 
     return (alloc_stms,
-            Op $ Inner $ SegGenRed kspace ops'' ts kbody'')
+            Op $ Inner $ HostOp $ SegGenRed kspace ops'' ts kbody'')
 
   where bound_in_kernel =
           S.fromList $ map fst (spaceDimensions kspace) ++
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
@@ -503,7 +503,7 @@
                              Stms Kernels -> m (Stms ExplicitMemory)
 explicitAllocationsInStms stms = do
   scope <- askScope
-  runAllocM handleKernel $ localScope scope $ allocInStms stms return
+  runAllocM handleHostOp $ localScope scope $ allocInStms stms return
 
 memoryInRetType :: [RetType Kernels] -> [RetType ExplicitMemory]
 memoryInRetType ts = evalState (mapM addAttr ts) $ startOfFreeIDRange ts
@@ -522,35 +522,35 @@
 
 allocInFun :: MonadFreshNames m => FunDef Kernels -> m (FunDef ExplicitMemory)
 allocInFun (FunDef entry fname rettype params fbody) =
-  runAllocM handleKernel $
+  runAllocM handleHostOp $
   allocInFParams (zip params $ repeat DefaultSpace) $ \params' -> do
     fbody' <- insertStmsM $ allocInFunBody
               (map (const $ Just DefaultSpace) rettype) fbody
     return $ FunDef entry fname (memoryInRetType rettype) params' fbody'
 
-handleKernel :: Kernel InInKernel
-             -> AllocM Kernels ExplicitMemory (MemOp (Kernel OutInKernel))
-handleKernel (GetSize key size_class) =
+handleHostOp :: HostOp Kernels (Kernel InInKernel)
+             -> AllocM Kernels ExplicitMemory (MemOp (HostOp ExplicitMemory (Kernel OutInKernel)))
+handleHostOp (GetSize key size_class) =
   return $ Inner $ GetSize key size_class
-handleKernel (GetSizeMax size_class) =
+handleHostOp (GetSizeMax size_class) =
   return $ Inner $ GetSizeMax size_class
-handleKernel (CmpSizeLe key size_class x) =
+handleHostOp (CmpSizeLe key size_class x) =
   return $ Inner $ CmpSizeLe key size_class x
-handleKernel (Kernel desc space kernel_ts kbody) = subInKernel $
-  Inner . Kernel desc space kernel_ts <$>
+handleHostOp (HostOp (Kernel desc space kernel_ts kbody)) = subInKernel $
+  Inner . HostOp . Kernel desc space kernel_ts <$>
   localScope (scopeOfKernelSpace space) (allocInKernelBody kbody)
 
-handleKernel (SegRed space comm red_op nes ts body) = do
+handleHostOp (HostOp (SegRed space comm red_op nes ts body)) = do
   body' <- subInKernel $ localScope (scopeOfKernelSpace space) $ allocInBodyNoDirect body
   red_op' <- allocInSegRedLambda (spaceGlobalId space) (spaceNumThreads space) red_op
-  return $ Inner $ SegRed space comm red_op' nes ts body'
+  return $ Inner $ HostOp $ SegRed space comm red_op' nes ts body'
 
-handleKernel (SegGenRed space ops ts body) = do
+handleHostOp (HostOp (SegGenRed space ops ts body)) = do
   body' <- subInKernel $ localScope (scopeOfKernelSpace space) $ allocInBodyNoDirect body
   ops' <- forM ops $ \op -> do
     lam <- allocInSegRedLambda (spaceGlobalId space) (spaceNumThreads space) $ genReduceOp op
     return op { genReduceOp = lam }
-  return $ Inner $ SegGenRed space ops' ts body'
+  return $ Inner $ HostOp $ SegGenRed space ops' ts body'
 
 subInKernel :: AllocM InInKernel OutInKernel a
             -> AllocM fromlore2 ExplicitMemory a
@@ -873,6 +873,10 @@
 class SizeSubst op where
   opSizeSubst :: PatternT attr -> op -> ChunkMap
 
+instance SizeSubst op => SizeSubst (HostOp lore op) where
+  opSizeSubst pat (HostOp op) = opSizeSubst pat op
+  opSizeSubst _ _ = mempty
+
 instance SizeSubst (Kernel lore) where
   opSizeSubst _ _ = mempty
 
@@ -1010,7 +1014,7 @@
 data ExpHint = NoHint
              | Hint IxFun Space
 
-kernelExpHints :: (Allocator lore m, Op lore ~ MemOp (Kernel somelore)) =>
+kernelExpHints :: (Allocator lore m, Op lore ~ MemOp (HostOp lore (Kernel somelore))) =>
                   Exp lore -> m [ExpHint]
 kernelExpHints (BasicOp (Manifest perm v)) = do
   dims <- arrayDims <$> lookupType v
@@ -1020,7 +1024,7 @@
               perm_inv
   return [Hint ixfun DefaultSpace]
 
-kernelExpHints (Op (Inner (Kernel _ space rets kbody))) =
+kernelExpHints (Op (Inner (HostOp (Kernel _ space rets kbody)))) =
   zipWithM hint rets $ kernelBodyResult kbody
   where num_threads = spaceNumThreads space
 
@@ -1053,7 +1057,7 @@
 
         hint _ _ = return NoHint
 
-kernelExpHints (Op (Inner (SegRed space _ _ nes ts body))) =
+kernelExpHints (Op (Inner (HostOp (SegRed space _ _ nes ts body)))) =
   (map (const NoHint) red_res <>) <$> zipWithM mapHint (drop (length nes) ts) map_res
   where (red_res, map_res) = splitAt (length nes) $ bodyResult body
 
diff --git a/src/Futhark/Pass/ExtractKernels.hs b/src/Futhark/Pass/ExtractKernels.hs
--- a/src/Futhark/Pass/ExtractKernels.hs
+++ b/src/Futhark/Pass/ExtractKernels.hs
@@ -461,7 +461,7 @@
     mapKernel w (FlatThreadSpace [(write_i,w)]) inputs (map rowType $ patternTypes pat) body
   certifying cs $ do
     addStms bnds
-    letBind_ pat $ Op kernel
+    letBind_ pat $ Op $ HostOp kernel
 
 transformStm _ (Let orig_pat (StmAux cs _) (Op (GenReduce w ops bucket_fun imgs))) = do
   bfun' <- Kernelise.transformLambda bucket_fun
@@ -1268,7 +1268,7 @@
     let pat = Pattern [] $ rearrangeShape perm $
               patternValueElements $ loopNestingPattern $ fst nest
 
-    certifying cs $ letBind_ pat $ Op k
+    certifying cs $ letBind_ pat $ Op $ HostOp k
   where findInput kernel_inps a =
           maybe bad return $ find ((==a) . kernelInputName) kernel_inps
         bad = fail "Ill-typed nested scatter encountered."
diff --git a/src/Futhark/Pass/ExtractKernels/BlockedKernel.hs b/src/Futhark/Pass/ExtractKernels/BlockedKernel.hs
--- a/src/Futhark/Pass/ExtractKernels/BlockedKernel.hs
+++ b/src/Futhark/Pass/ExtractKernels/BlockedKernel.hs
@@ -46,7 +46,7 @@
 import Futhark.Util
 import Futhark.Util.IntegralExp
 
-getSize :: (MonadBinder m, Op (Lore m) ~ Kernel innerlore) =>
+getSize :: (MonadBinder m, Op (Lore m) ~ HostOp (Lore m) inner) =>
            String -> SizeClass -> m SubExp
 getSize desc size_class = do
   size_key <- nameFromString . pretty <$> newVName desc
@@ -95,7 +95,7 @@
 
   step_one <- chunkedReduceKernel w step_one_size comm reduce_lam' fold_lam'
               ispace nes arrs_copies
-  addStm =<< renameStm (Let step_one_pat (defAux ()) $ Op step_one)
+  addStm =<< renameStm (Let step_one_pat (defAux ()) $ Op $ HostOp step_one)
 
   step_two_pat <- basicPattern [] <$>
                   mapM (mkIntermediateIdent $ constant (1 :: Int32)) acc_idents
@@ -104,7 +104,7 @@
 
   step_two <- reduceKernel step_two_size reduce_lam' nes $ take (length nes) $ patternNames step_one_pat
 
-  addStm $ Let step_two_pat (defAux ()) $ Op step_two
+  addStm $ Let step_two_pat (defAux ()) $ Op $ HostOp step_two
 
   forM_ (zip (patternIdents step_two_pat) (patternIdents pat)) $ \(arr, x) ->
     addStm $ mkLet [] [x] $ BasicOp $ Index (identName arr) $
@@ -308,7 +308,7 @@
         BasicOp $ Index arr $ fullSlice arr_t [DimFix $ Var gtid]
     return $ lambdaBody map_lam
 
-  letBind_ pat $ Op $
+  letBind_ pat $ Op $ HostOp $
     SegRed kspace comm reduce_lam nes (lambdaReturnType map_lam) body
 
 nonSegRed :: (MonadFreshNames m, HasScope Kernels m) =>
@@ -385,7 +385,7 @@
         BasicOp $ Index arr $ fullSlice arr_t [DimFix $ Var gtid]
     return $ lambdaBody lam
 
-  letBind_ pat $ Op $ SegGenRed kspace ops (lambdaReturnType lam) body
+  letBind_ pat $ Op $ HostOp $ SegGenRed kspace ops (lambdaReturnType lam) body
 
 blockedMap :: (MonadFreshNames m, HasScope Kernels m) =>
               Pattern Kernels -> SubExp
@@ -421,7 +421,7 @@
   concat_rets <- forM chunk_map_pes $ \pe ->
     return $ ConcatReturns ordering' w elems_per_thread Nothing $ patElemName pe
 
-  return $ Let pat (defAux ()) $ Op $ Kernel (KernelDebugHints "chunked_map" []) space ts $
+  return $ Let pat (defAux ()) $ Op $ HostOp $ Kernel (KernelDebugHints "chunked_map" []) space ts $
     KernelBody () chunk_and_fold $ nonconcat_rets ++ concat_rets
 
 blockedPerThread :: (MonadBinder m, Lore m ~ InKernel) =>
@@ -835,7 +835,7 @@
               mapM (mkIntermediateIdent "red_carry_out" [num_groups]) red_idents,
               pure arr_idents]
 
-  addStm . Let first_scan_pat (defAux ()) . Op =<< scanKernel1 w first_scan_size
+  addStm . Let first_scan_pat (defAux ()) . Op . HostOp =<< scanKernel1 w first_scan_size
     (first_scan_lam, scan_nes)
     (comm, first_scan_red_lam, red_nes)
     first_scan_foldlam arrs
@@ -846,7 +846,7 @@
   let second_scan_size = KernelSize one num_groups one num_groups num_groups
   unless (null group_red_res) $ do
     second_stage_red_lam <- renameLambda first_scan_red_lam
-    red_res <- letTupExp "red_res" . Op =<<
+    red_res <- letTupExp "red_res" . Op . HostOp =<<
                reduceKernel second_scan_size second_stage_red_lam red_nes group_red_res
     forM_ (zip red_idents red_res) $ \(dest, arr) -> do
       arr_t <- lookupType arr
@@ -856,7 +856,7 @@
   second_scan_lam <- renameLambda first_scan_lam
 
   group_carry_out_scanned <-
-    letTupExp "group_carry_out_scanned" . Op =<<
+    letTupExp "group_carry_out_scanned" . Op . HostOp =<<
     scanKernel2 second_scan_size
     second_scan_lam (zip scan_nes group_carry_out)
 
@@ -902,7 +902,7 @@
   (mapk_bnds, mapk) <- mapKernelFromBody w (FlatThreadSpace [(j, w)]) result_map_input
                        (lambdaReturnType scan_lam) result_map_body
   addStms mapk_bnds
-  letBind_ final_res_pat $ Op mapk
+  letBind_ final_res_pat $ Op $ HostOp mapk
 
   return carries
   where one = constant (1 :: Int32)
@@ -936,7 +936,7 @@
 
 -- Given the desired minium number of threads, compute the group size,
 -- number of groups and total number of threads.
-numThreadsAndGroups :: (MonadBinder m, Op (Lore m) ~ Kernel innerlore) =>
+numThreadsAndGroups :: (MonadBinder m, Op (Lore m) ~ HostOp (Lore m) inner) =>
                        SubExp -> m (SubExp, SubExp, SubExp)
 numThreadsAndGroups w = do
   group_size <- getSize "group_size" SizeGroup
diff --git a/src/Futhark/Pass/ExtractKernels/Distribution.hs b/src/Futhark/Pass/ExtractKernels/Distribution.hs
--- a/src/Futhark/Pass/ExtractKernels/Distribution.hs
+++ b/src/Futhark/Pass/ExtractKernels/Distribution.hs
@@ -253,7 +253,7 @@
   let kbnds = w_bnds <> ksize_bnds
   return (kbnds,
           w,
-          Let (loopNestingPattern first_nest) (StmAux cs ()) $ Op k)
+          Let (loopNestingPattern first_nest) (StmAux cs ()) $ Op $ HostOp k)
   where
     first_nest = fst kernel_nest
     inputIsUsed input = kernelInputName input `S.member`
diff --git a/src/Futhark/Pass/ExtractKernels/Intragroup.hs b/src/Futhark/Pass/ExtractKernels/Intragroup.hs
--- a/src/Futhark/Pass/ExtractKernels/Intragroup.hs
+++ b/src/Futhark/Pass/ExtractKernels/Intragroup.hs
@@ -103,7 +103,7 @@
         return $ PatElem name t'
   flat_pat <- lift $ Pattern [] <$> mapM flatPatElem (patternValueElements nested_pat)
 
-  let kstm = Let flat_pat (StmAux cs ()) $ Op $
+  let kstm = Let flat_pat (StmAux cs ()) $ Op $ HostOp $
              Kernel (KernelDebugHints "map_intra_group" []) kspace rts kbody'
       reshapeStm nested_pe flat_pe =
         Let (Pattern [] [nested_pe]) (StmAux cs ()) $
diff --git a/src/Futhark/Pass/ExtractKernels/Segmented.hs b/src/Futhark/Pass/ExtractKernels/Segmented.hs
--- a/src/Futhark/Pass/ExtractKernels/Segmented.hs
+++ b/src/Futhark/Pass/ExtractKernels/Segmented.hs
@@ -69,7 +69,7 @@
       return $ resultBody [flag]
   (mapk_bnds, mapk) <- mapKernelFromBody w (FlatThreadSpace [(flags_i, w)]) [] [Prim Bool] flags_body
   addStms mapk_bnds
-  flags <- letExp "flags" $ Op mapk
+  flags <- letExp "flags" $ Op $ HostOp mapk
 
   lam' <- addFlagToLambda nes lam
 
diff --git a/src/Futhark/Pass/KernelBabysitting.hs b/src/Futhark/Pass/KernelBabysitting.hs
--- a/src/Futhark/Pass/KernelBabysitting.hs
+++ b/src/Futhark/Pass/KernelBabysitting.hs
@@ -56,7 +56,7 @@
     Just (Let _ _ (BasicOp (Rearrange perm _))) -> Just $ Just $ rearrangeInverse perm
     Just (Let _ _ (BasicOp (Reshape _ arr))) -> nonlinearInMemory arr m
     Just (Let _ _ (BasicOp (Manifest perm _))) -> Just $ Just perm
-    Just (Let pat _ (Op (Kernel _ _ ts _))) ->
+    Just (Let pat _ (Op (HostOp (Kernel _ _ ts _)))) ->
       nonlinear =<< find ((==name) . patElemName . fst)
       (zip (patternElements pat) ts)
     _ -> Nothing
@@ -68,7 +68,7 @@
 
 transformStm :: ExpMap -> Stm Kernels -> BabysitM ExpMap
 
-transformStm expmap (Let pat aux ke@(Op (Kernel desc space ts kbody))) = do
+transformStm expmap (Let pat aux ke@(Op (HostOp (Kernel desc space ts kbody)))) = do
   -- Go spelunking for accesses to arrays that are defined outside the
   -- kernel body and where the indices are kernel thread indices.
   scope <- askScope
@@ -83,7 +83,7 @@
                          kbody)
              mempty
 
-  let bnd' = Let pat aux $ Op $ Kernel desc space ts kbody''
+  let bnd' = Let pat aux $ Op $ HostOp $ Kernel desc space ts kbody''
   addStm bnd'
   return $ M.fromList [ (name, bnd') | name <- patternNames pat ] <> expmap
   where num_threads = spaceNumThreads space
diff --git a/src/Futhark/Representation/AST/Attributes/Aliases.hs b/src/Futhark/Representation/AST/Attributes/Aliases.hs
--- a/src/Futhark/Representation/AST/Attributes/Aliases.hs
+++ b/src/Futhark/Representation/AST/Attributes/Aliases.hs
@@ -102,7 +102,7 @@
   funcallAliases args $ retTypeValues t
 expAliases (Op op) = opAliases op
 
-returnAliases :: [TypeBase shaper Uniqueness] -> [(Names, Diet)] -> [Names]
+returnAliases :: [TypeBase shape Uniqueness] -> [(Names, Diet)] -> [Names]
 returnAliases rts args = map returnType' rts
   where returnType' (Array _ _ Nonunique) =
           mconcat $ map (uncurry maskAliases) args
@@ -115,6 +115,7 @@
 
 maskAliases :: Names -> Diet -> Names
 maskAliases _   Consume = mempty
+maskAliases _   ObservePrim = mempty
 maskAliases als Observe = als
 
 consumedInStm :: Aliased lore => Stm lore -> Names
@@ -124,7 +125,7 @@
 consumedInExp (Apply _ args _ _) =
   mconcat (map (consumeArg . first subExpAliases) args)
   where consumeArg (als, Consume) = als
-        consumeArg (_,   Observe) = mempty
+        consumeArg _              = mempty
 consumedInExp (If _ tb fb _) =
   consumedInBody tb <> consumedInBody fb
 consumedInExp (DoLoop _ merge _ _) =
diff --git a/src/Futhark/Representation/AST/Attributes/Types.hs b/src/Futhark/Representation/AST/Attributes/Types.hs
--- a/src/Futhark/Representation/AST/Attributes/Types.hs
+++ b/src/Futhark/Representation/AST/Attributes/Types.hs
@@ -301,7 +301,7 @@
 -- | @diet t@ returns a description of how a function parameter of
 -- type @t@ might consume its argument.
 diet :: TypeBase shape Uniqueness -> Diet
-diet (Prim _) = Observe
+diet (Prim _) = ObservePrim
 diet (Array _ _ Unique) = Consume
 diet (Array _ _ Nonunique) = Observe
 diet Mem{} = Observe
diff --git a/src/Futhark/Representation/AST/Pretty.hs b/src/Futhark/Representation/AST/Pretty.hs
--- a/src/Futhark/Representation/AST/Pretty.hs
+++ b/src/Futhark/Representation/AST/Pretty.hs
@@ -225,7 +225,7 @@
   ppr (Apply fname args _ (safety, _, _)) =
     text (nameToString fname) <> safety' <> apply (map (align . pprArg) args)
     where pprArg (arg, Consume) = text "*" <> ppr arg
-          pprArg (arg, Observe) = ppr arg
+          pprArg (arg, _)       = ppr arg
           safety' = case safety of Unsafe -> text "<unsafe>"
                                    Safe   -> mempty
   ppr (Op op) = ppr op
diff --git a/src/Futhark/Representation/AST/Syntax/Core.hs b/src/Futhark/Representation/AST/Syntax/Core.hs
--- a/src/Futhark/Representation/AST/Syntax/Core.hs
+++ b/src/Futhark/Representation/AST/Syntax/Core.hs
@@ -191,7 +191,10 @@
 -- Observe]@.
 data Diet = Consume -- ^ Consumes this value.
           | Observe -- ^ Only observes value in this position, does
-                    -- not consume.
+                    -- not consume.  A result may alias this.
+          | ObservePrim -- ^ As 'Observe', but the result will not
+                        -- alias, because the parameter does not carry
+                        -- aliases.
             deriving (Eq, Ord, Show)
 
 -- | An identifier consists of its name and the type of the value
diff --git a/src/Futhark/Representation/AST/Traversals.hs b/src/Futhark/Representation/AST/Traversals.hs
--- a/src/Futhark/Representation/AST/Traversals.hs
+++ b/src/Futhark/Representation/AST/Traversals.hs
@@ -1,4 +1,3 @@
------------------------------------------------------------------------------
 -- |
 --
 -- Functions for generic traversals across Futhark syntax trees.  The
@@ -16,14 +15,12 @@
 -- tree.  The implementation is rather tedious, but the interface is
 -- easy to use.
 --
--- A traversal of the Futhark syntax tree is expressed as a tuple of
+-- A traversal of the Futhark syntax tree is expressed as a record of
 -- functions expressing the operations to be performed on the various
 -- types of nodes.
 --
--- The "Futhark.Transform.Rename" is a simple example of how to use
--- this facility.
---
------------------------------------------------------------------------------
+-- The "Futhark.Transform.Rename" module is a simple example of how to
+-- use this facility.
 module Futhark.Representation.AST.Traversals
   (
   -- * Mapping
diff --git a/src/Futhark/Representation/ExplicitMemory.hs b/src/Futhark/Representation/ExplicitMemory.hs
--- a/src/Futhark/Representation/ExplicitMemory.hs
+++ b/src/Futhark/Representation/ExplicitMemory.hs
@@ -231,7 +231,7 @@
   type LParamAttr ExplicitMemory = MemInfo SubExp NoUniqueness MemBind
   type RetType    ExplicitMemory = FunReturns
   type BranchType ExplicitMemory = BodyReturns
-  type Op         ExplicitMemory = MemOp (Kernel InKernel)
+  type Op         ExplicitMemory = MemOp (HostOp ExplicitMemory (Kernel InKernel))
 
 instance Annotations InKernel where
   type LetAttr    InKernel = MemInfo SubExp NoUniqueness MemBind
@@ -505,7 +505,7 @@
 
 instance TC.CheckableOp ExplicitMemory where
   checkOp (Alloc size _) = TC.require [Prim int64] size
-  checkOp (Inner k) = TC.subCheck $ typeCheckKernel k
+  checkOp (Inner op) = typeCheckHostOp (TC.subCheck . typeCheckKernel) op
 
 instance TC.CheckableOp InKernel where
   checkOp (Alloc size _) = TC.require [Prim int64] size
@@ -1010,14 +1010,14 @@
 instance OpReturns ExplicitMemory where
   opReturns (Alloc size space) =
     return [MemMem (Free size) space]
-  opReturns (Inner k@(Kernel _ _ _ body)) =
+  opReturns (Inner (HostOp k@(Kernel _ _ _ body))) =
     zipWithM correct (kernelBodyResult body) =<< (extReturns <$> opType k)
     where correct (WriteReturn _ arr _) _ = varReturns arr
           correct (KernelInPlaceReturn arr) _ =
             extendedScope (varReturns arr)
             (castScope $ scopeOf $ kernelBodyStms body)
           correct _ ret = return ret
-  opReturns (Inner (SegGenRed _ ops _ _)) =
+  opReturns (Inner (HostOp (SegGenRed _ ops _ _))) =
     concat <$> mapM (mapM varReturns . genReduceDest) ops
   opReturns k =
     extReturns <$> opType k
diff --git a/src/Futhark/Representation/Kernels.hs b/src/Futhark/Representation/Kernels.hs
--- a/src/Futhark/Representation/Kernels.hs
+++ b/src/Futhark/Representation/Kernels.hs
@@ -34,7 +34,7 @@
 data Kernels
 
 instance Annotations Kernels where
-  type Op Kernels = Kernel InKernel
+  type Op Kernels = HostOp Kernels (Kernel InKernel)
 instance Attributes Kernels where
   expTypesFromPattern = return . expExtTypesFromPattern
 
@@ -46,7 +46,7 @@
 instance PrettyLore InKernel where
 
 instance TypeCheck.CheckableOp Kernels where
-  checkOp = TypeCheck.subCheck . typeCheckKernel
+  checkOp = typeCheckHostOp $ TypeCheck.subCheck . typeCheckKernel
 
 instance TypeCheck.CheckableOp InKernel where
   checkOp = TypeCheck.subCheck . typeCheckKernelExp
diff --git a/src/Futhark/Representation/Kernels/Kernel.hs b/src/Futhark/Representation/Kernels/Kernel.hs
--- a/src/Futhark/Representation/Kernels/Kernel.hs
+++ b/src/Futhark/Representation/Kernels/Kernel.hs
@@ -33,6 +33,10 @@
        , KernelWalker(..)
        , identityKernelWalker
        , walkKernelM
+
+       -- * Host operations
+       , HostOp(..)
+       , typeCheckHostOp
        )
        where
 
@@ -95,12 +99,8 @@
               }
   deriving (Eq, Ord, Show)
 
-data Kernel lore =
-    GetSize Name SizeClass -- ^ Produce some runtime-configurable size.
-  | GetSizeMax SizeClass -- ^ The maximum size of some class.
-  | CmpSizeLe Name SizeClass SubExp
-    -- ^ Compare size (likely a threshold) with some Int32 value.
-  | Kernel KernelDebugHints KernelSpace [Type] (KernelBody lore)
+data Kernel lore
+  = Kernel KernelDebugHints KernelSpace [Type] (KernelBody lore)
   | SegRed KernelSpace Commutativity (Lambda lore) [SubExp] [Type] (Body lore)
     -- ^ The KernelSpace must always have at least two dimensions,
     -- implying that the result of a SegRed is always an array.
@@ -203,12 +203,6 @@
 -- and is done left-to-right.
 mapKernelM :: (Applicative m, Monad m) =>
               KernelMapper flore tlore m -> Kernel flore -> m (Kernel tlore)
-mapKernelM _ (GetSize name size_class) =
-  pure $ GetSize name size_class
-mapKernelM _ (GetSizeMax size_class) =
-  pure $ GetSizeMax size_class
-mapKernelM tv (CmpSizeLe name size_class x) =
-  CmpSizeLe name size_class <$> mapOnKernelSubExp tv x
 mapKernelM tv (SegRed space comm red_op nes ts lam) =
   SegRed
   <$> mapOnKernelSpace tv space
@@ -457,10 +451,6 @@
   where dims = map snd $ spaceDimensions space
         segment_dims = init dims
 
-kernelType GetSize{} = [Prim int32]
-kernelType GetSizeMax{} = [Prim int32]
-kernelType CmpSizeLe{} = [Prim Bool]
-
 chunkedKernelNonconcatOutputs :: Lambda lore -> Int
 chunkedKernelNonconcatOutputs fun =
   length $ takeWhile (not . outerSizeIsChunk) $ lambdaReturnType fun
@@ -609,9 +599,6 @@
   usageInOp (SegGenRed _ ops _ body) =
     mconcat $ map UT.consumedUsage $ S.toList (consumedInBody body) <>
     concatMap genReduceDest ops
-  usageInOp GetSize{} = mempty
-  usageInOp GetSizeMax{} = mempty
-  usageInOp CmpSizeLe{} = mempty
 
 consumedInKernelBody :: Aliased lore =>
                         KernelBody lore -> Names
@@ -620,10 +607,6 @@
 
 typeCheckKernel :: TC.Checkable lore => Kernel (Aliases lore) -> TC.TypeM lore ()
 
-typeCheckKernel GetSize{} = return ()
-typeCheckKernel GetSizeMax{} = return ()
-typeCheckKernel (CmpSizeLe _ _ x) = TC.require [Prim int32] x
-
 typeCheckKernel (SegRed space _ red_op nes ts body) = do
   checkSpace space
   mapM_ TC.checkType ts
@@ -747,21 +730,8 @@
   opMetrics (SegGenRed _ ops _ body) =
     inside "SegGenRed" $ do mapM_ (lambdaMetrics . genReduceOp) ops
                             bodyMetrics body
-  opMetrics GetSize{} = seen "GetSize"
-  opMetrics GetSizeMax{} = seen "GetSizeMax"
-  opMetrics CmpSizeLe{} = seen "CmpSizeLe"
 
 instance PrettyLore lore => PP.Pretty (Kernel lore) where
-  ppr (GetSize name size_class) =
-    text "get_size" <> parens (commasep [ppr name, ppr size_class])
-
-  ppr (GetSizeMax size_class) =
-    text "get_size_max" <> parens (ppr size_class)
-
-  ppr (CmpSizeLe name size_class x) =
-    text "get_size" <> parens (commasep [ppr name, ppr size_class]) <+>
-    text "<" <+> ppr x
-
   ppr (Kernel desc space ts body) =
     text "kernel" <+> text (kernelName desc) <>
     PP.align (ppr space) <+>
@@ -835,3 +805,129 @@
                                        Just se -> "," <+> "offset=" <> ppr se
   ppr (KernelInPlaceReturn what) =
     text "kernel returns" <+> ppr what
+
+--- Host operations
+
+-- | A host-level operation; parameterised by what else it can do.
+data HostOp lore inner
+  = GetSize Name SizeClass
+    -- ^ Produce some runtime-configurable size.
+  | GetSizeMax SizeClass
+    -- ^ The maximum size of some class.
+  | CmpSizeLe Name SizeClass SubExp
+    -- ^ Compare size (likely a threshold) with some Int32 value.
+  | HostOp inner
+    -- ^ The arbitrary operation.
+  deriving (Eq, Ord, Show)
+
+instance Substitute inner => Substitute (HostOp lore inner) where
+  substituteNames substs (HostOp op) =
+    HostOp $ substituteNames substs op
+  substituteNames substs (CmpSizeLe name sclass x) =
+    CmpSizeLe name sclass $ substituteNames substs x
+  substituteNames _ x = x
+
+instance Rename inner => Rename (HostOp lore inner) where
+  rename (HostOp op) = HostOp <$> rename op
+  rename (CmpSizeLe name sclass x) = CmpSizeLe name sclass <$> rename x
+  rename x = pure x
+
+instance IsOp inner => IsOp (HostOp lore inner) where
+  safeOp (HostOp op) = safeOp op
+  safeOp _ = True
+  cheapOp (HostOp op) = cheapOp op
+  cheapOp _ = True
+
+instance TypedOp inner => TypedOp (HostOp lore inner) where
+  opType GetSize{} = pure [Prim int32]
+  opType GetSizeMax{} = pure [Prim int32]
+  opType CmpSizeLe{} = pure [Prim Bool]
+  opType (HostOp op) = opType op
+
+instance AliasedOp inner => AliasedOp (HostOp lore inner) where
+  opAliases (HostOp op) = opAliases op
+  opAliases _ = [mempty]
+
+  consumedInOp (HostOp op) = consumedInOp op
+  consumedInOp _ = mempty
+
+instance RangedOp inner => RangedOp (HostOp lore inner) where
+  opRanges (HostOp op) = opRanges op
+  opRanges _ = [unknownRange]
+
+instance FreeIn inner => FreeIn (HostOp lore inner) where
+  freeIn (HostOp op) = freeIn op
+  freeIn (CmpSizeLe _ _ x) = freeIn x
+  freeIn _ = mempty
+
+instance CanBeAliased inner => CanBeAliased (HostOp lore inner) where
+  type OpWithAliases (HostOp lore inner) = HostOp (Aliases lore) (OpWithAliases inner)
+
+  addOpAliases (HostOp op) = HostOp $ addOpAliases op
+  addOpAliases (GetSize name sclass) = GetSize name sclass
+  addOpAliases (GetSizeMax sclass) = GetSizeMax sclass
+  addOpAliases (CmpSizeLe name sclass x) = CmpSizeLe name sclass x
+
+  removeOpAliases (HostOp op) = HostOp $ removeOpAliases op
+  removeOpAliases (GetSize name sclass) = GetSize name sclass
+  removeOpAliases (GetSizeMax sclass) = GetSizeMax sclass
+  removeOpAliases (CmpSizeLe name sclass x) = CmpSizeLe name sclass x
+
+instance CanBeRanged inner => CanBeRanged (HostOp lore inner) where
+  type OpWithRanges (HostOp lore inner) = HostOp (Ranges lore) (OpWithRanges inner)
+
+  addOpRanges (HostOp op) = HostOp $ addOpRanges op
+  addOpRanges (GetSize name sclass) = GetSize name sclass
+  addOpRanges (GetSizeMax sclass) = GetSizeMax sclass
+  addOpRanges (CmpSizeLe name sclass x) = CmpSizeLe name sclass x
+
+  removeOpRanges (HostOp op) = HostOp $ removeOpRanges op
+  removeOpRanges (GetSize name sclass) = GetSize name sclass
+  removeOpRanges (GetSizeMax sclass) = GetSizeMax sclass
+  removeOpRanges (CmpSizeLe name sclass x) = CmpSizeLe name sclass x
+
+instance CanBeWise inner => CanBeWise (HostOp lore inner) where
+  type OpWithWisdom (HostOp lore inner) = HostOp (Wise lore) (OpWithWisdom inner)
+
+  removeOpWisdom (HostOp op) = HostOp $ removeOpWisdom op
+  removeOpWisdom (GetSize name sclass) = GetSize name sclass
+  removeOpWisdom (GetSizeMax sclass) = GetSizeMax sclass
+  removeOpWisdom (CmpSizeLe name sclass x) = CmpSizeLe name sclass x
+
+instance ST.IndexOp op => ST.IndexOp (HostOp lore op) where
+  indexOp vtable k (HostOp op) is = ST.indexOp vtable k op is
+  indexOp _ _ _ _ = Nothing
+
+instance PP.Pretty inner => PP.Pretty (HostOp lore inner) where
+  ppr (GetSize name size_class) =
+    text "get_size" <> parens (commasep [ppr name, ppr size_class])
+
+  ppr (GetSizeMax size_class) =
+    text "get_size_max" <> parens (ppr size_class)
+
+  ppr (CmpSizeLe name size_class x) =
+    text "get_size" <> parens (commasep [ppr name, ppr size_class]) <+>
+    text "<" <+> ppr x
+
+  ppr (HostOp op) = ppr op
+
+instance OpMetrics inner => OpMetrics (HostOp lore inner) where
+  opMetrics GetSize{} = seen "GetSize"
+  opMetrics GetSizeMax{} = seen "GetSizeMax"
+  opMetrics CmpSizeLe{} = seen "CmpSizeLe"
+  opMetrics (HostOp op) = opMetrics op
+
+instance UsageInOp inner => UsageInOp (HostOp lore inner) where
+  usageInOp GetSize{} = mempty
+  usageInOp GetSizeMax{} = mempty
+  usageInOp CmpSizeLe{} = mempty
+  usageInOp (HostOp op) = usageInOp op
+
+typeCheckHostOp :: TC.Checkable lore =>
+                   (inner -> TC.TypeM lore ())
+                -> HostOp (Aliases lore) inner
+                -> TC.TypeM lore ()
+typeCheckHostOp _ GetSize{} = return ()
+typeCheckHostOp _ GetSizeMax{} = return ()
+typeCheckHostOp _ (CmpSizeLe _ _ x) = TC.require [Prim int32] x
+typeCheckHostOp f (HostOp op) = f op
diff --git a/src/Futhark/Representation/Kernels/Simplify.hs b/src/Futhark/Representation/Kernels/Simplify.hs
--- a/src/Futhark/Representation/Kernels/Simplify.hs
+++ b/src/Futhark/Representation/Kernels/Simplify.hs
@@ -59,8 +59,11 @@
                      RetType lore ~ RetType outerlore,
                      BranchType lore ~ BranchType outerlore) =>
                     (KernelSpace -> Engine.SimpleOps lore) -> Engine.Env lore
-                 -> Kernel lore -> Engine.SimpleM outerlore (Kernel (Wise lore), Stms (Wise outerlore))
-simplifyKernelOp mk_ops env (Kernel desc space ts kbody) = do
+                 -> HostOp outerlore (Kernel lore)
+                 -> Engine.SimpleM outerlore (HostOp (Wise outerlore) (Kernel (Wise lore)),
+                                              Stms (Wise outerlore))
+
+simplifyKernelOp mk_ops env (HostOp (Kernel desc space ts kbody)) = do
   space' <- Engine.simplify space
   ts' <- mapM Engine.simplify ts
   outer_vtable <- Engine.askVtable
@@ -74,13 +77,13 @@
                         `Engine.orIf` Engine.isConsumed) $
         simplifyKernelBodyM kbody
   kbody_hoisted' <- mapM processHoistedStm kbody_hoisted
-  return (Kernel desc space' ts' $ mkWiseKernelBody () kbody_stms kbody_res,
+  return (HostOp $ Kernel desc space' ts' $ mkWiseKernelBody () kbody_stms kbody_res,
           kbody_hoisted')
   where scope = scopeOfKernelSpace space
         scope_vtable = ST.fromScope scope
         bound_here = S.fromList $ M.keys scope
 
-simplifyKernelOp mk_ops env (SegRed space comm red_op nes ts body) = do
+simplifyKernelOp mk_ops env (HostOp (SegRed space comm red_op nes ts body)) = do
   space' <- Engine.simplify space
   nes' <- mapM Engine.simplify nes
   ts' <- mapM Engine.simplify ts
@@ -94,13 +97,13 @@
 
   (body', body_hoisted) <- hoistFromBody space' (mk_ops space') env ts body
 
-  return (SegRed space' comm red_op' nes' ts' body',
+  return (HostOp $ SegRed space' comm red_op' nes' ts' body',
           red_op_hoisted' <> body_hoisted)
 
   where scope_vtable = ST.fromScope scope
         scope = scopeOfKernelSpace space
 
-simplifyKernelOp mk_ops env (SegGenRed space ops ts body) = do
+simplifyKernelOp mk_ops env (HostOp (SegGenRed space ops ts body)) = do
   outer_vtable <- Engine.askVtable
 
   space' <- Engine.simplify space
@@ -124,14 +127,16 @@
 
   (body', body_hoisted) <- hoistFromBody space' (mk_ops space') env ts body
 
-  return (SegGenRed space' ops' ts' body',
+  return (HostOp $ SegGenRed space' ops' ts' body',
           red_op_hoisted' <> body_hoisted)
 
   where scope_vtable = ST.fromScope scope
         scope = scopeOfKernelSpace space
 
-simplifyKernelOp _ _ (GetSize key size_class) = return (GetSize key size_class, mempty)
-simplifyKernelOp _ _ (GetSizeMax size_class) = return (GetSizeMax size_class, mempty)
+simplifyKernelOp _ _ (GetSize key size_class) =
+  return (GetSize key size_class, mempty)
+simplifyKernelOp _ _ (GetSizeMax size_class) =
+  return (GetSizeMax size_class, mempty)
 simplifyKernelOp _ _ (CmpSizeLe key size_class x) = do
   x' <- Engine.simplify x
   return (CmpSizeLe key size_class x', mempty)
@@ -410,7 +415,7 @@
 -- into a replicate.
 removeInvariantKernelResults :: TopDownRuleOp (Wise Kernels)
 removeInvariantKernelResults vtable (Pattern [] kpes) attr
-                                    (Kernel desc space ts (KernelBody _ kstms kres)) = do
+                             (HostOp (Kernel desc space ts (KernelBody _ kstms kres))) = do
   (ts', kpes', kres') <-
     unzip3 <$> filterM checkForInvarianceResult (zip3 ts kpes kres)
 
@@ -418,7 +423,7 @@
   when (kres == kres')
     cannotSimplify
 
-  addStm $ Let (Pattern [] kpes') attr $ Op $ Kernel desc space ts' $
+  addStm $ Let (Pattern [] kpes') attr $ Op $ HostOp $ Kernel desc space ts' $
     mkWiseKernelBody () kstms kres'
   where isInvariant Constant{} = True
         isInvariant (Var v) = isJust $ ST.lookup v vtable
@@ -447,7 +452,7 @@
 -- simplify further analysis.
 distributeKernelResults :: BottomUpRuleOp (Wise Kernels)
 distributeKernelResults (vtable, used)
-  (Pattern [] kpes) attr (Kernel desc kspace kts (KernelBody _ kstms kres)) = do
+  (Pattern [] kpes) attr (HostOp (Kernel desc kspace kts (KernelBody _ kstms kres))) = do
   -- Iterate through the bindings.  For each, we check whether it is
   -- in kres and can be moved outside.  If so, we remove it from kres
   -- and kpes and make it a binding outside.
@@ -457,8 +462,8 @@
   when (kpes' == kpes)
     cannotSimplify
 
-  addStm $ Let (Pattern [] kpes') attr $
-    Op $ Kernel desc kspace kts' $ mkWiseKernelBody () (stmsFromList $ reverse kstms_rev) kres'
+  addStm $ Let (Pattern [] kpes') attr $ Op $ HostOp $
+    Kernel desc kspace kts' $ mkWiseKernelBody () (stmsFromList $ reverse kstms_rev) kres'
   where
     free_in_kstms = fold $ fmap freeInStm kstms
 
diff --git a/src/Futhark/TypeCheck.hs b/src/Futhark/TypeCheck.hs
--- a/src/Futhark/TypeCheck.hs
+++ b/src/Futhark/TypeCheck.hs
@@ -17,8 +17,6 @@
   , lookupVar
   , lookupAliases
   , Occurences
-  , UsageMap
-  , usageMap
   , collectOccurences
   , subCheck
 
@@ -184,15 +182,6 @@
 
 type Occurences = [Occurence]
 
-type UsageMap = M.Map VName [Usage]
-
-usageMap :: Occurences -> UsageMap
-usageMap = foldl comb M.empty
-  where comb m (Occurence obs cons) =
-          let m' = S.foldl' (ins Observed) m obs
-          in S.foldl' (ins Consumed) m' cons
-        ins v m k = M.insertWith (++) k [v] m
-
 allConsumed :: Occurences -> Names
 allConsumed = S.unions . map consumed
 
@@ -378,20 +367,12 @@
         bindVar env name (LetInfo (Names' als, attr)) =
           let als' | primType (typeOf attr) = mempty
                    | otherwise = expandAliases als env
-              inedges = S.toList als'
-              update (LetInfo (Names' thesenames, thisattr)) =
-                LetInfo (Names' $ S.insert name thesenames, thisattr)
-              update b = b
           in env { envVtable =
-                      M.insert name (LetInfo (Names' als', attr)) $
-                      adjustSeveral update inedges $
-                      envVtable env
+                     M.insert name (LetInfo (Names' als', attr)) $ envVtable env
                  }
         bindVar env name attr =
           env { envVtable = M.insert name attr $ envVtable env }
 
-        adjustSeveral f = flip $ foldl $ flip $ M.adjust f
-
         -- Check whether the bound variables have been used correctly
         -- within their scope.
         check m = do
@@ -511,7 +492,7 @@
                body) consumable $ do
       checkFunParams params
       checkRetType rettype
-      checkFunBody rettype body
+      context "When checking function body" $ checkFunBody rettype body
         where consumable = [ (paramName param, mempty)
                            | param <- params
                            , unique $ paramDeclType param
@@ -550,7 +531,8 @@
       check
       scope <- askScope
       let isArray = maybe False ((>0) . arrayRank . typeOf) . (`M.lookup` scope)
-      checkReturnAlias $ map (S.filter isArray) $ bodyAliases body
+      context ("When checking the body aliases: " ++ pretty (bodyAliases body)) $
+        checkReturnAlias $ map (S.filter isArray) $ bodyAliases body
   where param_names = map fst params
 
         checkNoDuplicateParams = foldM_ expand [] param_names
@@ -928,7 +910,8 @@
 
 checkPatElem :: Checkable lore =>
                 PatElemT (LetAttr lore) -> TypeM lore ()
-checkPatElem (PatElem name attr) = checkLetBoundLore name attr
+checkPatElem (PatElem name attr) = context ("When checking pattern element " ++ pretty name) $
+                                   checkLetBoundLore name attr
 
 checkDimIndex :: Checkable lore =>
                  DimIndex SubExp -> TypeM lore ()
@@ -940,8 +923,8 @@
          -> TypeM lore a
          -> TypeM lore a
 checkStm stm@(Let pat (StmAux (Certificates cs) (_,attr)) e) m = do
-  mapM_ (requireI [Prim Cert]) cs
-  checkExpLore attr
+  context "When checking certificates" $ mapM_ (requireI [Prim Cert]) cs
+  context "When checking expression annotation" $ checkExpLore attr
   context ("When matching\n" ++ message "  " pat ++ "\nwith\n" ++ message "  " e) $
     matchPattern pat e
   binding (scopeOf stm) $ do
@@ -1029,7 +1012,7 @@
   forM_ (zip (map diet paramts) args) $ \(d, (_, als)) ->
     occur [consumption (consumeArg als d)]
   where consumeArg als Consume = als
-        consumeArg _   Observe = mempty
+        consumeArg _   _       = mempty
 
 checkLambda :: Checkable lore =>
                Lambda (Aliases lore) -> [Arg] -> TypeM lore ()
diff --git a/src/Language/Futhark/Attributes.hs b/src/Language/Futhark/Attributes.hs
--- a/src/Language/Futhark/Attributes.hs
+++ b/src/Language/Futhark/Attributes.hs
@@ -26,7 +26,7 @@
   , typeOf
 
   -- * Queries on patterns and params
-  , patIdentSet
+  , patternIdents
   , patternType
   , patternStructType
   , patternPatternType
@@ -42,8 +42,6 @@
   , diet
   , arrayRank
   , nestedDims
-  , returnType
-  , concreteType
   , orderZero
   , unfoldFunType
   , foldFunType
@@ -55,18 +53,15 @@
   , peelArray
   , stripArray
   , arrayOf
-  , arrayOfWithAliases
   , toStructural
   , toStruct
   , fromStruct
   , setAliases
   , addAliases
   , setUniqueness
-  , modifyShapeAnnotations
-  , setArrayShape
   , removeShapeAnnotations
   , vacuousShapeAnnotations
-  , typeToRecordArrayElem
+  , anyDimShapeAnnotations
   , recordArrayElemToType
   , tupleRecord
   , isTupleRecord
@@ -74,6 +69,8 @@
   , tupleFieldNames
   , sortFields
   , isTypeParam
+  , combineTypeShapes
+  , unscopeType
 
   -- | Values of these types are produces by the parser.  They use
   -- unadorned names and have no type information, apart from that
@@ -156,20 +153,18 @@
         notV Nothing  = const True
         notV (Just v) = (/=NamedDim (qualName v))
 
--- | Set the dimensions of an array.  If the given type is not an
--- array, return the type unchanged.
-setArrayShape :: TypeBase dim as -> ShapeDecl dim -> TypeBase dim as
-setArrayShape (Array a u t _) ds = Array a u t ds
-setArrayShape t _ = t
-
 -- | Change the shape of a type to be just the 'Rank'.
-removeShapeAnnotations :: TypeBase dim as -> TypeBase () as
+removeShapeAnnotations :: TypeBase (DimDecl vn) as -> TypeBase () as
 removeShapeAnnotations = modifyShapeAnnotations $ const ()
 
--- | Change all size annotations to be 'AnyDim'.
-vacuousShapeAnnotations :: TypeBase dim as -> TypeBase (DimDecl vn) as
+-- | Add size annotations that are all 'AnyDim'.
+vacuousShapeAnnotations :: TypeBase () as -> TypeBase (DimDecl vn) as
 vacuousShapeAnnotations = modifyShapeAnnotations $ const AnyDim
 
+-- | Change all size annotations to be 'AnyDim'.
+anyDimShapeAnnotations :: TypeBase (DimDecl vn) as -> TypeBase (DimDecl vn) as
+anyDimShapeAnnotations = modifyShapeAnnotations $ const AnyDim
+
 -- | Change the size annotations of a type.
 modifyShapeAnnotations :: (oldshape -> newshape)
                        -> TypeBase oldshape as
@@ -202,24 +197,11 @@
 diet (Array _ Nonunique _ _) = Observe
 diet (Enum _)                = Observe
 
--- | @t `maskAliases` d@ removes aliases (sets them to 'mempty') from
--- the parts of @t@ that are denoted as 'Consumed' by the 'Diet' @d@.
-maskAliases :: Monoid as =>
-               TypeBase shape as
-            -> Diet
-            -> TypeBase shape as
-maskAliases t Consume = t `setAliases` mempty
-maskAliases t Observe = t
-maskAliases (Record ets) (RecordDiet ds) =
-  Record $ M.intersectionWith maskAliases ets ds
-maskAliases t FuncDiet{} = t
-maskAliases _ _ = error "Invalid arguments passed to maskAliases."
-
 -- | Convert any type to one that has rank information, no alias
 -- information, and no embedded names.
 toStructural :: TypeBase dim as
              -> TypeBase () ()
-toStructural = removeNames . removeShapeAnnotations
+toStructural = flip setAliases () . modifyShapeAnnotations (const ())
 
 -- | Remove aliasing information from a type.
 toStruct :: TypeBase dim as
@@ -258,12 +240,6 @@
   return $ Array als u et shape'
 peelArray _ _ = Nothing
 
--- | Remove names from a type - this involves removing all size
--- annotations from arrays, as well as all aliasing.
-removeNames :: TypeBase dim as
-            -> TypeBase () ()
-removeNames = flip setAliases () . removeShapeAnnotations
-
 -- | @arrayOf t s u@ constructs an array type.  The convenience
 -- compared to using the 'Array' constructor directly is that @t@ can
 -- itself be an array.  If @t@ is an @n@-dimensional array, and @s@ is
@@ -370,7 +346,40 @@
 isTypeParam TypeParamType{}       = True
 isTypeParam TypeParamDim{}        = False
 
+-- | Combine the shape information of types as much as possible. The first
+-- argument is the orignal type and the second is the type of the transformed
+-- expression. This is necessary since the original type may contain additional
+-- information (e.g., shape restrictions) from the user given annotation.
+combineTypeShapes :: (Monoid as, ArrayDim dim) =>
+                     TypeBase dim as -> TypeBase dim as -> TypeBase dim as
+combineTypeShapes (Record ts1) (Record ts2)
+  | M.keys ts1 == M.keys ts2 =
+      Record $ M.map (uncurry combineTypeShapes) (M.intersectionWith (,) ts1 ts2)
+combineTypeShapes (Array als1 u1 et1 shape1) (Array als2 _u2 et2 shape2)
+  | Just new_shape <- unifyShapes shape1 shape2 =
+      Array (als1<>als2) u1 (combineElemTypeInfo et1 et2) new_shape
+combineTypeShapes _ new_tp = new_tp
 
+combineElemTypeInfo :: ArrayDim dim =>
+                       ArrayElemTypeBase dim
+                    -> ArrayElemTypeBase dim -> ArrayElemTypeBase dim
+combineElemTypeInfo (ArrayRecordElem et1) (ArrayRecordElem et2) =
+  ArrayRecordElem $ M.map (uncurry combineRecordArrayTypeInfo)
+                          (M.intersectionWith (,) et1 et2)
+combineElemTypeInfo _ new_tp = new_tp
+
+combineRecordArrayTypeInfo :: ArrayDim dim =>
+                              RecordArrayElemTypeBase dim
+                           -> RecordArrayElemTypeBase dim
+                           -> RecordArrayElemTypeBase dim
+combineRecordArrayTypeInfo (RecordArrayElem et1) (RecordArrayElem et2) =
+  RecordArrayElem $ combineElemTypeInfo et1 et2
+combineRecordArrayTypeInfo (RecordArrayArrayElem et1 shape1)
+                           (RecordArrayArrayElem et2 shape2)
+  | Just new_shape <- unifyShapes shape1 shape2 =
+      RecordArrayArrayElem (combineElemTypeInfo et1 et2) new_shape
+combineRecordArrayTypeInfo _ new_tp = new_tp
+
 -- | Set the uniqueness attribute of a type.  If the type is a tuple,
 -- the uniqueness of its components will be modified.
 setUniqueness :: TypeBase dim as -> Uniqueness -> TypeBase dim as
@@ -419,17 +428,22 @@
 rank :: Int -> ShapeDecl ()
 rank n = ShapeDecl $ replicate n ()
 
-unscopeAliases :: S.Set VName -> CompType -> CompType
-unscopeAliases bound_here t = t `addAliases` S.map unbind
+-- | The type is leaving a scope, so clean up any aliases that
+-- reference the bound variables, and turn any dimensions that name
+-- them into AnyDim instead.
+unscopeType :: S.Set VName -> PatternType -> PatternType
+unscopeType bound_here t = modifyShapeAnnotations onDim $ t `addAliases` S.map unbind
   where unbind (AliasBound v) | v `S.member` bound_here = AliasFree v
         unbind a = a
+        onDim (NamedDim qn) | qualLeaf qn `S.member` bound_here = AnyDim
+        onDim d = d
 
 -- | The type of an Futhark term.  The aliasing will refer to itself, if
 -- the term is a non-tuple-typed variable.
-typeOf :: ExpBase Info VName -> CompType
+typeOf :: ExpBase Info VName -> PatternType
 typeOf (Literal val _) = Prim $ primValueType val
-typeOf (IntLit _ (Info t) _) = fromStruct t
-typeOf (FloatLit _ (Info t) _) = fromStruct t
+typeOf (IntLit _ (Info t) _) = t
+typeOf (FloatLit _ (Info t) _) = t
 typeOf (Parens e _) = typeOf e
 typeOf (QualParens _ e _) = typeOf e
 typeOf (TupLit es _) = tupleRecord $ map typeOf es
@@ -438,57 +452,39 @@
   Record $ M.unions $ reverse $ map record fs
   where record (RecordFieldExplicit name e _) = M.singleton name $ typeOf e
         record (RecordFieldImplicit name (Info t) _) =
-          M.singleton (baseName name) $ t `addAliases` S.insert (AliasBound name)
+          M.singleton (baseName name) $ t
+          `addAliases` S.insert (AliasBound name)
 typeOf (ArrayLit _ (Info t) _) = t
 typeOf (Range _ _ _ (Info t) _) = t
-typeOf (BinOp _ _ _ _ (Info t) _) = removeShapeAnnotations t
+typeOf (BinOp _ _ _ _ (Info t) _) = t
 typeOf (Project _ _ (Info t) _) = t
 typeOf (If _ _ _ (Info t) _) = t
-typeOf (Var _ (Info t) _) = removeShapeAnnotations t
-typeOf (Ascript e _ _) = typeOf e
-typeOf (Apply _ _ _ (Info t) _) = removeShapeAnnotations t
+typeOf (Var _ (Info t) _) = t
+typeOf (Ascript _ _ (Info t) _) = t
+typeOf (Apply _ _ _ (Info t) _) = t
 typeOf (Negate e _) = typeOf e
-typeOf (LetPat _ pat _ body _) =
-  unscopeAliases (S.map identName $ patIdentSet pat) $ typeOf body
+typeOf (LetPat _ _ _ _ (Info t) _) = t
 typeOf (LetFun _ _ body _) = typeOf body
-typeOf (LetWith dest _ _ _ body _) =
-  unscopeAliases (S.singleton $ identName dest) $ typeOf body
+typeOf (LetWith _ _ _ _ _ (Info t) _) = t
 typeOf (Index _ _ (Info t) _) = t
 typeOf (Update e _ _ _) = typeOf e `setAliases` mempty
-typeOf (RecordUpdate _ _ _ (Info t) _) = removeShapeAnnotations t
+typeOf (RecordUpdate _ _ _ (Info t) _) = t
 typeOf (Unsafe e _) = typeOf e
 typeOf (Assert _ e _ _) = typeOf e
-typeOf (Map _ _ (Info t) _) = t `setUniqueness` Unique
-typeOf (Reduce _ _ _ arr _) =
-  stripArray 1 (typeOf arr) `setAliases` mempty
-typeOf (GenReduce hist _ _ _ _ _) =
-  typeOf hist `setAliases` mempty `setUniqueness` Unique
-typeOf (Scan _ _ arr _) = typeOf arr `setAliases` mempty `setUniqueness` Unique
-typeOf (Filter _ arr _) = typeOf arr `setAliases` mempty `setUniqueness` Unique
-typeOf (Partition _ _ arr _) =
-  tupleRecord [typeOf arr `setAliases` mempty `setUniqueness` Unique,
-               Array mempty Unique (ArrayPrimElem (Signed Int32)) (rank 1)]
-typeOf (Stream _ lam _ _) =
-  rettype (typeOf lam) `setUniqueness` Unique
-  where rettype (Arrow _ _ _ t) = rettype t
-        rettype t = t
 typeOf (DoLoop _ pat _ _ _ _) = patternType pat
 typeOf (Lambda tparams params _ _ (Info (als, t)) _) =
-  unscopeAliases bound_here $
-  removeShapeAnnotations (foldr (uncurry (Arrow ()) . patternParam) t params)
-  `setAliases` als
+  unscopeType bound_here $
+  foldr (uncurry (Arrow ()) . patternParam) t params `setAliases` als
   where bound_here = S.fromList (map typeParamName tparams) <>
-                     S.map identName (mconcat $ map patIdentSet params)
+                     S.map identName (mconcat $ map patternIdents params)
 typeOf (OpSection _ (Info t) _) =
-  removeShapeAnnotations t
+  t
 typeOf (OpSectionLeft _ _ _ (_, Info pt2) (Info ret) _)  =
-  removeShapeAnnotations $ foldFunType [fromStruct pt2] ret
+  foldFunType [fromStruct pt2] ret
 typeOf (OpSectionRight _ _ _ (Info pt1, _) (Info ret) _) =
-  removeShapeAnnotations $ foldFunType [fromStruct pt1] ret
-typeOf (ProjectSection _ (Info t) _) =
-  removeShapeAnnotations t
-typeOf (IndexSection _ (Info t) _) =
-  removeShapeAnnotations t
+  foldFunType [fromStruct pt1] ret
+typeOf (ProjectSection _ (Info t) _) = t
+typeOf (IndexSection _ (Info t) _) = t
 typeOf (VConstr0 _ (Info t) _)  = t
 typeOf (Match _ _ (Info t) _) = t
 
@@ -525,47 +521,6 @@
         typeArgFree (TypeArgType ta _) = typeVars ta
         typeArgFree TypeArgDim{} = mempty
 
--- | The result of applying the arguments of the given types to a
--- function with the given return type, consuming its parameters with
--- the given diets.
-returnType :: TypeBase dim Aliasing
-           -> Diet
-           -> CompType
-           -> TypeBase dim Aliasing
-returnType (Array _ Unique et shape) _ _ =
-  Array mempty Unique et shape
-returnType (Array als Nonunique et shape) d arg =
-  Array (als<>arg_als) Unique et shape -- Intentional!
-  where arg_als = aliases $ maskAliases arg d
-returnType (Record fs) d arg =
-  Record $ fmap (\et -> returnType et d arg) fs
-returnType (Prim t) _ _ = Prim t
-returnType (TypeVar _ Unique t targs) _ _ =
-  TypeVar mempty Unique t targs
-returnType (TypeVar als Nonunique t targs) d arg =
-  TypeVar (als<>arg_als) Unique t targs -- Intentional!
-  where arg_als = aliases $ maskAliases arg d
-returnType (Arrow _ v t1 t2) d arg =
-  Arrow als v (bimap id (const mempty) t1) (t2 `setAliases` als)
-  where als = aliases $ maskAliases arg d
-returnType (Enum cs) _ _ = Enum cs
-
--- | Is the type concrete, i.e, without any type variables or function arrows?
-concreteType :: TypeBase f vn -> Bool
-concreteType Prim{} = True
-concreteType TypeVar{} = False
-concreteType Arrow{} = False
-concreteType (Record ts) = all concreteType ts
-concreteType Enum{} = True
-concreteType (Array _ _ at _) = concreteArrayType at
-  where concreteArrayType ArrayPrimElem{}      = True
-        concreteArrayType ArrayPolyElem{}      = False
-        concreteArrayType (ArrayRecordElem ts) = all concreteRecordArrayElem ts
-        concreteArrayType ArrayEnumElem{}      = True
-
-        concreteRecordArrayElem (RecordArrayElem et) = concreteArrayType et
-        concreteRecordArrayElem (RecordArrayArrayElem et _) = concreteArrayType et
-
 -- | @orderZero t@ is 'True' if the argument type has order 0, i.e., it is not
 -- a function type, does not contain a function type as a subcomponent, and may
 -- not be instantiated with a function type.
@@ -608,24 +563,24 @@
   PatternLit _ (Info t) _ -> orderZero t
 
 -- | The set of identifiers bound in a pattern.
-patIdentSet :: (Functor f, Ord vn) => PatternBase f vn -> S.Set (IdentBase f vn)
-patIdentSet (Id v t loc)              = S.singleton $ Ident v (removeShapeAnnotations <$> t) loc
-patIdentSet (PatternParens p _)       = patIdentSet p
-patIdentSet (TuplePattern pats _)     = mconcat $ map patIdentSet pats
-patIdentSet (RecordPattern fs _)      = mconcat $ map (patIdentSet . snd) fs
-patIdentSet Wildcard{}                = mempty
-patIdentSet (PatternAscription p _ _) = patIdentSet p
-patIdentSet PatternLit{}              = mempty
+patternIdents :: (Functor f, Ord vn) => PatternBase f vn -> S.Set (IdentBase f vn)
+patternIdents (Id v t loc)              = S.singleton $ Ident v t loc
+patternIdents (PatternParens p _)       = patternIdents p
+patternIdents (TuplePattern pats _)     = mconcat $ map patternIdents pats
+patternIdents (RecordPattern fs _)      = mconcat $ map (patternIdents . snd) fs
+patternIdents Wildcard{}                = mempty
+patternIdents (PatternAscription p _ _) = patternIdents p
+patternIdents PatternLit{}              = mempty
 
 -- | The type of values bound by the pattern.
-patternType :: PatternBase Info VName -> CompType
-patternType (Wildcard (Info t) _)     = removeShapeAnnotations t
+patternType :: PatternBase Info VName -> PatternType
+patternType (Wildcard (Info t) _)     = t
 patternType (PatternParens p _)       = patternType p
-patternType (Id _ (Info t) _)         = removeShapeAnnotations t
+patternType (Id _ (Info t) _)         = t
 patternType (TuplePattern pats _)     = tupleRecord $ map patternType pats
 patternType (RecordPattern fs _)      = Record $ patternType <$> M.fromList fs
 patternType (PatternAscription p _ _) = patternType p
-patternType (PatternLit _ (Info t) _) = removeShapeAnnotations t
+patternType (PatternLit _ (Info t) _) = t
 
 -- | The type of a pattern, including shape annotations.
 patternPatternType :: PatternBase Info VName -> PatternType
@@ -656,19 +611,19 @@
 patternNoShapeAnnotations :: PatternBase Info VName -> PatternBase Info VName
 patternNoShapeAnnotations (PatternAscription p (TypeDecl te (Info t)) loc) =
   PatternAscription (patternNoShapeAnnotations p)
-  (TypeDecl te $ Info $ vacuousShapeAnnotations t) loc
+  (TypeDecl te $ Info $ anyDimShapeAnnotations t) loc
 patternNoShapeAnnotations (PatternParens p loc) =
   PatternParens (patternNoShapeAnnotations p) loc
 patternNoShapeAnnotations (Id v (Info t) loc) =
-  Id v (Info $ vacuousShapeAnnotations t) loc
+  Id v (Info $ anyDimShapeAnnotations t) loc
 patternNoShapeAnnotations (TuplePattern ps loc) =
   TuplePattern (map patternNoShapeAnnotations ps) loc
 patternNoShapeAnnotations (RecordPattern ps loc) =
   RecordPattern (map (fmap patternNoShapeAnnotations) ps) loc
 patternNoShapeAnnotations (Wildcard (Info t) loc) =
-  Wildcard (Info (vacuousShapeAnnotations t)) loc
+  Wildcard (Info (anyDimShapeAnnotations t)) loc
 patternNoShapeAnnotations (PatternLit e (Info t) loc) =
-  PatternLit e (Info (vacuousShapeAnnotations t)) loc
+  PatternLit e (Info (anyDimShapeAnnotations t)) loc
 
 -- | Names of primitive types to types.  This is only valid if no
 -- shadowing is going on, but useful for tools.
@@ -739,7 +694,7 @@
                          [arr_a, arr_a] uarr_a),
               ("rotate", IntrinsicPolyFun [tp_a]
                          [Prim $ Signed Int32, arr_a] arr_a),
-              ("transpose", IntrinsicPolyFun [tp_a] [arr_a] arr_a),
+              ("transpose", IntrinsicPolyFun [tp_a] [arr_2d_a] arr_2d_a),
 
               ("cmp_threshold", IntrinsicPolyFun []
                                 [Prim $ Signed Int32,
@@ -799,6 +754,7 @@
         tv_a' = typeName tv_a
         t_a = TypeVar () Nonunique tv_a' []
         arr_a = Array () Nonunique (ArrayPolyElem tv_a' []) (rank 1)
+        arr_2d_a = Array () Nonunique (ArrayPolyElem tv_a' []) (rank 2)
         uarr_a = Array () Unique (ArrayPolyElem tv_a' []) (rank 1)
         tp_a = TypeParamType Unlifted tv_a noLoc
 
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
@@ -555,7 +555,7 @@
           v <- eval env e
           return (k, v)
         evalField (RecordFieldImplicit k t loc) = do
-          v <- eval env $ Var (qualName k) (vacuousShapeAnnotations <$> t) loc
+          v <- eval env $ Var (qualName k) t loc
           return (baseName k, v)
 
 eval env (ArrayLit vs _ _) = toArray =<< mapM (eval env) vs
@@ -584,7 +584,7 @@
 
 eval env (Var qv _ _) = evalTermVar env qv
 
-eval env (Ascript e td loc) = do
+eval env (Ascript e td _ loc) = do
   v <- eval env e
   let t = evalType env $ unInfo $ expandedType td
   case matchValueToType env t v of
@@ -592,7 +592,7 @@
     Left err -> bad loc env $ "Value `" <> pretty v <> "` cannot match shape of type `" <>
                 pretty (declaredType td) <> "` (`" <> pretty t <> "`): " ++ err
 
-eval env (LetPat _ p e body _) = do
+eval env (LetPat _ p e body _ _) = do
   v <- eval env e
   env' <- matchPattern env p v
   eval env' body
@@ -677,11 +677,11 @@
               ValueRecord $ M.insert f (update f_v fs v') src'
         update _ _ _ = error "eval RecordUpdate: invalid value."
 
-eval env (LetWith dest src is v body loc) = do
+eval env (LetWith dest src is v body _ loc) = do
   dest' <- maybe oob return =<<
     updateArray <$> mapM (evalDimIndex env) is <*>
     evalTermVar env (qualName $ identName src) <*> eval env v
-  let t = T.BoundV [] $ vacuousShapeAnnotations $ toStruct $ unInfo $ identType dest
+  let t = T.BoundV [] $ toStruct $ unInfo $ identType dest
   eval (valEnv (M.singleton (identName dest) (Just t, dest')) <> env) body
   where oob = bad loc env "Bad update"
 
@@ -795,8 +795,6 @@
           case c' of
             Just v' -> return v'
             Nothing -> match v cs'
-
-eval _ e = error $ "eval not yet: " ++ show e
 
 evalCase :: Value -> Env -> CaseBase Info VName
          -> EvalM (Maybe Value)
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
@@ -512,7 +512,7 @@
 -- permit inside array indices operations (there is an ambiguity with
 -- array slices).
 Exp :: { UncheckedExp }
-     : Exp ':' TypeExpDecl { Ascript $1 $3 (srcspan $1 $>) }
+     : Exp ':' TypeExpDecl { Ascript $1 $3 NoInfo (srcspan $1 $>) }
      | Exp2 %prec ':'      { $1 }
 
 Exp2 :: { UncheckedExp }
@@ -581,7 +581,7 @@
        { RecordUpdate $1 (map fst $3) $5 NoInfo (srcspan $1 $>) }
 
      | '\\' TypeParams FunParams1 maybeAscription(TypeExpTerm) '->' Exp
-       { Lambda $2 (fst $3 : snd $3) $6 (fmap (flip TypeDecl NoInfo) $4) NoInfo (srcspan $1 $>) }
+       { Lambda $2 (fst $3 : snd $3) $6 $4 NoInfo (srcspan $1 $>) }
 
      | Apply { $1 }
 
@@ -696,9 +696,9 @@
 
 LetExp :: { UncheckedExp }
      : let Pattern '=' Exp LetBody
-                      { LetPat [] $2 $4 $5 (srcspan $1 $>) }
+                      { LetPat [] $2 $4 $5 NoInfo (srcspan $1 $>) }
      | let TypeParams1 Pattern '=' Exp LetBody
-                      { LetPat (fst $2 : snd $2) $3 $5 $6 (srcspan $1 $>) }
+                      { LetPat (fst $2 : snd $2) $3 $5 $6 NoInfo (srcspan $1 $>) }
 
      | let id TypeParams FunParams1 maybeAscription(TypeExpDecl) '=' Exp LetBody
        { let L _ (ID name) = $2
@@ -706,7 +706,7 @@
 
      | let VarSlice '=' Exp LetBody
                       { let (v,slice,loc) = $2; ident = Ident v NoInfo loc
-                        in LetWith ident ident slice $4 $5 (srcspan $1 $>) }
+                        in LetWith ident ident slice $4 $5 NoInfo (srcspan $1 $>) }
 
 LetBody :: { UncheckedExp }
     : in Exp %prec letprec { $2 }
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
@@ -201,7 +201,7 @@
   pprPrec _ (Var name _ _) = ppr name
   pprPrec _ (Parens e _) = align $ parens $ ppr e
   pprPrec _ (QualParens v e _) = ppr v <> text "." <> align (parens $ ppr e)
-  pprPrec _ (Ascript e t _) = pprPrec 0 e <> colon <+> pprPrec 0 t
+  pprPrec _ (Ascript e t _ _) = pprPrec 0 e <> colon <+> pprPrec 0 t
   pprPrec _ (Literal v _) = ppr v
   pprPrec _ (IntLit v _ _) = ppr v
   pprPrec _ (FloatLit v _ _) = ppr v
@@ -230,7 +230,7 @@
   pprPrec p (Apply f arg _ _ _) =
     parensIf (p >= 10) $ ppr f <+> pprPrec 10 arg
   pprPrec _ (Negate e _) = text "-" <> ppr e
-  pprPrec p (LetPat tparams pat e body _) =
+  pprPrec p (LetPat tparams pat e body _ _) =
     parensIf (p /= -1) $ align $
     text "let" <+> align (spread $ map ppr tparams ++ [ppr pat]) <+>
     (if linebreak
@@ -239,11 +239,6 @@
     (case body of LetPat{} -> ppr body
                   _        -> text "in" <+> align (ppr body))
     where linebreak = case e of
-                        Map{}       -> True
-                        Reduce{}    -> True
-                        GenReduce{} -> True
-                        Filter{}    -> True
-                        Scan{}      -> True
                         DoLoop{}    -> True
                         LetPat{}    -> True
                         LetWith{}   -> True
@@ -257,7 +252,7 @@
     where retdecl' = case (ppr <$> unAnnot rettype) `mplus` (ppr <$> retdecl) of
                        Just rettype' -> text ":" <+> rettype'
                        Nothing       -> mempty
-  pprPrec _ (LetWith dest src idxs ve body _)
+  pprPrec _ (LetWith dest src idxs ve body _ _)
     | dest == src =
       text "let" <+> ppr dest <> list (map ppr idxs) <+>
       equals <+> align (ppr ve) <+>
@@ -277,32 +272,12 @@
     text "<-" <+> align (ppr ve)
   pprPrec _ (Index e idxs _ _) =
     pprPrec 9 e <> brackets (commasep (map ppr idxs))
-  pprPrec _ (Map lam a _ _) = ppSOAC "map" [lam] [a]
-  pprPrec _ (Reduce Commutative lam e a _) = ppSOAC "reduce_comm" [lam] [e, a]
-  pprPrec _ (Reduce Noncommutative lam e a _) = ppSOAC "reduce" [lam] [e, a]
-  pprPrec _ (GenReduce hist op ne bfun img _) =
-    ppSOAC "gen_reduce" [op, bfun] [hist, ne, img] -- do this manually
-  pprPrec _ (Stream form lam arr _) =
-    case form of
-      MapLike o ->
-        let ord_str = if o == Disorder then "_per" else ""
-        in  text ("stream_map"++ord_str) <>
-            ppr lam </> pprPrec 10 arr
-      RedLike o comm lam0 ->
-        let ord_str = if o == Disorder then "_per" else ""
-            comm_str = case comm of Commutative    -> "_comm"
-                                    Noncommutative -> ""
-        in  text ("stream_red"++ord_str++comm_str) <>
-            ppr lam0 </> ppr lam </> pprPrec 10 arr
-  pprPrec _ (Scan lam e a _) = ppSOAC "scan" [lam] [e, a]
-  pprPrec _ (Filter lam a _) = ppSOAC "filter" [lam] [a]
-  pprPrec _ (Partition k lam a _) = text "partition" <+> ppr k <+> spread (map (pprPrec 10) [lam, a])
   pprPrec _ (Unsafe e _) = text "unsafe" <+> pprPrec (-1) e
   pprPrec _ (Assert e1 e2 _ _) = text "assert" <+> pprPrec 10 e1 <+> pprPrec 10 e2
-  pprPrec p (Lambda tparams params body ascript _ _) =
+  pprPrec p (Lambda tparams params body rettype _ _) =
     parensIf (p /= -1) $
     text "\\" <> spread (map ppr tparams ++ map ppr params) <>
-    ppAscription ascript <+>
+    ppAscription rettype <+>
     text "->" </> indent 2 (ppr body)
   pprPrec _ (OpSection binop _ _) =
     parens $ ppr binop
@@ -351,7 +326,7 @@
                                     Nothing -> text "_"
   ppr (PatternLit e _ _)        = ppr e
 
-ppAscription :: (Eq vn, IsName vn, Annot f) => Maybe (TypeDeclBase f vn) -> Doc
+ppAscription :: Pretty t => Maybe t -> Doc
 ppAscription Nothing  = mempty
 ppAscription (Just t) = text ":" <> ppr t
 
@@ -474,9 +449,3 @@
         rprecedence Minus  = 10
         rprecedence Divide = 10
         rprecedence op     = precedence op
-
-ppSOAC :: (Eq vn, IsName vn, Pretty fn, Annot f) =>
-          String -> [fn] -> [ExpBase f vn] -> Doc
-ppSOAC name funs es =
-  text name <+> align (spread (map (parens . ppr) funs) </>
-                       spread (map (pprPrec 10) es))
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
@@ -31,7 +31,6 @@
   , TypeArgExp(..)
   , RecordArrayElemTypeBase(..)
   , ArrayElemTypeBase(..)
-  , CompType
   , PatternType
   , StructType
   , Diet(..)
@@ -54,7 +53,6 @@
   , CaseBase(..)
   , LoopFormBase (..)
   , PatternBase(..)
-  , StreamForm(..)
 
   -- * Module language
   , SpecBase(..)
@@ -113,17 +111,12 @@
        Show (f String),
        Show (f [VName]),
        Show (f PatternType),
-       Show (f CompType),
-       Show (f (TypeBase () ())),
        Show (f Int),
-       Show (f [TypeBase () ()]),
        Show (f StructType),
        Show (f (Aliasing, StructType)),
-       Show (f ([TypeBase () ()], PatternType)),
        Show (f (M.Map VName VName)),
        Show (f [RecordArrayElemTypeBase ()]),
-       Show (f Uniqueness),
-       Show (f ([CompType], CompType))) => Showable f vn where
+       Show (f Uniqueness)) => Showable f vn where
 
 -- | No information functor.  Usually used for placeholder type- or
 -- aliasing information.
@@ -197,7 +190,7 @@
 instance IsPrimValue Bool where
   primValue = BoolValue
 
-class (Eq dim, Ord dim) => ArrayDim dim where
+class Eq dim => ArrayDim dim where
   -- | @unifyDims x y@ combines @x@ and @y@ to contain their maximum
   -- common information, and fails if they conflict.
   unifyDims :: dim -> dim -> Maybe dim
@@ -214,7 +207,9 @@
                   -- ^ The size is a constant.
                 | AnyDim
                   -- ^ No dimension declaration.
-                deriving (Eq, Ord, Show)
+                deriving Show
+deriving instance Eq (DimDecl Name)
+deriving instance Eq (DimDecl VName)
 
 instance Functor DimDecl where
   fmap = fmapDefault
@@ -227,7 +222,7 @@
   traverse _ (ConstDim x) = pure $ ConstDim x
   traverse _ AnyDim = pure AnyDim
 
-instance (Eq vn, Ord vn) => ArrayDim (DimDecl vn) where
+instance ArrayDim (DimDecl VName) where
   unifyDims AnyDim y = Just y
   unifyDims x AnyDim = Just x
   unifyDims (NamedDim x) (NamedDim y) | x == y = Just $ NamedDim x
@@ -397,14 +392,14 @@
 -- aliased.
 type Aliasing = S.Set Alias
 
--- | A type with aliasing information and no shape annotations, used
--- for describing the type of a computation.
-type CompType = TypeBase () Aliasing
-
 -- | A type with aliasing information and shape annotations, used for
--- describing the type of a pattern.
+-- describing the type patterns and expressions.
 type PatternType = TypeBase (DimDecl VName) Aliasing
 
+-- | A "structural" type with shape annotations and no aliasing
+-- information, used for declarations.
+type StructType = TypeBase (DimDecl VName) ()
+
 -- | An unstructured type with type variables and possibly shape
 -- declarations - this is what the user types in the source program.
 data TypeExp vn = TEVar (QualName vn) SrcLoc
@@ -415,7 +410,9 @@
                 | TEApply (TypeExp vn) (TypeArgExp vn) SrcLoc
                 | TEArrow (Maybe vn) (TypeExp vn) (TypeExp vn) SrcLoc
                 | TEEnum [Name] SrcLoc
-                 deriving (Eq, Show)
+                 deriving (Show)
+deriving instance Eq (TypeExp Name)
+deriving instance Eq (TypeExp VName)
 
 instance Located (TypeExp vn) where
   locOf (TEArray _ _ loc)   = locOf loc
@@ -429,16 +426,14 @@
 
 data TypeArgExp vn = TypeArgExpDim (DimDecl vn) SrcLoc
                    | TypeArgExpType (TypeExp vn)
-                deriving (Eq, Show)
+                deriving (Show)
+deriving instance Eq (TypeArgExp Name)
+deriving instance Eq (TypeArgExp VName)
 
 instance Located (TypeArgExp vn) where
   locOf (TypeArgExpDim _ loc) = locOf loc
   locOf (TypeArgExpType t)    = locOf t
 
--- | A "structural" type with shape annotations and no aliasing
--- information, used for declarations.
-type StructType = TypeBase (DimDecl VName) ()
-
 -- | A declaration of the type of something.
 data TypeDeclBase f vn =
   TypeDecl { declaredType :: TypeExp vn
@@ -473,7 +468,7 @@
 -- | An identifier consists of its name and the type of the value
 -- bound to the identifier.
 data IdentBase f vn = Ident { identName   :: vn
-                            , identType   :: f CompType
+                            , identType   :: f PatternType
                             , identSrcLoc :: SrcLoc
                             }
 deriving instance Showable f vn => Show (IdentBase f vn)
@@ -555,8 +550,20 @@
 data QualName vn = QualName { qualQuals :: ![vn]
                             , qualLeaf  :: !vn
                             }
-  deriving (Eq, Ord, Show)
+  deriving (Show)
 
+instance Eq (QualName Name) where
+  QualName qs1 v1 == QualName qs2 v2 = qs1 == qs2 && v1 == v2
+
+instance Eq (QualName VName) 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
+  QualName _ v1 `compare` QualName _ v2 = compare v1 v2
+
 instance Functor QualName where
   fmap = fmapDefault
 
@@ -579,10 +586,10 @@
 data ExpBase f vn =
               Literal PrimValue SrcLoc
 
-            | IntLit Integer (f (TypeBase () ())) SrcLoc
+            | IntLit Integer (f PatternType) SrcLoc
             -- ^ A polymorphic integral literal.
 
-            | FloatLit Double (f (TypeBase () ())) SrcLoc
+            | FloatLit Double (f PatternType) SrcLoc
             -- ^ A polymorphic decimal literal.
 
             | Parens (ExpBase f vn) SrcLoc
@@ -596,23 +603,23 @@
             | RecordLit [FieldBase f vn] SrcLoc
             -- ^ Record literals, e.g. @{x=2,y=3,z}@.
 
-            | ArrayLit  [ExpBase f vn] (f CompType) SrcLoc
+            | ArrayLit  [ExpBase f vn] (f PatternType) SrcLoc
             -- ^ Array literals, e.g., @[ [1+x, 3], [2, 1+4] ]@.
             -- Second arg is the row type of the rows of the array.
 
-            | Range (ExpBase f vn) (Maybe (ExpBase f vn)) (Inclusiveness (ExpBase f vn)) (f CompType) SrcLoc
+            | Range (ExpBase f vn) (Maybe (ExpBase f vn)) (Inclusiveness (ExpBase f vn)) (f PatternType) SrcLoc
 
             | Var (QualName vn) (f PatternType) SrcLoc
 
-            | Ascript (ExpBase f vn) (TypeDeclBase f vn) SrcLoc
+            | Ascript (ExpBase f vn) (TypeDeclBase f vn) (f PatternType) SrcLoc
             -- ^ Type ascription: @e : t@.
 
-            | LetPat [TypeParamBase vn] (PatternBase f vn) (ExpBase f vn) (ExpBase f vn) SrcLoc
+            | LetPat [TypeParamBase vn] (PatternBase f vn) (ExpBase f vn) (ExpBase f vn) (f PatternType) SrcLoc
 
             | LetFun vn ([TypeParamBase vn], [PatternBase f vn], Maybe (TypeExp vn), f StructType, ExpBase f vn)
               (ExpBase f vn) SrcLoc
 
-            | If     (ExpBase f vn) (ExpBase f vn) (ExpBase f vn) (f CompType) SrcLoc
+            | If     (ExpBase f vn) (ExpBase f vn) (ExpBase f vn) (f PatternType) SrcLoc
 
             | Apply (ExpBase f vn) (ExpBase f vn) (f Diet) (f PatternType) SrcLoc
 
@@ -620,7 +627,7 @@
               -- ^ Numeric negation (ugly special case; Haskell did it first).
 
             | Lambda [TypeParamBase vn] [PatternBase f vn] (ExpBase f vn)
-              (Maybe (TypeDeclBase f vn)) (f (Aliasing, StructType)) SrcLoc
+              (Maybe (TypeExp vn)) (f (Aliasing, StructType)) SrcLoc
 
             | OpSection (QualName vn) (f PatternType) SrcLoc
               -- ^ @+@; first two types are operands, third is result.
@@ -647,70 +654,19 @@
               (ExpBase f vn, f StructType) (ExpBase f vn, f StructType)
               (f PatternType) SrcLoc
 
-            | Project Name (ExpBase f vn) (f CompType) SrcLoc
+            | Project Name (ExpBase f vn) (f PatternType) SrcLoc
 
             -- Primitive array operations
             | LetWith (IdentBase f vn) (IdentBase f vn)
                       [DimIndexBase f vn] (ExpBase f vn)
-                      (ExpBase f vn) SrcLoc
+                      (ExpBase f vn) (f PatternType) SrcLoc
 
-            | Index (ExpBase f vn) [DimIndexBase f vn] (f CompType) SrcLoc
+            | Index (ExpBase f vn) [DimIndexBase f vn] (f PatternType) SrcLoc
 
             | Update (ExpBase f vn) [DimIndexBase f vn] (ExpBase f vn) SrcLoc
 
             | RecordUpdate (ExpBase f vn) [Name] (ExpBase f vn) (f PatternType) SrcLoc
 
-            -- Second-Order Array Combinators accept curried and
-            -- anonymous functions as first params.
-            | Map (ExpBase f vn) (ExpBase f vn) (f CompType) SrcLoc
-             -- ^ @map (+1) [1, 2, ..., n] = [2, 3, ..., n+1]@.
-
-            | Reduce Commutativity (ExpBase f vn) (ExpBase f vn) (ExpBase f vn) SrcLoc
-             -- ^ @reduce (+) 0 ([1,2,...,n]) = (0+1+2+...+n)@.
-
-            | GenReduce (ExpBase f vn) (ExpBase f vn) (ExpBase f vn)
-                        (ExpBase f vn) (ExpBase f vn) SrcLoc
-             -- ^ @gen_reduce [1,1,1] (+) 0 [1,1,1] [1,1,1] = [4,1,1]@
-
-            | Scan (ExpBase f vn) (ExpBase f vn) (ExpBase f vn) SrcLoc
-             -- ^ @scan (+) 0 ([ 1, 2, 3 ]) = [ 1, 3, 6 ]@.
-
-            | Filter (ExpBase f vn) (ExpBase f vn) SrcLoc
-            -- ^ Return those elements of the array that satisfy the
-            -- predicate.
-
-            | Partition Int (ExpBase f vn) (ExpBase f vn) SrcLoc
-            -- ^ @partition k f a@, where @f@ returns an integer,
-            -- returns a tuple @(a', is)@ that describes a
-            -- partitioning of @a@ into @n@ equivalence classes.
-            -- Here, @a'@ is a re-ordering of @a@, and @is@ is an
-            -- array of @k@ offsets into @a'@.
-
-            | Stream (StreamForm f vn) (ExpBase f vn) (ExpBase f vn) SrcLoc
-            -- ^ Streaming: intuitively, this gives a size-parameterized
-            -- composition for SOACs that cannot be fused, e.g., due to scan.
-            -- For example, assuming @A : [int], f : int->int, g : real->real@,
-            -- the code: @let x = map(f,A) in let y = scan(op+,0,x) in map(g,y)@
-            -- can be re-written (streamed) in the source-Futhark language as:
-            -- @let (acc, z) =@
-            -- @  stream (fn (int,[real]) (real chunk, real acc, [int] a) =>@
-            -- @            let x = map (f,         A )@
-            -- @            let y0= scan(op +, 0,   x )@
-            -- @            let y = map (op +(acc), y0)@
-            -- @            ( acc+y0[chunk-1], map(g, y) )@
-            -- @         ) 0 A@
-            -- where (i)  @chunk@ is a symbolic int denoting the chunk
-            -- size, (ii) @0@ is the initial value of the accumulator,
-            -- which allows the streaming of @scan@.
-            -- Finally, the unnamed function (@fn...@) implements the a fold that:
-            -- computes the accumulator of @scan@, as defined inside its body, AND
-            -- implicitly concatenates each of the result arrays across
-            -- the iteration space.
-            -- In essence, sequential codegen can choose chunk = 1 and thus
-            -- eliminate the SOACs on the outermost level, while parallel codegen
-            -- may choose the maximal chunk size that still satisfies the memory
-            -- requirements of the device.
-
             | Unsafe (ExpBase f vn) SrcLoc
             -- ^ Explore the Danger Zone and elide safety checks on
             -- array operations and other assertions during execution
@@ -722,18 +678,14 @@
             -- and return the value of the second expression if it
             -- does.
 
-            | VConstr0 Name (f CompType) SrcLoc
+            | VConstr0 Name (f PatternType) SrcLoc
             -- ^ An enum element, e.g., @#foo@.
 
-            | Match (ExpBase f vn) [CaseBase f vn] (f CompType) SrcLoc
+            | Match (ExpBase f vn) [CaseBase f vn] (f PatternType) SrcLoc
             -- ^ A match expression.
 
 deriving instance Showable f vn => Show (ExpBase f vn)
 
-data StreamForm f vn = MapLike    StreamOrd
-                     | RedLike    StreamOrd Commutativity (ExpBase f vn)
-deriving instance Showable f vn => Show (StreamForm f vn)
-
 instance Located (ExpBase f vn) where
   locOf (Literal _ loc)                = locOf loc
   locOf (IntLit _ _ loc)               = locOf loc
@@ -748,21 +700,15 @@
   locOf (BinOp _ _ _ _ _ pos)          = locOf pos
   locOf (If _ _ _ _ pos)               = locOf pos
   locOf (Var _ _ loc)                  = locOf loc
-  locOf (Ascript _ _ loc)              = locOf loc
+  locOf (Ascript _ _ _ loc)            = locOf loc
   locOf (Negate _ pos)                 = locOf pos
   locOf (Apply _ _ _ _ pos)            = locOf pos
-  locOf (LetPat _ _ _ _ pos)           = locOf pos
+  locOf (LetPat _ _ _ _ _ loc)         = locOf loc
   locOf (LetFun _ _ _ loc)             = locOf loc
-  locOf (LetWith _ _ _ _ _ pos)        = locOf pos
+  locOf (LetWith _ _ _ _ _ _ loc)      = locOf loc
   locOf (Index _ _ _ loc)              = locOf loc
   locOf (Update _ _ _ pos)             = locOf pos
   locOf (RecordUpdate _ _ _ _ pos)     = locOf pos
-  locOf (Map _ _ _ loc)                = locOf loc
-  locOf (Reduce _ _ _ _ pos)           = locOf pos
-  locOf (GenReduce _ _ _ _ _ pos)      = locOf pos
-  locOf (Scan _ _ _ pos)               = locOf pos
-  locOf (Filter _ _ pos)               = locOf pos
-  locOf (Partition _ _ _ loc)          = locOf loc
   locOf (Lambda _ _ _ _ _ loc)         = locOf loc
   locOf (OpSection _ _ loc)            = locOf loc
   locOf (OpSectionLeft _ _ _ _ _ loc)  = locOf loc
@@ -770,7 +716,6 @@
   locOf (ProjectSection _ _ loc)       = locOf loc
   locOf (IndexSection _ _ loc)         = locOf loc
   locOf (DoLoop _ _ _ _ _ pos)         = locOf pos
-  locOf (Stream _ _ _  pos)            = locOf pos
   locOf (Unsafe _ loc)                 = locOf loc
   locOf (Assert _ _ _ loc)             = locOf loc
   locOf (VConstr0 _ _ loc)             = locOf loc
@@ -778,7 +723,7 @@
 
 -- | An entry in a record literal.
 data FieldBase f vn = RecordFieldExplicit Name (ExpBase f vn) SrcLoc
-                    | RecordFieldImplicit vn (f CompType) SrcLoc
+                    | RecordFieldImplicit vn (f PatternType) SrcLoc
 
 deriving instance Showable f vn => Show (FieldBase f 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
@@ -16,7 +16,7 @@
 -- tree.  The implementation is rather tedious, but the interface is
 -- easy to use.
 --
--- A traversal of the Futhark syntax tree is expressed as a tuple of
+-- A traversal of the Futhark syntax tree is expressed as a record of
 -- functions expressing the operations to be performed on the various
 -- types of nodes.
 module Language.Futhark.Traversals
@@ -35,8 +35,6 @@
     mapOnExp         :: ExpBase Info VName -> m (ExpBase Info VName)
   , mapOnName        :: VName -> m VName
   , mapOnQualName    :: QualName VName -> m (QualName VName)
-  , mapOnType        :: TypeBase () () -> m (TypeBase () ())
-  , mapOnCompType    :: CompType -> m CompType
   , mapOnStructType  :: StructType -> m StructType
   , mapOnPatternType :: PatternType -> m PatternType
   }
@@ -55,9 +53,9 @@
   astMap _ (Literal val loc) =
     pure $ Literal val loc
   astMap tv (IntLit val t loc) =
-    IntLit val <$> traverse (mapOnType tv) t <*> pure loc
+    IntLit val <$> traverse (mapOnPatternType tv) t <*> pure loc
   astMap tv (FloatLit val t loc) =
-    FloatLit val <$> traverse (mapOnType tv) t <*> pure loc
+    FloatLit val <$> traverse (mapOnPatternType tv) t <*> pure loc
   astMap tv (Parens e loc) =
     Parens <$> mapOnExp tv e <*> pure loc
   astMap tv (QualParens name e loc) =
@@ -67,12 +65,13 @@
   astMap tv (RecordLit fields loc) =
     RecordLit <$> astMap tv fields <*> pure loc
   astMap tv (ArrayLit els t loc) =
-    ArrayLit <$> mapM (mapOnExp tv) els <*> traverse (mapOnCompType tv) t <*> pure loc
+    ArrayLit <$> mapM (mapOnExp tv) els <*> traverse (mapOnPatternType tv) t <*> pure loc
   astMap tv (Range start next end t loc) =
     Range <$> mapOnExp tv start <*> traverse (mapOnExp tv) next <*>
-    traverse (mapOnExp tv) end <*> traverse (mapOnCompType tv) t <*> pure loc
-  astMap tv (Ascript e tdecl loc) =
-    Ascript <$> mapOnExp tv e <*> astMap tv tdecl <*> pure loc
+    traverse (mapOnExp tv) end <*> traverse (mapOnPatternType tv) t <*> pure loc
+  astMap tv (Ascript e tdecl t loc) =
+    Ascript <$> mapOnExp tv e <*> astMap tv tdecl <*>
+    traverse (mapOnPatternType tv) t <*> pure loc
   astMap tv (BinOp fname t (x,xt) (y,yt) (Info rt) loc) =
     BinOp <$> mapOnQualName tv fname <*> traverse (mapOnPatternType tv) t <*>
     ((,) <$> mapOnExp tv x <*> traverse (mapOnStructType tv) xt) <*>
@@ -82,26 +81,26 @@
     Negate <$> mapOnExp tv x <*> pure loc
   astMap tv (If c texp fexp t loc) =
     If <$> mapOnExp tv c <*> mapOnExp tv texp <*> mapOnExp tv fexp <*>
-    traverse (mapOnCompType tv) t <*> pure loc
+    traverse (mapOnPatternType tv) t <*> pure loc
   astMap tv (Apply f arg d (Info t) loc) =
     Apply <$> mapOnExp tv f <*> mapOnExp tv arg <*>
     pure d <*> (Info <$> mapOnPatternType tv t) <*>
     pure loc
-  astMap tv (LetPat tparams pat e body loc) =
+  astMap tv (LetPat tparams pat e body t loc) =
     LetPat <$> mapM (astMap tv) tparams <*>
     astMap tv pat <*> mapOnExp tv e <*>
-    mapOnExp tv body <*> pure loc
+    mapOnExp tv body <*> traverse (mapOnPatternType tv) t <*> pure loc
   astMap tv (LetFun name (fparams, params, ret, t, e) body loc) =
     LetFun <$> mapOnName tv name <*>
     ((,,,,) <$> mapM (astMap tv) fparams <*> mapM (astMap tv) params <*>
      traverse (astMap tv) ret <*> traverse (mapOnStructType tv) t <*>
      mapOnExp tv e) <*>
     mapOnExp tv body <*> pure loc
-  astMap tv (LetWith dest src idxexps vexp body loc) =
+  astMap tv (LetWith dest src idxexps vexp body t loc) =
     pure LetWith <*>
          astMap tv dest <*> astMap tv src <*>
          mapM (astMap tv) idxexps <*> mapOnExp tv vexp <*>
-         mapOnExp tv body <*> pure loc
+         mapOnExp tv body <*> traverse (mapOnPatternType tv) t <*> pure loc
   astMap tv (Update src slice v loc) =
     Update <$> mapOnExp tv src <*> mapM (astMap tv) slice <*>
     mapOnExp tv v <*> pure loc
@@ -109,40 +108,17 @@
     RecordUpdate <$> mapOnExp tv src <*> pure fs <*>
     mapOnExp tv v <*> (Info <$> mapOnPatternType tv t) <*> pure loc
   astMap tv (Project field e t loc) =
-    Project field <$> mapOnExp tv e <*> traverse (mapOnCompType tv) t <*> pure loc
+    Project field <$> mapOnExp tv e <*> traverse (mapOnPatternType tv) t <*> pure loc
   astMap tv (Index arr idxexps t loc) =
     pure Index <*>
          astMap tv arr <*>
          mapM (astMap tv) idxexps <*>
-         traverse (mapOnCompType tv) t <*>
+         traverse (mapOnPatternType tv) t <*>
          pure loc
-  astMap tv (Map fun e t loc) =
-    Map <$> mapOnExp tv fun <*> mapOnExp tv e <*>
-    traverse (mapOnCompType tv) t <*> pure loc
-  astMap tv (Reduce comm fun startexp arrexp loc) =
-    Reduce comm <$> mapOnExp tv fun <*>
-    mapOnExp tv startexp <*> mapOnExp tv arrexp <*> pure loc
-  astMap tv (GenReduce hist op ne bfun img loc) =
-    GenReduce <$> mapOnExp tv hist <*> mapOnExp tv op <*> mapOnExp tv ne
-    <*> mapOnExp tv bfun <*> mapOnExp tv img <*> pure loc
   astMap tv (Unsafe e loc) =
     Unsafe <$> mapOnExp tv e <*> pure loc
   astMap tv (Assert e1 e2 desc loc) =
     Assert <$> mapOnExp tv e1 <*> mapOnExp tv e2 <*> pure desc <*> pure loc
-  astMap tv (Scan fun startexp arrexp loc) =
-    pure Scan <*> mapOnExp tv fun <*>
-         mapOnExp tv startexp <*> mapOnExp tv arrexp <*>
-         pure loc
-  astMap tv (Filter fun arrexp loc) =
-    pure Filter <*> mapOnExp tv fun <*> mapOnExp tv arrexp <*> pure loc
-  astMap tv (Partition k fun arrexp loc) =
-    Partition k <$> mapOnExp tv fun <*> mapOnExp tv arrexp <*> pure loc
-  astMap tv (Stream form fun arr loc) =
-    pure Stream <*> mapOnStreamForm form <*> mapOnExp tv fun <*>
-         mapOnExp tv arr <*> pure loc
-    where mapOnStreamForm (MapLike o) = pure $ MapLike o
-          mapOnStreamForm (RedLike o comm lam) =
-              RedLike o comm <$> mapOnExp tv lam
   astMap tv (Lambda tparams params body ret t loc) =
     Lambda <$> mapM (astMap tv) tparams <*> mapM (astMap tv) params <*>
     astMap tv body <*> traverse (astMap tv) ret <*>
@@ -172,10 +148,10 @@
     mapOnExp tv mergeexp <*> astMap tv form <*>
     mapOnExp tv loopbody <*> pure loc
   astMap tv (VConstr0 name t loc) =
-    VConstr0 name <$> traverse (mapOnCompType tv) t <*> pure loc
+    VConstr0 name <$> traverse (mapOnPatternType tv) t <*> pure loc
   astMap tv (Match e cases t loc) =
     Match <$> mapOnExp tv e <*> astMap tv cases
-          <*> traverse (mapOnCompType tv) t <*> pure loc
+          <*> traverse (mapOnPatternType tv) t <*> pure loc
 
 instance ASTMappable (LoopFormBase Info VName) where
   astMap tv (For i bound) = For <$> astMap tv i <*> astMap tv bound
@@ -267,14 +243,6 @@
 traverseTypeArg _ g (TypeArgDim d loc) = TypeArgDim <$> g d <*> pure loc
 traverseTypeArg f g (TypeArgType t loc) = TypeArgType <$> traverseType f g pure t <*> pure loc
 
-instance ASTMappable (TypeBase () ()) where
-  astMap tv = traverseType f pure pure
-    where f = fmap typeNameFromQualName . mapOnQualName tv . qualNameFromTypeName
-
-instance ASTMappable CompType where
-  astMap tv = traverseType f pure (astMap tv)
-    where f = fmap typeNameFromQualName . mapOnQualName tv . qualNameFromTypeName
-
 instance ASTMappable StructType where
   astMap tv = traverseType f (astMap tv) pure
     where f = fmap typeNameFromQualName . mapOnQualName tv . qualNameFromTypeName
@@ -289,7 +257,7 @@
 
 instance ASTMappable (IdentBase Info VName) where
   astMap tv (Ident name (Info t) loc) =
-    Ident <$> mapOnName tv name <*> (Info <$> mapOnCompType tv t) <*> pure loc
+    Ident <$> mapOnName tv name <*> (Info <$> mapOnPatternType tv t) <*> pure loc
 
 instance ASTMappable (PatternBase Info VName) where
   astMap tv (Id name (Info t) loc) =
@@ -312,7 +280,7 @@
     RecordFieldExplicit name <$> mapOnExp tv e <*> pure loc
   astMap tv (RecordFieldImplicit name t loc) =
     RecordFieldImplicit <$> mapOnName tv name
-    <*> traverse (mapOnCompType tv) t <*> pure loc
+    <*> traverse (mapOnPatternType tv) t <*> pure loc
 
 instance ASTMappable (CaseBase Info VName) where
   astMap tv (CasePat pat e loc) =
diff --git a/src/Language/Futhark/TypeChecker.hs b/src/Language/Futhark/TypeChecker.hs
--- a/src/Language/Futhark/TypeChecker.hs
+++ b/src/Language/Futhark/TypeChecker.hs
@@ -389,8 +389,11 @@
 
   -- Apply type abbreviations from a_mty to body_mty.
   let a_abbrs = mtyTypeAbbrs a_mty
-  let type_subst = M.mapMaybe (fmap TypeSub . (`M.lookup` a_abbrs)) p_subst
-  let body_mty' = substituteTypesInMTy type_subst body_mty
+      isSub v = case M.lookup v a_abbrs of
+                  Just abbr -> Just $ TypeSub abbr
+                  _  -> Just $ DimSub $ NamedDim $ qualName v
+      type_subst = M.mapMaybe isSub p_subst
+      body_mty' = substituteTypesInMTy type_subst body_mty
   (body_mty'', body_subst) <- newNamesForMTy body_mty'
   return (body_mty'', p_subst, body_subst)
 
@@ -696,8 +699,11 @@
     matchVal loc spec_name spec_t name t
       | matchFunBinding loc spec_t t = return (spec_name, name)
     matchVal loc spec_name spec_v _ v =
-      Left $ TypeError loc $ "Value " ++ quote (baseString spec_name) ++ " specified as type " ++
-      ppValBind spec_v ++ " in signature, but has " ++ ppValBind v ++ " in structure."
+      Left $ TypeError loc $ unlines $
+      ["Module type specifies"] ++
+      map ("  "++) (lines $ ppValBind spec_name spec_v) ++
+      ["but module provides"] ++
+      map ("  "++) (lines $ppValBind spec_name v)
 
     matchFunBinding :: SrcLoc -> BoundV -> BoundV -> Bool
     matchFunBinding loc (BoundV _ orig_spec_t) (BoundV tps orig_t) =
@@ -752,7 +758,8 @@
                indent $ ppTypeAbbr abs name mod_t,
                "but module type requires this type to be non-functional."]
 
-    ppValBind (BoundV tps t) = unwords $ map pretty tps ++ [pretty t]
+    ppValBind v (BoundV tps t) =
+      unwords $ ["val", prettyName v] ++ map pretty tps ++ [":", pretty t]
 
     ppTypeAbbr abs name (ps, t) =
       "type " ++ unwords (pretty name : map pretty ps) ++ t'
@@ -804,6 +811,10 @@
   where subT name _
           | Just (TypeSub (TypeAbbr l ps t)) <- M.lookup name substs = TypeAbbr l ps t
         subT _ (TypeAbbr l ps t) = TypeAbbr l ps $ substituteTypes substs t
+
+substituteTypesInBoundV :: TypeSubs -> BoundV -> BoundV
+substituteTypesInBoundV substs (BoundV tps t) =
+  BoundV tps (substituteTypes substs t)
 
 allNamesInMTy :: MTy -> S.Set VName
 allNamesInMTy (MTy abs mod) =
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
@@ -208,7 +208,7 @@
   lookupMod :: SrcLoc -> QualName Name -> m (QualName VName, Mod)
   lookupMTy :: SrcLoc -> QualName Name -> m (QualName VName, MTy)
   lookupImport :: SrcLoc -> FilePath -> m (FilePath, Env)
-  lookupVar :: SrcLoc -> QualName Name -> m (QualName VName, CompType)
+  lookupVar :: SrcLoc -> QualName Name -> m (QualName VName, PatternType)
 
 checkName :: MonadTypeChecker m => Namespace -> Name -> SrcLoc -> m VName
 checkName space name loc = qualLeaf <$> checkQualName space (qualName name) loc
@@ -278,7 +278,7 @@
             case getType t of
               Left{} -> throwError $ TypeError loc $
                         "Attempt to use function " ++ baseString name ++ " as value."
-              Right t' -> return (qn', removeShapeAnnotations $ fromStruct $
+              Right t' -> return (qn', fromStruct $
                                        qualifyTypeVars outer_env mempty qs t')
 
 -- | Extract from a type either a function type comprising a list of
@@ -320,8 +320,6 @@
   where mapper = ASTMapper { mapOnExp = pure
                            , mapOnName = pure
                            , mapOnQualName = pure . qual
-                           , mapOnType = pure
-                           , mapOnCompType = pure
                            , mapOnStructType = pure
                            , mapOnPatternType = pure
                            }
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
@@ -183,7 +183,7 @@
 -- | Get the type of an expression, with all type variables
 -- substituted.  Never call 'typeOf' directly (except in a few
 -- carefully inspected locations)!
-expType :: Exp -> TermTypeM CompType
+expType :: Exp -> TermTypeM PatternType
 expType = normaliseType . typeOf
 
 -- | The state is a set of constraints and a counter for generating
@@ -295,7 +295,7 @@
 
     t <- case M.lookup name $ scopeVtable scope of
       Nothing -> throwError $ TypeError loc $
-                 "Missing component for module " ++ quote (pretty qn) ++ "."
+                 "Unknown variable " ++ quote (pretty qn) ++ "."
 
       Just (WasConsumed wloc) -> useAfterConsume (baseName name) loc wloc
 
@@ -304,7 +304,7 @@
         | otherwise -> do
             (tnames, t') <- instantiateTypeScheme loc tparams t
             let qual = qualifyTypeVars outer_env tnames qs
-            qual . removeShapeAnnotations <$> normaliseType t'
+            qual . anyDimShapeAnnotations <$> normaliseType t'
 
       Just OpaqueF -> do
         argtype <- newTypeVar loc "t"
@@ -320,7 +320,8 @@
         argtype <- newTypeVar loc "t"
         mustBeOneOf ts loc argtype
         let (pts', rt') = instOverloaded argtype pts rt
-        return $ fromStruct $ foldr (Arrow mempty Nothing) rt' pts'
+        return $ fromStruct $ vacuousShapeAnnotations $
+         foldr (Arrow mempty Nothing) rt' pts'
 
     observe $ Ident name (Info t) loc
     return (qn', t)
@@ -379,20 +380,19 @@
 instantiateTypeScheme loc tparams t = do
   let tparams' = filter isTypeParam tparams
       tnames = map typeParamName tparams'
-  (fresh_tnames, inst_list) <- unzip <$> mapM (instantiateTypeParam loc) tparams'
-  let substs = M.fromList $ zip tnames $
-               map (Subst . vacuousShapeAnnotations) inst_list
-      t' = substTypesAny (`M.lookup` substs) t
+  (fresh_tnames, substs) <- unzip <$> mapM (instantiateTypeParam loc) tparams'
+  let substs' = M.fromList $ zip tnames substs
+      t' = substTypesAny (`M.lookup` substs') t
   return (fresh_tnames, t')
 
 -- | Create a new type name and insert it (unconstrained) in the
 -- substitution map.
-instantiateTypeParam :: Monoid as => SrcLoc -> TypeParam -> TermTypeM (VName, TypeBase dim as)
+instantiateTypeParam :: Monoid as => SrcLoc -> TypeParam -> TermTypeM (VName, Subst (TypeBase dim as))
 instantiateTypeParam loc tparam = do
   i <- incCounter
   v <- newID $ mkTypeVarName (takeWhile isAlpha (baseString (typeParamName tparam))) i
   modifyConstraints $ M.insert v $ NoConstraint (Just l) loc
-  return (v, TypeVar mempty Nonunique (typeName v) [])
+  return (v, Subst $ TypeVar mempty Nonunique (typeName v) [])
   where l = case tparam of TypeParamType x _ _ -> x
                            _                   -> Lifted
 
@@ -438,15 +438,15 @@
 -- | Determine if two types are identical, ignoring uniqueness.
 -- Causes a 'TypeError' if they fail to match, and otherwise returns
 -- one of them.
-unifyExpTypes :: Exp -> Exp -> TermTypeM CompType
+unifyExpTypes :: Exp -> Exp -> TermTypeM PatternType
 unifyExpTypes e1 e2 = do
   e1_t <- expType e1
   e2_t <- expType e2
-  unify (srclocOf e2) (toStruct e1_t) (toStruct e2_t)
+  unify (srclocOf e2) (toStructural e1_t) (toStructural e2_t)
   return $ unifyTypeAliases e1_t e2_t
 
 -- | Assumes that the two types have already been unified.
-unifyTypeAliases :: CompType -> CompType -> CompType
+unifyTypeAliases :: PatternType -> PatternType -> PatternType
 unifyTypeAliases t1 t2 =
   case (t1, t2) of
     (Array als1 u1 et1 shape1, Array als2 u2 et2 _) ->
@@ -558,15 +558,15 @@
   e' <- checkExp e
   t' <- expType e'
   unify loc (toStructural t') (toStructural t)
-  return $ PatternLit e' (Info (vacuousShapeAnnotations t')) loc
+  return $ PatternLit e' (Info t') loc
 
 checkPattern' (PatternLit e NoInfo loc) NoneInferred = do
   e' <- checkExp e
   t' <- expType e'
-  return $ PatternLit e' (Info (vacuousShapeAnnotations t')) loc
+  return $ PatternLit e' (Info t') loc
 
 bindPatternNames :: PatternBase NoInfo Name -> TermTypeM a -> TermTypeM a
-bindPatternNames = bindSpaced . map asTerm . S.toList . patIdentSet
+bindPatternNames = bindSpaced . map asTerm . S.toList . patternIdents
   where asTerm v = (Term, identName v)
 
 checkPattern :: UncheckedPattern -> InferredType -> (Pattern -> TermTypeM a)
@@ -592,7 +592,7 @@
                 | otherwise = BoundV l tparams (in_t `addAliases` S.insert (AliasBound name))
               update b = b
 
-              tp' = vacuousShapeAnnotations tp `addAliases` S.insert (AliasBound name)
+              tp' = tp `addAliases` S.insert (AliasBound name)
           in scope { scopeVtable = M.insert name (BoundV Local [] tp') $
                                    adjustSeveral update inedges $
                                    scopeVtable scope
@@ -649,7 +649,7 @@
   Just $ Ident v (Info (Prim (Signed Int32))) loc
 typeParamIdent _ = Nothing
 
-bindingIdent :: IdentBase NoInfo Name -> CompType -> (Ident -> TermTypeM a)
+bindingIdent :: IdentBase NoInfo Name -> PatternType -> (Ident -> TermTypeM a)
              -> TermTypeM a
 bindingIdent (Ident v NoInfo vloc) t m =
   bindSpaced [(Term, v)] $ do
@@ -658,14 +658,14 @@
     binding [ident] $ m ident
 
 bindingPatternGroup :: [UncheckedTypeParam]
-                    -> [(UncheckedPattern, InferredType)]
+                    -> [UncheckedPattern]
                     -> ([TypeParam] -> [Pattern] -> TermTypeM a) -> TermTypeM a
 bindingPatternGroup tps orig_ps m = do
-  checkForDuplicateNames $ map fst orig_ps
+  checkForDuplicateNames orig_ps
   checkTypeParams tps $ \tps' -> bindingTypeParams tps' $ do
-    let descend ps' ((p,t):ps) =
-          checkPattern p t $ \p' ->
-            binding (S.toList $ patIdentSet p') $ descend (p':ps') ps
+    let descend ps' (p:ps) =
+          checkPattern p NoneInferred $ \p' ->
+            binding (S.toList $ patternIdents p') $ descend (p':ps') ps
         descend ps' [] = do
           -- Perform an observation of every type parameter.  This
           -- prevents unused-name warnings for otherwise unused
@@ -684,7 +684,7 @@
 bindingPattern tps p t m = do
   checkForDuplicateNames [p]
   checkTypeParams tps $ \tps' -> bindingTypeParams tps' $
-    checkPattern p t $ \p' -> binding (S.toList $ patIdentSet p') $ do
+    checkPattern p t $ \p' -> binding (S.toList $ patternIdents p') $ do
       -- Perform an observation of every declared dimension.  This
       -- prevents unused-name warnings for otherwise unused dimensions.
       mapM_ observe $ patternDims p'
@@ -727,12 +727,12 @@
 -- | @require ts e@ causes a 'TypeError' if @expType e@ is not one of
 -- the types in @ts@.  Otherwise, simply returns @e@.
 require :: [PrimType] -> Exp -> TermTypeM Exp
-require ts e = do mustBeOneOf ts (srclocOf e) . toStruct =<< expType e
+require ts e = do mustBeOneOf ts (srclocOf e) . toStructural =<< expType e
                   return e
 
 unifies :: TypeBase () () -> Exp -> TermTypeM Exp
 unifies t e = do
-  unify (srclocOf e) t =<< toStruct <$> expType e
+  unify (srclocOf e) t =<< toStructural <$> expType e
   return e
 
 -- The closure of a lambda or local function are those variables that
@@ -745,7 +745,7 @@
                     _ -> False
   return $ S.map AliasBound $ S.filter isLocal $
     allOccuring closure S.\\
-    S.map identName (mconcat (map patIdentSet params))
+    S.map identName (mconcat (map patternIdents params))
 
 checkExp :: UncheckedExp -> TermTypeM Exp
 
@@ -755,12 +755,12 @@
 checkExp (IntLit val NoInfo loc) = do
   t <- newTypeVar loc "t"
   mustBeOneOf anyNumberType loc t
-  return $ IntLit val (Info t) loc
+  return $ IntLit val (Info $ vacuousShapeAnnotations $ fromStruct t) loc
 
 checkExp (FloatLit val NoInfo loc) = do
   t <- newTypeVar loc "t"
   mustBeOneOf anyFloatType loc t
-  return $ FloatLit val (Info t) loc
+  return $ FloatLit val (Info $ vacuousShapeAnnotations $ fromStruct t) loc
 
 checkExp (TupLit es loc) =
   TupLit <$> mapM checkExp es <*> pure loc
@@ -795,14 +795,14 @@
   -- multidimensional array literals.
   case all_es of
     [] -> do et <- newTypeVar loc "t"
-             t <- arrayOfM loc et (rank 1) Unique
+             t <- arrayOfM loc et (ShapeDecl [AnyDim]) Unique
              return $ ArrayLit [] (Info t) loc
     e:es -> do
       e' <- checkExp e
       et <- expType e'
       es' <- mapM (unifies (toStructural et) <=< checkExp) es
       et' <- normaliseType et
-      t <- arrayOfM loc et' (rank 1) Unique
+      t <- arrayOfM loc et' (ShapeDecl [AnyDim]) Unique
       return $ ArrayLit (e':es') (Info t) loc
 
 checkExp (Range start maybe_step end NoInfo loc) = do
@@ -825,24 +825,25 @@
 
   t <- arrayOfM loc start_t (rank 1) Unique
 
-  return $ Range start' maybe_step' end' (Info (t `setAliases` mempty)) loc
+  return $ Range start' maybe_step' end'
+    (Info (vacuousShapeAnnotations t `setAliases` mempty)) loc
 
-checkExp (Ascript e decl loc) = do
+checkExp (Ascript e decl NoInfo loc) = do
   decl' <- checkTypeDecl decl
   e' <- checkExp e
-  t <- toStruct <$> expType e'
-  let decl_t = removeShapeAnnotations $ unInfo $ expandedType decl'
-  unify loc decl_t t
+  t <- expType e'
+  let decl_t = unInfo $ expandedType decl'
+  unify loc (toStructural decl_t) (toStructural t)
 
   -- We also have to make sure that uniqueness matches.  This is done
   -- explicitly, because uniqueness is ignored by unification.
   t' <- normaliseType t
   decl_t' <- normaliseType decl_t
-  unless (t' `subtypeOf` decl_t') $
-    typeError loc $ "Type \"" ++ pretty t' ++ " is not a subtype of \"" ++
-    pretty decl_t' ++ "\"."
+  unless (t' `subtypeOf` anyDimShapeAnnotations decl_t') $
+    typeError loc $ "Type " ++ quote (pretty t') ++ " is not a subtype of " ++
+    quote (pretty decl_t') ++ "."
 
-  return $ Ascript e' decl' loc
+  return $ Ascript e' decl' (Info (combineTypeShapes t $ fromStruct decl_t)) loc
 
 checkExp (BinOp op NoInfo (e1,_) (e2,_) NoInfo loc) = do
   (op', ftype) <- lookupVar loc op
@@ -850,9 +851,9 @@
   (e2', e2_arg) <- checkArg e2
 
   (p1_t, rt) <- checkApply loc ftype e1_arg
-  (p2_t, rt') <- checkApply loc (removeShapeAnnotations rt) e2_arg
+  (p2_t, rt') <- checkApply loc rt e2_arg
 
-  return $ BinOp op' (Info (vacuousShapeAnnotations ftype))
+  return $ BinOp op' (Info ftype)
     (e1', Info $ toStruct p1_t) (e2', Info $ toStruct p2_t)
     (Info rt') loc
 
@@ -871,7 +872,7 @@
   return $ If e1' e2' e3' (Info t') loc
   where checkCond = do
           e1' <- checkExp e1
-          unify (srclocOf e1') (Prim Bool) . toStruct =<< expType e1'
+          unify (srclocOf e1') (Prim Bool) . toStructural =<< expType e1'
           return e1'
 
 checkExp (Parens e loc) =
@@ -899,7 +900,7 @@
 
   (qn', t, fields) <- findRootVar (qualQuals qn) (qualLeaf qn)
 
-  foldM checkField (Var qn' (Info $ vacuousShapeAnnotations t) loc) fields
+  foldM checkField (Var qn' (Info t) loc) fields
 
   where findRootVar qs name =
           (whenFound <$> lookupVar loc (QualName qs name)) `catchError` notFound qs name
@@ -929,7 +930,7 @@
   (t1, rt) <- checkApply loc t arg
   return $ Apply e1' e2' (Info $ diet t1) (Info rt) loc
 
-checkExp (LetPat tparams pat e body loc) = do
+checkExp (LetPat tparams pat e body NoInfo loc) = do
   noTypeParamsPermitted tparams
   sequentially (checkExp e) $ \e' e_occs -> do
     -- Not technically an ascription, but we want the pattern to have
@@ -940,9 +941,10 @@
         let msg = "of value computed with consumption at " ++ locStr (location c)
         in zeroOrderType loc msg t
       _ -> return ()
-    bindingPattern tparams pat (Ascribed $ vacuousShapeAnnotations t) $ \tparams' pat' -> do
+    bindingPattern tparams pat (Ascribed $ anyDimShapeAnnotations t) $ \tparams' pat' -> do
       body' <- checkExp body
-      return $ LetPat tparams' pat' e' body' loc
+      body_t <- unscopeType (S.map identName $ patternIdents pat') <$> expType body'
+      return $ LetPat tparams' pat' e' body' (Info body_t) loc
 
 checkExp (LetFun name (tparams, params, maybe_retdecl, NoInfo, e) body loc) =
   sequentially (checkFunDef' (name, maybe_retdecl, tparams, params, e, loc)) $
@@ -959,13 +961,11 @@
 
     return $ LetFun name' (tparams', params', maybe_retdecl', Info rettype, e') body' loc
 
-checkExp (LetWith dest src idxes ve body loc) = do
+checkExp (LetWith dest src idxes ve body NoInfo loc) = do
   (t, _) <- newArrayType (srclocOf src) "src" $ length idxes
   let elemt = stripArray (length $ filter isFix idxes) t
   sequentially (checkIdent src) $ \src' _ -> do
-    let src'' = Var (qualName $ identName src')
-                    (vacuousShapeAnnotations <$> identType src')
-                    (srclocOf src)
+    let src'' = Var (qualName $ identName src') (identType src') (srclocOf src)
     void $ unifies t src''
 
     unless (unique $ unInfo $ identType src') $
@@ -988,7 +988,8 @@
 
       bindingIdent dest (unInfo (identType src') `setAliases` S.empty) $ \dest' -> do
         body' <- consuming src' $ checkExp body
-        return $ LetWith dest' src' idxes' ve' body' loc
+        body_t <- unscopeType (S.singleton $ identName dest') <$> expType body'
+        return $ LetWith dest' src' idxes' ve' body' (Info body_t) loc
   where isFix DimFix{} = True
         isFix _        = False
 
@@ -1019,15 +1020,16 @@
   ve' <- checkExp ve
   a <- expType src'
   r <- foldM (flip $ mustHaveField loc) a fields
-  unify loc (toStruct r) . toStruct =<< expType ve'
-  return $ RecordUpdate src' fields ve'
-    (Info $ vacuousShapeAnnotations $ fromStruct a) loc
+  unify loc (toStructural r) . toStructural =<< expType ve'
+  return $ RecordUpdate src' fields ve' (Info $ fromStruct a) loc
 
 checkExp (Index e idxes NoInfo loc) = do
   (t, _) <- newArrayType (srclocOf e) "e" $ length idxes
   e' <- unifies t =<< checkExp e
   idxes' <- mapM checkDimIndex idxes
-  t' <- stripArray (length $ filter isFix idxes) <$> normaliseType (typeOf e')
+  t' <- anyDimShapeAnnotations .
+        stripArray (length $ filter isFix idxes) <$>
+        normaliseType (typeOf e')
   return $ Index e' idxes' (Info t') loc
   where isFix DimFix{} = True
         isFix _        = False
@@ -1040,34 +1042,30 @@
   e2' <- checkExp e2
   return $ Assert e1' e2' (Info (pretty e1)) loc
 
-checkExp Map{} = error "Map nodes should not appear in source program"
-checkExp Reduce{} = error "Reduce nodes should not appear in source program"
-checkExp GenReduce{} = error "GenReduce nodes should not appear in source program"
-checkExp Scan{} = error "Scan nodes should not appear in source program"
-checkExp Filter{} = error "Filter nodes should not appear in source program"
-checkExp Partition{} = error "Partition nodes should not appear in source program"
-checkExp Stream{} = error "Stream nodes should not appear in source program"
-
-checkExp (Lambda tparams params body maybe_retdecl NoInfo loc) =
+checkExp (Lambda tparams params body rettype_te NoInfo loc) =
   removeSeminullOccurences $
-  bindingPatternGroup tparams (zip params $ repeat NoneInferred) $ \tparams' params' -> do
-    maybe_retdecl' <- traverse checkTypeDecl maybe_retdecl
-    (body', closure) <- tapOccurences $ noUnique $
-                        checkFunBody body (unInfo . expandedType <$> maybe_retdecl') loc
+  bindingPatternGroup tparams params $ \tparams' params' -> do
+    rettype_checked <- traverse checkTypeExp rettype_te
+    let declared_rettype =
+          case rettype_checked of Just (_, st, _) -> Just st
+                                  Nothing -> Nothing
+    (body', closure) <-
+      tapOccurences $ noUnique $ checkFunBody body declared_rettype loc
     body_t <- expType body'
-    let (maybe_retdecl'', rettype) =
-          case maybe_retdecl' of
-            Just retdecl'@(TypeDecl _ (Info st)) -> (Just retdecl', st)
+    let (rettype', rettype_st) =
+          case rettype_checked of
+            Just (te, st, _) -> (Just te, st)
             Nothing -> (Nothing, inferReturnUniqueness params' body_t)
 
     checkGlobalAliases params' body_t loc
 
     closure' <- lexicalClosure params' closure
-    return $ Lambda tparams' params' body' maybe_retdecl'' (Info (closure', rettype)) loc
 
+    return $ Lambda tparams' params' body' rettype' (Info (closure', rettype_st)) loc
+
 checkExp (OpSection op _ loc) = do
   (op', ftype) <- lookupVar loc op
-  return $ OpSection op' (Info $ vacuousShapeAnnotations ftype) loc
+  return $ OpSection op' (Info ftype) loc
 
 checkExp (OpSectionLeft op _ e _ _ loc) = do
   (op', ftype) <- lookupVar loc op
@@ -1075,7 +1073,7 @@
   (t1, rt) <- checkApply loc ftype e_arg
   case rt of
     Arrow _ _ t2 rettype ->
-      return $ OpSectionLeft op' (Info (vacuousShapeAnnotations ftype)) e'
+      return $ OpSectionLeft op' (Info ftype) e'
       (Info $ toStruct t1, Info $ toStruct t2) (Info rettype) loc
     _ -> typeError loc $
          "Operator section with invalid operator of type " ++ pretty ftype
@@ -1087,7 +1085,7 @@
     Arrow as1 m1 t1 (Arrow as2 m2 t2 ret) -> do
       (t2', Arrow _ _ t1' rettype) <-
         checkApply loc (Arrow as2 m2 t2 (Arrow as1 m1 t1 ret)) e_arg
-      return $ OpSectionRight op' (Info (vacuousShapeAnnotations ftype)) e'
+      return $ OpSectionRight op' (Info ftype) e'
         (Info $ toStruct t1', Info $ toStruct t2') (Info rettype) loc
     _ -> typeError loc $
          "Operator section with invalid operator of type " ++ pretty ftype
@@ -1115,7 +1113,7 @@
 
   merge_t <- do
     merge_t <- expType mergeexp'
-    return $ Ascribed $ vacuousShapeAnnotations $ merge_t `setAliases` mempty
+    return $ Ascribed $ anyDimShapeAnnotations $ merge_t `setAliases` mempty
 
   -- First we do a basic check of the loop body to figure out which of
   -- the merge parameters are being consumed.  For this, we first need
@@ -1144,7 +1142,7 @@
         t <- expType e'
         case t of
           _ | Just t' <- peelArray 1 t ->
-                bindingPattern [] xpat (Ascribed $ vacuousShapeAnnotations t') $ \_ xpat' ->
+                bindingPattern [] xpat (Ascribed t') $ \_ xpat' ->
                 noUnique $ bindingPattern tparams mergepat merge_t $
                 \tparams' mergepat' -> onlySelfAliasing $ tapOccurences $ do
                   loopbody' <- checkExp loopbody
@@ -1185,7 +1183,7 @@
 
   where
     convergePattern pat body_cons body_t body_loc = do
-      let consumed_merge = S.map identName (patIdentSet pat) `S.intersection`
+      let consumed_merge = S.map identName (patternIdents pat) `S.intersection`
                            body_cons
           uniquePat (Wildcard (Info t) wloc) =
             Wildcard (Info $ t `setUniqueness` Nonunique) wloc
@@ -1211,7 +1209,7 @@
           pat' = uniquePat pat
 
       -- Now check that the loop returned the right type.
-      unify body_loc (toStruct body_t) $ toStruct $ patternType pat'
+      unify body_loc (toStructural body_t) $ toStructural $ patternType pat'
       body_t' <- normaliseType body_t
       pat_t <- normaliseType $ patternType pat'
       unless (body_t' `subtypeOf` pat_t) $
@@ -1272,25 +1270,25 @@
     zeroOrderType loc "returned from pattern match" t
     return $ Match e' cs' (Info t) loc
 
-checkCases :: CompType
+checkCases :: PatternType
            -> CaseBase NoInfo Name
            -> [CaseBase NoInfo Name]
-           -> TermTypeM ([CaseBase Info VName], CompType)
+           -> TermTypeM ([CaseBase Info VName], PatternType)
 checkCases mt c [] = do
   (c', t) <- checkCase mt c
   return ([c'], t)
 checkCases mt c (c2:cs) = do
   (((c', c_t), (cs', cs_t)), dflow) <-
     tapOccurences $ checkCase mt c `alternative` checkCases mt c2 cs
-  unify (srclocOf c) (toStruct c_t) (toStruct cs_t)
+  unify (srclocOf c) (toStructural c_t) (toStructural cs_t)
   let t = unifyTypeAliases c_t cs_t `addAliases`
         (`S.difference` S.map AliasBound (allConsumed dflow))
   return (c':cs', t)
 
-checkCase :: CompType -> CaseBase NoInfo Name
-          -> TermTypeM (CaseBase Info VName, CompType)
+checkCase :: PatternType -> CaseBase NoInfo Name
+          -> TermTypeM (CaseBase Info VName, PatternType)
 checkCase mt (CasePat p caseExp loc) =
-  bindingPattern [] p (Ascribed $ vacuousShapeAnnotations mt) $ \_ p' -> do
+  bindingPattern [] p (Ascribed mt) $ \_ p' -> do
     caseExp' <- checkExp caseExp
     caseType <- expType caseExp'
     return (CasePat p' caseExp' loc, caseType)
@@ -1355,8 +1353,6 @@
                            \e' -> checkUnmatched' e' >> return e'
                        , mapOnName        = pure
                        , mapOnQualName    = pure
-                       , mapOnType        = pure
-                       , mapOnCompType    = pure
                        , mapOnStructType  = pure
                        , mapOnPatternType = pure
                        }
@@ -1377,7 +1373,7 @@
         localUnmatched :: [Pattern] -> [Unmatched Pattern]
         localUnmatched [] = []
         localUnmatched ps'@(p':_) =
-          case vacuousShapeAnnotations $ patternType p'  of
+          case patternType p'  of
             Enum cs'' ->
               let matched = nub $ mapMaybe (pExp >=> constr) ps'
               in map (UnmatchedEnum . buildEnum (Enum cs'')) $ cs'' \\ matched
@@ -1400,7 +1396,7 @@
         pExp _ = Nothing
 
         constr (VConstr0 c _ _) = Just c
-        constr (Ascript e' _ _)  = constr e'
+        constr (Ascript e' _ _ _)  = constr e'
         constr _ = Nothing
 
         isPatternLit PatternLit{} = True
@@ -1418,7 +1414,7 @@
         bool _ = Nothing
 
         buildEnum t c =
-          PatternLit (VConstr0 c (Info t) noLoc) (Info (vacuousShapeAnnotations t)) noLoc
+          PatternLit (VConstr0 c (Info t) noLoc) (Info t) noLoc
         buildBool t b =
           PatternLit (Literal (BoolValue b) noLoc) (Info (vacuousShapeAnnotations t)) noLoc
         buildId t n =
@@ -1449,9 +1445,9 @@
   occur $ m1flow `seqOccurences` m2flow
   return b
 
-type Arg = (CompType, Occurences, SrcLoc)
+type Arg = (PatternType, Occurences, SrcLoc)
 
-argType :: Arg -> CompType
+argType :: Arg -> PatternType
 argType (t, _, _) = t
 
 checkArg :: UncheckedExp -> TermTypeM (Exp, Arg)
@@ -1460,10 +1456,10 @@
   arg_t <- expType arg'
   return (arg', (arg_t, dflow, srclocOf arg'))
 
-checkApply :: SrcLoc -> CompType -> Arg
+checkApply :: SrcLoc -> PatternType -> Arg
            -> TermTypeM (PatternType, PatternType)
 checkApply loc (Arrow as _ tp1 tp2) (argtype, dflow, argloc) = do
-  unify argloc (toStruct tp1) (toStruct argtype)
+  unify argloc (toStructural tp1) (toStructural argtype)
 
   -- Perform substitutions of instantiated variables in the types.
   tp1' <- normaliseType tp1
@@ -1482,12 +1478,12 @@
     _ -> return ()
 
   occur $ dflow `seqOccurences` occurs
-  let tp2'' = vacuousShapeAnnotations $ returnType tp2' (diet tp1') argtype'
-  return (vacuousShapeAnnotations tp1', tp2'')
+  let tp2'' = anyDimShapeAnnotations $ returnType tp2' (diet tp1') argtype'
+  return (tp1', tp2'')
 
 checkApply loc tfun@TypeVar{} arg = do
   tv <- newTypeVar loc "b"
-  unify loc (toStruct tfun) $ Arrow mempty Nothing (toStruct (argType arg)) tv
+  unify loc (toStructural tfun) $ Arrow mempty Nothing (toStructural (argType arg)) tv
   constraints <- getConstraints
   checkApply loc (applySubst (`lookupSubst` constraints) tfun) arg
 
@@ -1496,7 +1492,45 @@
   "Attempt to apply an expression of type " ++ pretty ftype ++
   " to an argument of type " ++ pretty (argType arg) ++ "."
 
-consumeArg :: SrcLoc -> CompType -> Diet -> TermTypeM [Occurence]
+-- | @returnType ret_type arg_diet arg_type@ gives result of applying
+-- an argument the given types to a function with the given return
+-- type, consuming the argument with the given diet.
+returnType :: PatternType
+           -> Diet
+           -> PatternType
+           -> PatternType
+returnType (Array _ Unique et shape) _ _ =
+  Array mempty Unique et shape
+returnType (Array als Nonunique et shape) d arg =
+  Array (als<>arg_als) Unique et shape -- Intentional!
+  where arg_als = aliases $ maskAliases arg d
+returnType (Record fs) d arg =
+  Record $ fmap (\et -> returnType et d arg) fs
+returnType (Prim t) _ _ = Prim t
+returnType (TypeVar _ Unique t targs) _ _ =
+  TypeVar mempty Unique t targs
+returnType (TypeVar als Nonunique t targs) d arg =
+  TypeVar (als<>arg_als) Unique t targs -- Intentional!
+  where arg_als = aliases $ maskAliases arg d
+returnType (Arrow _ v t1 t2) d arg =
+  Arrow als v (t1 `setAliases` mempty) (t2 `setAliases` als)
+  where als = aliases $ maskAliases arg d
+returnType (Enum cs) _ _ = Enum cs
+
+-- | @t `maskAliases` d@ removes aliases (sets them to 'mempty') from
+-- the parts of @t@ that are denoted as 'Consumed' by the 'Diet' @d@.
+maskAliases :: Monoid as =>
+               TypeBase shape as
+            -> Diet
+            -> TypeBase shape as
+maskAliases t Consume = t `setAliases` mempty
+maskAliases t Observe = t
+maskAliases (Record ets) (RecordDiet ds) =
+  Record $ M.intersectionWith maskAliases ets ds
+maskAliases t FuncDiet{} = t
+maskAliases _ _ = error "Invalid arguments passed to maskAliases."
+
+consumeArg :: SrcLoc -> PatternType -> Diet -> TermTypeM [Occurence]
 consumeArg loc (Record ets) (RecordDiet ds) =
   concat . M.elems <$> traverse (uncurry $ consumeArg loc) (M.intersectionWith (,) ets ds)
 consumeArg loc (Array _ Nonunique _ _) Consume =
@@ -1522,8 +1556,8 @@
 checkOneExp :: UncheckedExp -> TypeM ([TypeParam], Exp)
 checkOneExp e = fmap fst . runTermTypeM $ do
   e' <- checkExp e
-  let t = vacuousShapeAnnotations $ toStruct $ typeOf e'
-  tparams <- letGeneralise [] [t] mempty
+  let t = toStruct $ typeOf e'
+  tparams <- letGeneralise [] t mempty
   fixOverloadedTypes
   e'' <- updateExpTypes e'
   return (tparams, e'')
@@ -1603,7 +1637,7 @@
 
   then_substs <- getConstraints
 
-  bindingPatternGroup tparams (zip params $ repeat NoneInferred) $ \tparams' params' -> do
+  bindingPatternGroup tparams params $ \tparams' params' -> do
     maybe_retdecl' <- traverse checkTypeExp maybe_retdecl
 
     body' <- checkFunBody body ((\(_,t,_)->t) <$> maybe_retdecl') (maybe loc srclocOf maybe_retdecl)
@@ -1618,14 +1652,17 @@
 
         when (null params) $ nothingMustBeUnique loc rettype_structural
 
+        warnOnDubiousShapeAnnotations loc params'' retdecl_type
+
         return (Just retdecl', retdecl_type)
       Nothing
         | null params ->
-            return (Nothing, vacuousShapeAnnotations $ toStruct $ body_t `setUniqueness` Nonunique)
+            return (Nothing, toStruct $ body_t `setUniqueness` Nonunique)
         | otherwise ->
             return (Nothing, inferReturnUniqueness params'' body_t)
 
-    tparams'' <- letGeneralise tparams' (rettype : map patternStructType params'') then_substs
+    let fun_t = foldFunType (map patternStructType params'') rettype
+    tparams'' <- letGeneralise tparams' fun_t then_substs
 
     bindSpaced [(Term, fname)] $ do
       fname' <- checkName Term fname loc
@@ -1651,7 +1688,7 @@
           forM_ params' $ \p ->
           let consumedNonunique p' =
                 not (unique $ unInfo $ identType p') && (identName p' `S.member` names)
-          in case find consumedNonunique $ S.toList $ patIdentSet p of
+          in case find consumedNonunique $ S.toList $ patternIdents p of
                Just p' ->
                  returnAliased fname (baseName $ identName p') loc
                Nothing ->
@@ -1664,7 +1701,23 @@
         returnAliasing expected got =
           [(uniqueness expected, S.map aliasVar $ aliases got)]
 
-checkGlobalAliases :: [Pattern] -> CompType -> SrcLoc -> TermTypeM ()
+warnOnDubiousShapeAnnotations :: SrcLoc -> [Pattern] -> StructType -> TermTypeM ()
+warnOnDubiousShapeAnnotations loc params rettype =
+  onDubiousNames $ S.filter patternNameButNotParamName $
+  mconcat $ map typeDimNames $
+  rettype : map patternStructType params
+  where param_names = S.fromList $ mapMaybe (fst . patternParam) params
+        all_pattern_names = S.map identName $ mconcat $ map patternIdents params
+        patternNameButNotParamName v = v `S.member` all_pattern_names && not (v `S.member` param_names)
+        onDubiousNames dubious
+          | S.null dubious = return ()
+          | otherwise = warn loc $ unlines
+                        [ "Size annotations in parameter and/or return type refers to the following names,"
+                        , "which will not be visible to the caller, because they are nested in tuples or records:"
+                        , "  " ++ intercalate ", " (map (quote . prettyName) $ S.toList dubious)
+                        , "To eliminate this warning, make these names parameters on their own."]
+
+checkGlobalAliases :: [Pattern] -> PatternType -> SrcLoc -> TermTypeM ()
 checkGlobalAliases params body_t loc = do
   vtable <- asks scopeVtable
   let isLocal v = case v `M.lookup` vtable of
@@ -1672,7 +1725,7 @@
                     _ -> False
   let als = filter (not . isLocal) $ S.toList $
             boundArrayAliases body_t `S.difference`
-            S.map identName (mconcat (map patIdentSet params))
+            S.map identName (mconcat (map patternIdents params))
   case als of
     v:_ | not $ null params ->
       typeError loc $
@@ -1683,7 +1736,7 @@
       return ()
 
 
-inferReturnUniqueness :: [Pattern] -> CompType -> StructType
+inferReturnUniqueness :: [Pattern] -> PatternType -> StructType
 inferReturnUniqueness params t =
   let forbidden = aliasesMultipleTimes t
       uniques = uniqueParamNames params
@@ -1695,10 +1748,10 @@
             toStruct t'
         | otherwise =
             toStruct $ t' `setUniqueness` Nonunique
-  in vacuousShapeAnnotations $ delve t
+  in delve t
 
 -- An alias inhibits uniqueness if it is used in disjoint values.
-aliasesMultipleTimes :: CompType -> Names
+aliasesMultipleTimes :: PatternType -> Names
 aliasesMultipleTimes = S.fromList . map fst . filter ((>1) . snd) . M.toList . delve
   where delve (Record fs) =
           foldl' (M.unionWith (+)) mempty $ map delve $ M.elems fs
@@ -1709,9 +1762,9 @@
 uniqueParamNames =
   S.fromList . map identName
   . filter (unique . unInfo . identType)
-  . S.toList . mconcat . map patIdentSet
+  . S.toList . mconcat . map patternIdents
 
-boundArrayAliases :: CompType -> S.Set VName
+boundArrayAliases :: PatternType -> S.Set VName
 boundArrayAliases (Array als _ _ _) = boundAliases als
 boundArrayAliases Prim{} = mempty
 boundArrayAliases Enum{} = mempty
@@ -1734,10 +1787,10 @@
         bad = typeError loc "A top-level constant cannot have a unique type."
 
 letGeneralise :: [TypeParam]
-              -> [StructType]
+              -> StructType
               -> Constraints
               -> TermTypeM [TypeParam]
-letGeneralise tparams ts then_substs = do
+letGeneralise tparams t then_substs = do
   now_substs <- getConstraints
   -- Candidates for let-generalisation are those type variables that
   --
@@ -1758,7 +1811,7 @@
                             overloadedTypeVars now_substs
 
   let new_substs = M.filterWithKey (\k _ -> not (k `S.member` keep_type_variables)) now_substs
-  tparams' <- closeOverTypes new_substs tparams ts
+  tparams' <- closeOverTypes new_substs tparams t
 
   -- We keep those type variables that were not closed over by
   -- let-generalisation.
@@ -1780,12 +1833,12 @@
       void $ unifies rettype_structural body'
       -- We also have to make sure that uniqueness matches.  This is done
       -- explicitly, because uniqueness is ignored by unification.
-      rettype_structural' <- normaliseType rettype_structural
+      rettype' <- normaliseType rettype
       body_t <- expType body'
-      unless (body_t `subtypeOf` rettype_structural') $
+      unless (body_t `subtypeOf` anyDimShapeAnnotations rettype') $
         typeError (srclocOf body) $ "Body type " ++ quote (pretty body_t) ++
         " is not a subtype of annotated type " ++
-        quote (pretty rettype_structural') ++ "."
+        quote (pretty rettype') ++ "."
 
     Nothing -> return ()
 
@@ -1795,14 +1848,14 @@
 -- the constraints, and produce type parameters that close over them.
 -- Produce an error if the given list of type parameters is non-empty,
 -- yet does not cover all type variables in the type.
-closeOverTypes :: Constraints -> [TypeParam] -> [StructType] -> TermTypeM [TypeParam]
-closeOverTypes substs tparams ts =
+closeOverTypes :: Constraints -> [TypeParam] -> StructType -> TermTypeM [TypeParam]
+closeOverTypes substs tparams t =
   case tparams of
     [] -> fmap catMaybes $ mapM closeOver $ M.toList substs'
     _ -> do mapM_ checkClosedOver $ M.toList substs'
             return tparams
   where substs' = M.filterWithKey (\k _ -> k `S.member` visible) substs
-        visible = mconcat (map typeVars ts)
+        visible = typeVars t
 
         checkClosedOver (k, v)
           | not (canBeClosedOver v) ||
@@ -1922,8 +1975,6 @@
       tv = ASTMapper { mapOnExp         = astMap tv
                      , mapOnName        = pure
                      , mapOnQualName    = pure
-                     , mapOnType        = pure . applySubst look
-                     , mapOnCompType    = pure . applySubst look
                      , mapOnStructType  = pure . applySubst look
                      , mapOnPatternType = pure . applySubst look
                      }
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
@@ -16,7 +16,6 @@
   , TypeSub(..)
   , TypeSubs
   , substituteTypes
-  , substituteTypesInBoundV
 
   , Subst(..)
   , Substitutable(..)
@@ -419,10 +418,6 @@
         substituteInDim (NamedDim v)
           | Just (DimSub d) <- M.lookup (qualLeaf v) substs = d
         substituteInDim d = d
-
-substituteTypesInBoundV :: TypeSubs -> BoundV -> BoundV
-substituteTypesInBoundV substs (BoundV tps t) =
-  BoundV tps (substituteTypes substs t)
 
 applyType :: Monoid als =>
              [TypeParam] -> TypeBase (DimDecl VName) als -> [StructTypeArg] -> TypeBase (DimDecl VName) als
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
@@ -151,11 +151,11 @@
             unifyTypeArg _ _ = typeError loc
               "Cannot unify a type argument with a dimension argument (or vice versa)."
 
-applySubstInConstraint :: VName -> TypeBase () () -> Constraint -> Constraint
-applySubstInConstraint vn tp (Constraint t loc) =
-  Constraint (applySubst (flip M.lookup $ M.singleton vn $ Subst tp) t) loc
-applySubstInConstraint vn tp (HasFields fs loc) =
-  HasFields (M.map (applySubst (flip M.lookup $ M.singleton vn $ Subst tp)) fs) loc
+applySubstInConstraint :: VName -> Subst (TypeBase () ()) -> Constraint -> Constraint
+applySubstInConstraint vn subst (Constraint t loc) =
+  Constraint (applySubst (flip M.lookup $ M.singleton vn subst) t) loc
+applySubstInConstraint vn subst (HasFields fs loc) =
+  HasFields (M.map (applySubst (flip M.lookup $ M.singleton vn subst)) fs) loc
 applySubstInConstraint _ _ (NoConstraint l loc) = NoConstraint l loc
 applySubstInConstraint _ _ (Overloaded ts loc) = Overloaded ts loc
 applySubstInConstraint _ _ (Equality loc) = Equality loc
@@ -169,7 +169,7 @@
     then typeError loc $ "Occurs check: cannot instantiate " ++
          prettyName vn ++ " with " ++ pretty tp'
     else do modifyConstraints $ M.insert vn $ Constraint tp' loc
-            modifyConstraints $ M.map $ applySubstInConstraint vn tp'
+            modifyConstraints $ M.map $ applySubstInConstraint vn $ Subst tp'
             case M.lookup vn constraints of
               Just (NoConstraint (Just Unlifted) unlift_loc) ->
                 zeroOrderType loc ("used at " ++ locStr unlift_loc) tp'