diff --git a/idris2.ipkg b/idris2.ipkg
index 12b4a2839..dccdf5b08 100644
--- a/idris2.ipkg
+++ b/idris2.ipkg
@@ -40,8 +40,10 @@ modules =
 
     Data.ANameMap,
     Data.Bool.Extra,
+    Data.Either.Extra,
     Data.IntMap,
     Data.IOArray,
+    Data.List.NonEmpty,
     Data.NameMap,
     Data.StringMap,
     Data.These,
diff --git a/src/Compiler/CompileExpr.idr b/src/Compiler/CompileExpr.idr
index bc19821cd..a06621fa3 100644
--- a/src/Compiler/CompileExpr.idr
+++ b/src/Compiler/CompileExpr.idr
@@ -380,7 +380,7 @@ mutual
                   then pure (fromMaybe (CErased fc) def)
                   else pure $ natHackTree $
                             CConCase fc (CLocal fc x) cases def
-  toCExpTree' tags n (Case _ x scTy alts@(DelayCase _ _ _ :: _))
+  toCExpTree' tags n (Case _ x scTy (DelayCase _ _ _ :: _))
       = throw (InternalError "Unexpected DelayCase")
   toCExpTree' tags n (Case fc x scTy alts@(ConstCase _ _ :: _))
       = let fc = getLoc scTy in
@@ -389,7 +389,7 @@ mutual
                if isNil cases
                   then pure (fromMaybe (CErased fc) def)
                   else pure $ CConstCase fc (CLocal fc x) cases def
-  toCExpTree' tags n (Case _ x scTy alts@(DefaultCase sc :: _))
+  toCExpTree' tags n (Case _ x scTy (DefaultCase sc :: _))
       = toCExpTree tags n sc
   toCExpTree' tags n (Case _ x scTy [])
       = pure $ CCrash (getLoc scTy) $ "Missing case tree in " ++ show n
diff --git a/src/Core/AutoSearch.idr b/src/Core/AutoSearch.idr
index 0edb603be..46b5e7c83 100644
--- a/src/Core/AutoSearch.idr
+++ b/src/Core/AutoSearch.idr
@@ -483,7 +483,7 @@ searchType fc rigc defaults trying depth def checkdets top env (Bind nfc x (Let
 searchType {vars} fc rigc defaults trying depth def checkdets top env target
     = do defs <- get Ctxt
          abandonIfCycle env target trying
-         let trying' = target :: trying
+         let trying' = the (List (Term vars)) (target :: trying)
          nty <- nf defs env target
          case nty of
               NTCon tfc tyn t a args =>
diff --git a/src/Core/CaseBuilder.idr b/src/Core/CaseBuilder.idr
index 65b11c8e7..90cf51d00 100644
--- a/src/Core/CaseBuilder.idr
+++ b/src/Core/CaseBuilder.idr
@@ -776,7 +776,7 @@ mutual
   -- will be a broken case tree... so we should find a way to express this
   -- in the type if we can.
   conRule {a} fc fn phase cs@(MkPatClause pvars (MkInfo pat pprf fty :: pats) rhs :: rest) err
-      = do refinedcs <- traverse (substInClause fc) cs
+      = do refinedcs <- Core.traverse (substInClause fc) cs
            groups <- groupCons fc fn pvars refinedcs
            ty <- case fty of
                       Known _ t => pure t
diff --git a/src/Data/Either/Extra.idr b/src/Data/Either/Extra.idr
new file mode 100644
index 000000000..151cd2132
--- /dev/null
+++ b/src/Data/Either/Extra.idr
@@ -0,0 +1,36 @@
+module Data.Either.Extra
+
+import Data.List.NonEmpty
+
+%default total
+
+mutual
+
+  ||| `group` compresses the list of Lefts and Rights by accumulating
+  ||| all of the lefts and rights into blocks.
+  export
+  group : List (Either a b) -> List (Either (List1 a) (List1 b))
+  group []               = []
+  group (Left a :: abs)  = lefts  [a] abs
+  group (Right b :: abs) = rights [b] abs
+
+  lefts : List1 a -> List (Either a b) -> List (Either (List1 a) (List1 b))
+  lefts acc (Left a :: abs) = lefts (cons a acc) abs
+  lefts acc abs             = Left (reverse acc) :: group abs
+  
+  rights : List1 b -> List (Either a b) -> List (Either (List1 a) (List1 b))
+  rights acc (Right b :: abs) = rights (cons b acc) abs
+  rights acc abs              = Right (reverse acc) :: group abs
+
+||| `ungroup` is the inverse of `group` (the converse is not true as nothing
+||| forces the input to be maximally grouped!)
+export
+ungroup : List (Either (List1 a) (List1 b)) -> List (Either a b)
+ungroup = concatMap $ \ abs => case abs of
+  Left as  => map Left  $ NonEmpty.toList as
+  Right bs => map Right $ NonEmpty.toList bs
+
+export
+pushInto : c -> Either a b -> Either (c, a) (c, b)
+pushInto c (Left a)  = Left (c, a)
+pushInto c (Right b) = Right (c, b)
diff --git a/src/Data/List/NonEmpty.idr b/src/Data/List/NonEmpty.idr
new file mode 100644
index 000000000..d42428313
--- /dev/null
+++ b/src/Data/List/NonEmpty.idr
@@ -0,0 +1,44 @@
+module Data.List.NonEmpty
+
+%default total
+
+public export
+record List1 (a : Type) where
+  constructor (::)
+  head : a
+  tail : List a
+
+export
+last : List1 a -> a
+last (x :: xs) = foldl (flip const) x xs
+
+||| Implementations
+
+public export
+Functor List1 where
+
+  map f (x :: xs) = f x :: map f xs
+
+public export
+Foldable List1 where
+
+  foldr c n (x :: xs) = c x (foldr c n xs)
+  foldl c n (x :: xs) = foldl c (c n x) xs
+
+||| We define a specialised version of `toList` because the one defined using
+||| a `Foldable` constraint would have to needlessly go through the whole tail.
+export
+toList : List1 a -> List a
+toList (x :: xs) = x :: xs
+
+export
+cons : a -> List1 a -> List1 a
+cons x (y :: ys) = x :: (y :: ys)
+
+export
+reverseOnto : List1 a -> List a -> List1 a
+reverseOnto = foldl (flip cons)
+
+export
+reverse : List1 a -> List1 a
+reverse (x :: xs) = reverseOnto (x :: []) xs
diff --git a/src/Idris/Elab/Implementation.idr b/src/Idris/Elab/Implementation.idr
index 76d7116c6..28e5e3b2d 100644
--- a/src/Idris/Elab/Implementation.idr
+++ b/src/Idris/Elab/Implementation.idr
@@ -173,7 +173,7 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
                -- Add the 'using' hints
                defs <- get Ctxt
                let hs = openHints defs -- snapshot open hint state
-               log 10 $ "Open hints: " ++ (show (impName :: nusing))
+               log 10 $ "Open hints: " ++ show (the (List Name) (impName :: nusing))
                traverse_ (\n => do n' <- checkUnambig fc n
                                    addOpenHint n') nusing
 
diff --git a/src/Idris/ModTree.idr b/src/Idris/ModTree.idr
index 7dd56fc51..30f974f68 100644
--- a/src/Idris/ModTree.idr
+++ b/src/Idris/ModTree.idr
@@ -32,7 +32,7 @@ Show ModTree where
 
 -- A module file to build, and its list of dependencies
 -- From this we can work out if the source file needs rebuilding, assuming
--- things are build in dependency order. A source file needs rebuilding
+-- things are built in dependency order. A source file needs rebuilding
 -- if:
 --  + Its corresponding ttc is older than the source file
 --  + Any of the import ttcs are *newer* than the corresponding ttc
@@ -162,7 +162,7 @@ buildMod loc num len mod
         let needsBuilding =
                case ttcTime of
                     Nothing => True
-                    Just t => any (\x => x > t) (srcTime :: map snd depTimes)
+                    Just t => any {t = List} (\x => x > t) (srcTime :: map snd depTimes)
         u <- newRef UST initUState
         m <- newRef MD initMetadata
         put Syn initSyntax
diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr
index 3a28abc7d..51b46c638 100644
--- a/src/Idris/Parser.idr
+++ b/src/Idris/Parser.idr
@@ -7,6 +7,8 @@ import        Parser.Lexer
 import        TTImp.TTImp
 
 import public Text.Parser
+import        Data.Either.Extra
+import        Data.List.NonEmpty
 import        Data.List.Views
 
 %default covering
@@ -522,10 +524,23 @@ mutual
        bindAll fc ((rig, pat, ty) :: rest) scope
            = PLam fc rig Explicit pat ty (bindAll fc rest scope)
 
-  letBinder : FileName -> IndentInfo ->
-              Rule (FilePos, FilePos, RigCount, PTerm, PTerm, PTerm, List PClause)
-  letBinder fname indents
+  LetBinder : Type
+  LetBinder = (RigCount, PTerm, PTerm, PTerm, List PClause)
+
+  LetDecl : Type
+  LetDecl = List PDecl
+
+  letBlock : FileName -> IndentInfo ->
+              Rule ((FilePos, FilePos), Either LetBinder LetDecl)
+  letBlock fname indents
       = do start <- location
+           res <- Left <$> letBinder fname indents start
+              <|> Right <$> topDecl fname indents
+           end <- location
+           pure ((start, end), res)
+
+  letBinder : FileName -> IndentInfo -> FilePos -> Rule LetBinder
+  letBinder fname indents start = do
            rigc <- multiplicity
            pat <- expr plhs fname indents
            tyend <- location
@@ -535,30 +550,29 @@ mutual
            symbol "="
            val <- expr pnowith fname indents
            alts <- block (patAlt fname)
-           end <- location
            rig <- getMult rigc
-           pure (start, end, rig, pat, ty, val, alts)
+           pure (rig, pat, ty, val, alts)
 
   buildLets : FileName ->
-              List (FilePos, FilePos, RigCount, PTerm, PTerm, PTerm, List PClause) ->
+              List ((FilePos, FilePos), LetBinder) ->
               PTerm -> PTerm
   buildLets fname [] sc = sc
-  buildLets fname ((start, end, rig, pat, ty, val, alts) :: rest) sc
+  buildLets fname (((start, end), rig, pat, ty, val, alts) :: rest) sc
       = let fc = MkFC fname start end in
             PLet fc rig pat ty val
                  (buildLets fname rest sc) alts
 
   buildDoLets : FileName ->
-                List (FilePos, FilePos, RigCount, PTerm, PTerm, PTerm, List PClause) ->
+                List ((FilePos, FilePos), LetBinder) ->
                 List PDo
   buildDoLets fname [] = []
-  buildDoLets fname ((start, end, rig, PRef fc' (UN n), ty, val, []) :: rest)
+  buildDoLets fname (((start, end), rig, PRef fc' (UN n), ty, val, []) :: rest)
       = let fc = MkFC fname start end in
             if lowerFirst n
                then DoLet fc (UN n) rig ty val :: buildDoLets fname rest
                else DoLetPat fc (PRef fc' (UN n)) ty val []
                          :: buildDoLets fname rest
-  buildDoLets fname ((start, end, rig, pat, ty, val, alts) :: rest)
+  buildDoLets fname (((start, end), rig, pat, ty, val, alts) :: rest)
       = let fc = MkFC fname start end in
             DoLetPat fc pat ty val alts :: buildDoLets fname rest
 
@@ -566,20 +580,48 @@ mutual
   let_ fname indents
       = do start <- location
            keyword "let"
-           res <- nonEmptyBlock (letBinder fname)
+           blocks <- nonEmptyBlock (letBlock fname)
            commitKeyword indents "in"
            scope <- typeExpr pdef fname indents
            end <- location
-           pure (buildLets fname res scope)
+           pure $ mkLets fname blocks scope
+
+  letFactory
+     : (List ((FilePos, FilePos), LetBinder) -> a -> a) ->
+       ((FilePos, FilePos) -> List PDecl -> a -> a) ->
+       List1 ((FilePos, FilePos), Either LetBinder LetDecl) ->
+       a -> a
+  letFactory {a} letBind letDeclare blocks scope = foldr mkLet scope groups where
+
+     LetBlock : Type
+     LetBlock = Either (List1 ((FilePos, FilePos), LetBinder))
+                       (List1 ((FilePos, FilePos), LetDecl))
+
+     groups : List LetBlock
+     groups = group (NonEmpty.toList $ map (uncurry pushInto) blocks)
+
+     mkLet : LetBlock -> a -> a
+     mkLet (Left  letBinds) = letBind (NonEmpty.toList letBinds)
+     mkLet (Right letDecls) =
+       let ((start,_), _) = head letDecls
+           ((_, end),_)   = last letDecls
+       in letDeclare (start, end) (concatMap snd letDecls)
+
+  mkLets : FileName ->
+           List1 ((FilePos, FilePos), Either LetBinder LetDecl) ->
+           PTerm -> PTerm
+  mkLets fname = letFactory (buildLets fname)
+    (\ (start, end), decls, scope => PLocal (MkFC fname start end) decls scope)
+
+  mkDoLets : FileName ->
+           List1 ((FilePos, FilePos), Either LetBinder LetDecl) ->
+           List PDo
+  mkDoLets fname lets = letFactory
+    (\ binds, rest => buildDoLets fname binds ++ rest)
+    (\ (start, end), decls, rest => DoLetLocal (MkFC fname start end) decls :: rest)
+    lets
+    []
 
-    <|> do start <- location
-           keyword "let"
-           commit
-           ds <- nonEmptyBlock (topDecl fname)
-           commitKeyword indents "in"
-           scope <- typeExpr pdef fname indents
-           end <- location
-           pure (PLocal (MkFC fname start end) (collectDefs (concat ds)) scope)
 
   case_ : FileName -> IndentInfo -> Rule PTerm
   case_ fname indents
@@ -709,15 +751,9 @@ mutual
            end <- location
            pure [DoBind (MkFC fname start end) n val]
     <|> do keyword "let"
-           res <- block (letBinder fname)
-           atEnd indents
-           pure (buildDoLets fname res)
-    <|> do start <- location
-           keyword "let"
-           res <- block (topDecl fname)
-           end <- location
+           res <- nonEmptyBlock (letBlock fname)
            atEnd indents
-           pure [DoLetLocal (MkFC fname start end) (concat res)]
+           pure (mkDoLets fname res)
     <|> do start <- location
            keyword "rewrite"
            rule <- expr pdef fname indents
@@ -840,7 +876,7 @@ mutual
             wval <- bracketedExpr fname wstart indents
             ws <- nonEmptyBlock (clause (S withArgs) fname)
             end <- location
-            pure (MkWithClause (MkFC fname start end) lhs wval ws)
+            pure (MkWithClause (MkFC fname start end) lhs wval (NonEmpty.toList ws))
      <|> do keyword "impossible"
             atEnd indents
             end <- location
diff --git a/src/Parser/Support.idr b/src/Parser/Support.idr
index bc44e1e66..838a68ef2 100644
--- a/src/Parser/Support.idr
+++ b/src/Parser/Support.idr
@@ -6,6 +6,7 @@ import public Parser.Unlit
 import public Text.Parser
 
 import Core.TT
+import Data.List.NonEmpty
 import Data.List.Views
 
 %default total
@@ -594,7 +595,7 @@ blockWithOptHeaderAfter {ty} mincol header item
                            pure (Nothing, ps)
 
 export
-nonEmptyBlock : (IndentInfo -> Rule ty) -> Rule (List ty)
+nonEmptyBlock : (IndentInfo -> Rule ty) -> Rule (List1 ty)
 nonEmptyBlock item
     = do symbol "{"
          commit
diff --git a/src/TTImp/Interactive/MakeLemma.idr b/src/TTImp/Interactive/MakeLemma.idr
index 0bc591fd4..f5b2350bc 100644
--- a/src/TTImp/Interactive/MakeLemma.idr
+++ b/src/TTImp/Interactive/MakeLemma.idr
@@ -25,9 +25,9 @@ bindable p tm
     = case getFnArgs tm of
            (Ref _ (TyCon _ _) n, args) => any (bindable p) args
            (Ref _ (DataCon _ _) _, args) => any (bindable p) args
-           (TDelayed _ _ t, args) => any (bindable p) (t :: args)
-           (TDelay _ _ _ t, args) => any (bindable p) (t :: args)
-           (TForce _ _ t, args) => any (bindable p) (t :: args)
+           (TDelayed _ _ t, args) => any {t = List} (bindable p) (t :: args)
+           (TDelay _ _ _ t, args) => any {t = List} (bindable p) (t :: args)
+           (TForce _ _ t, args) => any {t = List} (bindable p) (t :: args)
            (Local _ _ p' _, []) => p == p'
            _ => False
 
diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr
index 4c556483d..24e71b4af 100644
--- a/src/TTImp/Parser.idr
+++ b/src/TTImp/Parser.idr
@@ -4,6 +4,9 @@ import Core.Context
 import Core.Core
 import Core.Env
 import Core.TT
+
+import Data.List.NonEmpty
+
 import Parser.Support
 import TTImp.TTImp
 
@@ -487,7 +490,7 @@ mutual
            ws <- nonEmptyBlock (clause (S withArgs) fname)
            end <- location
            let fc = MkFC fname start end
-           pure (!(getFn lhs), WithClause fc lhs wval (map snd ws))
+           pure (!(getFn lhs), WithClause fc lhs wval (NonEmpty.toList $ map snd ws))
 
     <|> do keyword "impossible"
            atEnd indents
@@ -664,7 +667,7 @@ topDecl fname indents
          ns <- namespaceDecl
          ds <- assert_total (nonEmptyBlock (topDecl fname))
          end <- location
-         pure (INamespace (MkFC fname start end) ns ds)
+         pure (INamespace (MkFC fname start end) ns (NonEmpty.toList ds))
   <|> do start <- location
          visOpts <- many visOpt
          vis <- getVisibility Nothing visOpts
@@ -704,7 +707,7 @@ export
 prog : FileName -> Rule (List ImpDecl)
 prog fname
     = do ds <- nonEmptyBlock (topDecl fname)
-         pure (collectDefs ds)
+         pure (collectDefs (NonEmpty.toList ds))
 
 -- TTImp REPL commands
 export
diff --git a/src/TTImp/WithClause.idr b/src/TTImp/WithClause.idr
index f290706bc..009614bea 100644
--- a/src/TTImp/WithClause.idr
+++ b/src/TTImp/WithClause.idr
@@ -120,10 +120,11 @@ getNewLHS ploc drop nest wname wargnames lhs_raw patlhs
          (_, mlhs) <- bindNames False mlhs_raw
          setUnboundImplicits autoimp
 
-         let (warg :: rest) = reverse wrest
+         let wargs = reverse wrest
+         let (warg :: rest) = wargs
              | _ => throw (GenericMsg ploc "Badly formed 'with' clause")
          log 5 $ show lhs ++ " against " ++ show mlhs ++
-                 " dropping " ++ show (warg :: rest)
+                 " dropping " ++ show wargs
          ms <- getMatch True lhs mlhs
          log 5 $ "Matches: " ++ show ms
          let newlhs = apply (IVar ploc wname)