diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -6,9 +6,24 @@
 and this project adheres to the
 [Haskell Package Versioning Policy](https://pvp.haskell.org/).
 
+## v0.7.5 — 2024-08-18
+
+Minor changes:
+
+- Suport syntax sugar for nested Σ-types (see [#183](https://github.com/rzk-lang/rzk/pull/183))
+- Improve error reporting (see [#176](https://github.com/rzk-lang/rzk/pull/176) and [#179](https://github.com/rzk-lang/rzk/pull/179))
+
+Fixes:
+
+- Support newer `lsp` (specifically, `lsp-2.7.0.0`, see [#188](https://github.com/rzk-lang/rzk/pull/188))
+- Fix CI (see [#184](https://github.com/rzk-lang/rzk/pull/184))
+- Fix build of nix flake on aarch64-darwin (see [#181](https://github.com/rzk-lang/rzk/pull/181))
+- Small documentation fixes (see [#178](https://github.com/rzk-lang/rzk/pull/178))
+
 ## v0.7.4 — 2024-04-01
 
 Fixes:
+
 - Fix caching in Rzk Language Server, especially in presence of errors (see [#167](https://github.com/rzk-lang/rzk/pull/167))
 - Fix CI for the Rzk Playground (see [#174](https://github.com/rzk-lang/rzk/pull/174))
 
@@ -18,33 +33,37 @@
 ## v0.7.3 — 2023-12-16
 
 Fixes:
+
 - Fix overlapping edits in the formatter, hopefully making it idempotent (see [#160](https://github.com/rzk-lang/rzk/pull/160));
 - Fix formatter crashing the language server (see [#161](https://github.com/rzk-lang/rzk/pull/161));
 - Avoid unnecessary typechecking when semantics of a file has not changed (see [#159](https://github.com/rzk-lang/rzk/pull/159));
 - Stop typechecking after the first parse error (avoid invalid cache) (see [`68ab0b4`](https://github.com/rzk-lang/rzk/commit/68ab0b4dd3d627756e10adb55cb16845b08d09d9));
 
 Other:
+
 - Add unit tests for the formatter (see [#157](https://github.com/rzk-lang/rzk/pull/157));
 
 ## v0.7.2 — 2023-12-12
 
 Fixes:
+
 - Fixes for `rzk format`:
-    - Fix extra space after open parens in formatter (see [#155](https://github.com/rzk-lang/rzk/pull/155));
-    - Replace line string content with tokens when checking open parens (see [#156](https://github.com/rzk-lang/rzk/pull/156));
+  - Fix extra space after open parens in formatter (see [#155](https://github.com/rzk-lang/rzk/pull/155));
+  - Replace line string content with tokens when checking open parens (see [#156](https://github.com/rzk-lang/rzk/pull/156));
 - Throw an error when `rzk.yaml`'s `include` is empty (see [#154](https://github.com/rzk-lang/rzk/pull/154));
 
 Changes to the Rzk website:
-  - Support multiple languages in the documentation (see [#150](https://github.com/rzk-lang/rzk/pull/150));
-      - English is the default;
-      - Russian documentation is partially translated and is available at <http://rzk-lang.github.io/rzk/ru/>;
-  - Add a blog (see [#153](https://github.com/rzk-lang/rzk/pull/153) and [`e438820`](https://github.com/rzk-lang/rzk/commit/e4388202cea59531903c4c24b939841b2771ceb7));
-      - The blog is not versioned and is always available at <https://rzk-lang.github.io/rzk/en/blog/>;
-  - Add a new [Other proof assistants for HoTT](https://rzk-lang.github.io/rzk/en/v0.7.2/related/) page (also [in Russian](https://rzk-lang.github.io/rzk/ru/v0.7.2/related/));
-  - Add a new [Introduction to Dependent Types](https://rzk-lang.github.io/rzk/en/v0.7.2/getting-started/dependent-types.rzk/) page (also [in Russian](https://rzk-lang.github.io/rzk/ru/v0.7.2/getting-started/dependent-types.rzk/))
-  - Add (default) social cards
-  - Integrate ToC on the left
-  - Use Inria Sans for English, PT Sans for Russian
+
+- Support multiple languages in the documentation (see [#150](https://github.com/rzk-lang/rzk/pull/150));
+  - English is the default;
+  - Russian documentation is partially translated and is available at <http://rzk-lang.github.io/rzk/ru/>;
+- Add a blog (see [#153](https://github.com/rzk-lang/rzk/pull/153) and [`e438820`](https://github.com/rzk-lang/rzk/commit/e4388202cea59531903c4c24b939841b2771ceb7));
+  - The blog is not versioned and is always available at <https://rzk-lang.github.io/rzk/en/blog/>;
+- Add a new [Other proof assistants for HoTT](https://rzk-lang.github.io/rzk/en/v0.7.2/related/) page (also [in Russian](https://rzk-lang.github.io/rzk/ru/v0.7.2/related/));
+- Add a new [Introduction to Dependent Types](https://rzk-lang.github.io/rzk/en/v0.7.2/getting-started/dependent-types.rzk/) page (also [in Russian](https://rzk-lang.github.io/rzk/ru/v0.7.2/getting-started/dependent-types.rzk/))
+- Add (default) social cards
+- Integrate ToC on the left
+- Use Inria Sans for English, PT Sans for Russian
 
 ## v0.7.1 — 2023-12-08
 
diff --git a/app/Main.hs b/app/Main.hs
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -16,7 +16,7 @@
                                           (>=>))
 import           Data.Version            (showVersion)
 
-#ifdef LSP
+#ifdef LSP_ENABLED
 import           Language.Rzk.VSCode.Lsp (runLsp)
 #endif
 
@@ -66,7 +66,7 @@
         Right _decls -> putStrLn "Everything is ok!"
 
     Lsp ->
-#ifdef LSP
+#ifdef LSP_ENABLED
       void runLsp
 #else
       error "rzk lsp is not supported with this build"
diff --git a/grammar/Syntax.cf b/grammar/Syntax.cf
--- a/grammar/Syntax.cf
+++ b/grammar/Syntax.cf
@@ -60,6 +60,7 @@
 PatternUnit.      Pattern ::= "unit" ;
 PatternVar.       Pattern ::= VarIdent ;
 PatternPair.      Pattern ::= "(" Pattern "," Pattern ")" ;
+PatternTuple.     Pattern ::= "(" Pattern "," Pattern "," [Pattern] ")" ;
 separator nonempty Pattern "" ;
 
 -- Parameter introduction (for lambda abstractions)
@@ -78,6 +79,10 @@
 paramVarShapeDeprecated. ParamDecl ::= "{" Pattern ":" Term "|" Term "}" ;
 define paramVarShapeDeprecated pat cube tope = ParamVarShapeDeprecated pat cube tope ;
 
+-- Parameter declaration for Sigma types
+SigmaParam. SigmaParam ::= Pattern ":" Term ;
+separator nonempty SigmaParam "," ;
+
 Restriction. Restriction ::= Term "↦" Term ;
 separator nonempty Restriction "," ;
 
@@ -106,6 +111,7 @@
 -- Types
 TypeFun.        Term1 ::= ParamDecl "→" Term1 ;
 TypeSigma.      Term1 ::= "Σ" "(" Pattern ":" Term ")" "," Term1 ;
+TypeSigmaTuple. Term1 ::= "Σ" "(" SigmaParam "," [SigmaParam] ")" "," Term1 ;
 TypeUnit.       Term7 ::= "Unit" ;
 TypeId.         Term1 ::= Term2 "=_{" Term "}" Term2 ;
 TypeIdSimple.   Term1 ::= Term2 "=" Term2 ;
@@ -115,6 +121,7 @@
 App.            Term6 ::= Term6 Term7 ;
 Lambda.         Term1 ::= "\\" [Param] "→" Term1 ;
 Pair.           Term7 ::= "(" Term "," Term ")" ;
+Tuple.          Term7 ::= "(" Term "," Term "," [Term] ")" ;
 First.          Term6 ::= "π₁" Term7 ;
 Second.         Term6 ::= "π₂" Term7 ;
 Unit.           Term7 ::= "unit" ;
@@ -149,6 +156,7 @@
 
 ASCII_TypeFun.        Term1 ::= ParamDecl "->" Term1 ;
 ASCII_TypeSigma.      Term1 ::= "Sigma" "(" Pattern ":" Term ")" "," Term1 ;
+ASCII_TypeSigmaTuple. Term1 ::= "Sigma" "(" SigmaParam "," [SigmaParam] ")" "," Term1 ;
 
 ASCII_Lambda.         Term1 ::= "\\" [Param] "->" Term1 ;
 ASCII_Restriction. Restriction ::= Term "|->" Term ;
@@ -161,4 +169,6 @@
 -- Alternative Unicode syntax rules
 
 unicode_TypeSigmaAlt.   Term1 ::= "∑" "(" Pattern ":" Term ")" "," Term1 ;    -- \sum
+unicode_TypeSigmaTupleAlt. Term1 ::= "∑" "(" SigmaParam "," [SigmaParam] ")" "," Term1 ;
 define unicode_TypeSigmaAlt pat fst snd = TypeSigma pat fst snd ;
+define unicode_TypeSigmaTupleAlt par pars t = TypeSigmaTuple par pars t ;
diff --git a/rzk.cabal b/rzk.cabal
--- a/rzk.cabal
+++ b/rzk.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           rzk
-version:        0.7.4
+version:        0.7.5
 synopsis:       An experimental proof assistant for synthetic ∞-categories
 description:    Please see the README on GitHub at <https://github.com/rzk-lang/rzk#readme>
 category:       Dependent Types
@@ -13,7 +13,7 @@
 bug-reports:    https://github.com/rzk-lang/rzk/issues
 author:         Nikolai Kudasov
 maintainer:     nickolay.kudasov@gmail.com
-copyright:      2023 Nikolai Kudasov
+copyright:      2023-2024 Nikolai Kudasov
 license:        BSD3
 license-file:   LICENSE
 build-type:     Custom
@@ -76,7 +76,7 @@
     , yaml >=0.11.0.0
   default-language: Haskell2010
   if flag(lsp) && !impl(ghcjs)
-    cpp-options: -DLSP
+    cpp-options: -DLSP_ENABLED
   if flag(lsp) && !impl(ghcjs)
     exposed-modules:
         Language.Rzk.VSCode.Config
@@ -121,7 +121,7 @@
     , yaml >=0.11.0.0
   default-language: Haskell2010
   if flag(lsp) && !impl(ghcjs)
-    cpp-options: -DLSP
+    cpp-options: -DLSP_ENABLED
   if !impl(ghcjs)
     build-depends:
         optparse-generic >=1.4.0
@@ -153,7 +153,7 @@
     , yaml >=0.11.0.0
   default-language: Haskell2010
   if flag(lsp) && !impl(ghcjs)
-    cpp-options: -DLSP
+    cpp-options: -DLSP_ENABLED
 
 test-suite rzk-test
   type: exitcode-stdio-1.0
@@ -185,4 +185,4 @@
     , yaml >=0.11.0.0
   default-language: Haskell2010
   if flag(lsp) && !impl(ghcjs)
-    cpp-options: -DLSP
+    cpp-options: -DLSP_ENABLED
diff --git a/src/Language/Rzk/Free/Syntax.hs b/src/Language/Rzk/Free/Syntax.hs
--- a/src/Language/Rzk/Free/Syntax.hs
+++ b/src/Language/Rzk/Free/Syntax.hs
@@ -173,7 +173,13 @@
     bindings (Rzk.PatternVar _loc (Rzk.VarIdent _ "_")) _ = []
     bindings (Rzk.PatternVar _loc x)    t = [(varIdent x, t)]
     bindings (Rzk.PatternPair _loc l r) t = bindings l (First t) <> bindings r (Second t)
+    bindings (Rzk.PatternTuple loc p1 p2 ps) t = bindings (desugarTuple loc (reverse ps) p2 p1) t
 
+desugarTuple loc ps p2 p1 =
+  case ps of
+    []          -> Rzk.PatternPair loc p1 p2
+    pLast : ps' -> Rzk.PatternPair loc (desugarTuple loc ps' p2 p1) pLast
+
 toTerm :: (VarIdent -> Term a) -> Rzk.Term -> Term a
 toTerm bvars = go
   where
@@ -209,7 +215,6 @@
         (Rzk.TypeFun loc (Rzk.ParamTermShape loc' (patternToTerm pat) cube tope) ret)
       t@(Rzk.Lambda loc ((Rzk.ParamPatternShapeDeprecated loc' pat cube tope):params) body) -> deprecated t
         (Rzk.Lambda loc ((Rzk.ParamPatternShape loc' [pat] cube tope):params) body)
-
       -- ASCII versions
       Rzk.ASCII_CubeUnitStar loc -> go (Rzk.CubeUnitStar loc)
       Rzk.ASCII_Cube2_0 loc -> go (Rzk.Cube2_0 loc)
@@ -223,6 +228,7 @@
 
       Rzk.ASCII_TypeFun loc param ret -> go (Rzk.TypeFun loc param ret)
       Rzk.ASCII_TypeSigma loc pat ty ret -> go (Rzk.TypeSigma loc pat ty ret)
+      Rzk.ASCII_TypeSigmaTuple loc p ps tN -> go (Rzk.TypeSigmaTuple loc p ps tN)
       Rzk.ASCII_Lambda loc pat ret -> go (Rzk.Lambda loc pat ret)
       Rzk.ASCII_TypeExtensionDeprecated loc shape type_ -> go (Rzk.TypeExtensionDeprecated loc shape type_)
       Rzk.ASCII_First loc term -> go (Rzk.First loc term)
@@ -256,6 +262,8 @@
       Rzk.Unit _loc -> Unit
       Rzk.App _loc f x -> App (go f) (go x)
       Rzk.Pair _loc l r -> Pair (go l) (go r)
+      Rzk.Tuple _loc p1 p2 (p:ps) -> go (Rzk.Tuple _loc (Rzk.Pair _loc p1 p2) p ps)
+      Rzk.Tuple _loc p1 p2 [] -> go (Rzk.Pair _loc p1 p2)
       Rzk.First _loc term -> First (go term)
       Rzk.Second _loc term -> Second (go term)
       Rzk.Refl _loc -> Refl Nothing
@@ -280,11 +288,18 @@
       Rzk.TypeSigma _loc pat tA tB ->
         TypeSigma (patternVar pat) (go tA) (toScopePattern pat bvars tB)
 
+      Rzk.TypeSigmaTuple _loc (Rzk.SigmaParam _ patA tA) ((Rzk.SigmaParam _ patB tB) : ps) tN -> 
+        go (Rzk.TypeSigmaTuple _loc (Rzk.SigmaParam _loc patX tX) ps tN)
+        where
+          patX = Rzk.PatternPair _loc patA patB
+          tX = Rzk.TypeSigma _loc patA tA tB
+      Rzk.TypeSigmaTuple _loc (Rzk.SigmaParam _ pat tA) [] tB -> go (Rzk.TypeSigma _loc pat tA tB)
+
       Rzk.Lambda _loc [] body -> go body
       Rzk.Lambda _loc (Rzk.ParamPattern _ pat : params) body ->
         Lambda (patternVar pat) Nothing (toScopePattern pat bvars (Rzk.Lambda _loc params body))
       Rzk.Lambda _loc (Rzk.ParamPatternType _ [] _ty : params) body ->
-        go (Rzk.Lambda _loc params body)
+        go (Rzk.Lambda _loc params body)                        
       Rzk.Lambda _loc (Rzk.ParamPatternType _ (pat:pats) ty : params) body ->
         Lambda (patternVar pat) (Just (go ty, Nothing))
           (toScopePattern pat bvars (Rzk.Lambda _loc (Rzk.ParamPatternType _loc pats ty : params) body))
@@ -317,6 +332,7 @@
       Rzk.PatternVar loc x    -> Rzk.Var loc x
       Rzk.PatternPair loc l r -> Rzk.Pair loc (ptt l) (ptt r)
       Rzk.PatternUnit loc     -> Rzk.Unit loc
+      Rzk.PatternTuple loc p1 p2 ps -> patternToTerm (desugarTuple loc (reverse ps) p2 p1)
 
 unsafeTermToPattern :: Rzk.Term -> Rzk.Pattern
 unsafeTermToPattern = ttp
diff --git a/src/Language/Rzk/Syntax/Abs.hs b/src/Language/Rzk/Syntax/Abs.hs
--- a/src/Language/Rzk/Syntax/Abs.hs
+++ b/src/Language/Rzk/Syntax/Abs.hs
@@ -72,6 +72,7 @@
     = PatternUnit a
     | PatternVar a (VarIdent' a)
     | PatternPair a (Pattern' a) (Pattern' a)
+    | PatternTuple a (Pattern' a) (Pattern' a) [Pattern' a]
   deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)
 
 type Param = Param' BNFC'Position
@@ -91,6 +92,10 @@
     | ParamVarShapeDeprecated a (Pattern' a) (Term' a) (Term' a)
   deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)
 
+type SigmaParam = SigmaParam' BNFC'Position
+data SigmaParam' a = SigmaParam a (Pattern' a) (Term' a)
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)
+
 type Restriction = Restriction' BNFC'Position
 data Restriction' a
     = Restriction a (Term' a) (Term' a)
@@ -119,6 +124,7 @@
     | RecOrDeprecated a (Term' a) (Term' a) (Term' a) (Term' a)
     | TypeFun a (ParamDecl' a) (Term' a)
     | TypeSigma a (Pattern' a) (Term' a) (Term' a)
+    | TypeSigmaTuple a (SigmaParam' a) [SigmaParam' a] (Term' a)
     | TypeUnit a
     | TypeId a (Term' a) (Term' a) (Term' a)
     | TypeIdSimple a (Term' a) (Term' a)
@@ -127,6 +133,7 @@
     | App a (Term' a) (Term' a)
     | Lambda a [Param' a] (Term' a)
     | Pair a (Term' a) (Term' a)
+    | Tuple a (Term' a) (Term' a) [Term' a]
     | First a (Term' a)
     | Second a (Term' a)
     | Unit a
@@ -148,6 +155,7 @@
     | ASCII_TopeOr a (Term' a) (Term' a)
     | ASCII_TypeFun a (ParamDecl' a) (Term' a)
     | ASCII_TypeSigma a (Pattern' a) (Term' a) (Term' a)
+    | ASCII_TypeSigmaTuple a (SigmaParam' a) [SigmaParam' a] (Term' a)
     | ASCII_Lambda a [Param' a] (Term' a)
     | ASCII_TypeExtensionDeprecated a (ParamDecl' a) (Term' a)
     | ASCII_First a (Term' a)
@@ -184,6 +192,9 @@
 unicode_TypeSigmaAlt :: a -> Pattern' a -> Term' a -> Term' a -> Term' a
 unicode_TypeSigmaAlt = \ _a pat fst snd -> TypeSigma _a pat fst snd
 
+unicode_TypeSigmaTupleAlt :: a -> SigmaParam' a -> [SigmaParam' a] -> Term' a -> Term' a
+unicode_TypeSigmaTupleAlt = \ _a par pars t -> TypeSigmaTuple _a par pars t
+
 newtype VarIdentToken = VarIdentToken String
   deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic, Data.String.IsString)
 
@@ -253,6 +264,7 @@
     PatternUnit p -> p
     PatternVar p _ -> p
     PatternPair p _ _ -> p
+    PatternTuple p _ _ _ -> p
 
 instance HasPosition Param where
   hasPosition = \case
@@ -269,6 +281,10 @@
     ParamTermTypeDeprecated p _ _ -> p
     ParamVarShapeDeprecated p _ _ _ -> p
 
+instance HasPosition SigmaParam where
+  hasPosition = \case
+    SigmaParam p _ _ -> p
+
 instance HasPosition Restriction where
   hasPosition = \case
     Restriction p _ _ -> p
@@ -296,6 +312,7 @@
     RecOrDeprecated p _ _ _ _ -> p
     TypeFun p _ _ -> p
     TypeSigma p _ _ _ -> p
+    TypeSigmaTuple p _ _ _ -> p
     TypeUnit p -> p
     TypeId p _ _ _ -> p
     TypeIdSimple p _ _ -> p
@@ -304,6 +321,7 @@
     App p _ _ -> p
     Lambda p _ _ -> p
     Pair p _ _ -> p
+    Tuple p _ _ _ -> p
     First p _ -> p
     Second p _ -> p
     Unit p -> p
@@ -325,6 +343,7 @@
     ASCII_TopeOr p _ _ -> p
     ASCII_TypeFun p _ _ -> p
     ASCII_TypeSigma p _ _ _ -> p
+    ASCII_TypeSigmaTuple p _ _ _ -> p
     ASCII_Lambda p _ _ -> p
     ASCII_TypeExtensionDeprecated p _ _ -> p
     ASCII_First p _ -> p
diff --git a/src/Language/Rzk/Syntax/Par.y b/src/Language/Rzk/Syntax/Par.y
--- a/src/Language/Rzk/Syntax/Par.y
+++ b/src/Language/Rzk/Syntax/Par.y
@@ -23,6 +23,8 @@
   , pParam
   , pListParam
   , pParamDecl
+  , pSigmaParam
+  , pListSigmaParam
   , pRestriction
   , pListRestriction
   , pTerm7
@@ -58,6 +60,8 @@
 %name pParam_internal Param
 %name pListParam_internal ListParam
 %name pParamDecl_internal ParamDecl
+%name pSigmaParam_internal SigmaParam
+%name pListSigmaParam_internal ListSigmaParam
 %name pRestriction_internal Restriction
 %name pListRestriction_internal ListRestriction
 %name pTerm7_internal Term7
@@ -230,6 +234,7 @@
   : 'unit' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.PatternUnit (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
   | VarIdent { (fst $1, Language.Rzk.Syntax.Abs.PatternVar (fst $1) (snd $1)) }
   | '(' Pattern ',' Pattern ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.PatternPair (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | '(' Pattern ',' Pattern ',' ListPattern ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.PatternTuple (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }
 
 ListPattern :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Pattern]) }
 ListPattern
@@ -257,6 +262,15 @@
   | '{' '(' Pattern ':' Term ')' '|' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamVarShapeDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }
   | '{' Pattern ':' Term '|' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.paramVarShapeDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }
 
+SigmaParam :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.SigmaParam) }
+SigmaParam
+  : Pattern ':' Term { (fst $1, Language.Rzk.Syntax.Abs.SigmaParam (fst $1) (snd $1) (snd $3)) }
+
+ListSigmaParam :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.SigmaParam]) }
+ListSigmaParam
+  : SigmaParam { (fst $1, (:[]) (snd $1)) }
+  | SigmaParam ',' ListSigmaParam { (fst $1, (:) (snd $1) (snd $3)) }
+
 Restriction :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Restriction) }
 Restriction
   : Term '↦' Term { (fst $1, Language.Rzk.Syntax.Abs.Restriction (fst $1) (snd $1) (snd $3)) }
@@ -285,6 +299,7 @@
   | 'Unit' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TypeUnit (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
   | '<' ParamDecl '→' Term '>' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TypeExtensionDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
   | '(' Term ',' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Pair (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | '(' Term ',' Term ',' ListTerm ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Tuple (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }
   | 'unit' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Unit (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
   | 'refl' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Refl (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
   | 'refl_{' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ReflTerm (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
@@ -330,14 +345,17 @@
 Term1
   : ParamDecl '→' Term1 { (fst $1, Language.Rzk.Syntax.Abs.TypeFun (fst $1) (snd $1) (snd $3)) }
   | 'Σ' '(' Pattern ':' Term ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TypeSigma (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }
+  | 'Σ' '(' SigmaParam ',' ListSigmaParam ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TypeSigmaTuple (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }
   | Term2 '=_{' Term '}' Term2 { (fst $1, Language.Rzk.Syntax.Abs.TypeId (fst $1) (snd $1) (snd $3) (snd $5)) }
   | Term2 '=' Term2 { (fst $1, Language.Rzk.Syntax.Abs.TypeIdSimple (fst $1) (snd $1) (snd $3)) }
   | '\\' ListParam '→' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Lambda (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
   | Term2 { (fst $1, (snd $1)) }
   | ParamDecl '->' Term1 { (fst $1, Language.Rzk.Syntax.Abs.ASCII_TypeFun (fst $1) (snd $1) (snd $3)) }
   | 'Sigma' '(' Pattern ':' Term ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_TypeSigma (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }
+  | 'Sigma' '(' SigmaParam ',' ListSigmaParam ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_TypeSigmaTuple (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }
   | '\\' ListParam '->' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_Lambda (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
   | '∑' '(' Pattern ':' Term ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.unicode_TypeSigmaAlt (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }
+  | '∑' '(' SigmaParam ',' ListSigmaParam ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.unicode_TypeSigmaTupleAlt (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }
 
 Term6 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }
 Term6
@@ -420,6 +438,12 @@
 
 pParamDecl :: [Token] -> Err Language.Rzk.Syntax.Abs.ParamDecl
 pParamDecl = fmap snd . pParamDecl_internal
+
+pSigmaParam :: [Token] -> Err Language.Rzk.Syntax.Abs.SigmaParam
+pSigmaParam = fmap snd . pSigmaParam_internal
+
+pListSigmaParam :: [Token] -> Err [Language.Rzk.Syntax.Abs.SigmaParam]
+pListSigmaParam = fmap snd . pListSigmaParam_internal
 
 pRestriction :: [Token] -> Err Language.Rzk.Syntax.Abs.Restriction
 pRestriction = fmap snd . pRestriction_internal
diff --git a/src/Language/Rzk/Syntax/Print.hs b/src/Language/Rzk/Syntax/Print.hs
--- a/src/Language/Rzk/Syntax/Print.hs
+++ b/src/Language/Rzk/Syntax/Print.hs
@@ -198,6 +198,7 @@
     Language.Rzk.Syntax.Abs.PatternUnit _ -> prPrec i 0 (concatD [doc (showString "unit")])
     Language.Rzk.Syntax.Abs.PatternVar _ varident -> prPrec i 0 (concatD [prt 0 varident])
     Language.Rzk.Syntax.Abs.PatternPair _ pattern_1 pattern_2 -> prPrec i 0 (concatD [doc (showString "("), prt 0 pattern_1, doc (showString ","), prt 0 pattern_2, doc (showString ")")])
+    Language.Rzk.Syntax.Abs.PatternTuple _ pattern_1 pattern_2 patterns -> prPrec i 0 (concatD [doc (showString "("), prt 0 pattern_1, doc (showString ","), prt 0 pattern_2, doc (showString ","), prt 0 patterns, doc (showString ")")])
 
 instance Print [Language.Rzk.Syntax.Abs.Pattern' a] where
   prt _ [] = concatD []
@@ -224,6 +225,15 @@
     Language.Rzk.Syntax.Abs.ParamTermTypeDeprecated _ pattern_ term -> prPrec i 0 (concatD [doc (showString "{"), prt 0 pattern_, doc (showString ":"), prt 0 term, doc (showString "}")])
     Language.Rzk.Syntax.Abs.ParamVarShapeDeprecated _ pattern_ term1 term2 -> prPrec i 0 (concatD [doc (showString "{"), doc (showString "("), prt 0 pattern_, doc (showString ":"), prt 0 term1, doc (showString ")"), doc (showString "|"), prt 0 term2, doc (showString "}")])
 
+instance Print (Language.Rzk.Syntax.Abs.SigmaParam' a) where
+  prt i = \case
+    Language.Rzk.Syntax.Abs.SigmaParam _ pattern_ term -> prPrec i 0 (concatD [prt 0 pattern_, doc (showString ":"), prt 0 term])
+
+instance Print [Language.Rzk.Syntax.Abs.SigmaParam' a] where
+  prt _ [] = concatD []
+  prt _ [x] = concatD [prt 0 x]
+  prt _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs]
+
 instance Print (Language.Rzk.Syntax.Abs.Restriction' a) where
   prt i = \case
     Language.Rzk.Syntax.Abs.Restriction _ term1 term2 -> prPrec i 0 (concatD [prt 0 term1, doc (showString "\8614"), prt 0 term2])
@@ -256,6 +266,7 @@
     Language.Rzk.Syntax.Abs.RecOrDeprecated _ term1 term2 term3 term4 -> prPrec i 7 (concatD [doc (showString "recOR"), doc (showString "("), prt 0 term1, doc (showString ","), prt 0 term2, doc (showString ","), prt 0 term3, doc (showString ","), prt 0 term4, doc (showString ")")])
     Language.Rzk.Syntax.Abs.TypeFun _ paramdecl term -> prPrec i 1 (concatD [prt 0 paramdecl, doc (showString "\8594"), prt 1 term])
     Language.Rzk.Syntax.Abs.TypeSigma _ pattern_ term1 term2 -> prPrec i 1 (concatD [doc (showString "\931"), doc (showString "("), prt 0 pattern_, doc (showString ":"), prt 0 term1, doc (showString ")"), doc (showString ","), prt 1 term2])
+    Language.Rzk.Syntax.Abs.TypeSigmaTuple _ sigmaparam sigmaparams term -> prPrec i 1 (concatD [doc (showString "\931"), doc (showString "("), prt 0 sigmaparam, doc (showString ","), prt 0 sigmaparams, doc (showString ")"), doc (showString ","), prt 1 term])
     Language.Rzk.Syntax.Abs.TypeUnit _ -> prPrec i 7 (concatD [doc (showString "Unit")])
     Language.Rzk.Syntax.Abs.TypeId _ term1 term2 term3 -> prPrec i 1 (concatD [prt 2 term1, doc (showString "=_{"), prt 0 term2, doc (showString "}"), prt 2 term3])
     Language.Rzk.Syntax.Abs.TypeIdSimple _ term1 term2 -> prPrec i 1 (concatD [prt 2 term1, doc (showString "="), prt 2 term2])
@@ -264,6 +275,7 @@
     Language.Rzk.Syntax.Abs.App _ term1 term2 -> prPrec i 6 (concatD [prt 6 term1, prt 7 term2])
     Language.Rzk.Syntax.Abs.Lambda _ params term -> prPrec i 1 (concatD [doc (showString "\\"), prt 0 params, doc (showString "\8594"), prt 1 term])
     Language.Rzk.Syntax.Abs.Pair _ term1 term2 -> prPrec i 7 (concatD [doc (showString "("), prt 0 term1, doc (showString ","), prt 0 term2, doc (showString ")")])
+    Language.Rzk.Syntax.Abs.Tuple _ term1 term2 terms -> prPrec i 7 (concatD [doc (showString "("), prt 0 term1, doc (showString ","), prt 0 term2, doc (showString ","), prt 0 terms, doc (showString ")")])
     Language.Rzk.Syntax.Abs.First _ term -> prPrec i 6 (concatD [doc (showString "\960\8321"), prt 7 term])
     Language.Rzk.Syntax.Abs.Second _ term -> prPrec i 6 (concatD [doc (showString "\960\8322"), prt 7 term])
     Language.Rzk.Syntax.Abs.Unit _ -> prPrec i 7 (concatD [doc (showString "unit")])
@@ -285,6 +297,7 @@
     Language.Rzk.Syntax.Abs.ASCII_TopeOr _ term1 term2 -> prPrec i 2 (concatD [prt 3 term1, doc (showString "\\/"), prt 2 term2])
     Language.Rzk.Syntax.Abs.ASCII_TypeFun _ paramdecl term -> prPrec i 1 (concatD [prt 0 paramdecl, doc (showString "->"), prt 1 term])
     Language.Rzk.Syntax.Abs.ASCII_TypeSigma _ pattern_ term1 term2 -> prPrec i 1 (concatD [doc (showString "Sigma"), doc (showString "("), prt 0 pattern_, doc (showString ":"), prt 0 term1, doc (showString ")"), doc (showString ","), prt 1 term2])
+    Language.Rzk.Syntax.Abs.ASCII_TypeSigmaTuple _ sigmaparam sigmaparams term -> prPrec i 1 (concatD [doc (showString "Sigma"), doc (showString "("), prt 0 sigmaparam, doc (showString ","), prt 0 sigmaparams, doc (showString ")"), doc (showString ","), prt 1 term])
     Language.Rzk.Syntax.Abs.ASCII_Lambda _ params term -> prPrec i 1 (concatD [doc (showString "\\"), prt 0 params, doc (showString "->"), prt 1 term])
     Language.Rzk.Syntax.Abs.ASCII_TypeExtensionDeprecated _ paramdecl term -> prPrec i 7 (concatD [doc (showString "<"), prt 0 paramdecl, doc (showString "->"), prt 0 term, doc (showString ">")])
     Language.Rzk.Syntax.Abs.ASCII_First _ term -> prPrec i 6 (concatD [doc (showString "first"), prt 7 term])
diff --git a/src/Language/Rzk/VSCode/Handlers.hs b/src/Language/Rzk/VSCode/Handlers.hs
--- a/src/Language/Rzk/VSCode/Handlers.hs
+++ b/src/Language/Rzk/VSCode/Handlers.hs
@@ -1,10 +1,12 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
+{-# LANGUAGE CPP           #-}
 {-# LANGUAGE DataKinds           #-}
 {-# LANGUAGE LambdaCase          #-}
 {-# LANGUAGE OverloadedStrings   #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications    #-}
-{-# OPTIONS_GHC -Wno-orphans #-}
-{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ViewPatterns        #-}
+{-# LANGUAGE RecordWildCards     #-}
 
 module Language.Rzk.VSCode.Handlers (
   typecheckFromConfigFile,
@@ -40,6 +42,7 @@
 import           System.FilePath               (makeRelative, (</>))
 import           System.FilePath.Glob          (compile, globDir)
 
+import           Data.Char                     (isDigit)
 import           Language.Rzk.Free.Syntax      (RzkPosition (RzkPosition),
                                                 VarIdent (getVarIdent))
 import           Language.Rzk.Syntax           (Module, VarIdent' (VarIdent),
@@ -53,6 +56,7 @@
                                                 formatTextEdits)
 import           Rzk.Project.Config            (ProjectConfig (include))
 import           Rzk.TypeCheck
+import           Text.Read                     (readMaybe)
 
 -- | Given a list of file paths, reads them and parses them as Rzk modules,
 --   returning the same list of file paths but with the parsed module (or parse error)
@@ -181,7 +185,7 @@
         line = fromIntegral $ fromMaybe 0 $ extractLineNumber err
 
     diagnosticOfParseError :: String -> Diagnostic
-    diagnosticOfParseError err = Diagnostic (Range (Position 0 0) (Position 0 0))
+    diagnosticOfParseError err = Diagnostic (Range (Position errLine errColumnStart) (Position errLine errColumnEnd))
                       (Just DiagnosticSeverity_Error)
                       (Just $ InR "parse-error")
                       Nothing
@@ -190,6 +194,27 @@
                       Nothing
                       (Just [])
                       Nothing
+      where
+        (errLine, errColumnStart, errColumnEnd) = fromMaybe (0, 0, 0) $
+          case words err of
+            -- Happy parse error
+            (take 9 -> ["syntax", "error", "at", "line", lineStr, "column", columnStr, "before", token]) -> do
+              line <- readMaybe (takeWhile isDigit lineStr)
+              columnStart <- readMaybe (takeWhile isDigit columnStr)
+              return (line - 1, columnStart - 1, columnStart + fromIntegral (length token) - 3)
+            -- Happy parse error due to lexer error
+            (take 7 -> ["syntax", "error", "at", "line", lineStr, "column", columnStr]) -> do
+              line <- readMaybe (takeWhile isDigit lineStr)
+              columnStart <- readMaybe (takeWhile isDigit columnStr)
+              return (line - 1, columnStart - 1, columnStart - 1)
+            -- BNFC layout resolver error
+            (take 14 -> ["Layout", "error", "at", "line", _lineStr, "column", _columnStr, "found", token, "at", "line", lineStr', "column", columnStr']) -> do
+              -- line <- readMaybe (takeWhile isDigit lineStr)
+              -- columnStart <- readMaybe (takeWhile isDigit columnStr)
+              line' <- readMaybe (takeWhile isDigit lineStr')
+              columnStart' <- readMaybe (takeWhile isDigit columnStr')
+              return (line' - 1, columnStart', columnStart' + fromIntegral (length token) - 2)
+            _ -> Nothing
 
 instance Default T.Text where def = ""
 instance Default CompletionItem
@@ -220,7 +245,7 @@
     declsToItems :: FilePath -> (FilePath, [Decl']) -> [CompletionItem]
     declsToItems root (path, decls) = map (declToItem root path) decls
     declToItem :: FilePath -> FilePath -> Decl' -> CompletionItem
-    declToItem rootDir path (Decl name type' _ _ _) = def
+    declToItem rootDir path (Decl name type' _ _ _ _loc) = def
       & label .~ T.pack (printTree $ getVarIdent name)
       & detail ?~ T.pack (show type')
       & documentation ?~ InR (MarkupContent MarkupKind_Markdown $ T.pack $
@@ -255,7 +280,11 @@
         let edits = formatTextEdits (filter (/= '\r') $ T.unpack sourceCode)
         return (Right $ map formattingEditToTextEdit edits)
     case possibleEdits of
+#if MIN_VERSION_lsp(2,7,0)
+      Left err    -> res $ Left $ TResponseError (InR ErrorCodes_InternalError) err Nothing
+#else
       Left err    -> res $ Left $ ResponseError (InR ErrorCodes_InternalError) err Nothing
+#endif
       Right edits -> do
         res $ Right $ InL edits
   else do
diff --git a/src/Language/Rzk/VSCode/Tokenize.hs b/src/Language/Rzk/VSCode/Tokenize.hs
--- a/src/Language/Rzk/VSCode/Tokenize.hs
+++ b/src/Language/Rzk/VSCode/Tokenize.hs
@@ -63,6 +63,7 @@
   PatternVar _loc var    -> mkToken var SemanticTokenTypes_Parameter [SemanticTokenModifiers_Declaration]
   PatternPair _loc l r   -> foldMap tokenizePattern [l, r]
   pat@(PatternUnit _loc) -> mkToken pat SemanticTokenTypes_EnumMember [SemanticTokenModifiers_Declaration]
+  PatternTuple _loc p1 p2 ps -> foldMap tokenizePattern (p1 : p2 : ps)
 
 tokenizeTope :: Term -> [SemanticTokenAbsolute]
 tokenizeTope = tokenizeTerm' (Just SemanticTokenTypes_String)
@@ -125,8 +126,17 @@
         [ mkToken (VarIdent loc "Sigma") SemanticTokenTypes_Class [SemanticTokenModifiers_DefaultLibrary]
         , tokenizePattern pat
         , foldMap go [a, b] ]
+      TypeSigmaTuple loc p ps tN -> concat 
+        [ mkToken (VarIdent loc "∑") SemanticTokenTypes_Class [SemanticTokenModifiers_DefaultLibrary]
+        , foldMap tokenizeSigmaParam (p : ps)
+        , go tN ]
+      ASCII_TypeSigmaTuple loc p ps tN -> concat 
+        [ mkToken (VarIdent loc "Sigma") SemanticTokenTypes_Class [SemanticTokenModifiers_DefaultLibrary]
+        , foldMap tokenizeSigmaParam (p : ps)
+        , go tN ]
       TypeId _loc x a y -> foldMap go [x, a, y]
       TypeIdSimple _loc x y -> foldMap go [x, y]
+        
 
       TypeRestricted _loc type_ rs -> concat
         [ go type_
@@ -139,6 +149,7 @@
       ASCII_Lambda loc params body -> go (Lambda loc params body)
 
       Pair _loc l r -> foldMap go [l, r]
+      Tuple _loc p1 p2 ps -> foldMap go (p1:p2:ps)
       First loc t -> concat
         [ mkToken (VarIdent loc "π₁") SemanticTokenTypes_Function [SemanticTokenModifiers_DefaultLibrary]
         , go t ]
@@ -200,6 +211,11 @@
     , tokenizeTerm cube
     , tokenizeTope tope
     ]
+
+tokenizeSigmaParam :: SigmaParam -> [SemanticTokenAbsolute]
+tokenizeSigmaParam (SigmaParam _loc pat type_) = concat 
+  [ tokenizePattern pat 
+  , tokenizeTerm type_ ]
 
 mkToken :: (HasPosition a, Print a) => a -> SemanticTokenTypes -> [SemanticTokenModifiers] -> [SemanticTokenAbsolute]
 mkToken x tokenType tokenModifiers =
diff --git a/src/Rzk/TypeCheck.hs b/src/Rzk/TypeCheck.hs
--- a/src/Rzk/TypeCheck.hs
+++ b/src/Rzk/TypeCheck.hs
@@ -1,10 +1,10 @@
 {-# OPTIONS_GHC -fno-warn-type-defaults -fno-warn-orphans #-}
-{-# LANGUAGE DeriveFoldable       #-}
-{-# LANGUAGE DeriveFunctor        #-}
-{-# LANGUAGE FlexibleInstances    #-}
-{-# LANGUAGE LambdaCase           #-}
-{-# LANGUAGE OverloadedStrings    #-}
-{-# LANGUAGE RecordWildCards      #-}
+{-# LANGUAGE DeriveFoldable    #-}
+{-# LANGUAGE DeriveFunctor     #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE LambdaCase        #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards   #-}
 module Rzk.TypeCheck where
 
 import           Control.Applicative      ((<|>))
@@ -45,6 +45,7 @@
   , declValue        :: Maybe (TermT var)
   , declIsAssumption :: Bool
   , declUsedVars     :: [var]
+  , declLocation     :: Maybe LocationInfo
   } deriving Eq
 
 type Decl' = Decl VarIdent
@@ -135,7 +136,8 @@
           paramDecls <- concat <$> mapM paramToParamDecl params
           ty' <- typecheck (toTerm' (addParamDecls paramDecls ty)) universeT >>= whnfT
           term' <- typecheck (toTerm' (addParams params term)) ty' >>= whnfT
-          let decl = Decl (varIdentAt path name) ty' (Just term') False (varIdentAt path <$> vars)
+          loc <- asks location
+          let decl = Decl (varIdentAt path name) ty' (Just term') False (varIdentAt path <$> vars) loc
           fmap (first (decl :)) $
             localDeclPrepared decl $ do
               Context{..} <- ask
@@ -154,7 +156,8 @@
           mapM_ checkDefinedVar (varIdentAt path <$> vars)
           paramDecls <- concat <$> mapM paramToParamDecl params
           ty' <- typecheck (toTerm' (addParamDecls paramDecls ty)) universeT >>= whnfT
-          let decl = Decl (varIdentAt path name) ty' Nothing False (varIdentAt path <$> vars)
+          loc <- asks location
+          let decl = Decl (varIdentAt path name) ty' Nothing False (varIdentAt path <$> vars) loc
           fmap (first (decl :)) $
             localDeclPrepared decl $
               go (i + 1) moreCommands
@@ -191,7 +194,8 @@
           <> " Checking #assume " <> intercalate " " [ Rzk.printTree name | name <- names ] ) $ do
         withCommand command $ do
           ty' <- typecheck (toTerm' ty) universeT
-          let decls = [ Decl (varIdentAt path name) ty' Nothing True [] | name <- names ]
+          loc <- asks location
+          let decls = [ Decl (varIdentAt path name) ty' Nothing True [] loc | name <- names ]
           fmap (first (decls <>)) $
             localDeclsPrepared decls $
               go (i + 1) moreCommands
@@ -451,14 +455,17 @@
   trace ("Warning: " <> message) $
     return ()
 
-issueTypeError :: TypeError var -> TypeCheck var a
-issueTypeError err = do
+fromTypeError :: TypeError var -> TypeCheck var (TypeErrorInScopedContext var)
+fromTypeError err = do
   context <- ask
-  throwError $ PlainTypeError $ TypeErrorInContext
+  return $ PlainTypeError $ TypeErrorInContext
     { typeErrorError = err
     , typeErrorContext = context
     }
 
+issueTypeError :: TypeError var -> TypeCheck var a
+issueTypeError err = fromTypeError err >>= throwError
+
 panicImpossible :: String -> a
 panicImpossible msg = error $ unlines
   [ "PANIC! Impossible happened (" <> msg <> ")!"
@@ -576,7 +583,7 @@
 data LocationInfo = LocationInfo
   { locationFilePath :: Maybe FilePath
   , locationLine     :: Maybe Int
-  }
+  } deriving (Eq)
 
 data Verbosity
   = Debug
@@ -623,6 +630,7 @@
   , varOrig                :: Maybe VarIdent
   , varIsAssumption        :: Bool -- FIXME: perhaps, introduce something like decl kind?
   , varDeclaredAssumptions :: [var]
+  , varLocation            :: Maybe LocationInfo
   } deriving (Functor, Foldable)
 
 data Context var = Context
@@ -700,26 +708,34 @@
     (decls, errs) <- sectionBody
     localDeclsPrepared decls $
       performing (ActionCloseSection name) $ do
-        (\ decls' -> (decls', errs)) <$> endSection errs
+        result <- (Right <$> endSection errs) `catchError` (return . Left)
+        case result of
+          Left err              -> return ([], errs <> [err])
+          Right (decls', errs') -> return (decls', errs')
+        -- (\ decls' -> (decls', errs)) <$> endSection errs
 
 startSection :: Maybe Rzk.SectionName -> TypeCheck VarIdent a -> TypeCheck VarIdent a
 startSection name = local $ \Context{..} -> Context
   { localScopes = ScopeInfo { scopeName = name, scopeVars = [] } : localScopes
   , .. }
 
-endSection :: [TypeErrorInScopedContext VarIdent] -> TypeCheck VarIdent [Decl']
+endSection :: [TypeErrorInScopedContext VarIdent] -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent])
 endSection errs = askCurrentScope >>= scopeToDecls errs
 
-scopeToDecls :: Eq var => [TypeErrorInScopedContext VarIdent] -> ScopeInfo var -> TypeCheck var [Decl var]
+scopeToDecls :: Eq var => [TypeErrorInScopedContext var] -> ScopeInfo var -> TypeCheck var ([Decl var], [TypeErrorInScopedContext var])
 scopeToDecls errs ScopeInfo{..} = do
-  decls <- collectScopeDecls errs [] scopeVars
+  (decls, errs') <- collectScopeDecls errs [] scopeVars
   -- only issue unused variable errors if there were no errors prior in the section
-  when (null errs) $ do
-    forM_ decls $ \Decl{..} -> do
-      let unusedUsedVars = declUsedVars `intersect` map fst scopeVars
-      when (not (null unusedUsedVars)) $
-        issueTypeError $ TypeErrorUnusedUsedVariables unusedUsedVars declName
-  return decls
+  -- when (null errs) $ do
+  unusedErrors <- forM decls $ \Decl{..} -> do
+    let unusedUsedVars = declUsedVars `intersect` map fst scopeVars
+    if null errs && not (null unusedUsedVars)
+      then do
+        err <- local (\c -> c { location = declLocation }) $
+          fromTypeError (TypeErrorUnusedUsedVariables unusedUsedVars declName)
+        return [err]
+      else return []
+  return (decls, errs' <> concat unusedErrors)
 
 insertExplicitAssumptionFor
   :: Eq var => var -> (var, VarInfo var) -> TermT var -> TermT var
@@ -738,6 +754,7 @@
       , varIsAssumption = varIsAssumption
       , varOrig = varOrig
       , varDeclaredAssumptions = varDeclaredAssumptions
+      , varLocation = varLocation
       }
 
 makeAssumptionExplicit
@@ -776,29 +793,38 @@
       , varIsAssumption = varIsAssumption xInfo
       , varOrig = varOrig xInfo
       , varDeclaredAssumptions = varDeclaredAssumptions xInfo \\ [a]
+      , varLocation = varLocation xInfo
       }
     xs' = map (fmap (insertExplicitAssumptionFor' a (x, xInfo))) xs
 
-collectScopeDecls :: Eq var => [TypeErrorInScopedContext VarIdent] -> [(var, VarInfo var)] -> [(var, VarInfo var)] -> TypeCheck var [Decl var]
+collectScopeDecls :: Eq var => [TypeErrorInScopedContext var] -> [(var, VarInfo var)] -> [(var, VarInfo var)] -> TypeCheck var ([Decl var], [TypeErrorInScopedContext var])
 collectScopeDecls errs recentVars (decl@(var, VarInfo{..}) : vars)
   | varIsAssumption = do
       (used, recentVars') <- makeAssumptionExplicit decl recentVars
       -- only issue unused vars error if there were no other errors previously
-      when (null errs) $ do
-        when (not used) $ do
-          issueTypeError $ TypeErrorUnusedVariable var varType
-      collectScopeDecls errs recentVars' vars
+      -- when (null errs) $ do
+      unusedErr <-
+        if null errs && not used
+          then local (\c -> c { location = varLocation }) $
+            pure <$> fromTypeError (TypeErrorUnusedVariable var varType)
+          else return []
+      collectScopeDecls (errs <> unusedErr) recentVars' vars
   | otherwise = do
       collectScopeDecls errs (decl : recentVars) vars
-collectScopeDecls _ recentVars [] = return (toDecl <$> recentVars)
+collectScopeDecls errs recentVars [] = do
+  loc <- asks location
+  return (toDecl loc <$> recentVars, errs)
   where
-    toDecl (var, VarInfo{..}) = Decl
+    toDecl loc (var, VarInfo{..}) = Decl
       { declName = var
       , declType = varType
       , declValue = varValue
       , declIsAssumption = varIsAssumption
       , declUsedVars = varDeclaredAssumptions
+      , declLocation = updatePosition (varOrig >>= fmap fst . Rzk.hasPosition . fromVarIdent) <$> loc -- FIXME
       }
+    updatePosition Nothing l       = l
+    updatePosition (Just lineNo) l = l { locationLine = Just lineNo }
 
 abstractAssumption :: Eq var => (var, VarInfo var) -> Decl var -> Decl var
 abstractAssumption (var, VarInfo{..}) Decl{..} = Decl
@@ -807,6 +833,7 @@
   , declValue = (\body -> lambdaT newDeclType varOrig Nothing (abstract var body)) <$> declValue
   , declIsAssumption = declIsAssumption
   , declUsedVars = declUsedVars
+  , declLocation = declLocation
   }
   where
     newDeclType = typeFunT varOrig varType Nothing (abstract var declType)
@@ -923,13 +950,13 @@
 localDeclsPrepared (decl : decls) = localDeclPrepared decl . localDeclsPrepared decls
 
 localDecl :: Decl VarIdent -> TypeCheck VarIdent a -> TypeCheck VarIdent a
-localDecl (Decl x ty term isAssumption vars) tc = do
+localDecl (Decl x ty term isAssumption vars loc) tc = do
   ty' <- whnfT ty
   term' <- traverse whnfT term
-  localDeclPrepared (Decl x ty' term' isAssumption vars) tc
+  localDeclPrepared (Decl x ty' term' isAssumption vars loc) tc
 
 localDeclPrepared :: Decl VarIdent -> TypeCheck VarIdent a -> TypeCheck VarIdent a
-localDeclPrepared (Decl x ty term isAssumption vars) tc = do
+localDeclPrepared (Decl x ty term isAssumption vars loc) tc = do
   checkTopLevelDuplicate x
   local update tc
   where
@@ -939,6 +966,7 @@
       , varOrig = Just x
       , varIsAssumption = isAssumption
       , varDeclaredAssumptions = vars
+      , varLocation = loc
       }
 
 type TypeCheck var = ReaderT (Context var) (Except (TypeErrorInScopedContext var))
@@ -1302,15 +1330,16 @@
       switch Contravariant = Covariant
 
 enterScopeContext :: Maybe VarIdent -> TermT var -> Context var -> Context (Inc var)
-enterScopeContext orig ty =
+enterScopeContext orig ty context =
   addVarInCurrentScope Z VarInfo
     { varType   = S <$> ty
     , varValue  = Nothing
     , varOrig   = orig
     , varIsAssumption = False
     , varDeclaredAssumptions = []
+    , varLocation = location context
     }
-  . fmap S
+    (S <$> context)
 
 enterScope :: Maybe VarIdent -> TermT var -> TypeCheck (Inc var) b -> TypeCheck var b
 enterScope orig ty action = do
@@ -1774,7 +1803,7 @@
               []   -> nfT type_
               rs'' -> TypeRestrictedT ty <$> nfT type_ <*> pure rs''
 
-checkDefinedVar :: Eq var => var -> TypeCheck var ()
+checkDefinedVar :: VarIdent -> TypeCheck VarIdent ()
 checkDefinedVar x = asks (lookup x . varInfos) >>= \case
   Nothing  -> issueTypeError $ TypeErrorUndefined x
   Just _ty -> return ()