diff --git a/docs/language-reference.rst b/docs/language-reference.rst
--- a/docs/language-reference.rst
+++ b/docs/language-reference.rst
@@ -452,7 +452,7 @@
       : | "(" `pat` ")"
       : | "(" `pat` ("," `pat`)+ ")"
       : | "{" "}"
-      : | "{" `fieldid` ["=" `pat`] ["," `fieldid` ["=" `pat`]] "}"
+      : | "{" `fieldid` ["=" `pat`] ("," `fieldid` ["=" `pat`])* "}"
       : | `constructor` `pat`*
       : | `pat` ":" `type`
    loopform :   "for" `id` "<" `exp`
@@ -1660,6 +1660,17 @@
 ....................
 
 Exploit only outer parallelism in the attributed SOAC.
+
+``unroll``
+..........
+
+Fully unroll the attributed ``loop``.  If the compiler cannot
+determine the exact number of iterations (possibly after other
+optimisations and simplifications have taken place), then this
+attribute has no code generation effect, but instead results in a
+warning.  Be very careful with this attribute: it can massively
+increase program size (possibly crashing the compiler) if the loop has
+a huge number of iterations.
 
 ``unsafe``
 ..........
diff --git a/docs/usage.rst b/docs/usage.rst
--- a/docs/usage.rst
+++ b/docs/usage.rst
@@ -107,8 +107,7 @@
 ~~~~~~~~~~~~~~~~
 
 The following options are supported by executables generated with the
-GPU backends (``opencl``, ``pyopencl``, ``csopencl``, and
-``cuda``).
+GPU backends (``opencl``, ``pyopencl``, and ``cuda``).
 
   ``-d DEVICE``
 
@@ -142,7 +141,7 @@
 ~~~~~~~~~~~~~~~~~~~~~~~
 
 The following options are supported by executables generated with the
-OpenCL backends (``opencl``, ``pyopencl``, and ``csopencl``):
+OpenCL backends (``opencl``, ``pyopencl``):
 
   ``-P``
 
diff --git a/futhark.cabal b/futhark.cabal
--- a/futhark.cabal
+++ b/futhark.cabal
@@ -1,7 +1,7 @@
 cabal-version: 2.4
 
 name:           futhark
-version:        0.16.3
+version:        0.16.4
 synopsis:       An optimising compiler for a functional, array-oriented language.
 
 description:    Futhark is a small programming language designed to be compiled to
diff --git a/src/Futhark/Actions.hs b/src/Futhark/Actions.hs
--- a/src/Futhark/Actions.hs
+++ b/src/Futhark/Actions.hs
@@ -6,13 +6,19 @@
   , impCodeGenAction
   , kernelImpCodeGenAction
   , metricsAction
+  , compileCAction
+  , compileOpenCLAction
+  , compileCUDAAction
   )
 where
 
 import Control.Monad
 import Control.Monad.IO.Class
+import System.Exit
+import System.FilePath
+import qualified System.Info
 
-import Futhark.Pipeline
+import Futhark.Compiler.CLI
 import Futhark.Analysis.Alias
 import Futhark.IR
 import Futhark.IR.Prop.Aliases
@@ -20,7 +26,11 @@
 import Futhark.IR.SeqMem (SeqMem)
 import qualified Futhark.CodeGen.ImpGen.Sequential as ImpGenSequential
 import qualified Futhark.CodeGen.ImpGen.Kernels as ImpGenKernels
+import qualified Futhark.CodeGen.Backends.SequentialC as SequentialC
+import qualified Futhark.CodeGen.Backends.CCUDA as CCUDA
+import qualified Futhark.CodeGen.Backends.COpenCL as COpenCL
 import Futhark.Analysis.Metrics
+import Futhark.Util (runProgramWithExitCode)
 
 -- | Print the result to stdout, with alias annotations.
 printAction :: (ASTLore lore, CanBeAliased (Op lore)) => Action lore
@@ -53,3 +63,104 @@
          , actionDescription = "Translate program into imperative IL with kernels and write it on standard output."
          , actionProcedure = liftIO . putStrLn . pretty . snd <=< ImpGenKernels.compileProgOpenCL
          }
+
+-- | The @futhark c@ action.
+compileCAction :: FutharkConfig -> CompilerMode -> FilePath -> Action SeqMem
+compileCAction fcfg mode outpath =
+  Action { actionName = "Compile to OpenCL"
+         , actionDescription = "Compile to OpenCL"
+         , actionProcedure = helper }
+  where
+    helper prog = do
+      cprog <- handleWarnings fcfg $ SequentialC.compileProg prog
+      let cpath = outpath `addExtension` "c"
+          hpath = outpath `addExtension` "h"
+
+      case mode of
+        ToLibrary -> do
+          let (header, impl) = SequentialC.asLibrary cprog
+          liftIO $ writeFile hpath header
+          liftIO $ writeFile cpath impl
+        ToExecutable -> do
+          liftIO $ writeFile cpath $ SequentialC.asExecutable cprog
+          ret <- liftIO $ runProgramWithExitCode "gcc"
+                 [cpath, "-O3", "-std=c99", "-lm", "-o", outpath] mempty
+          case ret of
+            Left err ->
+              externalErrorS $ "Failed to run gcc: " ++ show err
+            Right (ExitFailure code, _, gccerr) ->
+              externalErrorS $ "gcc failed with code " ++
+              show code ++ ":\n" ++ gccerr
+            Right (ExitSuccess, _, _) ->
+              return ()
+
+-- | The @futhark opencl@ action.
+compileOpenCLAction :: FutharkConfig -> CompilerMode -> FilePath -> Action KernelsMem
+compileOpenCLAction fcfg mode outpath =
+  Action { actionName = "Compile to OpenCL"
+         , actionDescription = "Compile to OpenCL"
+         , actionProcedure = helper }
+  where
+    helper prog = do
+      cprog <- handleWarnings fcfg $ COpenCL.compileProg prog
+      let cpath = outpath `addExtension` "c"
+          hpath = outpath `addExtension` "h"
+          extra_options
+            | System.Info.os == "darwin" =
+                ["-framework", "OpenCL"]
+            | System.Info.os == "mingw32" =
+                ["-lOpenCL64"]
+            | otherwise =
+                ["-lOpenCL"]
+
+      case mode of
+        ToLibrary -> do
+          let (header, impl) = COpenCL.asLibrary cprog
+          liftIO $ writeFile hpath header
+          liftIO $ writeFile cpath impl
+        ToExecutable -> do
+          liftIO $ writeFile cpath $ COpenCL.asExecutable cprog
+          ret <- liftIO $ runProgramWithExitCode "gcc"
+                 ([cpath, "-O", "-std=c99", "-lm", "-o", outpath] ++ extra_options) mempty
+          case ret of
+            Left err ->
+              externalErrorS $ "Failed to run gcc: " ++ show err
+            Right (ExitFailure code, _, gccerr) ->
+              externalErrorS $ "gcc failed with code " ++
+              show code ++ ":\n" ++ gccerr
+            Right (ExitSuccess, _, _) ->
+              return ()
+
+-- | The @futhark cuda@ action.
+compileCUDAAction :: FutharkConfig -> CompilerMode -> FilePath -> Action KernelsMem
+compileCUDAAction fcfg mode outpath =
+  Action { actionName = "Compile to CUDA"
+         , actionDescription = "Compile to CUDA"
+         , actionProcedure = helper }
+  where
+    helper prog = do
+      cprog <- handleWarnings fcfg $ CCUDA.compileProg prog
+      let cpath = outpath `addExtension` "c"
+          hpath = outpath `addExtension` "h"
+          extra_options = [ "-lcuda"
+                          , "-lcudart"
+                          , "-lnvrtc"
+                          ]
+      case mode of
+        ToLibrary -> do
+          let (header, impl) = CCUDA.asLibrary cprog
+          liftIO $ writeFile hpath header
+          liftIO $ writeFile cpath impl
+        ToExecutable -> do
+          liftIO $ writeFile cpath $ CCUDA.asExecutable cprog
+          let args = [cpath, "-O", "-std=c99", "-lm", "-o", outpath]
+                     ++ extra_options
+          ret <- liftIO $ runProgramWithExitCode "gcc" args mempty
+          case ret of
+            Left err ->
+              externalErrorS $ "Failed to run gcc: " ++ show err
+            Right (ExitFailure code, _, gccerr) ->
+              externalErrorS $ "gcc failed with code " ++
+              show code ++ ":\n" ++ gccerr
+            Right (ExitSuccess, _, _) ->
+              return ()
diff --git a/src/Futhark/CLI/C.hs b/src/Futhark/CLI/C.hs
--- a/src/Futhark/CLI/C.hs
+++ b/src/Futhark/CLI/C.hs
@@ -2,39 +2,13 @@
 -- | @futhark c@
 module Futhark.CLI.C (main) where
 
-import Control.Monad.IO.Class
-import System.FilePath
-import System.Exit
-
-import Futhark.Pipeline
-import Futhark.Passes
-import qualified Futhark.CodeGen.Backends.SequentialC as SequentialC
+import Futhark.Actions (compileCAction)
+import Futhark.Passes (sequentialCpuPipeline)
 import Futhark.Compiler.CLI
-import Futhark.Util
 
 -- | Run @futhark c@
 main :: String -> [String] -> IO ()
 main = compilerMain () []
        "Compile sequential C" "Generate sequential C code from optimised Futhark program."
-       sequentialCpuPipeline $ \fcfg () mode outpath prog -> do
-         cprog <- handleWarnings fcfg $ SequentialC.compileProg prog
-         let cpath = outpath `addExtension` "c"
-             hpath = outpath `addExtension` "h"
-
-         case mode of
-           ToLibrary -> do
-             let (header, impl) = SequentialC.asLibrary cprog
-             liftIO $ writeFile hpath header
-             liftIO $ writeFile cpath impl
-           ToExecutable -> do
-             liftIO $ writeFile cpath $ SequentialC.asExecutable cprog
-             ret <- liftIO $ runProgramWithExitCode "gcc"
-                    [cpath, "-O3", "-std=c99", "-lm", "-o", outpath] mempty
-             case ret of
-               Left err ->
-                 externalErrorS $ "Failed to run gcc: " ++ show err
-               Right (ExitFailure code, _, gccerr) ->
-                 externalErrorS $ "gcc failed with code " ++
-                 show code ++ ":\n" ++ gccerr
-               Right (ExitSuccess, _, _) ->
-                 return ()
+       sequentialCpuPipeline $ \fcfg () mode outpath prog ->
+  actionProcedure (compileCAction fcfg mode outpath) prog
diff --git a/src/Futhark/CLI/CUDA.hs b/src/Futhark/CLI/CUDA.hs
--- a/src/Futhark/CLI/CUDA.hs
+++ b/src/Futhark/CLI/CUDA.hs
@@ -2,42 +2,13 @@
 -- | @futhark cuda@
 module Futhark.CLI.CUDA (main) where
 
-import Control.Monad.IO.Class
-import System.FilePath
-import System.Exit
-
-import Futhark.Passes
-import qualified Futhark.CodeGen.Backends.CCUDA as CCUDA
-import Futhark.Util
+import Futhark.Actions (compileCUDAAction)
+import Futhark.Passes (gpuPipeline)
 import Futhark.Compiler.CLI
 
 -- | Run @futhark cuda@.
 main :: String -> [String] -> IO ()
 main = compilerMain () []
        "Compile CUDA" "Generate CUDA/C code from optimised Futhark program."
-       gpuPipeline $ \fcfg () mode outpath prog -> do
-         cprog <- handleWarnings fcfg $ CCUDA.compileProg prog
-         let cpath = outpath `addExtension` "c"
-             hpath = outpath `addExtension` "h"
-             extra_options = [ "-lcuda"
-                             , "-lcudart"
-                             , "-lnvrtc"
-                             ]
-         case mode of
-           ToLibrary -> do
-             let (header, impl) = CCUDA.asLibrary cprog
-             liftIO $ writeFile hpath header
-             liftIO $ writeFile cpath impl
-           ToExecutable -> do
-             liftIO $ writeFile cpath $ CCUDA.asExecutable cprog
-             let args = [cpath, "-O", "-std=c99", "-lm", "-o", outpath]
-                        ++ extra_options
-             ret <- liftIO $ runProgramWithExitCode "gcc" args mempty
-             case ret of
-               Left err ->
-                 externalErrorS $ "Failed to run gcc: " ++ show err
-               Right (ExitFailure code, _, gccerr) ->
-                 externalErrorS $ "gcc failed with code " ++
-                 show code ++ ":\n" ++ gccerr
-               Right (ExitSuccess, _, _) ->
-                 return ()
+       gpuPipeline $ \fcfg () mode outpath prog ->
+  actionProcedure (compileCUDAAction fcfg mode outpath) prog
diff --git a/src/Futhark/CLI/Dev.hs b/src/Futhark/CLI/Dev.hs
--- a/src/Futhark/CLI/Dev.hs
+++ b/src/Futhark/CLI/Dev.hs
@@ -11,15 +11,15 @@
 import System.IO
 import System.Exit
 import System.Console.GetOpt
+import System.FilePath
 
 import Prelude hiding (id)
 
+import Futhark.Compiler.CLI
 import Futhark.Pass
 import Futhark.Actions
-import Futhark.Compiler
 import Language.Futhark.Parser (parseFuthark)
 import Futhark.Util.Options
-import Futhark.Pipeline
 import qualified Futhark.IR.SOACS as SOACS
 import qualified Futhark.IR.Kernels as Kernels
 import qualified Futhark.IR.Seq as Seq
@@ -125,15 +125,15 @@
 
 data UntypedAction = SOACSAction (Action SOACS.SOACS)
                    | KernelsAction (Action Kernels.Kernels)
-                   | KernelsMemAction (Action KernelsMem.KernelsMem)
-                   | SeqMemAction (Action SeqMem.SeqMem)
+                   | KernelsMemAction (FilePath -> Action KernelsMem.KernelsMem)
+                   | SeqMemAction (FilePath -> Action SeqMem.SeqMem)
                    | PolyAction AllActions
 
 untypedActionName :: UntypedAction -> String
 untypedActionName (SOACSAction a) = actionName a
 untypedActionName (KernelsAction a) = actionName a
-untypedActionName (SeqMemAction a) = actionName a
-untypedActionName (KernelsMemAction a) = actionName a
+untypedActionName (SeqMemAction a) = actionName $ a ""
+untypedActionName (KernelsMemAction a) = actionName $ a ""
 untypedActionName (PolyAction a) = actionName (actionSOACS a)
 
 instance Representation UntypedAction where
@@ -319,12 +319,20 @@
 
   , Option [] ["compile-imperative"]
     (NoArg $ Right $ \opts ->
-       opts { futharkAction = SeqMemAction impCodeGenAction })
+       opts { futharkAction = SeqMemAction $ const impCodeGenAction })
     "Translate program into the imperative IL and write it on standard output."
   , Option [] ["compile-imperative-kernels"]
     (NoArg $ Right $ \opts ->
-       opts { futharkAction = KernelsMemAction kernelImpCodeGenAction })
+       opts { futharkAction = KernelsMemAction $ const kernelImpCodeGenAction })
     "Translate program into the imperative IL with kernels and write it on standard output."
+  , Option [] ["compile-opencl"]
+    (NoArg $ Right $ \opts ->
+       opts { futharkAction = KernelsMemAction $ compileOpenCLAction newFutharkConfig ToExecutable })
+    "Compile the program using the OpenCL backend."
+  , Option [] ["compile-c"]
+    (NoArg $ Right $ \opts ->
+       opts { futharkAction = SeqMemAction $ compileCAction newFutharkConfig ToExecutable })
+    "Compile the program using the C backend."
   , Option "p" ["print"]
     (NoArg $ Right $ \opts ->
         opts { futharkAction = PolyAction $ AllActions printAction printAction printAction printAction printAction })
@@ -439,11 +447,11 @@
                 >>= Defunctionalise.transformProg
             Pipeline{} -> do
               prog <- runPipelineOnProgram (futharkConfig config) id file
-              runPolyPasses config prog
+              runPolyPasses config (file `replaceExtension` "") (SOACS prog)
 
-runPolyPasses :: Config -> Prog SOACS.SOACS -> FutharkM ()
-runPolyPasses config initial_prog = do
-    end_prog <- foldM (runPolyPass pipeline_config) (SOACS initial_prog)
+runPolyPasses :: Config -> FilePath -> UntypedPassState -> FutharkM ()
+runPolyPasses config base initial_prog = do
+    end_prog <- foldM (runPolyPass pipeline_config) initial_prog
                 (getFutharkPipeline config)
     logMsg $ "Running action " ++ untypedActionName (futharkAction config)
     case (end_prog, futharkAction config) of
@@ -452,9 +460,9 @@
       (Kernels prog, KernelsAction action) ->
         actionProcedure action prog
       (SeqMem prog, SeqMemAction action) ->
-        actionProcedure action prog
+        actionProcedure (action base) prog
       (KernelsMem prog, KernelsMemAction action) ->
-        actionProcedure action prog
+        actionProcedure (action base) prog
 
       (SOACS soacs_prog, PolyAction acs) ->
         actionProcedure (actionSOACS acs) soacs_prog
diff --git a/src/Futhark/CLI/OpenCL.hs b/src/Futhark/CLI/OpenCL.hs
--- a/src/Futhark/CLI/OpenCL.hs
+++ b/src/Futhark/CLI/OpenCL.hs
@@ -2,47 +2,13 @@
 -- | @futhark opencl@
 module Futhark.CLI.OpenCL (main) where
 
-import Control.Monad.IO.Class
-import System.FilePath
-import System.Exit
-import qualified System.Info
-
-import Futhark.Pipeline
-import Futhark.Passes
-import qualified Futhark.CodeGen.Backends.COpenCL as COpenCL
-import Futhark.Util
+import Futhark.Actions (compileOpenCLAction)
+import Futhark.Passes (gpuPipeline)
 import Futhark.Compiler.CLI
 
 -- | Run @futhark opencl@
 main :: String -> [String] -> IO ()
 main = compilerMain () []
        "Compile OpenCL" "Generate OpenCL/C code from optimised Futhark program."
-       gpuPipeline $ \fcfg () mode outpath prog -> do
-         cprog <- handleWarnings fcfg $ COpenCL.compileProg prog
-         let cpath = outpath `addExtension` "c"
-             hpath = outpath `addExtension` "h"
-             extra_options
-               | System.Info.os == "darwin" =
-                   ["-framework", "OpenCL"]
-               | System.Info.os == "mingw32" =
-                   ["-lOpenCL64"]
-               | otherwise =
-                   ["-lOpenCL"]
-
-         case mode of
-           ToLibrary -> do
-             let (header, impl) = COpenCL.asLibrary cprog
-             liftIO $ writeFile hpath header
-             liftIO $ writeFile cpath impl
-           ToExecutable -> do
-             liftIO $ writeFile cpath $ COpenCL.asExecutable cprog
-             ret <- liftIO $ runProgramWithExitCode "gcc"
-                    ([cpath, "-O", "-std=c99", "-lm", "-o", outpath] ++ extra_options) mempty
-             case ret of
-               Left err ->
-                 externalErrorS $ "Failed to run gcc: " ++ show err
-               Right (ExitFailure code, _, gccerr) ->
-                 externalErrorS $ "gcc failed with code " ++
-                 show code ++ ":\n" ++ gccerr
-               Right (ExitSuccess, _, _) ->
-                 return ()
+       gpuPipeline $ \fcfg () mode outpath prog ->
+  actionProcedure (compileOpenCLAction fcfg mode outpath) prog
diff --git a/src/Futhark/CodeGen/Backends/GenericPython.hs b/src/Futhark/CodeGen/Backends/GenericPython.hs
--- a/src/Futhark/CodeGen/Backends/GenericPython.hs
+++ b/src/Futhark/CodeGen/Backends/GenericPython.hs
@@ -436,7 +436,30 @@
                           , "Futhark type: {}"
                           , "Argument has Python type {} and value: {}"]
 
+badInputType :: Int -> PyExp -> String -> PyExp -> PyExp -> PyStmt
+badInputType i e t de dg =
+  Raise $ simpleCall "TypeError"
+  [Call (Field (String err_msg) "format")
+   [Arg (String t), Arg $ simpleCall "type" [e], Arg e, Arg de, Arg dg]]
+  where err_msg = unlines [ "Argument #" ++ show i ++ " has invalid value"
+                          , "Futhark type: {}"
+                          , "Argument has Python type {} and value: {}"
+                          , "Expected array with elements of dtype: {}"
+                          , "The array given has elements of dtype: {}"]
 
+badInputDim :: Int -> PyExp -> String -> Int -> PyStmt
+badInputDim i e typ dimf =
+  Raise $ simpleCall "TypeError"
+  [Call (Field (String err_msg) "format")
+   [Arg eft, Arg aft]]
+  where eft = String (concat (replicate dimf "[]") ++ typ)
+        aft = BinOp "+" (BinOp "*" (String "[]") (Field e "ndim")) (String typ)
+        err_msg = unlines [ "Argument #" ++ show i ++ " has invalid value"
+                          , "Dimensionality mismatch"
+                          , "Expected Futhark type: {}"
+                          , "Bad Python value passed"
+                          , "Actual Futhark type: {}"]
+
 entryPointInput :: (Int, Imp.ExternalValue, PyExp) -> CompilerM op s ()
 entryPointInput (i, Imp.OpaqueValue desc vs, e) = do
   let type_is_ok = BinOp "and" (simpleCall "isinstance" [e, Var "opaque"])
@@ -470,14 +493,21 @@
      prettySigned (ept==Imp.TypeUnsigned) bt]]
 
 entryPointInput (i, Imp.TransparentValue (Imp.ArrayValue mem _ t s dims), e) = do
-  let type_is_wrong =
-        UnOp "not" $
-        BinOp "and"
-        (BinOp "in" (simpleCall "type" [e]) (List [Var "np.ndarray"]))
-        (BinOp "==" (Field e "dtype") (Var (compilePrimToExtNp t s)))
+  let type_is_wrong = UnOp "not" $ BinOp "in" (simpleCall "type" [e]) $ List [Var "np.ndarray"]
+  let dtype_is_wrong = UnOp "not" $ BinOp "==" (Field e "dtype") $ Var $ compilePrimToExtNp t s
+  let dim_is_wrong = UnOp "not" $ BinOp "==" (Field e "ndim") $ Integer $ toInteger $ length dims
   stm $ If type_is_wrong
     [badInput i e $ concat (replicate (length dims) "[]") ++
      prettySigned (s==Imp.TypeUnsigned) t]
+    []
+  stm $ If dtype_is_wrong
+    [badInputType i e
+     (concat (replicate (length dims) "[]") ++ prettySigned (s==Imp.TypeUnsigned) t)
+     (simpleCall "np.dtype" [Var (compilePrimToExtNp t s)])
+     (Field e "dtype")]
+    []
+  stm $ If dim_is_wrong
+    [badInputDim i e (prettySigned (s==Imp.TypeUnsigned) t ) (length dims)]
     []
 
   zipWithM_ (unpackDim e) dims [0..]
diff --git a/src/Futhark/CodeGen/Backends/SimpleRep.hs b/src/Futhark/CodeGen/Backends/SimpleRep.hs
--- a/src/Futhark/CodeGen/Backends/SimpleRep.hs
+++ b/src/Futhark/CodeGen/Backends/SimpleRep.hs
@@ -461,16 +461,16 @@
 $esc:("#else")
 // FIXME: assumes GCC or clang.
    static typename int32_t $id:(funName' "ctz8") (typename int8_t x) {
-     return smin32(8, __builtin_ctz((typename uint32_t)x));
+     return x == 0 ? 8 : __builtin_ctz((typename uint32_t)x);
    }
    static typename int32_t $id:(funName' "ctz16") (typename int16_t x) {
-     return smin32(16, __builtin_ctz((typename uint32_t)x));
+     return x == 0 ? 16 : __builtin_ctz((typename uint32_t)x);
    }
    static typename int32_t $id:(funName' "ctz32") (typename int32_t x) {
-     return __builtin_ctz(x);
+     return x == 0 ? 32 :  __builtin_ctz(x);
    }
    static typename int32_t $id:(funName' "ctz64") (typename int64_t x) {
-     return __builtin_ctzl(x);
+     return x == 0 ? 64 : __builtin_ctzl(x);
    }
 $esc:("#endif")
                 |]
diff --git a/src/Futhark/CodeGen/ImpCode.hs b/src/Futhark/CodeGen/ImpCode.hs
--- a/src/Futhark/CodeGen/ImpCode.hs
+++ b/src/Futhark/CodeGen/ImpCode.hs
@@ -258,9 +258,10 @@
 
 -- | Find those memory blocks that are used only lexically.  That is,
 -- are not used as the source or target of a 'SetMem', or are the
--- result of the function.  This is interesting because such memory
--- blocks do not need reference counting, but can be managed in a
--- purely stack-like fashion.
+-- result of the function, nor passed as arguments to other functions.
+-- This is interesting because such memory blocks do not need
+-- reference counting, but can be managed in a purely stack-like
+-- fashion.
 --
 -- We do not look inside any 'Op's.  We assume that no 'Op' is going
 -- to 'SetMem' a memory block declared outside it.
@@ -283,6 +284,9 @@
         declared x = go declared x
 
         set (SetMem x y _) = namesFromList [x,y]
+        set (Call _ _ args) = foldMap onArg args
+          where onArg ExpArg{} = mempty
+                onArg (MemArg x) = oneName x
         set x = go set x
 
 -- | The set of functions that are called by this code.  Assumes there
diff --git a/src/Futhark/CodeGen/ImpGen.hs b/src/Futhark/CodeGen/ImpGen.hs
--- a/src/Futhark/CodeGen/ImpGen.hs
+++ b/src/Futhark/CodeGen/ImpGen.hs
@@ -110,6 +110,7 @@
 import Futhark.Construct (fullSliceNum)
 import Futhark.MonadFreshNames
 import Futhark.Util
+import Futhark.Util.Loc (noLoc)
 import Language.Futhark.Warnings
 
 -- | How to compile an t'Op'.
@@ -644,6 +645,10 @@
 defCompileExp pat (BasicOp op) = defCompileBasicOp pat op
 
 defCompileExp pat (DoLoop ctx val form body) = do
+  attrs <- askAttrs
+  when ("unroll" `inAttrs` attrs) $
+    warn (noLoc::SrcLoc) [] "#[unroll] on loop with unknown number of iterations." -- FIXME: no location.
+
   dFParams mergepat
   forM_ merge $ \(p, se) ->
     when ((==0) $ arrayRank $ paramType p) $
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
@@ -210,15 +210,14 @@
   destloc@(MemLocation destmem _ destIxFun) destslice
   srcloc@(MemLocation srcmem srcshape srcIxFun) srcslice
   | Just (destoffset, srcoffset,
-          num_arrays, size_x, size_y,
-          src_elems, dest_elems) <- isMapTransposeKernel bt destloc destslice srcloc srcslice = do
+          num_arrays, size_x, size_y) <-
+      isMapTransposeKernel bt destloc destslice srcloc srcslice = do
 
       fname <- mapTransposeForType bt
       emit $ Imp.Call [] fname
         [Imp.MemArg destmem, Imp.ExpArg destoffset,
          Imp.MemArg srcmem, Imp.ExpArg srcoffset,
-         Imp.ExpArg num_arrays, Imp.ExpArg size_x, Imp.ExpArg size_y,
-         Imp.ExpArg src_elems, Imp.ExpArg dest_elems]
+         Imp.ExpArg num_arrays, Imp.ExpArg size_x, Imp.ExpArg size_y]
 
   | bt_size <- primByteSize bt,
     Just destoffset <-
@@ -253,15 +252,14 @@
 
   where params = [memparam destmem, intparam destoffset,
                   memparam srcmem, intparam srcoffset,
-                  intparam num_arrays, intparam x, intparam y,
-                  intparam in_elems, intparam out_elems]
+                  intparam num_arrays, intparam x, intparam y]
 
         space = Space "device"
         memparam v = Imp.MemParam v space
         intparam v = Imp.ScalarParam v $ IntType Int32
 
         [destmem, destoffset, srcmem, srcoffset,
-         num_arrays, x, y, in_elems, out_elems,
+         num_arrays, x, y,
          mulx, muly, block] =
            zipWith (VName . nameFromString)
            ["destmem",
@@ -271,8 +269,6 @@
              "num_arrays",
              "x_elems",
              "y_elems",
-             "in_elems",
-             "out_elems",
              -- The following is only used for low width/height
              -- transpose kernels
              "mulx",
@@ -289,24 +285,12 @@
         block_dim = 16
 
         -- When an input array has either width==1 or height==1, performing a
-        -- transpose will be the same as performing a copy.  If 'input_size' or
-        -- 'output_size' is not equal to width*height, then this trick will not
-        -- work when there are more than one array to process, as it is a per
-        -- array limit. We could copy each array individually, but currently we
-        -- do not.
+        -- transpose will be the same as performing a copy.
         can_use_copy =
-          let in_out_eq = CmpOpExp (CmpEq $ IntType Int32) (v32 in_elems) (v32 out_elems)
-              onearr = CmpOpExp (CmpEq $ IntType Int32) (v32 num_arrays) 1
-              noprob_widthheight = CmpOpExp (CmpEq $ IntType Int32)
-                                     (v32 x * v32 y)
-                                     (v32 in_elems)
+          let onearr = CmpOpExp (CmpEq $ IntType Int32) (v32 num_arrays) 1
               height_is_one = CmpOpExp (CmpEq $ IntType Int32) (v32 y) 1
               width_is_one = CmpOpExp (CmpEq $ IntType Int32) (v32 x) 1
-          in BinOpExp LogAnd
-               in_out_eq
-               (BinOpExp LogAnd
-                 (BinOpExp LogOr onearr noprob_widthheight)
-                 (BinOpExp LogOr width_is_one height_is_one))
+          in onearr .&&. (width_is_one .||. height_is_one)
 
         transpose_code =
           Imp.If input_is_empty mempty $ mconcat
@@ -337,7 +321,7 @@
 
         copy_code =
           let num_bytes =
-                v32 in_elems * Imp.LeafExp (Imp.SizeOf bt) (IntType Int32)
+                v32 x * v32 y * Imp.LeafExp (Imp.SizeOf bt) (IntType Int32)
           in Imp.Copy
                destmem (Imp.Count $ v32 destoffset) space
                srcmem (Imp.Count $ v32 srcoffset) space
@@ -347,7 +331,7 @@
           Imp.Op . Imp.CallKernel .
           mapTransposeKernel (mapTransposeName bt) block_dim_int
           (destmem, v32 destoffset, srcmem, v32 srcoffset,
-            v32 x, v32 y, v32 in_elems, v32 out_elems,
+            v32 x, v32 y,
             v32 mulx, v32 muly, v32 num_arrays,
             block) bt
 
@@ -355,8 +339,7 @@
                      -> MemLocation -> Slice Imp.Exp
                      -> MemLocation -> Slice Imp.Exp
                      -> Maybe (Imp.Exp, Imp.Exp,
-                               Imp.Exp, Imp.Exp, Imp.Exp,
-                               Imp.Exp, Imp.Exp)
+                               Imp.Exp, Imp.Exp, Imp.Exp)
 isMapTransposeKernel bt
   (MemLocation _ _ destIxFun) destslice
   (MemLocation _ _ srcIxFun) srcslice
@@ -364,12 +347,12 @@
     (perm, destshape) <- unzip perm_and_destshape,
     Just src_offset <- IxFun.linearWithOffset srcIxFun' bt_size,
     Just (r1, r2, _) <- isMapTranspose perm =
-      isOk (product destshape) destshape swap r1 r2 dest_offset src_offset
+      isOk destshape swap r1 r2 dest_offset src_offset
   | Just dest_offset <- IxFun.linearWithOffset destIxFun' bt_size,
     Just (src_offset, perm_and_srcshape) <- IxFun.rearrangeWithOffset srcIxFun' bt_size,
     (perm, srcshape) <- unzip perm_and_srcshape,
     Just (r1, r2, _) <- isMapTranspose perm =
-      isOk (product srcshape) srcshape id r1 r2 dest_offset src_offset
+      isOk srcshape id r1 r2 dest_offset src_offset
   | otherwise =
       Nothing
   where bt_size = primByteSize bt
@@ -378,11 +361,10 @@
         destIxFun' = IxFun.slice destIxFun destslice
         srcIxFun' = IxFun.slice srcIxFun srcslice
 
-        isOk elems shape f r1 r2 dest_offset src_offset = do
+        isOk shape f r1 r2 dest_offset src_offset = do
           let (num_arrays, size_x, size_y) = getSizes shape f r1 r2
           return (dest_offset, src_offset,
-                  num_arrays, size_x, size_y,
-                  elems, elems)
+                  num_arrays, size_x, size_y)
 
         getSizes shape f r1 r2 =
           let (mapped, notmapped) = splitAt r1 shape
diff --git a/src/Futhark/CodeGen/ImpGen/Kernels/SegScan.hs b/src/Futhark/CodeGen/ImpGen/Kernels/SegScan.hs
--- a/src/Futhark/CodeGen/ImpGen/Kernels/SegScan.hs
+++ b/src/Futhark/CodeGen/ImpGen/Kernels/SegScan.hs
@@ -399,7 +399,7 @@
                -> [SegBinOp KernelsMem]
                -> KernelBody KernelsMem
                -> CallKernelGen ()
-compileSegScan pat lvl space scans kbody = do
+compileSegScan pat lvl space scans kbody = sWhen (0 .<. n) $ do
   emit $ Imp.DebugPrint "\n# SegScan" Nothing
 
   -- Since stage 2 involves a group size equal to the number of groups
@@ -421,3 +421,4 @@
 
   scanStage2 pat stage1_num_threads elems_per_group stage1_num_groups crossesSegment space scans
   scanStage3 pat (segNumGroups lvl) (segGroupSize lvl) elems_per_group crossesSegment space scans
+  where n = product $ map (toExp' int32) $ segSpaceDims space
diff --git a/src/Futhark/CodeGen/ImpGen/Kernels/Transpose.hs b/src/Futhark/CodeGen/ImpGen/Kernels/Transpose.hs
--- a/src/Futhark/CodeGen/ImpGen/Kernels/Transpose.hs
+++ b/src/Futhark/CodeGen/ImpGen/Kernels/Transpose.hs
@@ -24,7 +24,7 @@
 -- | The types of the arguments accepted by a transposition function.
 type TransposeArgs = (VName, Exp,
                       VName, Exp,
-                      Exp, Exp, Exp, Exp,
+                      Exp, Exp,
                       Exp, Exp, Exp,
                       VName)
 
@@ -51,7 +51,7 @@
       , dec index_in $ v32 y_index * width + v32 x_index
       , dec index_out $ v32 x_index * height + v32 y_index
 
-      , If (v32 get_global_id_0 .<. input_size)
+      , If (v32 get_global_id_0 .<. width * height * num_arrays)
         (Write odata (elements $ v32 odata_offset + v32 index_out) t (Space "global") Nonvolatile $
          index idata (elements $ v32 idata_offset + v32 index_in) t (Space "global") Nonvolatile)
         mempty
@@ -83,8 +83,7 @@
         For j Int32 elemsPerThread $
         let i = v32 j * (tile_dim `quot` elemsPerThread)
         in mconcat [ dec index_in $ (v32 y_index + i) * width + v32 x_index
-                   , when (v32 y_index + i .<. height .&&.
-                           v32 index_in .<. input_size) $
+                   , when (v32 y_index + i .<. height) $
                      Write block (elements $ (v32 get_local_id_1 + i) * (tile_dim+1)
                                              + v32 get_local_id_0)
                      t (Space "local") Nonvolatile $
@@ -97,8 +96,7 @@
         For j Int32 elemsPerThread $
         let i = v32 j * (tile_dim `quot` elemsPerThread)
         in mconcat [ dec index_out $ (v32 y_index + i) * height + v32 x_index
-                   , when (v32 y_index + i .<. width .&&.
-                           v32 index_out .<. output_size) $
+                   , when (v32 y_index + i .<. width) $
                      Write odata (elements $ v32 odata_offset + v32 index_out)
                      t (Space "global") Nonvolatile $
                      index block (elements $ v32 get_local_id_0 * (tile_dim+1)
@@ -114,8 +112,8 @@
         when a b = If a b mempty
 
         (odata, basic_odata_offset, idata, basic_idata_offset,
-         width, height, input_size, output_size,
-         mulx, muly, _num_arrays, block) = args
+         width, height,
+         mulx, muly, num_arrays, block) = args
 
         -- Be extremely careful when editing this list to ensure that
         -- the names match up.  Also, be careful that the tags on
@@ -168,7 +166,7 @@
           [ dec x_index x_in_index
           , dec y_index y_in_index
           , dec index_in $ v32 y_index * width + v32 x_index
-          , when (v32 x_index .<. width .&&. v32 y_index .<. height .&&. v32 index_in .<. input_size) $
+          , when (v32 x_index .<. width .&&. v32 y_index .<. height) $
             Write block (elements $ v32 get_local_id_1 * (block_dim+1) + v32 get_local_id_0)
             t (Space "local") Nonvolatile $
             index idata (elements $ v32 idata_offset + v32 index_in)
@@ -177,7 +175,7 @@
           , SetScalar x_index x_out_index
           , SetScalar y_index y_out_index
           , dec index_out $ v32 y_index * height + v32 x_index
-          , when (v32 x_index .<. height .&&. v32 y_index .<. width .&&. v32 index_out .<. output_size) $
+          , when (v32 x_index .<. height .&&. v32 y_index .<. width) $
             Write odata (elements $ v32 odata_offset + v32 index_out)
             t (Space "global") Nonvolatile $
             index block (elements $ v32 get_local_id_0 * (block_dim+1) + v32 get_local_id_1)
@@ -207,10 +205,6 @@
 -- of block_dim*2 by block_dim*2+1 elements. Padding each row with
 -- an additional element prevents bank conflicts from occuring when
 -- the tile is accessed column-wise.
---
--- Note that input_size and output_size may not equal width*height if
--- we are dealing with a truncated array - this happens sometimes for
--- coalescing optimisations.
 mapTransposeKernel :: String -> Integer -> TransposeArgs -> PrimType -> TransposeType
                    -> Kernel
 mapTransposeKernel desc block_dim_int args t kind =
@@ -235,7 +229,7 @@
         block_dim = fromInteger block_dim_int
 
         (odata, basic_odata_offset, idata, basic_idata_offset,
-         width, height, input_size, output_size,
+         width, height,
          mulx, muly, num_arrays,
          block) = args
 
@@ -258,7 +252,7 @@
         uses = map (`ScalarUse` int32)
                (namesToList $ mconcat $ map freeIn
                 [basic_odata_offset, basic_idata_offset, num_arrays,
-                 width, height, input_size, output_size, mulx, muly]) ++
+                 width, height, mulx, muly]) ++
                map MemoryUse [odata, idata]
 
         name =
diff --git a/src/Futhark/Construct.hs b/src/Futhark/Construct.hs
--- a/src/Futhark/Construct.hs
+++ b/src/Futhark/Construct.hs
@@ -328,7 +328,7 @@
 -- | Construct an unspecified value of the given type.
 eBlank :: MonadBinder m => Type -> m (Exp (Lore m))
 eBlank (Prim t) = return $ BasicOp $ SubExp $ Constant $ blankPrimValue t
-eBlank (Array pt shape _) = return $ BasicOp $ Scratch pt $ shapeDims shape
+eBlank (Array t shape _) = return $ BasicOp $ Scratch t $ shapeDims shape
 eBlank Mem{} = error "eBlank: cannot create blank memory"
 
 -- | Sign-extend to the given integer type.
@@ -375,8 +375,8 @@
 
 -- | As 'binOpLambda', but for t'CmpOp's.
 cmpOpLambda :: (MonadBinder m, Bindable (Lore m)) =>
-               CmpOp -> PrimType -> m (Lambda (Lore m))
-cmpOpLambda cop t = binLambda (CmpOp cop) t Bool
+               CmpOp -> m (Lambda (Lore m))
+cmpOpLambda cop = binLambda (CmpOp cop) (cmpOpType cop) Bool
 
 binLambda :: (MonadBinder m, Bindable (Lore m)) =>
              (SubExp -> SubExp -> BasicOp) -> PrimType -> PrimType
diff --git a/src/Futhark/IR/Primitive.hs b/src/Futhark/IR/Primitive.hs
--- a/src/Futhark/IR/Primitive.hs
+++ b/src/Futhark/IR/Primitive.hs
@@ -210,9 +210,29 @@
 -- | A floating-point value.
 data FloatValue = Float32Value !Float
                 | Float64Value !Double
-               deriving (Eq, Ord, Show)
+               deriving (Show)
 
+instance Eq FloatValue where
+  Float32Value x == Float32Value y = isNaN x && isNaN y || x == y
+  Float64Value x == Float64Value y = isNaN x && isNaN y || x == y
+  Float32Value _ == Float64Value _ = False
+  Float64Value _ == Float32Value _ = False
 
+-- The derived Ord instance does not handle NaNs correctly.
+instance Ord FloatValue where
+  Float32Value x <= Float32Value y = x <= y
+  Float64Value x <= Float64Value y = x <= y
+  Float32Value _ <= Float64Value _ = True
+  Float64Value _ <= Float32Value _ = False
+
+  Float32Value x < Float32Value y = x < y
+  Float64Value x < Float64Value y = x < y
+  Float32Value _ < Float64Value _ = True
+  Float64Value _ < Float32Value _ = False
+
+  (>) = flip (<)
+  (>=) = flip (<=)
+
 instance Pretty FloatValue where
   ppr (Float32Value v)
     | isInfinite v, v >= 0 = text "f32.inf"
@@ -790,6 +810,8 @@
 
 -- | Compare any two primtive values for exact equality.
 doCmpEq :: PrimValue -> PrimValue -> Bool
+doCmpEq (FloatValue (Float32Value v1)) (FloatValue (Float32Value v2)) = v1 == v2
+doCmpEq (FloatValue (Float64Value v1)) (FloatValue (Float64Value v2)) = v1 == v2
 doCmpEq v1 v2 = v1 == v2
 
 -- | Unsigned less than.
diff --git a/src/Futhark/IR/Prop/Names.hs b/src/Futhark/IR/Prop/Names.hs
--- a/src/Futhark/IR/Prop/Names.hs
+++ b/src/Futhark/IR/Prop/Names.hs
@@ -131,7 +131,9 @@
               Walker lore (State FV)
 freeWalker = identityWalker {
                walkOnSubExp = modify . (<>) . freeIn'
-             , walkOnBody = modify . (<>) . freeIn'
+             , walkOnBody = \scope body -> do
+                 modify $ (<>) $ freeIn' body
+                 modify $ fvBind (namesFromList (M.keys scope))
              , walkOnVName = modify . (<>) . fvName
              , walkOnOp = modify . (<>) . freeIn'
              }
diff --git a/src/Futhark/IR/Prop/Types.hs b/src/Futhark/IR/Prop/Types.hs
--- a/src/Futhark/IR/Prop/Types.hs
+++ b/src/Futhark/IR/Prop/Types.hs
@@ -34,6 +34,9 @@
        , transposeType
        , rearrangeType
 
+       , mapOnExtType
+       , mapOnType
+
        , diet
 
        , subtypeOf
@@ -43,12 +46,12 @@
        , fromDecl
 
        , isExt
+       , isFree
        , extractShapeContext
        , shapeContext
        , hasStaticShape
        , generaliseExtTypes
        , existentialiseExtTypes
-       , shapeMapping
        , shapeExtMapping
 
          -- * Abbreviations
@@ -281,6 +284,28 @@
   t `setArrayShape` Shape (rearrangeShape perm' $ arrayDims t)
   where perm' = perm ++ [length perm .. arrayRank t - 1]
 
+-- | Transform any t'SubExp's in the type.
+mapOnExtType :: Monad m =>
+                (SubExp -> m SubExp)
+             -> TypeBase ExtShape u
+             -> m (TypeBase ExtShape u)
+mapOnExtType _ (Prim bt) =
+  return $ Prim bt
+mapOnExtType _ (Mem space) =
+  pure $ Mem space
+mapOnExtType f (Array t shape u) =
+  Array t <$> (Shape <$> mapM (traverse f) (shapeDims shape)) <*> pure u
+
+-- | Transform any t'SubExp's in the type.
+mapOnType :: Monad m =>
+             (SubExp -> m SubExp)
+          -> TypeBase Shape u
+          -> m (TypeBase Shape u)
+mapOnType _ (Prim bt) = return $ Prim bt
+mapOnType _ (Mem space) = pure $ Mem space
+mapOnType f (Array t shape u) =
+  Array t <$> (Shape <$> mapM f (shapeDims shape)) <*> pure u
+
 -- | @diet t@ returns a description of how a function parameter of
 -- type @t@ might consume its argument.
 diet :: TypeBase shape Uniqueness -> Diet
@@ -333,6 +358,11 @@
 isExt (Ext i) = Just i
 isExt _ = Nothing
 
+-- | If a known size, then return that size.
+isFree :: Ext a -> Maybe a
+isFree (Free d) = Just d
+isFree _ = Nothing
+
 -- | Given the existential return type of a function, and the shapes
 -- of the values returned by the function, return the existential
 -- shape context.  That is, those sizes that are existential in the
@@ -357,15 +387,13 @@
   where ext (Ext x)  = Just x
         ext (Free _) = Nothing
 
--- | If all dimensions of the given 'ExtType' are statically known,
--- return the corresponding list of 'Type'.
-hasStaticShape :: ExtType -> Maybe Type
+-- | If all dimensions of the given 'ExtShape' are statically known,
+-- change to the corresponding 'Shape'.
+hasStaticShape :: TypeBase ExtShape u -> Maybe (TypeBase Shape u)
 hasStaticShape (Prim bt) = Just $ Prim bt
 hasStaticShape (Mem space) = Just $ Mem space
 hasStaticShape (Array bt (Shape shape) u) =
   Array bt <$> (Shape <$> mapM isFree shape) <*> pure u
-  where isFree (Free s) = Just s
-        isFree (Ext _)  = Nothing
 
 -- | Given two lists of 'ExtType's of the same length, return a list
 -- of 'ExtType's that is a subtype of the two operands.
@@ -406,26 +434,7 @@
               Ext i
         checkDim d = d
 
--- | In the call @shapeMapping ts1 ts2@, the lists @ts1@ and @ts@ must
--- be of equal length and their corresponding elements have the same
--- types modulo exact dimensions (but matching array rank is
--- important).  The result is a mapping from named dimensions of @ts1@
--- to a set of the corresponding dimensions in @ts2@ (because they may
--- not fit exactly).
---
--- This function is useful when @ts1@ are the value parameters of some
--- function and @ts2@ are the value arguments, and we need to figure
--- out which shape context to pass.
-shapeMapping :: [TypeBase Shape u0] -> [TypeBase Shape u1] -> M.Map VName (S.Set SubExp)
-shapeMapping ts = shapeMapping' ts . map arrayDims
-
--- | Like @shapeMapping@, but works with explicit dimensions.
-shapeMapping' :: Ord a => [TypeBase Shape u] -> [[a]] -> M.Map VName (S.Set a)
-shapeMapping' = dimMapping arrayDims id match (M.unionWith (<>))
-  where match Constant{} _ = M.empty
-        match (Var v) dim  = M.singleton v $ S.singleton dim
-
--- | Like 'shapeMapping', but produces a mapping for the dimensions context.
+-- | Produce a mapping for the dimensions context.
 shapeExtMapping :: [TypeBase ExtShape u] -> [TypeBase Shape u1] -> M.Map Int SubExp
 shapeExtMapping = dimMapping arrayExtDims arrayDims match mappend
   where match Free{} _ =  mempty
diff --git a/src/Futhark/IR/SOACS/Simplify.hs b/src/Futhark/IR/SOACS/Simplify.hs
--- a/src/Futhark/IR/SOACS/Simplify.hs
+++ b/src/Futhark/IR/SOACS/Simplify.hs
@@ -656,7 +656,7 @@
         onOp = execWriter . mapSOACM identitySOACMapper { mapOnSOACLambda = onLambda }
         onLambda lam = do tell $ arrayOps $ lambdaBody lam
                           return lam
-        walker = identityWalker { walkOnBody = modify . (<>) . arrayOps
+        walker = identityWalker { walkOnBody = const $ modify . (<>) . arrayOps
                                 , walkOnOp = modify . (<>) . onOp }
 
 replaceArrayOps :: M.Map ArrayOp ArrayOp
diff --git a/src/Futhark/IR/SegOp.hs b/src/Futhark/IR/SegOp.hs
--- a/src/Futhark/IR/SegOp.hs
+++ b/src/Futhark/IR/SegOp.hs
@@ -648,7 +648,7 @@
 
 mapOnSegOpType :: Monad m =>
                   SegOpMapper lvl flore tlore m -> Type -> m Type
-mapOnSegOpType _tv (Prim pt) = pure $ Prim pt
+mapOnSegOpType _tv t@Prim{} = pure t
 mapOnSegOpType tv (Array pt shape u) = Array pt <$> f shape <*> pure u
   where f (Shape dims) = Shape <$> mapM (mapOnSegOpSubExp tv) dims
 mapOnSegOpType _tv (Mem s) = pure $ Mem s
diff --git a/src/Futhark/IR/Syntax/Core.hs b/src/Futhark/IR/Syntax/Core.hs
--- a/src/Futhark/IR/Syntax/Core.hs
+++ b/src/Futhark/IR/Syntax/Core.hs
@@ -67,6 +67,21 @@
 newtype ShapeBase d = Shape { shapeDims :: [d] }
                     deriving (Eq, Ord, Show)
 
+instance Functor ShapeBase where
+  fmap = fmapDefault
+
+instance Foldable ShapeBase where
+  foldMap = foldMapDefault
+
+instance Traversable ShapeBase where
+  traverse f = fmap Shape . traverse f . shapeDims
+
+instance Semigroup (ShapeBase d) where
+  Shape l1 <> Shape l2 = Shape $ l1 `mappend` l2
+
+instance Monoid (ShapeBase d) where
+  mempty = Shape mempty
+
 -- | The size of an array as a list of subexpressions.  If a variable,
 -- that variable must be in scope where this array is used.
 type Shape = ShapeBase SubExp
@@ -77,9 +92,15 @@
            deriving (Eq, Ord, Show)
 
 instance Functor Ext where
-  fmap _ (Ext i) = Ext i
-  fmap f (Free a) = Free $ f a
+  fmap = fmapDefault
 
+instance Foldable Ext where
+  foldMap = foldMapDefault
+
+instance Traversable Ext where
+  traverse _ (Ext i) = pure $ Ext i
+  traverse f (Free v) = Free <$> f v
+
 -- | The size of this dimension.
 type ExtSize = Ext SubExp
 
@@ -101,15 +122,6 @@
   stripDims :: Int -> a -> a
   -- | Check whether one shape if a subset of another shape.
   subShapeOf :: a -> a -> Bool
-
-instance Semigroup (ShapeBase d) where
-  Shape l1 <> Shape l2 = Shape $ l1 `mappend` l2
-
-instance Monoid (ShapeBase d) where
-  mempty = Shape mempty
-
-instance Functor ShapeBase where
-  fmap f = Shape . map f . shapeDims
 
 instance ArrayShape (ShapeBase SubExp) where
   shapeRank (Shape l) = length l
diff --git a/src/Futhark/IR/Traversals.hs b/src/Futhark/IR/Traversals.hs
--- a/src/Futhark/IR/Traversals.hs
+++ b/src/Futhark/IR/Traversals.hs
@@ -29,7 +29,6 @@
   , identityMapper
   , mapExpM
   , mapExp
-  , mapOnType
 
   -- * Walking
   , Walker(..)
@@ -45,6 +44,7 @@
 
 import Futhark.IR.Syntax
 import Futhark.IR.Prop.Scope
+import Futhark.IR.Prop.Types (mapOnType)
 
 -- | Express a monad mapping operation on a syntax node.  Each element
 -- of this structure expresses the operation to be performed on a
@@ -162,20 +162,12 @@
 mapExp :: Mapper flore tlore Identity -> Exp flore -> Exp tlore
 mapExp m = runIdentity . mapExpM m
 
--- | Transform any t'SubExp's in the type.
-mapOnType :: Monad m =>
-             (SubExp -> m SubExp) -> Type -> m Type
-mapOnType _ (Prim bt) = return $ Prim bt
-mapOnType _ (Mem space) = pure $ Mem space
-mapOnType f (Array bt shape u) =
-  Array bt <$> (Shape <$> mapM f (shapeDims shape)) <*> pure u
-
 -- | Express a monad expression on a syntax node.  Each element of
 -- this structure expresses the action to be performed on a given
 -- child.
 data Walker lore m = Walker {
     walkOnSubExp :: SubExp -> m ()
-  , walkOnBody :: Body lore -> m ()
+  , walkOnBody :: Scope lore -> Body lore -> m ()
   , walkOnVName :: VName -> m ()
   , walkOnRetType :: RetType lore -> m ()
   , walkOnBranchType :: BranchType lore -> m ()
@@ -188,7 +180,7 @@
 identityWalker :: Monad m => Walker lore m
 identityWalker = Walker {
                    walkOnSubExp = const $ return ()
-                 , walkOnBody = const $ return ()
+                 , walkOnBody = const $ const $ return ()
                  , walkOnVName = const $ return ()
                  , walkOnRetType = const $ return ()
                  , walkOnBranchType = const $ return ()
@@ -200,11 +192,10 @@
 walkOnShape :: Monad m => Walker lore m -> Shape -> m ()
 walkOnShape tv (Shape ds) = mapM_ (walkOnSubExp tv) ds
 
-walkOnType :: Monad m =>
-             (SubExp -> m ()) -> Type -> m ()
+walkOnType :: Monad m => Walker lore m -> Type -> m ()
 walkOnType _ Prim{} = return ()
 walkOnType _ Mem{} = return ()
-walkOnType f (Array _ shape _) = mapM_ f $ shapeDims shape
+walkOnType tv (Array _ shape _) = walkOnShape tv shape
 
 walkOnLoopForm :: Monad m => Walker lore m -> LoopForm lore -> m ()
 walkOnLoopForm tv (ForLoop i _ bound loop_vars) =
@@ -219,7 +210,7 @@
 walkExpM tv (BasicOp (SubExp se)) =
   walkOnSubExp tv se
 walkExpM tv (BasicOp (ArrayLit els rowt)) =
-  mapM_ (walkOnSubExp tv) els >> walkOnType (walkOnSubExp tv) rowt
+  mapM_ (walkOnSubExp tv) els >> walkOnType tv rowt
 walkExpM tv (BasicOp (BinOp _ x y)) =
   walkOnSubExp tv x >> walkOnSubExp tv y
 walkExpM tv (BasicOp (CmpOp _ x y)) =
@@ -228,9 +219,11 @@
   walkOnSubExp tv x
 walkExpM tv (BasicOp (UnOp _ x)) =
   walkOnSubExp tv x
-walkExpM tv (If c texp fexp (IfDec ts _)) =
-  walkOnSubExp tv c >> walkOnBody tv texp >>
-  walkOnBody tv fexp >> mapM_ (walkOnBranchType tv) ts
+walkExpM tv (If c texp fexp (IfDec ts _)) = do
+  walkOnSubExp tv c
+  walkOnBody tv mempty texp
+  walkOnBody tv mempty fexp
+  mapM_ (walkOnBranchType tv) ts
 walkExpM tv (Apply _ args ret _) =
   mapM_ (walkOnSubExp tv . fst) args >> mapM_ (walkOnRetType tv) ret
 walkExpM tv (BasicOp (Index arr slice)) =
@@ -267,7 +260,8 @@
   walkOnLoopForm tv form
   mapM_ (walkOnSubExp tv) ctxinits
   mapM_ (walkOnSubExp tv) valinits
-  walkOnBody tv loopbody
+  let scope = scopeOfFParams (ctxparams++valparams) <> scopeOf form
+  walkOnBody tv scope loopbody
   where (ctxparams,ctxinits) = unzip ctxmerge
         (valparams,valinits) = unzip valmerge
 walkExpM tv (Op op) =
diff --git a/src/Futhark/Internalise.hs b/src/Futhark/Internalise.hs
--- a/src/Futhark/Internalise.hs
+++ b/src/Futhark/Internalise.hs
@@ -2,8 +2,8 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE Safe #-}
 {-# LANGUAGE Strict #-}
+{-# LANGUAGE Safe #-}
 -- |
 --
 -- This module implements a transformation from source to core
@@ -73,24 +73,26 @@
 internaliseValBind :: E.ValBind -> InternaliseM ()
 internaliseValBind fb@(E.ValBind entry fname retdecl (Info (rettype, _)) tparams params body _ attrs loc) = do
   localConstsScope $ bindingParams tparams params $ \shapeparams params' -> do
-    rettype_bad <- internaliseReturnType rettype
-    let rettype' = zeroExts rettype_bad
-
     let shapenames = map I.paramName shapeparams
         normal_params = shapenames ++ map I.paramName (concat params')
         normal_param_names = namesFromList normal_params
 
     fname' <- internaliseFunName fname params
 
-    body' <- do
-      msg <- case retdecl of
-               Just dt -> errorMsg .
-                          ("Function return value does not match shape of type ":) <$>
-                          typeExpForError dt
-               Nothing -> return $ errorMsg ["Function return value does not match shape of declared return type."]
-      internaliseBody body >>=
-        ensureResultExtShape msg loc (map I.fromDecl rettype')
+    msg <- case retdecl of
+             Just dt -> errorMsg .
+                        ("Function return value does not match shape of type ":) <$>
+                        typeExpForError dt
+             Nothing -> return $ errorMsg ["Function return value does not match shape of declared return type."]
 
+    ((rettype', body_res), body_stms) <- collectStms $ do
+      body_res <- internaliseExp "res" body
+      rettype_bad <- internaliseReturnType rettype
+      let rettype' = zeroExts rettype_bad
+      return (rettype', body_res)
+    body' <- ensureResultExtShape msg loc (map I.fromDecl rettype') $
+             mkBody body_stms body_res
+
     constants <- allConsts
     let free_in_fun = freeIn body'
                       `namesSubtract` normal_param_names
@@ -131,7 +133,8 @@
 allDimsFreshInType = bitraverse onDim pure
   where onDim (E.NamedDim v) =
           E.NamedDim . E.qualName <$> newVName (baseString $ E.qualLeaf v)
-        onDim _ = pure AnyDim
+        onDim _ =
+          E.NamedDim . E.qualName <$> newVName "size"
 
 -- | Replace all named dimensions with a fresh name, and remove all
 -- constant dimensions.  The point is to remove the constraints, but
@@ -327,8 +330,8 @@
         letSubExp desc $ I.BasicOp $ I.Reshape new_shape' flat_arr
 
   | otherwise = do
-      arr_t_ext <- internaliseReturnType $ E.toStruct arr_t
       es' <- mapM (internaliseExp "arr_elem") es
+      arr_t_ext <- internaliseReturnType (E.toStruct arr_t)
 
       rowtypes <-
         case mapM (fmap rowType . hasStaticShape . I.fromDecl) arr_t_ext of
@@ -535,8 +538,8 @@
   bindExtSizes ret retext ses
   return ses
 
-internaliseExp desc (E.LetPat pat e body (Info ret, Info retext) loc) = do
-  ses <- internalisePat desc pat e body loc (internaliseExp desc)
+internaliseExp desc (E.LetPat pat e body (Info ret, Info retext) _) = do
+  ses <- internalisePat desc pat e body (internaliseExp desc)
   bindExtSizes (E.toStruct ret) retext ses
   return ses
 
@@ -553,11 +556,9 @@
   addStms initstms
   mergeinit_ts' <- mapM subExpType mergeinit'
 
-  let ctxinit = argShapes
-                (map I.paramName shapepat)
-                (map I.paramType mergepat')
-                mergeinit_ts'
-      ctxmerge = zip shapepat ctxinit
+  ctxinit <- argShapes (map I.paramName shapepat) mergepat' mergeinit_ts'
+
+  let ctxmerge = zip shapepat ctxinit
       valmerge = zip mergepat' mergeinit'
       dropCond = case form of E.While{} -> drop 1
                               _         -> id
@@ -578,23 +579,20 @@
         loc (map (I.paramName . fst) ctxmerge) merge_ts
     =<< bodyBind loopbody'
 
-  loop_res <- map I.Var . dropCond <$>
-              letTupExp desc (I.DoLoop ctxmerge valmerge form' loopbody'')
+  attrs <- asks envAttrs
+  loop_res <- map I.Var . dropCond <$> attributing attrs
+              (letTupExp desc (I.DoLoop ctxmerge valmerge form' loopbody''))
   bindExtSizes (E.toStruct ret) retext loop_res
   return loop_res
 
   where
     sparams' = map (`TypeParamDim` mempty) sparams
 
-    forLoop nested_mergepat shapepat mergeinit form' = do
-      let mergepat' = concat nested_mergepat
+    forLoop mergepat' shapepat mergeinit form' =
       bodyFromStms $ inScopeOf form' $ do
         ses <- internaliseExp "loopres" loopbody
         sets <- mapM subExpType ses
-        let shapeargs = argShapes
-                        (map I.paramName shapepat)
-                        (map I.paramType mergepat')
-                        sets
+        shapeargs <- argShapes (map I.paramName shapepat) mergepat' sets
         return (shapeargs ++ ses,
                 (form',
                  shapepat,
@@ -608,11 +606,11 @@
 
       i <- newVName "i"
 
-      bindingParams sparams' [mergepat] $
-        \shapepat nested_mergepat ->
+      bindingLoopParams sparams' mergepat $
+        \shapepat mergepat' ->
         bindingLambdaParams [x] (map rowType arr_ts) $ \x_params -> do
           let loopvars = zip x_params arr'
-          forLoop nested_mergepat shapepat mergeinit $
+          forLoop mergepat' shapepat mergeinit $
             I.ForLoop i Int32 w loopvars
 
     handleForm mergeinit (E.For i num_iterations) = do
@@ -623,30 +621,26 @@
               I.Prim (IntType it) -> return it
               _                   -> error "internaliseExp DoLoop: invalid type"
 
-      bindingParams sparams' [mergepat] $
-        \shapepat nested_mergepat ->
-          forLoop nested_mergepat shapepat mergeinit $
+      bindingLoopParams sparams' mergepat $
+        \shapepat mergepat' ->
+          forLoop mergepat' shapepat mergeinit $
           I.ForLoop i' it num_iterations' []
 
     handleForm mergeinit (E.While cond) =
-      bindingParams sparams' [mergepat] $ \shapepat nested_mergepat -> do
+      bindingLoopParams sparams' mergepat $ \shapepat mergepat' -> do
         mergeinit_ts <- mapM subExpType mergeinit
-        let mergepat' = concat nested_mergepat
         -- We need to insert 'cond' twice - once for the initial
         -- condition (do we enter the loop at all?), and once with the
         -- result values of the loop (do we continue into the next
         -- iteration?).  This is safe, as the type rules for the
         -- external language guarantees that 'cond' does not consume
         -- anything.
-        let shapeinit = argShapes
-                        (map I.paramName shapepat)
-                        (map I.paramType mergepat')
-                        mergeinit_ts
+        shapeinit <- argShapes (map I.paramName shapepat) mergepat' mergeinit_ts
 
         (loop_initial_cond, init_loop_cond_bnds) <- collectStms $ do
           forM_ (zip shapepat shapeinit) $ \(p, se) ->
             letBindNames [paramName p] $ BasicOp $ SubExp se
-          forM_ (zip (concat nested_mergepat) mergeinit) $ \(p, se) ->
+          forM_ (zip mergepat' mergeinit) $ \(p, se) ->
             unless (se == I.Var (paramName p)) $
             letBindNames [paramName p] $ BasicOp $
             case se of I.Var v | not $ primType $ paramType p ->
@@ -660,17 +654,14 @@
           ses <- internaliseExp "loopres" loopbody
           sets <- mapM subExpType ses
           loop_while <- newParam "loop_while" $ I.Prim I.Bool
-          let shapeargs = argShapes
-                          (map I.paramName shapepat)
-                          (map I.paramType mergepat')
-                          sets
+          shapeargs <- argShapes (map I.paramName shapepat) mergepat' sets
 
           -- Careful not to clobber anything.
           loop_end_cond_body <- renameBody <=< insertStmsM $ do
             forM_ (zip shapepat shapeargs) $ \(p, se) ->
               unless (se == I.Var (paramName p)) $
               letBindNames [paramName p] $ BasicOp $ SubExp se
-            forM_ (zip (concat nested_mergepat) ses) $ \(p, se) ->
+            forM_ (zip mergepat' ses) $ \(p, se) ->
               unless (se == I.Var (paramName p)) $
               letBindNames [paramName p] $ BasicOp $
               case se of I.Var v | not $ primType $ paramType p ->
@@ -770,14 +761,14 @@
   ses <- internaliseExp (desc ++ "_scrutinee") e
   res <-
     case NE.uncons cs of
-    (CasePat pCase eCase locCase, Nothing) -> do
+    (CasePat pCase eCase _, Nothing) -> do
       (_, pertinent) <- generateCond pCase ses
-      internalisePat' pCase pertinent eCase locCase (internaliseExp desc)
+      internalisePat' pCase pertinent eCase (internaliseExp desc)
     (c, Just cs') -> do
-      let CasePat pLast eLast locLast = NE.last cs'
+      let CasePat pLast eLast _ = NE.last cs'
       bFalse <- do
         (_, pertinent) <- generateCond pLast ses
-        eLast' <- internalisePat' pLast pertinent eLast locLast internaliseBody
+        eLast' <- internalisePat' pLast pertinent eLast internaliseBody
         foldM (\bf c' -> eBody $ return $ generateCaseIf ses c' bf) eLast' $
           reverse $ NE.init cs'
       letTupExp' desc =<< generateCaseIf ses c bFalse
@@ -871,7 +862,7 @@
     -- Literals are always primitive values.
     compares (E.PatternLit e _ _) (se:ses) = do
       e' <- internaliseExp1 "constant" e
-      t' <- I.elemType <$> subExpType se
+      t' <- elemType <$> subExpType se
       cmp <- letSubExp "match_lit" $ I.BasicOp $ I.CmpOp (I.CmpEq t') e' se
       return ([cmp], [se], ses)
 
@@ -922,29 +913,28 @@
               ses'')
 
 generateCaseIf :: [I.SubExp] -> Case -> I.Body -> InternaliseM I.Exp
-generateCaseIf ses (CasePat p eCase loc) bFail = do
+generateCaseIf ses (CasePat p eCase _) bFail = do
   (cond, pertinent) <- generateCond p ses
-  eCase' <- internalisePat' p pertinent eCase loc internaliseBody
+  eCase' <- internalisePat' p pertinent eCase internaliseBody
   eIf (eSubExp cond) (return eCase') (return bFail)
 
 internalisePat :: String -> E.Pattern -> E.Exp
-               -> E.Exp -> SrcLoc -> (E.Exp -> InternaliseM a)
+               -> E.Exp -> (E.Exp -> InternaliseM a)
                -> InternaliseM a
-internalisePat desc p e body loc m = do
+internalisePat desc p e body m = do
   ses <- internaliseExp desc' e
-  internalisePat' p ses body loc m
+  internalisePat' p ses body m
   where desc' = case S.toList $ E.patternIdents p of
                   [v] -> baseString $ E.identName v
                   _ -> desc
 
 internalisePat' :: E.Pattern -> [I.SubExp]
-                -> E.Exp -> SrcLoc -> (E.Exp -> InternaliseM a)
+                -> E.Exp -> (E.Exp -> InternaliseM a)
                 -> InternaliseM a
-internalisePat' p ses body loc m = do
-  t <- I.staticShapes <$> mapM I.subExpType ses
-  stmPattern p t $ \pat_names match -> do
-    ses' <- match loc ses
-    forM_ (zip pat_names ses') $ \(v,se) ->
+internalisePat' p ses body m = do
+  ses_ts <- mapM subExpType ses
+  stmPattern p ses_ts $ \pat_names -> do
+    forM_ (zip pat_names ses) $ \(v,se) ->
       letBindNames [v] $ I.BasicOp $ I.SubExp se
     m body
 
@@ -1389,9 +1379,9 @@
 
 internaliseLambda (E.Lambda params body _ (Info (_, rettype)) _) rowtypes =
   bindingLambdaParams params rowtypes $ \params' -> do
-    rettype' <- internaliseReturnType rettype
     body' <- internaliseBody body
-    return (params', body', map I.fromDecl rettype')
+    rettype' <- internaliseLambdaReturnType rettype
+    return (params', body', rettype')
 
 internaliseLambda e _ = error $ "internaliseLambda: unexpected expression:\n" ++ pretty e
 
@@ -1482,7 +1472,7 @@
                       y_flat <- letExp "y_flat" $ I.BasicOp $ I.Reshape [I.DimNew x_num_elems] y'
 
                       -- Compare the elements.
-                      cmp_lam <- cmpOpLambda (I.CmpEq (elemType x_t)) (elemType x_t)
+                      cmp_lam <- cmpOpLambda $ I.CmpEq (elemType x_t)
                       cmps <- letExp "cmps" $ I.Op $
                               I.Screma x_num_elems (I.mapSOAC cmp_lam) [x_flat, y_flat]
 
@@ -1625,6 +1615,7 @@
            <*> internaliseExp (desc ++ "_zip_y") y
 
     handleRest [x] "unzip" = Just $ flip internaliseExp x
+
     handleRest [x] "trace" = Just $ flip internaliseExp x
     handleRest [x] "break" = Just $ flip internaliseExp x
 
@@ -1726,16 +1717,13 @@
   (fname', closure, shapes, value_paramts, fun_params, rettype_fun) <-
     lookupFunction fname
   argts <- mapM subExpType args
-  closure_ts <- mapM lookupType closure
-  let shapeargs = argShapes shapes value_paramts argts
-      diets = replicate (length closure + length shapeargs) I.ObservePrim ++
+
+  shapeargs <- argShapes shapes fun_params argts
+  let diets = replicate (length closure + length shapeargs) I.ObservePrim ++
               map I.diet value_paramts
-      constOrShape = const $ I.Prim int32
-      paramts = closure_ts ++
-                map constOrShape shapeargs ++ map I.fromDecl value_paramts
   args' <- ensureArgShapes "function arguments of wrong shape"
            loc (map I.paramName fun_params)
-           paramts (map I.Var closure ++ shapeargs ++ args)
+           (map I.paramType fun_params) (map I.Var closure ++ shapeargs ++ args)
   argts' <- mapM subExpType args'
   case rettype_fun $ zip args' argts' of
     Nothing -> error $ "Cannot apply " ++ pretty fname ++ " to arguments\n " ++
@@ -1756,8 +1744,7 @@
 -- language.
 bindExtSizes :: E.StructType -> [VName] -> [SubExp] -> InternaliseM ()
 bindExtSizes ret retext ses = do
-  ts <- concat <$>
-        internaliseParamTypes mempty (M.fromList $ zip retext retext) [ret]
+  ts <- internaliseType ret
   ses_ts <- mapM subExpType ses
 
   let combine t1 t2 =
diff --git a/src/Futhark/Internalise/AccurateSizes.hs b/src/Futhark/Internalise/AccurateSizes.hs
--- a/src/Futhark/Internalise/AccurateSizes.hs
+++ b/src/Futhark/Internalise/AccurateSizes.hs
@@ -10,21 +10,40 @@
   where
 
 import Control.Monad
+import Data.Maybe
 import qualified Data.Map.Strict as M
-import qualified Data.Set as S
 
 import Futhark.Construct
 import Futhark.Internalise.Monad
 import Futhark.IR.SOACS
+import Futhark.Util (takeLast)
 
-argShapes :: [VName] -> [TypeBase Shape u0] -> [TypeBase Shape u1] -> [SubExp]
-argShapes shapes valts valargts =
-  map addShape shapes
-  where mapping = shapeMapping valts valargts
-        addShape name =
-          case M.lookup name mapping of
-            Just s | se:_ <- S.toList s -> se
-            _ -> intConst Int32 0
+shapeMapping :: HasScope SOACS m =>
+                [FParam] -> [Type]
+             -> m (M.Map VName SubExp)
+shapeMapping all_params value_arg_types =
+  mconcat <$> zipWithM f value_params value_arg_types
+  where value_params = takeLast (length value_arg_types) all_params
+
+        f (Param _ t1@Array{}) t2@Array{} =
+          pure $ M.fromList $ mapMaybe match $ zip (arrayDims t1) (arrayDims t2)
+        f _ _ =
+          pure mempty
+
+        match (Var v, se) = Just (v, se)
+        match _ = Nothing
+
+argShapes :: (HasScope SOACS m, Monad m) =>
+             [VName] -> [FParam] -> [Type] -> m [SubExp]
+argShapes shapes all_params valargts = do
+  mapping <- shapeMapping all_params valargts
+  let addShape name =
+        case M.lookup name mapping of
+          Just se -> se
+          _ -> intConst Int32 0 -- FIXME: we only need this because
+                                -- the defunctionaliser throws away
+                                -- sizes.
+  return $ map addShape shapes
 
 ensureResultShape :: ErrorMsg SubExp -> SrcLoc -> [Type] -> Body
                   -> InternaliseM Body
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
@@ -1,28 +1,25 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE Safe #-}
+-- | Internalising bindings.
 module Futhark.Internalise.Bindings
   (
-  -- * Internalising bindings
     bindingParams
+  , bindingLoopParams
   , bindingLambdaParams
   , stmPattern
-  , MatchPattern
   )
   where
 
 import Control.Monad.State  hiding (mapM)
 import Control.Monad.Reader hiding (mapM)
-import Control.Monad.Writer hiding (mapM)
 
 import qualified Data.Map.Strict as M
-import qualified Data.Set as S
 
 import Language.Futhark as E hiding (matchDims)
 import qualified Futhark.IR.SOACS as I
 import Futhark.MonadFreshNames
 import Futhark.Internalise.Monad
 import Futhark.Internalise.TypesValues
-import Futhark.Internalise.AccurateSizes
 import Futhark.Util
 
 bindingParams :: [E.TypeParam] -> [E.Pattern]
@@ -30,43 +27,44 @@
               -> InternaliseM a
 bindingParams tparams params m = do
   flattened_params <- mapM flattenPattern params
-  let (params_idents, params_types) = unzip $ concat flattened_params
-      bound = boundInTypes tparams
-      param_names = M.fromList [ (E.identName x, y) | (x,y) <- params_idents ]
-  params_ts <- internaliseParamTypes bound param_names params_types
+  let params_idents = concat flattened_params
+  params_ts <-
+    internaliseParamTypes $
+    map (flip E.setAliases () . E.unInfo . E.identType) params_idents
   let num_param_idents = map length flattened_params
       num_param_ts = map (sum . map length) $ chunks num_param_idents params_ts
 
-  (params_ts', unnamed_shape_params) <-
-    fmap unzip $ forM params_ts $ \param_ts -> do
-      (param_ts', param_unnamed_dims) <- instantiateShapesWithDecls mempty param_ts
+  let shape_params = [ I.Param v $ I.Prim I.int32 | E.TypeParamDim v _ <- tparams ]
+      shape_subst = M.fromList [ (I.paramName p, [I.Var $ I.paramName p]) | p <- shape_params ]
+  bindingFlatPattern params_idents (concat params_ts) $ \valueparams ->
+    I.localScope (I.scopeOfFParams $ shape_params++concat valueparams) $
+    substitutingVars shape_subst $ m shape_params $
+    chunks num_param_ts (concat valueparams)
 
-      return (param_ts',
-              param_unnamed_dims)
+bindingLoopParams :: [E.TypeParam] -> E.Pattern
+                  -> ([I.FParam] -> [I.FParam] -> InternaliseM a)
+                  -> InternaliseM a
+bindingLoopParams tparams pat m = do
+  pat_idents <- flattenPattern pat
+  pat_ts <- internaliseLoopParamType (E.patternStructType pat)
 
-  let named_shape_params = [ I.Param v $ I.Prim I.int32 | E.TypeParamDim v _ <- tparams ]
-      shape_params = named_shape_params ++ concat unnamed_shape_params
+  let shape_params = [ I.Param v $ I.Prim I.int32 | E.TypeParamDim v _ <- tparams ]
       shape_subst = M.fromList [ (I.paramName p, [I.Var $ I.paramName p]) | p <- shape_params ]
-  bindingFlatPattern params_idents (concat params_ts') $ \valueparams ->
+
+  bindingFlatPattern pat_idents pat_ts $ \valueparams ->
     I.localScope (I.scopeOfFParams $ shape_params++concat valueparams) $
-    substitutingVars shape_subst $ m shape_params $ chunks num_param_ts (concat valueparams)
+    substitutingVars shape_subst $ m shape_params $ concat valueparams
 
 bindingLambdaParams :: [E.Pattern] -> [I.Type]
                     -> ([I.LParam] -> InternaliseM a)
                     -> InternaliseM a
 bindingLambdaParams params ts m = do
-  (params_idents, params_types) <-
-    unzip . concat <$> mapM flattenPattern params
-  let param_names = M.fromList [ (E.identName x, y) | (x,y) <- params_idents ]
-  params_ts <- internaliseParamTypes mempty param_names params_types
-
-  let ascript_substs = lambdaShapeSubstitutions (concat params_ts) ts
+  params_idents <- concat <$> mapM flattenPattern params
 
   bindingFlatPattern params_idents ts $ \params' ->
-    local (\env -> env { envSubsts = ascript_substs `M.union` envSubsts env }) $
     I.localScope (I.scopeOfLParams $ concat params') $ m $ concat params'
 
-processFlatPattern :: Show t => [(E.Ident,VName)] -> [t]
+processFlatPattern :: Show t => [E.Ident] -> [t]
                    -> InternaliseM ([[I.Param t]], VarSubstitutions)
 processFlatPattern x y = processFlatPattern' [] x y
   where
@@ -76,8 +74,8 @@
           idents = reverse vs
       return (idents, substs')
 
-    processFlatPattern' pat ((p,name):rest) ts = do
-      (ps, subst, rest_ts) <- handleMapping ts <$> internaliseBindee (p, name)
+    processFlatPattern' pat (p:rest) ts = do
+      (ps, subst, rest_ts) <- handleMapping ts <$> internaliseBindee p
       processFlatPattern' ((ps, (E.identName p, map (I.Var . I.paramName) subst)) : pat) rest rest_ts
 
     handleMapping ts [] =
@@ -87,26 +85,21 @@
             (pss, repss, ts'') = handleMapping ts' rs
         in (ps++pss, reps:repss, ts'')
 
-    handleMapping' (t:ts) (vname,_) =
+    handleMapping' (t:ts) vname =
       let v' = I.Param vname t
       in ([v'], v', ts)
     handleMapping' [] _ =
       error $ "processFlatPattern: insufficient identifiers in pattern." ++ show (x, y)
 
-    internaliseBindee :: (E.Ident, VName) -> InternaliseM [(VName, I.DeclExtType)]
-    internaliseBindee (bindee, name) = do
-      tss <- internaliseParamTypes nothing_bound mempty
-             [flip E.setAliases () $ E.unInfo $ E.identType bindee]
-      case concat tss of
-        [t] -> return [(name, t)]
-        tss' -> forM tss' $ \t -> do
-          name' <- newVName $ baseString name
-          return (name', t)
-
-    -- Fixed up later.
-    nothing_bound = boundInTypes []
+    internaliseBindee :: E.Ident -> InternaliseM [VName]
+    internaliseBindee bindee = do
+      let name = E.identName bindee
+      n <- internalisedTypeSize $ flip E.setAliases () $ E.unInfo $ E.identType bindee
+      case n of
+        1 -> return [name]
+        _ -> replicateM n $ newVName $ baseString name
 
-bindingFlatPattern :: Show t => [(E.Ident, VName)] -> [t]
+bindingFlatPattern :: Show t => [E.Ident] -> [t]
                    -> ([[I.Param t]] -> InternaliseM a)
                    -> InternaliseM a
 bindingFlatPattern idents ts m = do
@@ -116,17 +109,15 @@
 
 -- | Flatten a pattern.  Returns a list of identifiers.  The
 -- structural type of each identifier is returned separately.
-flattenPattern :: MonadFreshNames m => E.Pattern -> m [((E.Ident, VName), E.StructType)]
+flattenPattern :: MonadFreshNames m => E.Pattern -> m [E.Ident]
 flattenPattern = flattenPattern'
   where flattenPattern' (E.PatternParens p _) =
           flattenPattern' p
         flattenPattern' (E.Wildcard t loc) = do
           name <- newVName "nameless"
           flattenPattern' $ E.Id name t loc
-        flattenPattern' (E.Id v (Info t) loc) = do
-          new_name <- newVName $ baseString v
-          return [((E.Ident v (Info t) loc, new_name),
-                   t `E.setAliases` ())]
+        flattenPattern' (E.Id v (Info t) loc) =
+          return [E.Ident v (Info t) loc]
         -- XXX: treat empty tuples and records as bool.
         flattenPattern' (E.TuplePattern [] loc) =
           flattenPattern' (E.Wildcard (Info $ E.Scalar $ E.Prim E.Bool) loc)
@@ -143,63 +134,11 @@
         flattenPattern' (E.PatternConstr _ _ ps _) =
           concat <$> mapM flattenPattern' ps
 
-type MatchPattern = SrcLoc -> [I.SubExp] -> InternaliseM [I.SubExp]
-
-stmPattern :: E.Pattern -> [I.ExtType]
-           -> ([VName] -> MatchPattern -> InternaliseM a)
+stmPattern :: E.Pattern -> [I.Type]
+           -> ([VName] -> InternaliseM a)
            -> InternaliseM a
 stmPattern pat ts m = do
-  (pat', pat_types) <- unzip <$> flattenPattern pat
-  (ts',_) <- instantiateShapes' ts
-  pat_types' <- internaliseParamTypes mempty mempty pat_types
-  let pat_types'' = map I.fromDecl $ concat pat_types'
+  pat' <- flattenPattern pat
   let addShapeStms l =
-        m (map I.paramName $ concat l) (matchPattern pat_types'')
-  bindingFlatPattern pat' ts' addShapeStms
-
-matchPattern :: [I.ExtType] -> MatchPattern
-matchPattern exts loc ses =
-  forM (zip exts ses) $ \(et, se) -> do
-  se_t <- I.subExpType se
-  et' <- unExistentialise mempty et se_t
-  ensureExtShape (I.ErrorMsg [I.ErrorString "value cannot match pattern"])
-    loc et' "correct_shape" se
-
-unExistentialise :: S.Set VName -> I.ExtType -> I.Type -> InternaliseM I.ExtType
-unExistentialise tparam_names et t = do
-  new_dims <- zipWithM inspectDim (I.shapeDims $ I.arrayShape et) (I.arrayDims t)
-  return $ t `I.setArrayShape` I.Shape new_dims
-  where inspectDim (I.Free (I.Var v)) d
-          | v `S.member` tparam_names = do
-              letBindNames [v] $ I.BasicOp $ I.SubExp d
-              return $ I.Free $ I.Var v
-        inspectDim ed _ = return ed
-
-instantiateShapesWithDecls :: MonadFreshNames m =>
-                              M.Map Int I.Ident
-                           -> [I.DeclExtType]
-                           -> m ([I.DeclType], [I.FParam])
-instantiateShapesWithDecls ctx ts =
-  runWriterT $ instantiateShapes instantiate ts
-  where instantiate x
-          | Just v <- M.lookup x ctx =
-            return $ I.Var $ I.identName v
-
-          | otherwise = do
-            v <- lift $ nonuniqueParamFromIdent <$> newIdent "size" (I.Prim I.int32)
-            tell [v]
-            return $ I.Var $ I.paramName v
-
-lambdaShapeSubstitutions :: [I.TypeBase I.ExtShape Uniqueness]
-                         -> [I.Type]
-                         -> VarSubstitutions
-lambdaShapeSubstitutions param_ts ts =
-  mconcat $ zipWith matchTypes param_ts ts
-  where matchTypes pt t =
-          mconcat $ zipWith matchDims (I.shapeDims $ I.arrayShape pt) (I.arrayDims t)
-        matchDims (I.Free (I.Var v)) d = M.singleton v [d]
-        matchDims _ _ = mempty
-
-nonuniqueParamFromIdent :: I.Ident -> I.FParam
-nonuniqueParamFromIdent (I.Ident name t) =
-  I.Param name $ I.toDecl t Nonunique
+        m (map I.paramName $ concat l)
+  bindingFlatPattern pat' ts addShapeStms
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
@@ -6,9 +6,11 @@
   ( transformProg ) where
 
 import qualified Control.Arrow as Arrow
+import           Control.Monad.Identity
 import           Control.Monad.State
 import           Control.Monad.RWS hiding (Sum)
 import           Data.Bifunctor
+import           Data.Bitraversable
 import           Data.Foldable
 import           Data.List (sortOn, nub, partition, tails)
 import qualified Data.List.NonEmpty as NE
@@ -19,6 +21,7 @@
 
 import           Futhark.MonadFreshNames
 import           Language.Futhark
+import           Language.Futhark.Traversals
 import           Futhark.IR.Pretty ()
 
 -- | An expression or an extended 'Lambda' (with size parameters,
@@ -125,7 +128,11 @@
 arraySizes (Scalar Arrow{}) = mempty
 arraySizes (Scalar (Record fields)) = foldMap arraySizes fields
 arraySizes (Scalar (Sum cs)) = foldMap (foldMap arraySizes) cs
-arraySizes (Scalar TypeVar{}) = mempty
+arraySizes (Scalar (TypeVar _ _ _ targs)) =
+  mconcat $ map f targs
+  where f (TypeArgDim (NamedDim d) _) = S.singleton $ qualLeaf d
+        f TypeArgDim{} = mempty
+        f (TypeArgType t _) = arraySizes t
 arraySizes (Scalar Prim{}) = mempty
 arraySizes (Array _ _ t shape) =
   arraySizes (Scalar t) <> foldMap dimName (shapeDims shape)
@@ -176,7 +183,7 @@
 
   -- The closure parts that are sizes are proactively turned into size
   -- parameters.
-  let sizes_of_arrays = foldMap (arraySizes . toStruct . typeFromSV) used_env <>
+  let sizes_of_arrays = foldMap (arraySizes . toStruct . typeFromSV') used_env <>
                         patternArraySizes pat
       notSize = not . (`S.member` sizes_of_arrays)
       (fields, env) = unzip $ map closureFromDynamicFun $
@@ -184,8 +191,11 @@
       env' = M.fromList env
       closure_dims = S.toList sizes_of_arrays
 
+  global <- asks fst
+
   return (RecordLit fields loc,
-          LambdaSV (nub $ dims<>closure_dims) pat ret' e0' env')
+          LambdaSV (nub $ filter (`S.notMember` global) $
+                    dims<>closure_dims) pat ret' e0' env')
 
   where closureFromDynamicFun (vn, DynamicFun (clsr_env, sv) _) =
           let name = nameFromString $ pretty vn
@@ -193,7 +203,7 @@
 
         closureFromDynamicFun (vn, sv) =
           let name = nameFromString $ pretty vn
-              tp' = typeFromSV sv
+              tp' = typeFromSV' sv
           in (RecordFieldExplicit name
                (Var (qualName vn) (Info tp') mempty) mempty, (vn, sv))
 
@@ -243,7 +253,7 @@
                                                 (vn', sv'))
             -- The field may refer to a functional expression, so we get the
             -- type from the static value and not the one from the AST.
-            _ -> let tp = Info $ typeFromSV sv
+            _ -> let tp = Info $ typeFromSV' sv
                  in return (RecordFieldImplicit vn tp loc', (baseName vn, sv))
 
 defuncExp (ArrayLit es t@(Info t') loc) = do
@@ -268,7 +278,7 @@
     IntrinsicSV -> do
       (pats, body, tp) <- etaExpand (typeOf e) e
       defuncExp $ Lambda pats body Nothing (Info (mempty, tp)) mempty
-    _ -> let tp = typeFromSV sv
+    _ -> let tp = typeFromSV' sv
          in return (Var qn (Info tp) loc, sv)
 
 defuncExp (Ascript e0 tydecl loc)
@@ -284,7 +294,7 @@
 defuncExp (LetPat pat e1 e2 (Info t, retext) loc) = do
   (e1', sv1) <- defuncExp e1
   let env  = matchPatternSV pat sv1
-      pat' = updatePattern pat sv1
+      pat' = updatePattern' pat sv1
   (e2', sv2) <- localEnv env $ defuncExp e2
   -- To maintain any sizes going out of scope, we need to compute the
   -- old size substitution induced by retext and also apply it to the
@@ -295,13 +305,20 @@
   return (LetPat pat' e1' e2' (Info t', retext) loc, sv2)
 
 -- Local functions are handled by rewriting them to lambdas, so that
--- the same machinery can be re-used.
-defuncExp (LetFun vn (dims, pats, _, Info ret, e1) e2 _ loc) = do
-  (e1', sv1) <- defuncFun dims pats e1 (mempty, ret) loc
-  (e2', sv2) <- localEnv (M.singleton vn sv1) $ defuncExp e2
-  return (LetPat (Id vn (Info (typeOf e1')) loc) e1' e2' (Info $ typeOf e2', Info []) loc,
-          sv2)
+-- the same machinery can be re-used.  But we may have to eta-expand
+-- first.
+defuncExp (LetFun vn (dims, pats, _, Info ret, e1) e2 let_t loc)
+  | Scalar Arrow{} <- ret = do
+      (body_pats, e1', ret') <- etaExpand (fromStruct ret) e1
+      let f = (dims, pats <> body_pats, Nothing, Info ret', e1')
+      defuncExp $ LetFun vn f e2 let_t loc
 
+  | otherwise = do
+      (e1', sv1) <- defuncFun dims pats e1 (mempty, ret) loc
+      (e2', sv2) <- localEnv (M.singleton vn sv1) $ defuncExp e2
+      return (LetPat (Id vn (Info (typeOf e1')) loc) e1' e2' (Info $ typeOf e2', Info []) loc,
+              sv2)
+
 defuncExp (If e1 e2 e3 tp loc) = do
   (e1', _ ) <- defuncExp e1
   (e2', sv) <- defuncExp e2
@@ -361,7 +378,7 @@
   (e0', sv0) <- defuncExp e0
   case sv0 of
     RecordSV svs -> case lookup vn svs of
-      Just sv -> return (Project vn e0' (Info $ typeFromSV sv) loc, sv)
+      Just sv -> return (Project vn e0' (Info $ typeFromSV' sv) loc, sv)
       Nothing -> error "Invalid record projection."
     Dynamic _ -> return (Project vn e0' tp loc, Dynamic tp')
     _ -> error $ "Projection of an expression with static value " ++ show sv0
@@ -391,7 +408,7 @@
   (e1', sv1) <- defuncExp e1
   (e2', sv2) <- defuncExp e2
   let sv = staticField sv1 sv2 fs
-  return (RecordUpdate e1' fs e2' (Info $ 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
@@ -411,7 +428,7 @@
   (es', svs) <- unzip <$> mapM defuncExp es
   let sv = SumSV name svs $ M.toList $
            name `M.delete` M.map (map defuncType) all_fs
-  return (Constr name es' (Info (typeFromSV sv)) loc, sv)
+  return (Constr name es' (Info (typeFromSV' sv)) loc, sv)
   where defuncType :: Monoid als =>
                       TypeBase (DimDecl VName) als
                    -> TypeBase (DimDecl VName) als
@@ -453,7 +470,7 @@
 
 defuncCase :: StaticVal -> Case -> DefM (Case, StaticVal)
 defuncCase sv (CasePat p e loc) = do
-  let p'  = updatePattern p sv
+  let p'  = updatePattern' p sv
       env = matchPatternSV p sv
   (e', sv') <- localEnv env $ defuncExp e
   return (CasePat p' e' loc, sv')
@@ -534,6 +551,16 @@
           RecordSV $ M.toList $ M.intersectionWith imposeType (M.fromList fs1) fs2
         imposeType sv _ = sv
 
+sizesForAll :: MonadFreshNames m => [Pattern] -> m ([VName], [Pattern])
+sizesForAll params = do
+  (params', sizes) <- runStateT (mapM (astMap tv) params) []
+  return (sizes, params')
+  where tv = identityMapper { mapOnPatternType = bitraverse onDim pure }
+        onDim AnyDim = do v <- lift $ newVName "size"
+                          modify (v:)
+                          pure $ NamedDim $ qualName v
+        onDim d = pure d
+
 -- | Defunctionalize an application expression at a given depth of application.
 -- Calls to dynamic (first-order) functions are preserved at much as possible,
 -- but a new lifted function is created if a dynamic function is only partially
@@ -553,6 +580,8 @@
       let closure_pat = buildEnvPattern closure_env
           pat' = updatePattern pat sv2
 
+      globals <- asks fst
+
       -- Lift lambda to top-level function definition.  We put in
       -- a lot of effort to try to infer the uniqueness attributes
       -- of the lifted function, but this is ultimately all a sham
@@ -563,7 +592,7 @@
           svParams _                         = []
           rettype = buildRetType closure_env params_for_rettype e0_t $ typeOf e0'
 
-          already_bound = S.fromList dims <>
+          already_bound = globals <> S.fromList dims <>
                           S.map identName (foldMap patternIdents params)
           more_dims = S.toList $
                       S.filter (`S.notMember` already_bound) $
@@ -578,8 +607,14 @@
             liftedName (i+1) f
           liftedName _ _ = "lifted"
 
+      -- Ensure that no parameter sizes are AnyDim.  The internaliser
+      -- expects this.  This is easy, because they are all
+      -- first-order.
+      (missing_dims, params') <- sizesForAll params
+
       fname <- newNameFromString $ liftedName (0::Int) e1
-      liftValDec fname rettype (dims ++ more_dims) params e0'
+      liftValDec fname rettype (dims ++ more_dims ++ missing_dims)
+        params' e0'
 
       let t1 = toStruct $ typeOf e1'
           t2 = toStruct $ typeOf e2'
@@ -655,7 +690,7 @@
 
       IntrinsicSV -> return (e, IntrinsicSV)
 
-      _ -> return (Var qn (Info (typeFromSV sv)) loc, sv)
+      _ -> return (Var qn (Info (typeFromSV' sv)) loc, sv)
 
 defuncApply depth (Parens e _) = defuncApply depth e
 
@@ -741,7 +776,7 @@
 buildEnvPattern env = RecordPattern (map buildField $ M.toList env) mempty
   where buildField (vn, sv) =
           (nameFromString (pretty vn),
-           Id vn (Info $ typeFromSV sv) mempty)
+           Id vn (Info $ snd $ typeFromSV sv) mempty)
 
 -- | Given a closure environment pattern and the type of a term,
 -- construct the type of that term, where uniqueness is set to
@@ -772,29 +807,38 @@
         descend t = t
 
 -- | Compute the corresponding type for a given static value.
-typeFromSV :: StaticVal -> PatternType
-typeFromSV (Dynamic tp) = tp
+typeFromSV :: StaticVal -> ([VName], PatternType)
+typeFromSV (Dynamic tp) =
+  (mempty, tp)
 typeFromSV (LambdaSV sizes _ _ _ env) =
-  unscopeType (S.fromList sizes) $ typeFromEnv env
+  (sizes <> env_sizes,
+   Scalar $ Record $ M.fromList $ map (fmap snd) env')
+  where env' = map (bimap (nameFromString . pretty) typeFromSV) $ M.toList env
+        env_sizes = concatMap (fst . snd) env'
 typeFromSV (RecordSV ls) =
-  Scalar $ Record $ M.fromList $ map (fmap typeFromSV) ls
+  let ts = map (fmap typeFromSV) ls
+  in (concatMap (fst . snd) ts,
+      Scalar $ Record $ M.fromList $ map (fmap snd) ts)
 typeFromSV (DynamicFun (_, sv) _) =
   typeFromSV sv
 typeFromSV (SumSV name svs fields) =
-  Scalar $ Sum $ M.insert name (map typeFromSV svs) $ M.fromList fields
+  let (sizes, svs') = unzip $ map typeFromSV svs
+  in (concat sizes,
+      Scalar $ Sum $ M.insert name svs' $ M.fromList fields)
 typeFromSV IntrinsicSV =
   error "Tried to get the type from the static value of an intrinsic."
 
-typeFromEnv :: Env -> PatternType
-typeFromEnv = Scalar . Record . M.fromList .
-              map (bimap (nameFromString . pretty) typeFromSV) . M.toList
+typeFromSV' :: StaticVal -> PatternType
+typeFromSV' sv =
+  let (sizes, t) = typeFromSV sv
+  in unscopeType (S.fromList sizes) t
 
 -- | Construct the type for a fully-applied dynamic function from its
 -- static value and the original types of its arguments.
 dynamicFunType :: StaticVal -> [PatternType] -> ([PatternType], PatternType)
 dynamicFunType (DynamicFun _ sv) (p:ps) =
   let (ps', ret) = dynamicFunType sv ps in (p : ps', ret)
-dynamicFunType sv _ = ([], 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
@@ -850,7 +894,7 @@
 updatePattern (PatternParens pat loc) sv =
   PatternParens (updatePattern pat sv) loc
 updatePattern (Id vn (Info tp) loc) sv =
-  Id vn (Info $ comb tp (typeFromSV sv  `setUniqueness` Nonunique)) loc
+  Id vn (Info $ comb tp (snd (typeFromSV sv)  `setUniqueness` Nonunique)) loc
   -- Preserve any original zeroth-order types.
   where comb (Scalar Arrow{}) t2 = t2
         comb (Scalar (Record m1)) (Scalar (Record m2)) =
@@ -860,7 +904,7 @@
         comb t1 _ = t1 -- t1 must be array or prim.
 updatePattern pat@(Wildcard (Info tp) loc) sv
   | orderZero tp = pat
-  | otherwise = Wildcard (Info $ typeFromSV sv) loc
+  | otherwise = Wildcard (Info $ snd $ typeFromSV sv) loc
 updatePattern (PatternAscription pat tydecl loc) sv
   | orderZero . unInfo $ expandedType tydecl =
       PatternAscription (updatePattern pat sv) tydecl loc
@@ -869,7 +913,7 @@
 updatePattern pat@(PatternConstr c1 (Info t) ps loc) sv@(SumSV _ svs _)
   | orderZero t = pat
   | otherwise = PatternConstr c1 (Info t') ps' loc
-  where t' = typeFromSV sv `setUniqueness` Nonunique
+  where t' = snd (typeFromSV sv) `setUniqueness` Nonunique
         ps' = zipWith updatePattern ps svs
 updatePattern (PatternConstr c1 _ ps loc) (Dynamic t) =
   PatternConstr c1 (Info t) ps loc
@@ -878,6 +922,18 @@
   error $ "Tried to update pattern " ++ pretty pat
        ++ "to reflect the static value " ++ show sv
 
+-- Like updatePattern, but discard sizes.  This is used for
+-- let-bindings, where we might otherwise introduce sizes that are
+-- free.
+updatePattern' :: Pattern -> StaticVal -> Pattern
+updatePattern' pat sv =
+  let pat' = updatePattern pat sv
+      (sizes, _) = typeFromSV sv
+      tr = identityMapper { mapOnPatternType =
+                              pure . unscopeType (S.fromList sizes)
+                          }
+  in runIdentity $ astMap tr pat'
+
 -- | 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 :: PatternType -> StaticVal
@@ -1003,17 +1059,20 @@
 defuncValBind valbind@(ValBind _ name retdecl (Info (rettype, retext)) tparams params body _ _ _) = do
   (tparams', params', body', sv) <- defuncLet tparams params body rettype
   let rettype' = combineTypeShapes rettype $ anySizes $ toStruct $ typeOf body'
+  (missing_dims, params'') <- sizesForAll params'
   return ( valbind { valBindRetDecl    = retdecl
                    , valBindRetType    = Info (if null params'
                                                then rettype' `setUniqueness` Nonunique
                                                else rettype',
                                                retext)
-                   , valBindTypeParams = tparams'
-                   , valBindParams     = params'
+                   , valBindTypeParams = tparams' ++
+                                         map (`TypeParamDim` mempty) missing_dims
+                   , valBindParams     = params''
                    , valBindBody       = body'
                    }
          , M.singleton name sv
          , case sv of DynamicFun{} -> True
+                      Dynamic{}    -> True
                       _            -> False)
 
 -- | Defunctionalize a list of top-level declarations.
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
@@ -176,7 +176,7 @@
         let forward (k,v) = (lookupSubst k outer_substs, v)
             p_substs' = M.fromList $ map forward $ M.toList p_substs
             abs_substs = M.filterWithKey (const . flip S.member abs) $
-                         p_substs' <>
+                         M.map (`lookupSubst` scopeSubsts (modScope arg_mod)) p_substs' <>
                          scopeSubsts f_closure <>
                          scopeSubsts (modScope arg_mod)
         extendScope (Scope abs_substs (M.singleton (modParamName f_p) $
diff --git a/src/Futhark/Internalise/Lambdas.hs b/src/Futhark/Internalise/Lambdas.hs
--- a/src/Futhark/Internalise/Lambdas.hs
+++ b/src/Futhark/Internalise/Lambdas.hs
@@ -17,7 +17,7 @@
 
 -- | A function for internalising lambdas.
 type InternaliseLambda =
-  E.Exp -> [I.Type] -> InternaliseM ([I.LParam], I.Body, [I.ExtType])
+  E.Exp -> [I.Type] -> InternaliseM ([I.LParam], I.Body, [I.Type])
 
 internaliseMapLambda :: InternaliseLambda
                      -> E.Exp
@@ -27,12 +27,11 @@
   argtypes <- mapM I.subExpType args
   let rowtypes = map I.rowType argtypes
   (params, body, rettype) <- internaliseLambda lam rowtypes
-  (rettype', _) <- instantiateShapes' rettype
   body' <- localScope (scopeOfLParams params) $
            ensureResultShape
            (ErrorMsg [ErrorString "not all iterations produce same shape"])
-           (srclocOf lam) rettype' body
-  return $ I.Lambda params body' rettype'
+           (srclocOf lam) rettype body
+  return $ I.Lambda params body' rettype
 
 internaliseStreamMapLambda :: InternaliseLambda
                            -> E.Exp
@@ -50,13 +49,12 @@
     body <- runBodyBinder $ do
       letBindNames [paramName orig_chunk_param] $ I.BasicOp $ I.SubExp $ I.Var chunk_size
       return orig_body
-    (rettype', _) <- instantiateShapes' rettype
     body' <- localScope (scopeOfLParams params) $ insertStmsM $ do
       letBindNames [paramName orig_chunk_param] $ I.BasicOp $ I.SubExp $ I.Var chunk_size
       ensureResultShape
         (ErrorMsg [ErrorString "not all iterations produce same shape"])
-        (srclocOf lam) (map outer rettype') body
-    return $ I.Lambda (chunk_param:params) body' (map outer rettype')
+        (srclocOf lam) (map outer rettype) body
+    return $ I.Lambda (chunk_param:params) body' (map outer rettype)
 
 internaliseFoldLambda :: InternaliseLambda
                       -> E.Exp
diff --git a/src/Futhark/Internalise/Monad.hs b/src/Futhark/Internalise/Monad.hs
--- a/src/Futhark/Internalise/Monad.hs
+++ b/src/Futhark/Internalise/Monad.hs
@@ -29,14 +29,6 @@
 
   , assert
 
-  -- * Type Handling
-  , InternaliseTypeM
-  , liftInternaliseM
-  , runInternaliseTypeM
-  , lookupDim
-  , withDims
-  , DimTable
-
     -- * Convenient reexports
   , module Futhark.Tools
   )
@@ -216,29 +208,3 @@
 assertingOne :: InternaliseM VName
              -> InternaliseM Certificates
 assertingOne m = asserting $ Certificates . pure <$> m
-
-type DimTable = M.Map VName ExtSize
-
-newtype TypeEnv = TypeEnv { typeEnvDims  :: DimTable }
-
-type TypeState = Int
-
-newtype InternaliseTypeM a =
-  InternaliseTypeM (ReaderT TypeEnv (StateT TypeState InternaliseM) a)
-  deriving (Functor, Applicative, Monad,
-            MonadReader TypeEnv,
-            MonadState TypeState)
-
-liftInternaliseM :: InternaliseM a -> InternaliseTypeM a
-liftInternaliseM = InternaliseTypeM . lift . lift
-
-runInternaliseTypeM :: InternaliseTypeM a
-                    -> InternaliseM a
-runInternaliseTypeM (InternaliseTypeM m) =
-  evalStateT (runReaderT m (TypeEnv mempty)) 0
-
-withDims :: DimTable -> InternaliseTypeM a -> InternaliseTypeM a
-withDims dtable = local $ \env -> env { typeEnvDims = dtable <> typeEnvDims env }
-
-lookupDim :: VName -> InternaliseTypeM (Maybe ExtSize)
-lookupDim name = asks $ M.lookup name . typeEnvDims
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
@@ -197,6 +197,16 @@
            then second (mconcat . map replace . S.toList) t
            else t
 
+sizesForPat :: MonadFreshNames m => Pattern -> m ([VName], Pattern)
+sizesForPat pat = do
+  (params', sizes) <- runStateT (astMap tv pat) []
+  return (sizes, params')
+  where tv = identityMapper { mapOnPatternType = bitraverse onDim pure }
+        onDim AnyDim = do v <- lift $ newVName "size"
+                          modify (v:)
+                          pure $ NamedDim $ qualName v
+        onDim d = pure d
+
 -- Monomorphization of expressions.
 transformExp :: Exp -> MonoM Exp
 transformExp e@Literal{} = return e
@@ -329,7 +339,11 @@
     ForIn pat2 e2 -> ForIn pat2 <$> transformExp e2
     While e2      -> While <$> transformExp e2
   e3' <- transformExp e3
-  return $ DoLoop sparams pat e1' form' e3' ret loc
+  -- Maybe monomorphisation introduced new arrays to the loop, and
+  -- maybe they have AnyDim sizes.  This is not allowed.  Invent some
+  -- sizes for them.
+  (pat_sizes, pat') <- sizesForPat pat
+  return $ DoLoop (sparams++pat_sizes) pat' e1' form' e3' ret loc
 
 transformExp (BinOp (fname, oploc) (Info t) (e1, d1) (e2, d2) tp ext loc) = do
   fname' <- transformFName loc fname $ toStruct 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
@@ -4,12 +4,12 @@
 module Futhark.Internalise.TypesValues
   (
    -- * Internalising types
-    BoundInTypes
-  , boundInTypes
-  , internaliseReturnType
+    internaliseReturnType
+  , internaliseLambdaReturnType
   , internaliseEntryReturnType
-  , internaliseParamTypes
   , internaliseType
+  , internaliseParamTypes
+  , internaliseLoopParamType
   , internalisePrimType
   , internalisedTypeSize
   , internaliseSumType
@@ -18,12 +18,11 @@
   , internalisePrimValue
   )
   where
-
+import Control.Monad.Reader
 import Control.Monad.State
 import Data.List (delete, find, foldl')
-import qualified Data.Map.Strict as M
-import qualified Data.Set as S
 import Data.Maybe
+import qualified Data.Map.Strict as M
 
 import qualified Language.Futhark as E
 import Futhark.IR.SOACS as I
@@ -33,39 +32,50 @@
 internaliseUniqueness E.Nonunique = I.Nonunique
 internaliseUniqueness E.Unique = I.Unique
 
--- | The names that are bound for some types, either implicitly or
--- explicitly.
-newtype BoundInTypes = BoundInTypes (S.Set VName)
-                       deriving (Semigroup, Monoid)
+type TypeState = Int
 
--- | Determine the names bound for some types.
-boundInTypes :: [E.TypeParam] -> BoundInTypes
-boundInTypes = BoundInTypes . S.fromList . mapMaybe isTypeParam
-  where isTypeParam (E.TypeParamDim v _) = Just v
-        isTypeParam _ = Nothing
+newtype InternaliseTypeM a =
+  InternaliseTypeM (StateT TypeState InternaliseM a)
+  deriving (Functor, Applicative, Monad, MonadState TypeState)
 
-internaliseParamTypes :: BoundInTypes
-                      -> M.Map VName VName
-                      -> [E.TypeBase (E.DimDecl VName) ()]
-                      -> InternaliseM [[I.TypeBase ExtShape Uniqueness]]
-internaliseParamTypes (BoundInTypes bound) pnames ts =
-  runInternaliseTypeM $ withDims (bound' <> M.map (Free . Var) pnames) $
-  mapM internaliseTypeM ts
-  where bound' = M.fromList (zip (S.toList bound)
-                                 (map (Free . Var) $ S.toList bound))
+liftInternaliseM :: InternaliseM a -> InternaliseTypeM a
+liftInternaliseM = InternaliseTypeM . lift
 
+runInternaliseTypeM :: InternaliseTypeM a
+                    -> InternaliseM a
+runInternaliseTypeM (InternaliseTypeM m) =
+  evalStateT m 0
+
+internaliseParamTypes :: [E.TypeBase (E.DimDecl VName) ()]
+                      -> InternaliseM [[I.TypeBase Shape Uniqueness]]
+internaliseParamTypes ts =
+  runInternaliseTypeM $ mapM (fmap (map onType) . internaliseTypeM) ts
+  where onType = fromMaybe bad . hasStaticShape
+        bad = error $ "internaliseParamTypes: " ++ pretty ts
+
+internaliseLoopParamType :: E.TypeBase (E.DimDecl VName) ()
+                         -> InternaliseM [I.TypeBase Shape Uniqueness]
+internaliseLoopParamType et =
+  concat <$> internaliseParamTypes [et]
+
 internaliseReturnType :: E.TypeBase (E.DimDecl VName) ()
                       -> InternaliseM [I.TypeBase ExtShape Uniqueness]
-internaliseReturnType = fmap concat . internaliseEntryReturnType
+internaliseReturnType et =
+  runInternaliseTypeM (internaliseTypeM et)
 
+internaliseLambdaReturnType :: E.TypeBase (E.DimDecl VName) ()
+                            -> InternaliseM [I.TypeBase Shape NoUniqueness]
+internaliseLambdaReturnType = fmap (map fromDecl) . internaliseLoopParamType
+
 -- | As 'internaliseReturnType', but returns components of a top-level
 -- tuple type piecemeal.
 internaliseEntryReturnType :: E.TypeBase (E.DimDecl VName) ()
                            -> InternaliseM [[I.TypeBase ExtShape Uniqueness]]
-internaliseEntryReturnType t = do
-  let ts = case E.isTupleRecord t of Just tts | not $ null tts -> tts
-                                     _ -> [t]
-  runInternaliseTypeM $ mapM internaliseTypeM ts
+internaliseEntryReturnType et =
+  runInternaliseTypeM $ mapM internaliseTypeM $
+  case E.isTupleRecord et of
+    Just ets | not $ null ets -> ets
+    _ -> [et]
 
 internaliseType :: E.TypeBase (E.DimDecl VName) ()
                 -> InternaliseM [I.TypeBase I.ExtShape Uniqueness]
@@ -85,11 +95,8 @@
     E.NamedDim name -> namedDim name
   where namedDim (E.QualName _ name) = do
           subst <- liftInternaliseM $ lookupSubst name
-          is_dim <- lookupDim name
-
-          case (is_dim, subst) of
-            (Just dim, _) -> return dim
-            (Nothing, Just [v]) -> return $ I.Free v
+          case subst of
+            Just [v] -> return $ I.Free v
             _ -> return $ I.Free $ I.Var name
 
 internaliseTypeM :: E.StructType
diff --git a/src/Futhark/Optimise/InliningDeadFun.hs b/src/Futhark/Optimise/InliningDeadFun.hs
--- a/src/Futhark/Optimise/InliningDeadFun.hs
+++ b/src/Futhark/Optimise/InliningDeadFun.hs
@@ -30,6 +30,10 @@
 import Futhark.Pass
 
 parMapM :: MonadFreshNames m => (a -> State VNameSource b) -> [a] -> m [b]
+-- The special-casing of [] is quite important here!  If 'as' is
+-- empty, then we might otherwise create an empty name source below,
+-- which can wreak all kinds of havoc.
+parMapM _ [] = pure []
 parMapM f as =
   modifyNameSource $ \src ->
   let f' a = runState (f a) src
@@ -125,14 +129,10 @@
     (bodyResult (funDefBody fun))
   let res_stms =
         certify (stmAuxCerts aux) <$>
-        zipWith (reshapeIfNecessary (patternNames pat))
-        (patternIdents pat) res
+        zipWith bindSubExp (patternIdents pat) res
   pure $ stmsToList stms <> res_stms
-  where param_names =
-          map paramName $ funDefParams fun
-
-        param_stms =
-          zipWith (reshapeIfNecessary param_names)
+  where param_stms =
+          zipWith bindSubExp
           (map paramIdent $ funDefParams fun) (map fst args)
 
         body_stms =
@@ -140,13 +140,11 @@
           addLocations (stmAuxAttrs aux) safety (filter notmempty (loc:locs)) $
           bodyStms $ funDefBody fun
 
-        reshapeIfNecessary dim_names ident se
-          | t@Array{} <- identType ident,
-            any (`elem` dim_names) (subExpVars $ arrayDims t),
-            Var v <- se =
-              mkLet [] [ident] $ shapeCoerce (arrayDims t) v
-          | otherwise =
-              mkLet [] [ident] $ BasicOp $ SubExp se
+        -- Note that the sizes of arrays may not be correct at this
+        -- point - it is crucial that we run copy propagation before
+        -- the type checker sees this!
+        bindSubExp ident se =
+          mkLet [] [ident] $ BasicOp $ SubExp se
 
         notmempty = (/=mempty) . locOf
 
diff --git a/src/Futhark/Optimise/Simplify/Rules.hs b/src/Futhark/Optimise/Simplify/Rules.hs
--- a/src/Futhark/Optimise/Simplify/Rules.hs
+++ b/src/Futhark/Optimise/Simplify/Rules.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE Safe #-}
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE OverloadedStrings #-}
 -- | This module defines a collection of simplification rules, as per
 -- "Futhark.Optimise.Simplify.Rule".  They are used in the
 -- simplifier.
@@ -34,13 +35,14 @@
 import Futhark.Analysis.PrimExp.Convert
 import Futhark.IR
 import Futhark.IR.Prop.Aliases
+import Futhark.Transform.Rename
 import Futhark.Construct
 import Futhark.Util
 
 topDownRules :: (BinderOps lore, Aliased lore) => [TopDownRule lore]
 topDownRules = [ RuleDoLoop hoistLoopInvariantMergeVariables
                , RuleDoLoop simplifyClosedFormLoop
-               , RuleDoLoop simplifKnownIterationLoop
+               , RuleDoLoop simplifyKnownIterationLoop
                , RuleDoLoop simplifyLoopVariables
                , RuleGeneric constantFoldPrimFun
                , RuleIf ruleIf
@@ -76,7 +78,7 @@
 -- perfect, but it should suffice for many cases, and should never
 -- generate wrong code.
 removeRedundantMergeVariables :: BinderOps lore => BottomUpRuleDoLoop lore
-removeRedundantMergeVariables (_, used) pat _ (ctx, val, form, body)
+removeRedundantMergeVariables (_, used) pat aux (ctx, val, form, body)
   | not $ all (usedAfterLoop . fst) val,
     null ctx = -- FIXME: things get tricky if we can remove all vals
                -- but some ctxs are still used.  We take the easy way
@@ -126,7 +128,7 @@
          mapM_ (uncurry letBindNames) $ dummyStms discard_ctx
          mapM_ (uncurry letBindNames) $ dummyStms discard_val
          return body'
-       letBind pat' $ DoLoop ctx' val' form body''
+       auxing aux $ letBind pat' $ DoLoop ctx' val' form body''
   where pat_used = map (`UT.isUsedDirectly` used) $ patternValueNames pat
         used_vals = map fst $ filter snd $ zip (map (paramName . fst) val) pat_used
         usedAfterLoop = flip elem used_vals . paramName
@@ -147,7 +149,7 @@
 -- We may change the type of the loop if we hoist out a shape
 -- annotation, in which case we also need to tweak the bound pattern.
 hoistLoopInvariantMergeVariables :: BinderOps lore => TopDownRuleDoLoop lore
-hoistLoopInvariantMergeVariables _ pat _ (ctx, val, form, loopbody) =
+hoistLoopInvariantMergeVariables _ pat aux (ctx, val, form, loopbody) =
     -- Figure out which of the elements of loopresult are
     -- loop-invariant, and hoist them out.
   case foldr checkInvariance ([], explpat, [], []) $
@@ -168,7 +170,7 @@
           (ctx', val') = splitAt (length implpat') merge'
       forM_ (invariant ++ implinvariant') $ \(v1,v2) ->
         letBindNames [identName v1] $ BasicOp $ SubExp v2
-      letBind (Pattern implpat'' explpat'') $
+      auxing aux $ letBind (Pattern implpat'' explpat'') $
         DoLoop ctx' val' form loopbody'
   where merge = ctx ++ val
         res = bodyResult loopbody
@@ -250,7 +252,7 @@
 simplifyClosedFormLoop _ _ _ _ = Skip
 
 simplifyLoopVariables :: (BinderOps lore, Aliased lore) => TopDownRuleDoLoop lore
-simplifyLoopVariables vtable pat _ (ctx, val, form@(ForLoop i it num_iters loop_vars), body)
+simplifyLoopVariables vtable pat aux (ctx, val, form@(ForLoop i it num_iters loop_vars), body)
   | simplifiable <- map checkIfSimplifiable loop_vars,
     not $ all isNothing simplifiable = Simplify $ do
       -- Check if the simplifications throw away more information than
@@ -263,7 +265,7 @@
         else do body' <- insertStmsM $ do
                   addStms $ mconcat body_prefix_stms
                   resultBodyM =<< bodyBind body
-                letBind pat $ DoLoop ctx val
+                auxing aux $ letBind pat $ DoLoop ctx val
                   (ForLoop i it num_iters $ catMaybes maybe_loop_vars) body'
 
   where seType (Var v)
@@ -310,30 +312,46 @@
         notIndex _                 = True
 simplifyLoopVariables _ _ _ _ = Skip
 
-simplifKnownIterationLoop :: BinderOps lore => TopDownRuleDoLoop lore
-simplifKnownIterationLoop _ pat _ (ctx, val, ForLoop i it (Constant iters) loop_vars, body)
-  | zeroIsh iters = Simplify $ do
-      let bindResult p r = letBindNames [patElemName p] $ BasicOp $ SubExp r
-      zipWithM_ bindResult (patternContextElements pat) (map snd ctx)
-      zipWithM_ bindResult (patternValueElements pat) (map snd val)
+unroll :: BinderOps lore =>
+          Integer
+       -> [(FParam lore, SubExp)]
+       -> (VName, IntType, Integer)
+       -> [(LParam lore, VName)]
+       -> Body lore
+       -> RuleM lore [SubExp]
+unroll n merge (iv, it, i) loop_vars body
+  | i >= n =
+      return $ map snd merge
+  | otherwise = do
+      iter_body <- insertStmsM $ do
+        forM_ merge $ \(mergevar, mergeinit) ->
+          letBindNames [paramName mergevar] $ BasicOp $ SubExp mergeinit
 
-  | oneIsh iters = Simplify $ do
+        letBindNames [iv] $ BasicOp $ SubExp $ intConst it i
 
-  forM_ (ctx++val) $ \(mergevar, mergeinit) ->
-    letBindNames [paramName mergevar] $ BasicOp $ SubExp mergeinit
+        forM_ loop_vars $ \(p,arr) ->
+          letBindNames [paramName p] $ BasicOp $ Index arr $
+          DimFix (intConst Int32 i) : fullSlice (paramType p) []
 
-  letBindNames [i] $ BasicOp $ SubExp $ intConst it 0
+        -- Some of the sizes in the types here might be temporarily wrong
+        -- until copy propagation fixes it up.
+        pure body
 
-  forM_ loop_vars $ \(p,arr) ->
-    letBindNames [paramName p] $ BasicOp $ Index arr $
-    DimFix (intConst Int32 0) : fullSlice (paramType p) []
+      iter_body' <- renameBody iter_body
+      addStms $ bodyStms iter_body'
 
-  -- Some of the sizes in the types here might be temporarily wrong
-  -- until copy propagation fixes it up.
-  res <- bodyBind body
-  forM_ (zip (patternNames pat) res) $ \(v, se) ->
-    letBindNames [v] $ BasicOp $ SubExp se
-simplifKnownIterationLoop _ _ _ _ =
+      let merge' = zip (map fst merge) $ bodyResult iter_body'
+      unroll n merge' (iv, it, i+1) loop_vars body
+
+simplifyKnownIterationLoop :: BinderOps lore => TopDownRuleDoLoop lore
+simplifyKnownIterationLoop _ pat aux (ctx, val, ForLoop i it (Constant iters) loop_vars, body)
+  | IntValue n <- iters,
+    zeroIshInt n || oneIshInt n || "unroll" `inAttrs` stmAuxAttrs aux = Simplify $ do
+      res <- unroll (valueIntegral n) (ctx++val) (i, it, 0) loop_vars body
+      forM_ (zip (patternNames pat) res) $ \(v, se) ->
+        letBindNames [v] $ BasicOp $ SubExp se
+
+simplifyKnownIterationLoop _ _ _ _ =
   Skip
 
 -- | Turn @copy(x)@ into @x@ iff @x@ is not used after this copy
@@ -662,7 +680,9 @@
             fmap (SubExpResult cs) $ letSubExp "slice_iota" $
               BasicOp $ Iota i_n i_offset'' i_stride'' to_it
 
-    Just (Rotate offsets a, cs) -> Just $ do
+    -- A rotate cannot be simplified away if we are slicing a rotated dimension.
+    Just (Rotate offsets a, cs)
+      | not $ or $ zipWith rotateAndSlice offsets inds -> Just $ do
       dims <- arrayDims <$> lookupType a
       let adjustI i o d = do
             i_p_o <- letSubExp "i_p_o" $ BasicOp $ BinOp (Add Int32 OverflowWrap) i o
@@ -672,6 +692,8 @@
           adjust (DimSlice i n s, o, d) =
             DimSlice <$> adjustI i o d <*> pure n <*> pure s
       IndexResult cs a <$> mapM adjust (zip3 inds offsets dims)
+        where rotateAndSlice r DimSlice{} = not $ isCt0 r
+              rotateAndSlice _ _ = False
 
     Just (Index aa ais, cs) ->
       Just $ IndexResult cs aa <$>
diff --git a/src/Futhark/Optimise/Sink.hs b/src/Futhark/Optimise/Sink.hs
--- a/src/Futhark/Optimise/Sink.hs
+++ b/src/Futhark/Optimise/Sink.hs
@@ -67,11 +67,12 @@
 multiplicity stm =
   case stmExp stm of
     If cond tbranch fbranch _ ->
-      free cond 1 <> M.unionWith (+) (free tbranch 1) (free fbranch 1)
+      free cond 1 `comb` free tbranch 1 `comb` free fbranch 1
     Op{} -> free stm 2
     DoLoop{} -> free stm 2
     _ -> free stm 1
   where free x k = M.fromList $ zip (namesToList $ freeIn x) $ repeat k
+        comb = M.unionWith (+)
 
 optimiseBranch :: SymbolTable -> Sinking -> Body SinkLore
                -> (Body SinkLore, Sunk)
@@ -95,7 +96,7 @@
   in (stmsFromList all_stms', sunk)
   where
     multiplicities = foldl' (M.unionWith (+))
-                     (M.fromList (zip (namesToList free_in_res) [1..]))
+                     (M.fromList (zip (namesToList free_in_res) (repeat 1)))
                      (map multiplicity $ stmsToList all_stms)
 
     optimiseStms' _ _ [] = ([], mempty)
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
@@ -485,7 +485,7 @@
                   localScope (scopeOfFParams $ map fst merge) $ do
 
         -- Collectively read a tile.
-        tile <- tilingReadTile tiling TileFull privstms (Var tile_id) arrs_and_perms
+        tile <- tilingReadTile tiling TilePartial privstms (Var tile_id) arrs_and_perms
 
         -- Now each thread performs a traversal of the tile and
         -- updates its accumulator.
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
@@ -583,7 +583,7 @@
           | DoLoop _ _ _ body <- stmExp stm =
               bodyInterest body * 10
           | If _ tbody fbody _ <- stmExp stm =
-              bodyInterest tbody + bodyInterest fbody -- Ad-hoc.
+              max (bodyInterest tbody) (bodyInterest fbody)
           | Op (Screma w (ScremaForm _ _ lam') _) <- stmExp stm =
               zeroIfTooSmall w + bodyInterest (lambdaBody lam')
           | Op (Stream _ (Sequential _) lam' _) <- stmExp stm =
@@ -637,9 +637,8 @@
 
 onTopLevelStms :: KernelPath -> Stms SOACS
                -> DistNestT Out.Kernels DistribM KernelsStms
-onTopLevelStms path stms = do
-  scope <- askScope
-  lift $ localScope scope $ transformStms path $ stmsToList stms
+onTopLevelStms path stms =
+  liftInner $ transformStms path $ stmsToList stms
 
 onMap :: KernelPath -> MapLoop -> DistribM KernelsStms
 onMap path (MapLoop pat aux w lam arrs) = do
@@ -788,9 +787,8 @@
       -- parallelism.
       dist_env <- ask
       let extra_scope = targetsScope $ distTargets acc'
-      scope <- (extra_scope<>) <$> askScope
 
-      stms <- lift $ localScope scope $ do
+      stms <- liftInner $ localScope extra_scope $ do
         let maploop' = MapLoop pat aux w lam arrs
 
             exploitInnerParallelism path' = do
diff --git a/src/Futhark/Pass/ExtractKernels/DistributeNests.hs b/src/Futhark/Pass/ExtractKernels/DistributeNests.hs
--- a/src/Futhark/Pass/ExtractKernels/DistributeNests.hs
+++ b/src/Futhark/Pass/ExtractKernels/DistributeNests.hs
@@ -20,6 +20,7 @@
   , DistAcc (..)
   , runDistNestT
   , DistNestT
+  , liftInner
 
   , distributeMap
 
@@ -43,6 +44,7 @@
 import Control.Monad.Trans.Maybe
 import Data.Maybe
 import Data.List (find, partition, tails)
+import qualified Data.Map as M
 
 import Futhark.IR
 import qualified Futhark.IR.SOACS as SOACS
@@ -134,8 +136,12 @@
             MonadReader (DistEnv lore m),
             MonadWriter (DistRes lore))
 
-instance MonadTrans (DistNestT lore) where
-  lift = DistNestT . lift . lift
+liftInner :: (LocalScope lore m, DistLore lore) => m a -> DistNestT lore m a
+liftInner m = do
+  outer_scope <- askScope
+  DistNestT $ lift $ lift $ do
+    inner_scope <- askScope
+    localScope (outer_scope `M.difference` inner_scope) m
 
 instance MonadFreshNames m => MonadFreshNames (DistNestT lore m) where
   getNameSource = DistNestT $ lift getNameSource
@@ -283,7 +289,8 @@
 lambdaContainsParallelism :: Lambda SOACS -> Bool
 lambdaContainsParallelism = bodyContainsParallelism . lambdaBody
 
-distributeMapBodyStms :: (MonadFreshNames m, DistLore lore) => DistAcc lore -> Stms SOACS -> DistNestT lore m (DistAcc lore)
+distributeMapBodyStms :: (MonadFreshNames m, LocalScope lore m, DistLore lore) =>
+                         DistAcc lore -> Stms SOACS -> DistNestT lore m (DistAcc lore)
 distributeMapBodyStms orig_acc = distribute <=< onStms orig_acc . stmsToList
   where
     onStms acc [] = return acc
@@ -312,7 +319,7 @@
   f <- asks distOnTopLevelStms
   postStm =<< f stms
 
-maybeDistributeStm :: (MonadFreshNames m, DistLore lore) =>
+maybeDistributeStm :: (MonadFreshNames m, LocalScope lore m, DistLore lore) =>
                       Stm SOACS -> DistAcc lore
                    -> DistNestT lore m (DistAcc lore)
 
@@ -596,7 +603,7 @@
 maybeDistributeStm bnd acc =
   addStmToAcc bnd acc
 
-distributeSingleUnaryStm :: (MonadFreshNames m, DistLore lore) =>
+distributeSingleUnaryStm :: (MonadFreshNames m, LocalScope lore m, DistLore lore) =>
                             DistAcc lore -> Stm SOACS
                          -> (KernelNest -> PatternT Type -> VName -> DistNestT lore m (Stms lore))
                          -> DistNestT lore m (DistAcc lore)
@@ -624,20 +631,22 @@
           | otherwise =
               False
 
-distribute :: (MonadFreshNames m, DistLore lore) => DistAcc lore -> DistNestT lore m (DistAcc lore)
+distribute :: (MonadFreshNames m, LocalScope lore m, DistLore lore) =>
+              DistAcc lore -> DistNestT lore m (DistAcc lore)
 distribute acc =
   fromMaybe acc <$> distributeIfPossible acc
 
-mkSegLevel :: (MonadFreshNames m, DistLore lore) => DistNestT lore m (MkSegLevel lore (DistNestT lore m))
+mkSegLevel :: (MonadFreshNames m, LocalScope lore m, DistLore lore) =>
+              DistNestT lore m (MkSegLevel lore (DistNestT lore m))
 mkSegLevel = do
   mk_lvl <- asks distSegLevel
   return $ \w desc r -> do
-    scope <- askScope
-    (lvl, stms) <- lift $ lift $ runBinderT (mk_lvl w desc r) scope
+    (lvl, stms) <- lift $ liftInner $ runBinderT' $ mk_lvl w desc r
     addStms stms
     return lvl
 
-distributeIfPossible :: (MonadFreshNames m, DistLore lore) => DistAcc lore -> DistNestT lore m (Maybe (DistAcc lore))
+distributeIfPossible :: (MonadFreshNames m, LocalScope lore m, DistLore lore) =>
+                        DistAcc lore -> DistNestT lore m (Maybe (DistAcc lore))
 distributeIfPossible acc = do
   nest <- asks distNest
   mk_lvl <- mkSegLevel
@@ -649,7 +658,7 @@
                             , distStms = mempty
                             }
 
-distributeSingleStm :: (MonadFreshNames m, DistLore lore) =>
+distributeSingleStm :: (MonadFreshNames m, LocalScope lore m, DistLore lore) =>
                        DistAcc lore -> Stm SOACS
                     -> DistNestT lore m (Maybe (PostStms lore,
                                                 Result,
@@ -671,7 +680,7 @@
                                  , distStms = mempty
                                  })
 
-segmentedScatterKernel :: (MonadFreshNames m, DistLore lore) =>
+segmentedScatterKernel :: (MonadFreshNames m, LocalScope lore m, DistLore lore) =>
                           KernelNest
                        -> [Int]
                        -> PatternT Type
@@ -737,7 +746,7 @@
           [ (map DimFix $ map Var (init gtids)++[i], v) | (i,v) <- is_vs ]
           where (gtids,ws) = unzip ispace
 
-segmentedUpdateKernel :: (MonadFreshNames m, DistLore lore) =>
+segmentedUpdateKernel :: (MonadFreshNames m, LocalScope lore m, DistLore lore) =>
                          KernelNest
                       -> [Int]
                       -> Certificates
@@ -781,7 +790,7 @@
 
     letBind pat $ Op $ segOp k
 
-segmentedGatherKernel :: (MonadFreshNames m, DistLore lore) =>
+segmentedGatherKernel :: (MonadFreshNames m, LocalScope lore m, DistLore lore) =>
                          KernelNest
                       -> Certificates
                       -> VName
@@ -814,7 +823,7 @@
 
     letBind pat $ Op $ segOp k
 
-segmentedHistKernel :: (MonadFreshNames m, DistLore lore) =>
+segmentedHistKernel :: (MonadFreshNames m, LocalScope lore m, DistLore lore) =>
                        KernelNest
                     -> [Int]
                     -> Certificates
@@ -841,10 +850,9 @@
     <*> pure op
 
   mk_lvl <- asks distSegLevel
-  scope <- askScope
   onLambda <- asks distOnSOACSLambda
   let onLambda' = fmap fst . runBinder . onLambda
-  lift $ flip runBinderT_ scope $ do
+  liftInner $ runBinderT'_ $ do
     -- It is important not to launch unnecessarily many threads for
     -- histograms, because it may mean we unnecessarily need to reduce
     -- subhistograms as well.
@@ -905,7 +913,7 @@
       in (Shape [w] <> shape, lam')
   | otherwise = (mempty, lam)
 
-segmentedScanomapKernel :: (MonadFreshNames m, DistLore lore) =>
+segmentedScanomapKernel :: (MonadFreshNames m, LocalScope lore m, DistLore lore) =>
                            KernelNest
                         -> [Int]
                         -> SubExp
@@ -921,7 +929,7 @@
     addStms =<< traverse renameStm =<<
       segScan lvl pat segment_size [scan_op] map_lam arrs ispace inps
 
-regularSegmentedRedomapKernel :: (MonadFreshNames m, DistLore lore) =>
+regularSegmentedRedomapKernel :: (MonadFreshNames m, LocalScope lore m, DistLore lore) =>
                                  KernelNest
                               -> [Int]
                               -> SubExp -> Commutativity
@@ -937,7 +945,7 @@
       addStms =<< traverse renameStm =<<
         segRed lvl pat segment_size [red_op] map_lam arrs ispace inps
 
-isSegmentedOp :: (MonadFreshNames m, DistLore lore) =>
+isSegmentedOp :: (MonadFreshNames m, LocalScope lore m, DistLore lore) =>
                  KernelNest
               -> [Int]
               -> Names -> Names
@@ -988,9 +996,8 @@
   nes' <- mapM prepareNe nes
 
   mk_arrs <- mapM prepareArr arrs
-  scope <- lift askScope
 
-  lift $ lift $ flip runBinderT_ scope $ do
+  lift $ liftInner $ runBinderT'_ $ do
     nested_arrs <- sequence mk_arrs
 
     let pat = Pattern [] $ rearrangeShape perm $
@@ -1041,7 +1048,7 @@
   postStm $ fmap (certify cs) bnds
   return acc'
 
-distributeMap :: (MonadFreshNames m, DistLore lore) =>
+distributeMap :: (MonadFreshNames m, LocalScope lore m, DistLore lore) =>
                  MapLoop -> DistAcc lore
               -> DistNestT lore m (DistAcc lore)
 distributeMap (MapLoop pat aux w lam arrs) acc =
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
@@ -63,8 +63,12 @@
     intraGroupParalleliseBody intra_lvl body
 
   outside_scope <- lift askScope
-  unless (all (`M.member` outside_scope) $ namesToList $
-          freeIn (wss_min ++ wss_avail)) $
+  -- outside_scope may also contain the inputs, even though those are
+  -- not actually available outside the kernel.
+  let available v =
+        v `M.member` outside_scope &&
+        v `notElem` map kernelInputName inps
+  unless (all available $ namesToList $ freeIn (wss_min ++ wss_avail)) $
     fail "Irregular parallelism"
 
   ((intra_avail_par, kspace, read_input_stms), prelude_stms) <- lift $ runBinder $ do
@@ -144,7 +148,7 @@
 
 intraGroupBody :: SegLevel -> Body -> IntraGroupM (Out.Body Out.Kernels)
 intraGroupBody lvl body = do
-  stms <- collectStms_ $ mapM_ (intraGroupStm lvl) $ bodyStms body
+  stms <- collectStms_ $ intraGroupStms lvl $ bodyStms body
   return $ mkBody stms $ bodyResult body
 
 intraGroupStm :: SegLevel -> Stm -> IntraGroupM ()
@@ -171,7 +175,7 @@
 
     Op soac
       | "sequential_outer" `inAttrs` stmAuxAttrs aux ->
-          mapM_ (intraGroupStm lvl) . fmap (certify (stmAuxCerts aux)) =<<
+          intraGroupStms lvl . fmap (certify (stmAuxCerts aux)) =<<
           runBinder_ (FOT.transformSOAC pat soac)
 
     Op (Screma w form arrs)
@@ -185,7 +189,7 @@
                         , distOnInnerMap =
                             distributeMap
                         , distOnTopLevelStms =
-                            lift . collectStms_ . intraGroupStms lvl
+                            liftInner . collectStms_ . intraGroupStms lvl
                         , distSegLevel = \minw _ _ -> do
                             lift $ parallelMin minw
                             return lvl
@@ -240,7 +244,7 @@
           replace se = se
           replaceSets (Acc x y log) =
             Acc (S.map (map replace) x) (S.map (map replace) y) log
-      censor replaceSets $ mapM_ (intraGroupStm lvl) stream_bnds
+      censor replaceSets $ intraGroupStms lvl stream_bnds
 
     Op (Scatter w lam ivs dests) -> do
       write_i <- newVName "write_i"
diff --git a/src/Futhark/Transform/Rename.hs b/src/Futhark/Transform/Rename.hs
--- a/src/Futhark/Transform/Rename.hs
+++ b/src/Futhark/Transform/Rename.hs
@@ -216,7 +216,10 @@
     ctxinit' <- mapM rename ctxinit
     valinit' <- mapM rename valinit
     case form of
-      ForLoop loopvar it boundexp loop_vars -> do
+      -- It is important that 'i' is renamed before the loop_vars, as
+      -- 'i' may be used in the annotations for loop_vars (e.g. index
+      -- functions).
+      ForLoop i it boundexp loop_vars -> bind [i] $ do
         let (loop_params, loop_arrs) = unzip loop_vars
         boundexp' <- rename boundexp
         loop_arrs' <- rename loop_arrs
@@ -225,13 +228,12 @@
           ctxparams' <- mapM rename ctxparams
           valparams' <- mapM rename valparams
           loop_params' <- mapM rename loop_params
-          bind [loopvar] $ do
-            loopvar'  <- rename loopvar
-            loopbody' <- rename loopbody
-            return $ DoLoop
-              (zip ctxparams' ctxinit') (zip valparams' valinit')
-              (ForLoop loopvar' it boundexp' $
-               zip loop_params' loop_arrs') loopbody'
+          i' <- rename i
+          loopbody' <- rename loopbody
+          return $ DoLoop
+            (zip ctxparams' ctxinit') (zip valparams' valinit')
+            (ForLoop i' it boundexp' $
+             zip loop_params' loop_arrs') loopbody'
       WhileLoop cond ->
         bind (map paramName $ ctxparams++valparams) $ do
           ctxparams' <- mapM rename ctxparams
diff --git a/src/Futhark/TypeCheck.hs b/src/Futhark/TypeCheck.hs
--- a/src/Futhark/TypeCheck.hs
+++ b/src/Futhark/TypeCheck.hs
@@ -507,18 +507,9 @@
 
 checkFunParams :: Checkable lore =>
                   [FParam lore] -> TypeM lore ()
-checkFunParams params = foldM_ check mempty params
-  where param_bound = namesFromList $ map paramName params
-        check prev param =
-          context ("In function parameter " ++ pretty param) $ do
-            checkFParamLore (paramName param) (paramDec param)
-            case namesToList $
-                 (freeIn param `namesIntersection` param_bound)
-                 `namesSubtract` prev of
-              [] -> return ()
-              v:_ ->
-                bad $ TypeError $ pretty v ++ " bound in a later parameter."
-            return $ oneName (paramName param) <> prev
+checkFunParams = mapM_ $ \param ->
+  context ("In function parameter " ++ pretty param) $
+    checkFParamLore (paramName param) (paramDec param)
 
 checkLambdaParams :: Checkable lore =>
                      [LParam lore] -> TypeM lore ()
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
@@ -1354,7 +1354,7 @@
         _ ->
           error $ "Invalid arguments to map intrinsic:\n" ++
           unlines [pretty t, pretty v]
-      where typeRowShape = traverse id . structTypeShape mempty . stripArray 1
+      where typeRowShape = sequenceA . structTypeShape mempty . stripArray 1
 
     def s | "reduce" `isPrefixOf` s = Just $ fun3t $ \f ne xs ->
       foldM (apply2 noLoc mempty f) ne $ snd $ fromArray xs
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
@@ -23,7 +23,6 @@
 import Control.Monad.Except
 import Control.Monad.Reader
 import Control.Monad.Trans.State
-import Control.Arrow
 import Data.Array
 import qualified Data.Text as T
 import Codec.Binary.UTF8.String (encode)
@@ -38,6 +37,7 @@
 import Language.Futhark.Prop
 import Language.Futhark.Pretty
 import Language.Futhark.Parser.Lexer
+import Futhark.Util.Pretty
 import Futhark.Util.Loc hiding (L) -- Lexer has replacements.
 
 }
@@ -610,9 +610,7 @@
      | Apply_ { $1 }
 
 Apply_ :: { UncheckedExp }
-       : ApplyList { case $1 of
-                       ((Constr n [] _ loc1):_) -> Constr n (tail $1) NoInfo (srcspan loc1 (last $1))
-                       _                -> foldl1 (\f x -> Apply f x NoInfo (NoInfo, NoInfo) (srcspan f x)) $1 }
+       : ApplyList {% applyExp $1 }
 
 ApplyList :: { [UncheckedExp] }
           : ApplyList Atom %prec juxtprec
@@ -725,7 +723,7 @@
 
 LetExp :: { UncheckedExp }
      : let Pattern '=' Exp LetBody
-                      { LetPat $2 $4 $5 (NoInfo, NoInfo) (srcspan $1 $>) }
+       { LetPat $2 $4 $5 (NoInfo, NoInfo) (srcspan $1 $>) }
 
      | let id TypeParams FunParams1 maybeAscription(TypeExpDecl) '=' Exp LetBody
        { let L _ (ID name) = $2
@@ -733,24 +731,26 @@
             $8 NoInfo (srcspan $1 $>) }
 
      | let VarSlice '=' Exp LetBody
-                      { let ((v,_),slice,loc) = $2; ident = Ident v NoInfo loc
-                        in LetWith ident ident slice $4 $5 NoInfo (srcspan $1 $>) }
+       { let ((v,_),slice,loc) = $2; ident = Ident v NoInfo loc
+         in LetWith ident ident slice $4 $5 NoInfo (srcspan $1 $>) }
 
 LetBody :: { UncheckedExp }
     : in Exp %prec letprec { $2 }
     | LetExp %prec letprec { $1 }
+    | error {% throwError "Unexpected end of file - missing \"in\"?" }
 
 MatchExp :: { UncheckedExp }
-          : match Exp Cases  { let loc = srcspan $1 (NE.toList $>)
-                               in Match $2 $> (NoInfo, NoInfo) loc  }
+          : match Exp Cases
+            { let loc = srcspan $1 (NE.toList $>)
+              in Match $2 $> (NoInfo, NoInfo) loc  }
 
 Cases :: { NE.NonEmpty (CaseBase NoInfo Name) }
        : Case  %prec caseprec { $1 NE.:| [] }
        | Case Cases           { NE.cons $1 $2 }
 
 Case :: { CaseBase NoInfo Name }
-      : case CPattern '->' Exp       { let loc = srcspan $1 $>
-                                       in CasePat $2 $> loc }
+      : case CPattern '->' Exp
+        { let loc = srcspan $1 $> in CasePat $2 $> loc }
 
 CPattern :: { PatternBase NoInfo Name }
           : CInnerPattern ':' TypeExpDecl { PatternAscription $1 $3 (srcspan $1 $>) }
@@ -815,8 +815,8 @@
 
 VarSlice :: { ((Name, SrcLoc), [UncheckedDimIndex], SrcLoc) }
           : 'id[' DimIndices ']'
-              { let L vloc (INDEXING v) = $1
-                in ((v, vloc), $2, srcspan $1 $>) }
+            { let L vloc (INDEXING v) = $1
+              in ((v, vloc), $2, srcspan $1 $>) }
 
 QualVarSlice :: { ((QualName Name, SrcLoc), [UncheckedDimIndex], SrcLoc) }
               : VarSlice
@@ -873,7 +873,7 @@
               : FieldId '=' Pattern
                 { (fst $1, $3) }
               | FieldId ':' TypeExpDecl
-              { (fst $1, PatternAscription (Id (fst $1) NoInfo (snd $1)) $3 (srcspan (snd $1) $>)) }
+                { (fst $1, PatternAscription (Id (fst $1) NoInfo (snd $1)) $3 (srcspan (snd $1) $>)) }
               | FieldId
                 { (fst $1, Id (fst $1) NoInfo (snd $1)) }
 
@@ -1083,6 +1083,20 @@
 
 arrayFromList :: [a] -> Array Int a
 arrayFromList l = listArray (0, length l-1) l
+
+applyExp :: [UncheckedExp] -> ParserMonad UncheckedExp
+applyExp all@((Constr n [] _ loc1):es) =
+  return $ Constr n es NoInfo (srcspan loc1 (last all))
+applyExp es =
+  foldM ap (head es) (tail es)
+  where
+     ap (Index e is _ floc) (ArrayLit xs _ xloc) =
+       parseErrorAt (srcspan floc xloc) $
+       Just $ pretty $ "Incorrect syntax for multi-dimensional indexing." </>
+       "Use" <+> align (ppr index)
+       where index = Index e (is++map DimFix xs) (NoInfo, NoInfo) xloc
+     ap f x =
+        return $ Apply f x NoInfo (NoInfo, NoInfo) (srcspan f x)
 
 patternExp :: UncheckedPattern -> ParserMonad UncheckedExp
 patternExp (Id v _ loc) = return $ Var (qualName v) NoInfo loc
diff --git a/src/Language/Futhark/Pretty.hs b/src/Language/Futhark/Pretty.hs
--- a/src/Language/Futhark/Pretty.hs
+++ b/src/Language/Futhark/Pretty.hs
@@ -222,9 +222,9 @@
   pprPrec _ (Parens e _) = align $ parens $ ppr e
   pprPrec _ (QualParens (v, _) e _) = ppr v <> text "." <> align (parens $ ppr e)
   pprPrec p (Ascript e t _) =
-    parensIf (p /= -1) $ pprPrec 0 e <+> text ":" <+> pprPrec 0 t
+    parensIf (p /= -1) $ pprPrec 0 e <+> text ":" <+> align (pprPrec 0 t)
   pprPrec p (Coerce e t _ _) =
-    parensIf (p /= -1) $ pprPrec 0 e <+> text ":>" <+> pprPrec 0 t
+    parensIf (p /= -1) $ pprPrec 0 e <+> text ":>" <+> align (pprPrec 0 t)
   pprPrec _ (Literal v _) = ppr v
   pprPrec _ (IntLit v _ _) = ppr v
   pprPrec _ (FloatLit v _ _) = ppr v
@@ -281,7 +281,7 @@
     retdecl' <+> equals </> indent 2 (ppr e) </>
     letBody body
     where retdecl' = case (ppr <$> unAnnot rettype) `mplus` (ppr <$> retdecl) of
-                       Just rettype' -> text ":" <+> rettype'
+                       Just rettype' -> colon <+> align rettype'
                        Nothing       -> mempty
   pprPrec _ (LetWith dest src idxs ve body _ _)
     | dest == src =
@@ -349,10 +349,10 @@
     text "while" <+> ppr cond
 
 instance (Eq vn, IsName vn, Annot f) => Pretty (PatternBase f vn) where
-  ppr (PatternAscription p t _) = ppr p <> text ":" <+> ppr t
+  ppr (PatternAscription p t _) = ppr p <> colon <+> align (ppr t)
   ppr (PatternParens p _)       = parens $ ppr p
   ppr (Id v t _)                = case unAnnot t of
-                                    Just t' -> parens $ pprName v <> colon <+> ppr t'
+                                    Just t' -> parens $ pprName v <> colon <+> align (ppr t')
                                     Nothing -> pprName v
   ppr (TuplePattern pats _)     = parens $ commasep $ map ppr pats
   ppr (RecordPattern fs _)      = braces $ commasep $ map ppField fs
@@ -365,7 +365,7 @@
 
 ppAscription :: Pretty t => Maybe t -> Doc
 ppAscription Nothing  = mempty
-ppAscription (Just t) = text ":" <> ppr t
+ppAscription (Just t) = colon <> align (ppr t)
 
 instance (Eq vn, IsName vn, Annot f) => Pretty (ProgBase f vn) where
   ppr = stack . punctuate line . map ppr . progDecs
@@ -415,7 +415,7 @@
     where fun | isJust entry = "entry"
               | otherwise    = "let"
           retdecl' = case (ppr . fst <$> unAnnot rettype) `mplus` (ppr <$> retdecl) of
-                       Just rettype' -> text ":" <+> rettype'
+                       Just rettype' -> colon <+> align rettype'
                        Nothing       -> mempty
 
 instance (Eq vn, IsName vn, Annot f) => Pretty (SpecBase f vn) where
diff --git a/src/Language/Futhark/Prop.hs b/src/Language/Futhark/Prop.hs
--- a/src/Language/Futhark/Prop.hs
+++ b/src/Language/Futhark/Prop.hs
@@ -399,6 +399,11 @@
       Scalar $ Record $ M.map (uncurry combineTypeShapes) (M.intersectionWith (,) ts1 ts2)
 combineTypeShapes (Scalar (Arrow als1 p1 a1 b1)) (Scalar (Arrow als2 _p2 a2 b2)) =
   Scalar $ Arrow (als1<>als2) p1 (combineTypeShapes a1 a2) (combineTypeShapes b1 b2)
+combineTypeShapes (Scalar (TypeVar als1 u1 v targs1)) (Scalar (TypeVar als2 _ _ targs2)) =
+  Scalar $ TypeVar (als1<>als2) u1 v $ zipWith f targs1 targs2
+  where f (TypeArgType t1 loc) (TypeArgType t2 _) =
+          TypeArgType (combineTypeShapes t1 t2) loc
+        f targ _ = targ
 combineTypeShapes (Array als1 u1 et1 shape1) (Array als2 _u2 et2 _shape2) =
   arrayOfWithAliases (combineTypeShapes (Scalar et1) (Scalar et2)
                        `setAliases` mempty)
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
@@ -994,8 +994,11 @@
   | ModImport FilePath (f FilePath) SrcLoc
     -- ^ The contents of another file as a module.
   | ModDecs [DecBase f vn] SrcLoc
-  | ModApply (ModExpBase f vn) (ModExpBase f vn) (f (M.Map VName VName)) (f (M.Map VName VName)) SrcLoc
-    -- ^ Functor application.
+  | ModApply (ModExpBase f vn) (ModExpBase f vn)
+    (f (M.Map VName VName)) (f (M.Map VName VName)) SrcLoc
+    -- ^ Functor application.  The first mapping is from parameter
+    -- names to argument names, while the second maps names in the
+    -- constructed module to the names inside the functor.
   | ModAscript (ModExpBase f vn) (SigExpBase f vn) (f (M.Map VName VName)) SrcLoc
   | ModLambda (ModParamBase f vn)
     (Maybe (SigExpBase f vn, f (M.Map VName VName)))