diff --git a/.github/workflows/telomare-ci.yml b/.github/workflows/telomare-ci.yml
index 7320978a..da4cb348 100644
--- a/.github/workflows/telomare-ci.yml
+++ b/.github/workflows/telomare-ci.yml
@@ -93,7 +93,7 @@ jobs:
           extraPullNames: nix-community
       - name: hlint linting
         run: |
-          output=$(nix develop -c hlint "--ignore=Parse error" app/Evaluare.hs . --no-exit-code)
+          output=$(nix develop -c hlint . --no-exit-code)
           if [ "$output" = "No hints" ]; then
               echo "Success! No Hlint suggestions."
           else
diff --git a/Prelude.tel b/Prelude.tel
index c54a782f..897d8060 100644
--- a/Prelude.tel
+++ b/Prelude.tel
@@ -143,44 +143,19 @@ gcd = \a b ->
 lcm = \a b -> dDiv (dTimes a b) (gcd a b)
 
 [Rational, fromRational, toRational, rPlus, rTimes, rMinus, rDiv] = \h ->
-  [ \n d -> if dEqual d 0
-            then abort "Denominator cannot be zero"
-            else
-              let g   = gcd n d
-                  num = dDiv n g
-                  den = dDiv d g
-              in (h, (num, den))
-  , \i -> Rational i
-  , \a b ->
-      let n1 = left (right a)
-          d1 = right (right a)
-          n2 = left (right b)
-          d2 = right (right b)
-          num = dPlus (dTimes n1 d2) (dTimes n2 d1)
-          den = dTimes d1 d2
-      in fromRational num den
-  , \a b ->
-      let n1 = left (right a)
-          d1 = right (right a)
-          n2 = left (right b)
-          d2 = right (right b)
-          num = dTimes n1 n2
-          den = dTimes d1 d2
-      in fromRational num den
-  , \a b ->
-      let n1 = left (right a)
-          d1 = right (right a)
-          n2 = left (right b)
-          d2 = right (right b)
-          num = dMinus (dTimes n1 d2) (dTimes n2 d1)
-          den = dTimes d1 d2
-      in fromRational num den
-  , \a b ->
-      let n1 = left (right a)
-          d1 = right (right a)
-          n2 = left (right b)
-          d2 = right (right b)
-          num = dTimes n1 d2
-          den = dTimes d1 n2
-      in fromRational num den
-  ]
+  let rNum = \x -> left (right x)
+      rDen = \x -> right (right x)
+  in [ \n d -> if dEqual d 0
+               then abort "Denominator cannot be zero"
+               else let g = gcd n d
+                    in (h, (dDiv n g, dDiv d g))
+     , Rational
+     , \a b -> fromRational (dPlus (dTimes (rNum a) (rDen b)) (dTimes (rNum b) (rDen a)))
+                            (dTimes (rDen a) (rDen b))
+     , \a b -> fromRational (dTimes (rNum a) (rNum b))
+                            (dTimes (rDen a) (rDen b))
+     , \a b -> fromRational (dMinus (dTimes (rNum a) (rDen b)) (dTimes (rNum b) (rDen a)))
+                            (dTimes (rDen a) (rDen b))
+     , \a b -> fromRational (dTimes (rNum a) (rDen b))
+                            (dTimes (rDen a) (rNum b))
+     ]
diff --git a/README.md b/README.md
index cbbd552b..5f34b9af 100644
--- a/README.md
+++ b/README.md
@@ -53,7 +53,136 @@ This project is in active development. Do expect bugs and general trouble, and p
    $ cabal run telomare-repl -- --haskell # or nix run .#repl
    ```
 2. Profit!
-   
+
+## Editor Support (LSP)
+
+Telomare ships a language server (`telomare-lsp`) and an Emacs major mode
+under [`emacs-telomare-mode/`](emacs-telomare-mode/), with variants for
+Spacemacs, Doom, and vanilla Emacs.
+
+### LSP capabilities
+
+The language server provides:
+
+- **Diagnostics** — on every document open and edit it reports parse
+  errors, missing imported modules, undefined variable references, and
+  resolver errors. Diagnostics are cleared when the document is closed.
+- **Go to definition** — jumps to local `let`, lambda, and case-pattern
+  binders, to top-level definitions, and to definitions in qualified
+  imported modules.
+- **Find references** — lists every reference to a symbol, optionally
+  including its declaration.
+- **Semantic-token highlighting** — keywords, comments, strings,
+  numbers, and operators, for the whole file or a requested range.
+- **Code action** — *Partially evaluate*: select an expression and the
+  server evaluates it, reporting the result in an editor popup.
+- **Workspace commands**:
+  - `telomare.version` — reports the server version as a UTC timestamp.
+  - `telomare.partialEval` — evaluates a given expression; this backs
+    the partial-evaluation code action.
+
+Document sync is full-text (whole-document). Hover and rename are not
+implemented yet.
+
+### Installing the Emacs mode
+
+The recommended Spacemacs setup is to load Telomare's Emacs mode from the
+same Telomare flake input that provides the language server. Do not point
+Spacemacs at a random checkout unless you are actively developing the mode;
+make the editor use the same pinned source that NixOS or Home Manager builds.
+
+For a NixOS/Home Manager Spacemacs config, add Telomare as a flake input and
+load the mode file from that input:
+
+```elisp
+(load "${telomare}/emacs-telomare-mode/telomare-mode-spacemacs.el")
+```
+
+The mode auto-detects the surrounding flake source path and starts the LSP with
+`nix run path:<telomare-source>#lsp --`. This matters for Nix store paths:
+`nix run /nix/store/...-source#lsp --` is parsed incorrectly by Nix, while
+`nix run path:/nix/store/...-source#lsp --` is the intended absolute-path flake
+form.
+
+For a manual checkout-based setup, load the mode from this repository and set
+`TELOMARE_ROOT` only if auto-detection cannot find `flake.nix`:
+
+```elisp
+(load "/path/to/telomare/emacs-telomare-mode/telomare-mode-spacemacs.el")
+```
+
+For Doom and vanilla Emacs setup, see
+[`emacs-telomare-mode/README.md`](emacs-telomare-mode/README.md).
+
+### Keybindings
+
+The mode binds only features the server implements. Some entries below
+come from `lsp-mode` rather than Telomare's mode — these are marked
+*(lsp-mode)*. Spacemacs exposes the major-mode leader as `SPC m` in Evil
+state and as `M-m m` in holy-mode; the leader entries are otherwise the
+same bindings.
+
+**Spacemacs — Evil mode** (`SPC m` major-mode leader):
+
+| Key | Action |
+|-----|--------|
+| `SPC m g` | Go to definition |
+| `SPC m G` | Find references |
+| `SPC m a` | Execute code action (partial evaluation) |
+| `SPC m v` | Show Telomare LSP version |
+| `C-c C-v` | Show Telomare LSP version |
+| `g d` | Go to definition *(lsp-mode / Evil default)* |
+
+**Spacemacs — holy mode** (`M-m m` major-mode leader):
+
+| Key | Action |
+|-----|--------|
+| `M-m m g` | Go to definition |
+| `M-m m G` | Find references |
+| `M-m m a` | Execute code action (partial evaluation) |
+| `M-m m v` | Show Telomare LSP version |
+| `C-c C-v` | Show Telomare LSP version |
+| `M-.` | Go to definition *(lsp-mode)* |
+| `M-?` | Find references *(lsp-mode)* |
+| `M-,` | Jump back *(xref)* |
+
+Vanilla Emacs binds `M-.`, `M-?`, `C-c a`, and `C-c C-v`.
+
+### Troubleshooting
+
+If navigation does not work, check the active LSP session with
+`M-x lsp-describe-session`, restart it with `M-x lsp-workspace-restart`, and
+confirm the server command with:
+
+```elisp
+M-: (telomare--lsp-command)
+```
+
+The expected command shape is:
+
+```elisp
+("nix" "run" "path:/nix/store/...-source#lsp" "--")
+```
+
+### LSP version command
+
+`C-c C-v` (or `SPC m v` / `M-m m v` in Spacemacs) reports the server
+version as a UTC timestamp truncated to minutes, using the parent commit
+timestamp when git history is available and the flake source timestamp
+when launched from a Nix store source without `.git`. It can also be
+invoked directly:
+
+```elisp
+(lsp-request "workspace/executeCommand"
+             `(:command "telomare.version" :arguments []))
+```
+
+The command shows an editor message such as:
+
+```text
+Telomare LSP version: 2026-05-22T10:14Z
+```
+
 ## Git Hooks
 
 You can setup your git configuration to automatically format and look for lint suggestions. Just run:
diff --git a/app/LSP.hs b/app/LSP.hs
index 8771b62a..554f36f6 100644
--- a/app/LSP.hs
+++ b/app/LSP.hs
@@ -1,22 +1,35 @@
 {-# LANGUAGE DataKinds           #-}
 {-# LANGUAGE FlexibleContexts    #-}
 {-# LANGUAGE KindSignatures      #-}
+{-# LANGUAGE LambdaCase          #-}
 {-# LANGUAGE OverloadedStrings   #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators       #-}
 
 module Main where
 
+import Control.Applicative ((<|>))
+import Control.Comonad.Cofree (Cofree ((:<)))
 import Control.Concurrent.STM
 import Control.Exception (IOException, try)
-import Control.Monad (forM, void)
+import Control.Monad (join, void)
 import Control.Monad.IO.Class (MonadIO (liftIO))
+import Data.Bifunctor (first)
 import Data.Char (isAsciiLower, isAsciiUpper, isDigit)
-import Data.Either (isRight)
-import Data.List (sortOn)
+import Data.List (find, sortOn)
+import qualified Data.List.NonEmpty as NE
 import qualified Data.Map.Strict as Map
+import Data.Maybe (fromMaybe, listToMaybe, mapMaybe)
+import qualified Data.Set as Set
 import qualified Data.Text as T
-import System.FilePath ((</>))
+import Data.Time (defaultTimeLocale, formatTime, parseTimeM, zonedTimeToUTC)
+import Data.Time.LocalTime (ZonedTime)
+import Data.Void (Void)
+import System.Directory (doesFileExist, makeAbsolute)
+import System.Environment (lookupEnv)
+import System.Exit (ExitCode (..))
+import System.FilePath (takeDirectory, (<.>), (</>))
+import System.Process (readProcessWithExitCode)
 
 import Control.Lens ((^.))
 import qualified Data.Aeson as JSON
@@ -24,13 +37,20 @@ import qualified Language.LSP.Protocol.Lens as LSP
 import Language.LSP.Protocol.Message (SMethod (..))
 import qualified Language.LSP.Protocol.Message as LSPMsg
 import Language.LSP.Protocol.Types (NormalizedUri, Position (..), Range (..),
-                                    UInt, toNormalizedUri, type (|?))
+                                    UInt, toNormalizedUri)
 import qualified Language.LSP.Protocol.Types as LSPTypes
 import Language.LSP.Server
 
-import Telomare (IExpr)
+import Telomare (LocTag (..), Pattern (..), ResolverError (..),
+                 SourcePosition (..), SourceSpan (..),
+                 UnprocessedParsedTermF (..), letBindingName, letBindingValue,
+                 locStartLineColumn, locatedNameLoc, locatedNameText,
+                 renderResolverError)
 import Telomare.Eval (eval2IExpr)
-import Telomare.Parser (AnnotatedUPT, parseModule)
+import Telomare.Parser (AnnotatedUPT, parseModule, parseModuleDetailed)
+import Telomare.Resolver (main2Term3)
+import Text.Megaparsec.Error (ParseErrorBundle (..), errorBundlePretty,
+                              errorOffset)
 
 --------------------------------------------------------------------------------
 -- Document state tracking
@@ -43,13 +63,19 @@ type ParseResult = [Either AnnotatedUPT (String, AnnotatedUPT)]
 type ModuleBindings = [(String, ParseResult)]
 
 data DocState = DocState
-  { docText    :: T.Text
-  , docVersion :: Int
-  , docParse   :: Either String ParseResult
+  { docText        :: T.Text
+  , docVersion     :: Int
+  , docParse       :: Either String ParseResult
+  , docDiagnostics :: [LSPTypes.Diagnostic]
   } deriving (Show)
 
 type DocStore = TVar (Map.Map NormalizedUri DocState)
 
+data SymbolIndex = SymbolIndex
+  { symbolDefinitions :: Map.Map T.Text LSPTypes.Location
+  , symbolReferences  :: Map.Map T.Text [Range]
+  } deriving (Eq, Show)
+
 -- Global state for prelude and other module bindings
 data GlobalState = GlobalState
   { docStore       :: DocStore
@@ -124,7 +150,9 @@ serverOptions =
           (Just False)                              -- willSaveWaitUntil
           Nothing                                   -- save
   in defaultOptions { optTextDocumentSync = Just syncOpts
-                    , optExecuteCommandCommands = Just ["telomare.partialEval"]
+                    , optExecuteCommandCommands = Just [ "telomare.partialEval"
+                                                       , "telomare.version"
+                                                       ]
                     }
 
 -- Token type indices (matching the server's reported legend)
@@ -144,11 +172,13 @@ tokType     = 7    -- "type"
 handlers :: GlobalState -> Handlers (LspM ())
 handlers gState = mconcat
   [ notificationHandler SMethod_Initialized                   $ \_ -> pure ()
-  , notificationHandler SMethod_TextDocumentDidOpen           $ didOpenHandler (docStore gState)
-  , notificationHandler SMethod_TextDocumentDidChange         $ didChangeHandler (docStore gState)
+  , notificationHandler SMethod_TextDocumentDidOpen           $ didOpenHandler gState
+  , notificationHandler SMethod_TextDocumentDidChange         $ didChangeHandler gState
   , notificationHandler SMethod_TextDocumentDidClose          $ didCloseHandler (docStore gState)
   , requestHandler     SMethod_TextDocumentSemanticTokensFull  $ semanticTokensFullHandler (docStore gState)
   , requestHandler     SMethod_TextDocumentSemanticTokensRange $ semanticTokensRangeHandler (docStore gState)
+  , requestHandler     SMethod_TextDocumentDefinition          $ definitionHandler gState
+  , requestHandler     SMethod_TextDocumentReferences          $ referencesHandler (docStore gState)
   , requestHandler     SMethod_TextDocumentCodeAction          $ codeActionHandler gState
   , requestHandler     SMethod_CodeActionResolve               $ codeActionResolveHandler gState
   ]
@@ -185,42 +215,88 @@ executeCommandHandler gState req respond = do
               respond . Right $ LSPTypes.InL JSON.Null
             _ -> respond . Right $ LSPTypes.InL JSON.Null
         _ -> respond . Right $ LSPTypes.InL JSON.Null
+    "telomare.version" -> do
+      version <- liftIO lspVersion
+      sendNotification SMethod_WindowShowMessage $
+        LSPTypes.ShowMessageParams
+          LSPTypes.MessageType_Info
+          ("Telomare LSP version: " <> version)
+      respond . Right . LSPTypes.InL . JSON.String $ version
     _ -> respond . Right $ LSPTypes.InL JSON.Null
 
+lspVersion :: IO T.Text
+lspVersion = do
+  parentTimestamp <- gitParentCommitTimestamp
+  case parentTimestamp of
+    Just timestamp -> pure timestamp
+    Nothing -> do
+      envVersion <- lookupEnv "TELOMARE_LSP_VERSION"
+      pure . maybe "unknown" T.pack $ envVersion
+
+gitParentCommitTimestamp :: IO (Maybe T.Text)
+gitParentCommitTimestamp = do
+  result <- try (readProcessWithExitCode "git" ["log", "-1", "--format=%cI", "HEAD^"] "") :: IO (Either IOException (ExitCode, String, String))
+  pure $ case result of
+    Right (ExitSuccess, stdout, _) -> formatTimestampMinutesUTC stdout
+    _                              -> Nothing
+
+formatTimestampMinutesUTC :: String -> Maybe T.Text
+formatTimestampMinutesUTC rawTimestamp = do
+  zonedTime <- parseTimeM True defaultTimeLocale "%Y-%m-%dT%H:%M:%S%Q%z" (takeWhile (/= '\n') rawTimestamp) :: Maybe ZonedTime
+  pure . T.pack $ formatTime defaultTimeLocale "%Y-%m-%dT%H:%MZ" (zonedTimeToUTC zonedTime)
+
 --------------------------------------------------------------------------------
 -- Helpers: centralize parsing through parseModule
 
 parseTelomareModule :: T.Text -> Either String ParseResult
 parseTelomareModule = parseModule . T.unpack
 
+parseTelomareModuleDetailed :: T.Text -> Either (ParseErrorBundle String Void) ParseResult
+parseTelomareModuleDetailed = parseModuleDetailed . T.unpack
+
 storeParsedDoc
-  :: DocStore
+  :: GlobalState
   -> LSPTypes.Uri
   -> Int
   -> T.Text
   -> LspM () ()
-storeParsedDoc docStore' uri version text = do
-  let parseRes = parseTelomareModule text
-  liftIO . atomically . modifyTVar' docStore' $
-    Map.insert (toNormalizedUri uri) (DocState text version parseRes)
+storeParsedDoc gState uri version text = do
+  modules <- liftIO $ readTVarIO (moduleBindings gState)
+  let detailedParse = parseTelomareModuleDetailed text
+      parseRes = first errorBundlePretty detailedParse
+  diagnostics' <- case detailedParse of
+    Left err -> pure $ parseDiagnostics text err
+    Right parsed -> do
+      importedModules <- liftIO $ concat <$> mapM (loadImportedModuleBinding gState uri) (moduleImports parsed)
+      let modules' = importedModules <> modules
+          importDiagnostics' = importDiagnostics text modules' parsed
+          semanticDiagnostics = undefinedVariableDiagnostics modules' parsed
+      pure . dedupeDiagnostics $ importDiagnostics'
+          <> semanticDiagnostics
+          <> if null importDiagnostics'
+             then resolverDiagnostics modules' parsed
+             else []
+  liftIO . atomically . modifyTVar' (docStore gState) $
+    Map.insert (toNormalizedUri uri) (DocState text version parseRes diagnostics')
+  publishDocumentDiagnostics uri version diagnostics'
 
 --------------------------------------------------------------------------------
 -- Document lifecycle handlers
 
-didOpenHandler :: DocStore
+didOpenHandler :: GlobalState
                -> LSPMsg.TNotificationMessage 'LSPMsg.Method_TextDocumentDidOpen
                -> LspM () ()
-didOpenHandler docStore' notification = do
+didOpenHandler gState notification = do
   let doc     = notification ^. LSP.params . LSP.textDocument
       uri     = doc ^. LSP.uri
       version = fromIntegral (doc ^. LSP.version)
       text    = doc ^. LSP.text
-  storeParsedDoc docStore' uri version text
+  storeParsedDoc gState uri version text
 
-didChangeHandler :: DocStore
-                 -> LSPMsg.TNotificationMessage 'LSPMsg.Method_TextDocumentDidChange
-                 -> LspM () ()
-didChangeHandler docStore' notification = do
+didChangeHandler :: GlobalState
+                  -> LSPMsg.TNotificationMessage 'LSPMsg.Method_TextDocumentDidChange
+                  -> LspM () ()
+didChangeHandler gState notification = do
   let doc     = notification ^. LSP.params . LSP.textDocument
       uri     = doc ^. LSP.uri
       version = fromIntegral (doc ^. LSP.version)
@@ -230,9 +306,9 @@ didChangeHandler docStore' notification = do
     (LSPTypes.TextDocumentContentChangeEvent changeData : _) -> do
       -- Extract text from union (partial vs whole)
       let newText = case changeData of
-                      LSPTypes.InL partial -> partial ^. LSP.text
-                      LSPTypes.InR whole   -> whole   ^. LSP.text
-      storeParsedDoc docStore' uri version newText
+            LSPTypes.InL partial -> partial ^. LSP.text
+            LSPTypes.InR whole   -> whole   ^. LSP.text
+      storeParsedDoc gState uri version newText
 
 didCloseHandler :: DocStore
                 -> LSPMsg.TNotificationMessage 'LSPMsg.Method_TextDocumentDidClose
@@ -240,10 +316,506 @@ didCloseHandler :: DocStore
 didCloseHandler docStore' notification = do
   let uri = notification ^. LSP.params . LSP.textDocument . LSP.uri
   liftIO . atomically . modifyTVar' docStore' $ Map.delete (toNormalizedUri uri)
+  publishDocumentDiagnostics uri 0 []
+
+publishDocumentDiagnostics :: LSPTypes.Uri -> Int -> [LSPTypes.Diagnostic] -> LspM () ()
+publishDocumentDiagnostics uri version diagnostics =
+  sendNotification SMethod_TextDocumentPublishDiagnostics $
+    LSPTypes.PublishDiagnosticsParams uri (Just $ fromIntegral version) diagnostics
+
+parseDiagnostics :: T.Text -> ParseErrorBundle String Void -> [LSPTypes.Diagnostic]
+parseDiagnostics text bundle =
+  [ mkDiagnostic (offsetToRange text . errorOffset . NE.head $ bundleErrors bundle)
+      "parser"
+      (T.pack $ errorBundlePretty bundle)
+  ]
+
+loadImportedModuleBinding :: GlobalState -> LSPTypes.Uri -> ModuleImport -> IO ModuleBindings
+loadImportedModuleBinding gState currentUri moduleImport = do
+  mModule <- loadImportedModule gState currentUri (importModuleName moduleImport)
+  pure $ case mModule of
+    Nothing             -> []
+    Just (_, _, parsed) -> [(importModuleName moduleImport, parsed)]
+
+importDiagnostics :: T.Text -> ModuleBindings -> ParseResult -> [LSPTypes.Diagnostic]
+importDiagnostics text modules parsed =
+  [ mkDiagnostic (moduleImportRange text moduleImport) "resolver" $
+      T.pack ("module not found " <> show (importModuleName moduleImport))
+  | moduleImport <- moduleImports parsed
+  , importModuleName moduleImport `notElem` (fst <$> modules)
+  ]
+
+moduleImportRange :: T.Text -> ModuleImport -> Range
+moduleImportRange text moduleImport =
+  let moduleName = T.pack $ importModuleName moduleImport
+      importLines = zip [0..] $ T.lines text
+  in fromMaybe fallbackRange $ listToMaybe
+       [ textRange line column (T.length moduleName)
+       | (line, lineText) <- importLines
+       , "import" `T.isPrefixOf` T.stripStart lineText
+       , Just column <- [findIdentifierColumn moduleName lineText]
+       ]
+
+findIdentifierColumn :: T.Text -> T.Text -> Maybe Int
+findIdentifierColumn name lineText = go 0 lineText
+  where
+    go column remaining
+      | T.null remaining = Nothing
+      | T.isPrefixOf name remaining && beforeBoundary column && afterBoundary remaining = Just column
+      | otherwise = go (column + 1) (T.tail remaining)
+    beforeBoundary column =
+      column == 0 || not (lspIdentChar . T.last $ T.take column lineText)
+    afterBoundary remaining =
+      let afterName = T.drop (T.length name) remaining
+      in T.null afterName || not (lspIdentChar $ T.head afterName)
+
+undefinedVariableDiagnostics :: ModuleBindings -> ParseResult -> [LSPTypes.Diagnostic]
+undefinedVariableDiagnostics modules parsed =
+  dedupeDiagnostics
+    [ mkDiagnostic range "resolver" $ T.pack ("missing definition " <> show name)
+    | (name, range) <- unresolvedReferences globals parsed
+    ]
+  where
+    globals = Set.fromList $ builtinNames <> importedDefinitionNames modules parsed <> currentDefinitionNames parsed
+
+builtinNames :: [String]
+builtinNames = ["zero", "left", "right", "trace", "pair", "app"]
+
+importedDefinitionNames :: ModuleBindings -> ParseResult -> [String]
+importedDefinitionNames modules parsed =
+  [ maybe name (<> ('.' : name)) (importQualifier moduleImport)
+  | moduleImport <- moduleImports parsed
+  , Just moduleParsed <- [lookup (importModuleName moduleImport) modules]
+  , Right (name, _) <- moduleParsed
+  ]
+
+currentDefinitionNames :: ParseResult -> [String]
+currentDefinitionNames parsed = [name | Right (name, _) <- parsed]
+
+unresolvedReferences :: Set.Set String -> ParseResult -> [(String, Range)]
+unresolvedReferences globals parsed =
+  concatMap (unresolvedTerm globals) [term | Right (_, term) <- parsed]
+
+unresolvedTerm :: Set.Set String -> AnnotatedUPT -> [(String, Range)]
+unresolvedTerm globals = go Set.empty
+  where
+    go bound (loc :< term) = case term of
+      VarUPF name
+        | name `Set.member` bound || name `Set.member` globals -> []
+        | otherwise -> [(name, locTagToRange loc)]
+      LetUPF bindings body ->
+        let localNames = Set.fromList $ letBindingName <$> bindings
+            bound' = localNames <> bound
+        in concatMap (go bound' . letBindingValue) bindings <> go bound' body
+      LamUPF name body -> go (Set.insert (locatedNameText name) bound) body
+      UDTUPF names body -> go (Set.union (Set.fromList names) bound) body
+      CaseUPF scrutinee cases ->
+        go bound scrutinee <> concatMap (caseRefs bound) cases
+      ITEUPF i t e -> concatMap (go bound) [i, t, e]
+      ListUPF items -> concatMap (go bound) items
+      PairUPF a b -> concatMap (go bound) [a, b]
+      AppUPF f x -> concatMap (go bound) [f, x]
+      LeftUPF x -> go bound x
+      RightUPF x -> go bound x
+      TraceUPF x -> go bound x
+      CheckUPF checkExpr body -> go bound checkExpr <> go bound body
+      HashUPF x -> go bound x
+      UnsizedRecursionUPF t r b -> concatMap (go bound) [t, r, b]
+      _ -> []
+
+    caseRefs bound (pat, body) =
+      go (Set.union (Set.fromList $ patternBoundNames pat) bound) body
+
+dedupeDiagnostics :: [LSPTypes.Diagnostic] -> [LSPTypes.Diagnostic]
+dedupeDiagnostics = Map.elems . Map.fromList . fmap (\diagnostic -> (diagnosticKey diagnostic, diagnostic))
+
+diagnosticKey :: LSPTypes.Diagnostic -> (Range, Maybe T.Text, T.Text)
+diagnosticKey diagnostic =
+  (diagnostic ^. LSP.range, diagnostic ^. LSP.source, diagnostic ^. LSP.message)
+
+resolverDiagnostics :: ModuleBindings -> ParseResult -> [LSPTypes.Diagnostic]
+resolverDiagnostics modules parsed =
+  case main2Term3 (("Current", parsed) : modules) "Current" of
+    Left NoMainFunction{} -> []
+    Left err              -> resolverErrorDiagnostics err
+    Right _               -> []
+
+resolverErrorDiagnostics :: ResolverError -> [LSPTypes.Diagnostic]
+resolverErrorDiagnostics err =
+  case err of
+    MissingDefinitionAt loc _ ->
+      [mkDiagnostic (locTagToRange loc) "resolver" (T.pack $ renderResolverError err)]
+    _ ->
+      [mkDiagnostic fallbackRange "resolver" (T.pack $ renderResolverError err)]
+
+mkDiagnostic :: Range -> T.Text -> T.Text -> LSPTypes.Diagnostic
+mkDiagnostic range source message =
+  LSPTypes.Diagnostic
+    range
+    (Just LSPTypes.DiagnosticSeverity_Error)
+    Nothing
+    Nothing
+    (Just source)
+    message
+    Nothing
+    Nothing
+    Nothing
+
+locTagToRange :: LocTag -> Range
+locTagToRange loc = case loc of
+  SourceLoc sourceSpan -> sourceSpanToRange sourceSpan
+  _                    -> locTagStartToRange loc
+
+locTagStartToRange :: LocTag -> Range
+locTagStartToRange loc = case locStartLineColumn loc of
+  Just (line, column) -> pointRange (line - 1) (column - 1)
+  Nothing             -> fallbackRange
+
+sourceSpanToRange :: SourceSpan -> Range
+sourceSpanToRange sourceSpan =
+  Range
+    (sourcePositionToLSP $ sourceSpanStart sourceSpan)
+    (sourcePositionToLSP $ sourceSpanEnd sourceSpan)
+
+sourcePositionToLSP :: SourcePosition -> Position
+sourcePositionToLSP pos =
+  Position
+    (fromIntegral . max 0 $ sourcePositionLine pos - 1)
+    (fromIntegral . max 0 $ sourcePositionColumn pos - 1)
+
+offsetToRange :: T.Text -> Int -> Range
+offsetToRange text offset =
+  let prefix = T.take offset text
+      line = T.count "\n" prefix
+      column = T.length . last $ T.splitOn "\n" prefix
+  in pointRange line column
+
+pointRange :: Int -> Int -> Range
+pointRange line column =
+  let line' = max 0 line
+      column' = max 0 column
+  in Range (Position (fromIntegral line') (fromIntegral column'))
+           (Position (fromIntegral line') (fromIntegral $ column' + 1))
+
+fallbackRange :: Range
+fallbackRange = pointRange 0 0
+
+diagnosticFirstLine :: String -> String
+diagnosticFirstLine = takeWhile (/= '\n')
+
+definitionHandler :: GlobalState
+                  -> LSPMsg.TRequestMessage LSPMsg.Method_TextDocumentDefinition
+                  -> (Either (LSPMsg.TResponseError LSPMsg.Method_TextDocumentDefinition)
+                            (LSPTypes.Definition LSPTypes.|? ([LSPTypes.DefinitionLink] LSPTypes.|? LSPTypes.Null))
+                       -> LspM () ())
+                  -> LspM () ()
+definitionHandler gState req respond = do
+  let uri = req ^. LSP.params . LSP.textDocument . LSP.uri
+      position = req ^. LSP.params . LSP.position
+  mDoc <- liftIO . atomically $ Map.lookup (toNormalizedUri uri) <$> readTVar (docStore gState)
+  mDefinition <- liftIO $ maybe (pure Nothing) (definitionAt gState uri position) mDoc
+  case mDefinition of
+    Just location -> respond . Right . LSPTypes.InL . LSPTypes.Definition . LSPTypes.InL $ location
+    Nothing       -> respond . Right . LSPTypes.InR . LSPTypes.InR $ LSPTypes.Null
+
+referencesHandler :: DocStore
+                  -> LSPMsg.TRequestMessage LSPMsg.Method_TextDocumentReferences
+                  -> (Either (LSPMsg.TResponseError LSPMsg.Method_TextDocumentReferences)
+                           ([LSPTypes.Location] LSPTypes.|? LSPTypes.Null)
+                      -> LspM () ())
+                  -> LspM () ()
+referencesHandler docStore' req respond = do
+  let uri = req ^. LSP.params . LSP.textDocument . LSP.uri
+      position = req ^. LSP.params . LSP.position
+      includeDeclaration = req ^. LSP.params . LSP.context . LSP.includeDeclaration
+  mDoc <- liftIO . atomically $ Map.lookup (toNormalizedUri uri) <$> readTVar docStore'
+  let locations = foldMap (referencesAt uri includeDeclaration position) mDoc
+  case locations of
+    [] -> respond . Right $ LSPTypes.InR LSPTypes.Null
+    _  -> respond . Right . LSPTypes.InL $ locations
+
+--------------------------------------------------------------------------------
+-- Source index for definition/reference requests
+
+definitionAt :: GlobalState -> LSPTypes.Uri -> Position -> DocState -> IO (Maybe LSPTypes.Location)
+definitionAt gState uri position docState = case docParse docState of
+  Left _ -> pure Nothing
+  Right parsed -> do
+    importedDefinitions <- importedDefinitionIndex gState uri parsed
+    let currentIndex = buildSymbolIndex uri (docText docState) parsed
+        definitions = symbolDefinitions currentIndex <> importedDefinitions
+    pure $ do
+      localDefinitionAt uri position parsed <|> do
+        symbol <- symbolAtPosition position currentIndex
+        Map.lookup symbol definitions
+
+referencesAt :: LSPTypes.Uri -> Bool -> Position -> DocState -> [LSPTypes.Location]
+referencesAt uri includeDeclaration position docState =
+  case docParse docState of
+    Left _ -> []
+    Right parsed ->
+      let index = buildSymbolIndex uri (docText docState) parsed
+          symbol = symbolAtPosition position index
+      in case symbol of
+        Nothing -> []
+        Just name ->
+          let refs = Map.findWithDefault [] name (symbolReferences index)
+              defs = foldMap (pure . locationRange) $ Map.lookup name (symbolDefinitions index)
+              ranges = if includeDeclaration then defs <> refs else refs
+          in LSPTypes.Location uri <$> ranges
+
+importedDefinitionIndex :: GlobalState -> LSPTypes.Uri -> ParseResult -> IO (Map.Map T.Text LSPTypes.Location)
+importedDefinitionIndex gState currentUri parsed = do
+  imports <- mapM (loadImportedDefinitionIndex gState currentUri) $ moduleImports parsed
+  pure . Map.unions $ imports
+
+loadImportedDefinitionIndex :: GlobalState -> LSPTypes.Uri -> ModuleImport -> IO (Map.Map T.Text LSPTypes.Location)
+loadImportedDefinitionIndex gState currentUri moduleImport = do
+  mModule <- loadImportedModule gState currentUri (importModuleName moduleImport)
+  case mModule of
+    Nothing -> pure Map.empty
+    Just (moduleUri, moduleText, moduleParsed) -> do
+      let definitions = symbolDefinitions $ buildSymbolIndex moduleUri moduleText moduleParsed
+      pure $ qualifyDefinitions moduleImport definitions
+
+qualifyDefinitions :: ModuleImport -> Map.Map T.Text LSPTypes.Location -> Map.Map T.Text LSPTypes.Location
+qualifyDefinitions moduleImport definitions = case importQualifier moduleImport of
+  Nothing        -> definitions
+  Just qualifier -> Map.mapKeys ((T.pack qualifier <> ".") <>) definitions
+
+data ModuleImport = ModuleImport
+  { importModuleName :: String
+  , importQualifier  :: Maybe String
+  } deriving (Eq, Show)
+
+moduleImports :: ParseResult -> [ModuleImport]
+moduleImports = mapMaybe $ \case
+  Left (_ :< ImportUPF moduleName) ->
+    Just $ ModuleImport moduleName Nothing
+  Left (_ :< ImportQualifiedUPF qualifier moduleName) ->
+    Just $ ModuleImport moduleName (Just qualifier)
+  _ -> Nothing
+
+loadImportedModule :: GlobalState -> LSPTypes.Uri -> String -> IO (Maybe (LSPTypes.Uri, T.Text, ParseResult))
+loadImportedModule gState currentUri moduleName = do
+  candidates <- moduleFileCandidates currentUri moduleName
+  mPath <- firstExistingFile candidates
+  case mPath of
+    Nothing -> pure Nothing
+    Just path -> do
+      absolutePath <- makeAbsolute path
+      let moduleUri = LSPTypes.filePathToUri absolutePath
+      openDocs <- readTVarIO $ docStore gState
+      case Map.lookup (toNormalizedUri moduleUri) openDocs of
+        Just docState | Right parsed <- docParse docState ->
+          pure $ Just (moduleUri, docText docState, parsed)
+        _ -> do
+          loaded <- try (readFile absolutePath) :: IO (Either IOException String)
+          pure $ case loaded of
+            Left _ -> Nothing
+            Right content -> case parseTelomareModule (T.pack content) of
+              Left _       -> Nothing
+              Right parsed -> Just (moduleUri, T.pack content, parsed)
+
+moduleFileCandidates :: LSPTypes.Uri -> String -> IO [FilePath]
+moduleFileCandidates currentUri moduleName = do
+  cwdModule <- makeAbsolute moduleFile
+  pure $ maybe [cwdModule, "lib" </> moduleFile]
+               (\currentPath -> [takeDirectory currentPath </> moduleFile, cwdModule, "lib" </> moduleFile])
+               (LSPTypes.uriToFilePath currentUri)
+  where
+    moduleFile = moduleName <.> "tel"
+
+firstExistingFile :: [FilePath] -> IO (Maybe FilePath)
+firstExistingFile [] = pure Nothing
+firstExistingFile (path:paths) = do
+  exists <- doesFileExist path
+  if exists
+    then pure $ Just path
+    else firstExistingFile paths
+
+locationRange :: LSPTypes.Location -> Range
+locationRange (LSPTypes.Location _ range) = range
+
+symbolAtPosition :: Position -> SymbolIndex -> Maybe T.Text
+symbolAtPosition position index =
+  locatedDefinition <|> locatedReference
+  where
+    locatedDefinition = fst <$> find (positionInRange position . locationRange . snd) (Map.toList $ symbolDefinitions index)
+    locatedReference = fst <$> find (any (positionInRange position) . snd) (Map.toList $ symbolReferences index)
+
+buildSymbolIndex :: LSPTypes.Uri -> T.Text -> ParseResult -> SymbolIndex
+buildSymbolIndex uri text parsed = SymbolIndex definitions references
+  where
+    definitions = topLevelDefinitions uri text parsed
+    references = Map.fromListWith (<>)
+      [ (T.pack name, [range])
+      | Right (_, term) <- parsed
+      , (name, range) <- termReferences [] term
+      ]
+
+topLevelDefinitions :: LSPTypes.Uri -> T.Text -> ParseResult -> Map.Map T.Text LSPTypes.Location
+topLevelDefinitions uri text parsed = Map.fromList
+  [ (T.pack name, LSPTypes.Location uri range)
+  | Right (name, _) <- parsed
+  , Just range <- [findTopLevelDefinition text (T.pack name)]
+  ]
+
+findTopLevelDefinition :: T.Text -> T.Text -> Maybe Range
+findTopLevelDefinition text name =
+  let indexedLines = zip [0..] $ T.lines text
+      matchingLines =
+        [ textRange line column (T.length name)
+        | (line, lineText) <- indexedLines
+        , Just column <- [findTopLevelIdentifier name lineText]
+        ]
+  in listToMaybe matchingLines
+
+findTopLevelIdentifier :: T.Text -> T.Text -> Maybe Int
+findTopLevelIdentifier name lineText
+  | not (isTopLevelLine lineText) = Nothing
+  | T.isInfixOf "=" lineText = findIdentifierInLhs name lineText
+  | T.stripEnd lineText == name = Just 0
+  | otherwise = Nothing
+
+isTopLevelLine :: T.Text -> Bool
+isTopLevelLine lineText =
+  not (T.null lineText)
+    && notElem (T.head lineText) [' ', '\t']
+    && not ("--" `T.isPrefixOf` lineText)
+
+findIdentifierInLhs :: T.Text -> T.Text -> Maybe Int
+findIdentifierInLhs name lineText = go 0 lhs
+  where
+    lhs = T.takeWhile (/= '=') lineText
+    go column remaining
+      | T.null remaining = Nothing
+      | T.isPrefixOf name remaining && beforeBoundary column && afterBoundary remaining = Just column
+      | otherwise = go (column + 1) (T.tail remaining)
+    beforeBoundary column =
+      column == 0 || not (lspIdentChar . T.last $ T.take column lhs)
+    afterBoundary remaining =
+      let afterName = T.drop (T.length name) remaining
+      in T.null afterName || not (lspIdentChar $ T.head afterName)
+
+termReferences :: [String] -> AnnotatedUPT -> [(String, Range)]
+termReferences bound (loc :< term) =
+  let children = case term of
+        VarUPF name
+          | name `elem` bound -> []
+          | otherwise         -> [(name, locTagToRange loc)]
+        ITEUPF i t e -> termReferences bound i <> termReferences bound t <> termReferences bound e
+        LetUPF bindings body ->
+          let localNames = letBindingName <$> bindings
+              bound' = localNames <> bound
+          in concatMap (termReferences bound' . letBindingValue) bindings <> termReferences bound' body
+        ListUPF items -> concatMap (termReferences bound) items
+        PairUPF a b -> termReferences bound a <> termReferences bound b
+        AppUPF f x -> termReferences bound f <> termReferences bound x
+        LamUPF var body -> termReferences (locatedNameText var : bound) body
+        LeftUPF x -> termReferences bound x
+        RightUPF x -> termReferences bound x
+        TraceUPF x -> termReferences bound x
+        CheckUPF checkExpr body -> termReferences bound checkExpr <> termReferences bound body
+        HashUPF x -> termReferences bound x
+        UDTUPF names body -> termReferences (names <> bound) body
+        CaseUPF scrutinee cases -> termReferences bound scrutinee <> concatMap caseReferences cases
+        _ -> []
+  in children
+  where
+    caseReferences (pat, body) = termReferences (patternBoundNames pat <> bound) body
+
+localDefinitionAt :: LSPTypes.Uri -> Position -> ParseResult -> Maybe LSPTypes.Location
+localDefinitionAt uri position parsed =
+  listToMaybe [ location
+              | Right (_, term) <- parsed
+              , location <- foldMap pure $ localTermDefinitionAt uri position Map.empty term
+              ]
+
+localTermDefinitionAt :: LSPTypes.Uri
+                      -> Position
+                      -> Map.Map String (Maybe LSPTypes.Location)
+                      -> AnnotatedUPT
+                      -> Maybe LSPTypes.Location
+localTermDefinitionAt uri position env (loc :< term) = case term of
+  VarUPF name
+    | positionInRange position (locTagToRange loc) -> join $ Map.lookup name env
+    | otherwise -> Nothing
+  LetUPF bindings body ->
+    let bindingLocations = Map.fromList
+          [ (locatedNameText name, Just $ LSPTypes.Location uri (locTagToRange $ locatedNameLoc name))
+          | (name, _) <- bindings
+          ]
+        env' = bindingLocations <> env
+        bindingDefinition = listToMaybe
+          [ LSPTypes.Location uri (locTagToRange $ locatedNameLoc name)
+          | (name, _) <- bindings
+          , positionInRange position (locTagToRange $ locatedNameLoc name)
+          ]
+        bindingRefs = listToMaybe
+          [ location
+          | binding <- bindings
+          , location <- foldMap pure $ localTermDefinitionAt uri position env' (letBindingValue binding)
+          ]
+    in bindingDefinition <|> bindingRefs <|> localTermDefinitionAt uri position env' body
+  ITEUPF i t e -> firstJust [i, t, e]
+  ListUPF items -> firstJust items
+  PairUPF a b -> firstJust [a, b]
+  AppUPF f x -> firstJust [f, x]
+  LamUPF name body ->
+    let nameLoc = locatedNameLoc name
+        location = LSPTypes.Location uri (locTagToRange nameLoc)
+        env' = Map.insert (locatedNameText name) (Just location) env
+    in if positionInRange position (locTagToRange nameLoc)
+         then Just location
+         else localTermDefinitionAt uri position env' body
+  LeftUPF x -> localTermDefinitionAt uri position env x
+  RightUPF x -> localTermDefinitionAt uri position env x
+  TraceUPF x -> localTermDefinitionAt uri position env x
+  CheckUPF checkExpr body -> firstJust [checkExpr, body]
+  HashUPF x -> localTermDefinitionAt uri position env x
+  UDTUPF names body -> localTermDefinitionAt uri position (foldr (`Map.insert` Nothing) env names) body
+  CaseUPF scrutinee cases ->
+    localTermDefinitionAt uri position env scrutinee
+      <|> listToMaybe [ location
+                      | (pat, caseBody) <- cases
+                      , let env' = foldr (`Map.insert` Nothing) env $ patternBoundNames pat
+                      , location <- foldMap pure $ localTermDefinitionAt uri position env' caseBody
+                      ]
+  _ -> Nothing
+  where
+    firstJust = listToMaybe . mapMaybe (localTermDefinitionAt uri position env)
+
+patternBoundNames :: Pattern -> [String]
+patternBoundNames = \case
+  PatternVar name -> [name]
+  PatternAnnotated pat _ -> patternBoundNames pat
+  PatternPair left right -> patternBoundNames left <> patternBoundNames right
+  _ -> []
+
+lspIdentChar :: Char -> Bool
+lspIdentChar c = isAsciiLower c || isAsciiUpper c || isDigit c || c == '_' || c == '.' || c == '\''
+
+textRange :: Int -> Int -> Int -> Range
+textRange line column len =
+  Range
+    (Position (fromIntegral line) (fromIntegral column))
+    (Position (fromIntegral line) (fromIntegral $ column + len))
+
+positionInRange :: Position -> Range -> Bool
+positionInRange (Position line char) (Range (Position startLine startChar) (Position endLine endChar)) =
+  (line > startLine || line == startLine && char >= startChar)
+    && (line < endLine || line == endLine && char < endChar)
 
 --------------------------------------------------------------------------------
 -- Semantic tokens (kept using the simple lexer for now)
 
+semanticTokensFullHandler :: DocStore
+                          -> LSPMsg.TRequestMessage LSPMsg.Method_TextDocumentSemanticTokensFull
+                          -> (Either (LSPMsg.TResponseError LSPMsg.Method_TextDocumentSemanticTokensFull)
+                                   (LSPTypes.SemanticTokens LSPTypes.|? LSPTypes.Null)
+                             -> LspM () ())
+                          -> LspM () ()
 semanticTokensFullHandler docStore' req respond = do
   let uri = req ^. LSP.params . LSP.textDocument . LSP.uri
   mDoc <- liftIO . atomically $ Map.lookup (toNormalizedUri uri) <$> readTVar docStore'
@@ -254,6 +826,12 @@ semanticTokensFullHandler docStore' req respond = do
           encoded = tokensToLSP tokens
       respond . Right . LSPTypes.InL $ LSPTypes.SemanticTokens Nothing encoded
 
+semanticTokensRangeHandler :: DocStore
+                           -> LSPMsg.TRequestMessage LSPMsg.Method_TextDocumentSemanticTokensRange
+                           -> (Either (LSPMsg.TResponseError LSPMsg.Method_TextDocumentSemanticTokensRange)
+                                    (LSPTypes.SemanticTokens LSPTypes.|? LSPTypes.Null)
+                              -> LspM () ())
+                           -> LspM () ()
 semanticTokensRangeHandler docStore' req respond = do
   let uri   = req ^. LSP.params . LSP.textDocument . LSP.uri
       range = req ^. LSP.params . LSP.range
@@ -277,15 +855,14 @@ codeActionHandler :: GlobalState
 codeActionHandler gState req respond = do
   let uri = req ^. LSP.params . LSP.textDocument . LSP.uri
       range = req ^. LSP.params . LSP.range
-      context = req ^. LSP.params . LSP.context
 
   mDoc <- liftIO . atomically $ Map.lookup (toNormalizedUri uri) <$> readTVar (docStore gState)
   case mDoc of
     Nothing -> respond . Right . LSPTypes.InL $ []
     Just docState -> do
       case docParse docState of
-        Left err -> respond . Right . LSPTypes.InL $ []
-        Right parsedDoc -> do
+        Left _ -> respond . Right . LSPTypes.InL $ []
+        Right _ -> do
           -- Get the selected text
           let text = docText docState
               selectedText = getTextInRange text range
@@ -322,7 +899,7 @@ codeActionResolveHandler :: GlobalState
                                   LSPTypes.CodeAction
                             -> LspM () ())
                          -> LspM () ()
-codeActionResolveHandler gState req respond = do
+codeActionResolveHandler _ req respond = do
   -- For now, just return the action as-is since we're using commands
   -- The request body should contain a CodeAction
   let codeAction = req ^. LSP.params
@@ -330,7 +907,7 @@ codeActionResolveHandler gState req respond = do
 
 -- Execute partial evaluation and show result
 executePartialEvaluation :: GlobalState -> LSPTypes.Uri -> Range -> T.Text -> LspM () ()
-executePartialEvaluation gState uri range exprText = do
+executePartialEvaluation gState _ _ exprText = do
   bindings <- liftIO $ readTVarIO (moduleBindings gState)
   let evaluationResult = evaluateExpression bindings exprText
       message = case evaluationResult of
diff --git a/app/Repl.hs b/app/Repl.hs
index ad8f7c55..86f1341c 100644
--- a/app/Repl.hs
+++ b/app/Repl.hs
@@ -90,7 +90,7 @@ resolveBinding' :: String
                 -> Maybe Term3
 resolveBinding' name bindings = lookup name taggedBindings >>= (rightToMaybe . process)
   where
-    taggedBindings = (fmap . fmap) (tag DummyLoc) bindings
+    taggedBindings = (fmap . fmap) (tag UnknownLoc) bindings
 
 -- |Obtain expression from the bindings and transform them maybe into a IExpr.
 resolveBinding :: String -> [(String, UnprocessedParsedTerm)] -> Maybe CompiledExpr
@@ -105,7 +105,7 @@ printLastExpr :: (IExpr -> Either RunTimeError IExpr) -- ^Telomare backend
               -> [(String, UnprocessedParsedTerm)]
               -> IO ()
 printLastExpr eval bindings = do
-  let bindings' = (fmap . fmap) (tag DummyLoc) bindings
+  let bindings' = (fmap . fmap) (tag UnknownLoc) bindings
   res :: Either Exception.SomeException () <- Exception.try $
     case lookup "_tmp_" bindings' of
       Nothing -> putStrLn "Could not find _tmp_ in bindings"
@@ -116,7 +116,7 @@ printLastExpr eval bindings = do
                            Right r  -> case toTelomare r of
                              Just te -> pure $ fromTelomare te
                              _ -> Left . RTE . ResultConversionError $ "conversion error from compiled expr:\n" <> prettyPrint r
-        case compile' =<< first RE (process (DummyLoc :< LetUPF bindings' upt)) of
+        case compile' =<< first RE (process (UnknownLoc :< LetUPF (first (locatedName UnknownLoc) <$> bindings') upt)) of
           Left err -> print err
           Right iexpr' -> case eval iexpr' of
               Left e      -> putStrLn $ "error: " <> show e
diff --git a/emacs-telomare-mode/README.md b/emacs-telomare-mode/README.md
index b8d1f75c..8be37d64 100644
--- a/emacs-telomare-mode/README.md
+++ b/emacs-telomare-mode/README.md
@@ -6,17 +6,21 @@ LSP-enabled major mode for the Telomare programming language, with support for D
 
 Based on the Telomare LSP server capabilities:
 - **Syntax highlighting** via semantic tokens (keywords, comments, strings, numbers, operators)
-- **Hover information** showing expression evaluation and parse errors
 - **Go to definition** and **Find references** (via LSP)
-- **Rename symbol** support
-- **Parse error reporting** displayed on hover
+- **Diagnostics** for parse errors, undefined variables, missing imports, and resolver errors
+- **Partial evaluation** code action for a selected expression
+- **LSP version command**
 - **Comment support** (`-- comments`)
 
+Hover and rename are not implemented by the server yet.
+
 ## Installation
 
 ### Prerequisites
 
-Ensure your Telomare LSP server is available at the configured path (default: `/home/hhefesto/src/telomare#lsp`).
+Ensure your Telomare LSP server is available. By default the mode runs it
+through the Telomare flake (`nix run path:<telomare-source>#lsp --`); see
+"Customizing the LSP Command" below to point it at a different path or binary.
 
 ### Modular Configuration (4 files)
 
@@ -68,23 +72,33 @@ Place all four files in a directory in your load-path. All variants require `tel
 
 ## Key Bindings
 
-### Doom Emacs
-- `SPC m g` - Go to definition TODO: improve
-- `SPC m G` - Find references  
-- TODO: `SPC m h` - Describe at point (hover)
-- TODO: `SPC m r` - Rename symbol
+The mode binds only features the Telomare LSP server implements; there is
+no hover or rename.
 
 ### Spacemacs
-- `SPC m g` - Go to definition TODO: improve
-- `SPC m G` - Find references
-- TODO: `SPC m h` - Describe at point (hover)
-- TODO: `SPC m r` - Rename symbol
+
+Major-mode leader bindings, reachable as `SPC m ...` in Evil state and
+`M-m m ...` in holy-mode:
+
+- `g` - Go to definition
+- `G` - Find references
+- `a` - Execute code action (partial evaluation)
+- `v` - Show Telomare LSP version
+
+Also `C-c C-v` - Show Telomare LSP version.
+
+### Doom Emacs
+
+`telomare-mode-doom.el` adds no bindings of its own; navigation relies on
+`lsp-mode`/Evil defaults such as `g d` (go to definition). The version
+command is available as `M-x telomare-lsp-version`.
 
 ### Vanilla Emacs
+
 - `M-.` - Go to definition
 - `M-?` - Find references
-- TODO: `C-c h` - Describe at point (hover)
-- TODO: `C-c r` - Rename symbol
+- `C-c a` - Execute code action (partial evaluation)
+- `C-c C-v` - Show Telomare LSP version
 
 ## Troubleshooting
 
diff --git a/emacs-telomare-mode/telomare-mode-common.el b/emacs-telomare-mode/telomare-mode-common.el
index 226d78ae..ab7ed3e7 100644
--- a/emacs-telomare-mode/telomare-mode-common.el
+++ b/emacs-telomare-mode/telomare-mode-common.el
@@ -34,6 +34,15 @@
 ;;;###autoload
 (add-to-list 'auto-mode-alist '("\\.tel\\'" . telomare-mode))
 
+(defun telomare-lsp-version ()
+  "Show the Telomare LSP version."
+  (interactive)
+  (unless (bound-and-true-p lsp-mode)
+    (user-error "LSP is not active in this buffer"))
+  (let ((version (lsp-request "workspace/executeCommand"
+                              `(:command "telomare.version" :arguments []))))
+    (message "Telomare LSP version: %s" version)))
+
 ;; Common LSP setup function
 (defun telomare-register-lsp-client ()
   "Register the Telomare LSP client."
diff --git a/emacs-telomare-mode/telomare-mode-spacemacs.el b/emacs-telomare-mode/telomare-mode-spacemacs.el
index 10146fdb..7c3eb624 100644
--- a/emacs-telomare-mode/telomare-mode-spacemacs.el
+++ b/emacs-telomare-mode/telomare-mode-spacemacs.el
@@ -6,15 +6,16 @@
 
 (defcustom telomare-project-root
   (or (getenv "TELOMARE_ROOT")
-      ;; If this file lives inside the repo, try to auto-detect the flake root:
+      ;; This normally resolves to the Nix flake input source when the mode is
+      ;; loaded from a NixOS/Home Manager generated Spacemacs config.
       (let* ((this (or load-file-name (buffer-file-name)))
              (dir  (and this (file-name-directory this)))
              (root (and dir (locate-dominating-file dir "flake.nix"))))
         (when root (expand-file-name root))))
-  "Path to the Telomare flake directory (the folder containing flake.nix).
+  "Path to the Telomare flake directory or Nix store flake input source.
 
-Users should set this to something like \"~/src/telomare\".
-You can also set TELOMARE_ROOT in your environment."
+NixOS/Home Manager installs should leave this auto-detected from the loaded
+mode file. TELOMARE_ROOT is only an override for non-Nix/manual setups."
   :type '(choice (const :tag "Auto-detect / unset" nil)
                  (directory :tag "Telomare flake directory"))
   :group 'telomare)
@@ -29,8 +30,8 @@ You can also set TELOMARE_ROOT in your environment."
   (unless (and telomare-project-root
                (file-exists-p (expand-file-name "flake.nix" telomare-project-root)))
     (user-error "telomare-project-root is not set (or has no flake.nix). Set it to your Telomare repo path"))
-  (let* ((root  (file-truename (expand-file-name telomare-project-root)))
-         (flake (format "%s#%s" root telomare-lsp-flake-attr)))
+  (let* ((root  (directory-file-name (file-truename (expand-file-name telomare-project-root))))
+         (flake (format "path:%s#%s" root telomare-lsp-flake-attr)))
     (list "nix" "run" flake "--")))
 
 ;; Define Telomare mode
@@ -39,6 +40,17 @@ You can also set TELOMARE_ROOT in your environment."
   (setq-local comment-start "-- ")
   (setq-local comment-end ""))
 
+(defun telomare-lsp-version ()
+  "Show the Telomare LSP version."
+  (interactive)
+  (unless (bound-and-true-p lsp-mode)
+    (user-error "LSP is not active in this buffer"))
+  (let ((version (lsp-request "workspace/executeCommand"
+                              `(:command "telomare.version" :arguments []))))
+    (message "Telomare LSP version: %s" version)))
+
+(define-key telomare-mode-map (kbd "C-c C-v") #'telomare-lsp-version)
+
 ;; Associate .tel files with telomare-mode
 (add-to-list 'auto-mode-alist '("\\.tel\\'" . telomare-mode))
 
@@ -56,5 +68,16 @@ You can also set TELOMARE_ROOT in your environment."
 ;; Auto-start LSP in telomare-mode
 (add-hook 'telomare-mode-hook #'lsp)
 
+;; Major-mode leader bindings. Reachable as `SPC m ...` in Evil state and
+;; `M-m m ...` in holy-mode; only LSP features the server actually
+;; implements are bound (no hover, no rename).
+(with-eval-after-load 'lsp-mode
+  (when (fboundp 'spacemacs/set-leader-keys-for-major-mode)
+    (spacemacs/set-leader-keys-for-major-mode 'telomare-mode
+      "g" #'lsp-find-definition
+      "G" #'lsp-find-references
+      "a" #'lsp-execute-code-action
+      "v" #'telomare-lsp-version)))
+
 (provide 'telomare-mode-spacemacs)
 ;;; telomare-mode-spacemacs.el ends here
diff --git a/emacs-telomare-mode/telomare-mode-vanilla.el b/emacs-telomare-mode/telomare-mode-vanilla.el
index 57e65427..8a6a6a61 100644
--- a/emacs-telomare-mode/telomare-mode-vanilla.el
+++ b/emacs-telomare-mode/telomare-mode-vanilla.el
@@ -26,12 +26,12 @@
   ;; Add LSP hook
   (add-hook 'telomare-mode-hook #'lsp-deferred 'append)
 
-  ;; Set up minimal keybindings
+  ;; Set up minimal keybindings. Only LSP features the server
+  ;; implements are bound (the server has no hover or rename).
   (define-key telomare-mode-map (kbd "M-.") #'lsp-find-definition)
   (define-key telomare-mode-map (kbd "M-?") #'lsp-find-references)
-  (define-key telomare-mode-map (kbd "C-c h") #'lsp-describe-thing-at-point)
-  (define-key telomare-mode-map (kbd "C-c r") #'lsp-rename)
-  (define-key telomare-mode-map (kbd "C-c a") #'lsp-execute-code-action))
+  (define-key telomare-mode-map (kbd "C-c a") #'lsp-execute-code-action)
+  (define-key telomare-mode-map (kbd "C-c C-v") #'telomare-lsp-version))
 
 ;; Initialize
 (telomare-vanilla-setup)
diff --git a/flake.nix b/flake.nix
index d427f261..42e72210 100644
--- a/flake.nix
+++ b/flake.nix
@@ -13,7 +13,21 @@
     flake-parts.lib.mkFlake { inherit inputs; } {
       systems = [ "x86_64-linux" "aarch64-linux" ];
       imports = [ inputs.haskell-flake.flakeModule ];
-      perSystem = { self', system, pkgs, ... }: {
+      perSystem = { self', system, pkgs, ... }:
+        let
+          lspVersion =
+            if self ? lastModifiedDate then
+              let
+                timestamp = self.lastModifiedDate;
+                year = builtins.substring 0 4 timestamp;
+                month = builtins.substring 4 2 timestamp;
+                day = builtins.substring 6 2 timestamp;
+                hour = builtins.substring 8 2 timestamp;
+                minute = builtins.substring 10 2 timestamp;
+              in "${year}-${month}-${day}T${hour}:${minute}Z"
+            else
+              "unknown";
+        in {
         haskellProjects.default = {
           basePackages = pkgs.haskell.packages.ghc96;
           # To get access to non-Haskell dependencies one most add them to `extraBuildDepends`
@@ -68,7 +82,13 @@
       };
       apps.lsp = {
         type = "app";
-        program = "${self.packages.${system}.telomare}/bin/telomare-lsp";
+        program = "${pkgs.writeShellApplication {
+          name = "telomare-lsp";
+          text = ''
+            export TELOMARE_LSP_VERSION="${lspVersion}"
+            exec "${self.packages.${system}.telomare}/bin/telomare-lsp" "$@"
+          '';
+        }}/bin/telomare-lsp";
       };
       apps.format-lint = {
         type = "app";
@@ -77,8 +97,10 @@
           runtimeInputs = [
             pkgs.diffutils
             pkgs.git
-            pkgs.haskellPackages.hlint
-            pkgs.haskellPackages.stylish-haskell
+            # Use the project's GHC 9.6 tools so format-lint matches the
+            # hlint/stylish-haskell that the devShell and CI use.
+            pkgs.haskell.packages.ghc96.hlint
+            pkgs.haskell.packages.ghc96.stylish-haskell
           ];
           text = ''
             mapfile -t hs_files < <(git ls-files '*.hs')
@@ -99,11 +121,18 @@
               done
             fi
 
+            lint_status=0
+            hlint . || lint_status=$?
+
             if [ "$format_status" -ne 0 ]; then
-              exit "$format_status"
+              printf 'Formatting check failed\n'
+            fi
+            if [ "$lint_status" -ne 0 ]; then
+              printf 'Linting check failed\n'
+            fi
+            if [ "$format_status" -ne 0 ] || [ "$lint_status" -ne 0 ]; then
+              exit 1
             fi
-
-            hlint .
 
             printf 'Formatting and linting are OK\n'
           '';
diff --git a/src/PrettyPrint.hs b/src/PrettyPrint.hs
index f1d3c7e1..bf9e9979 100644
--- a/src/PrettyPrint.hs
+++ b/src/PrettyPrint.hs
@@ -13,7 +13,8 @@ import Telomare (DataType (..), FragExpr (..), FragExprF (..), FragExprUR (..),
                  RecursionSimulationPieces (..), Term1, Term3 (..), Term4 (..),
                  UnprocessedParsedTerm (..), UnprocessedParsedTermF (..),
                  forget, forgetAnnotationFragExprUR, g2i, indentWithChildren',
-                 indentWithOneChild', indentWithTwoChildren', isNum, rootFrag)
+                 indentWithOneChild', indentWithTwoChildren', isNum,
+                 locatedNameText, rootFrag)
 
 import qualified Control.Comonad.Trans.Cofree as CofreeT (CofreeF (..))
 import qualified Control.Monad.State as State
@@ -363,7 +364,7 @@ instance Show MultiLineShowUPT where
       (AppUPF x y) -> "AppUP\n" <>
                         "  " <> ind x <> "\n" <>
                         "  " <> ind y
-      (LamUPF str y) -> "LamUP " <> str <> "\n" <>
+      (LamUPF str y) -> "LamUP " <> locatedNameText str <> "\n" <>
                         "  " <> ind y
       (ChurchUPF x) -> "ChurchUP " <> show x
       (LeftUPF x) -> "LeftUP\n" <>
@@ -387,7 +388,7 @@ instance Show MultiLineShowUPT where
                         concatMap (\x -> "  , " <> ind x <> "\n") ls <>
                         "  ]"
       (LetUPF ls x) -> "LetUP\n" <>
-                         concatMap (\(n,v) -> "  , (" <> n <> ", " <> ind v <> ")\n") ls <>
+                         concatMap (\(n,v) -> "  , (" <> locatedNameText n <> ", " <> ind v <> ")\n") ls <>
                          "  ]\n" <>
                          "  " <> ind x
       (CaseUPF x ls) -> "CaseUP\n" <>
@@ -420,8 +421,7 @@ instance Show PrettyUPT where
         "let " <> indentSansFirstLine 4 (unlines (assignList <$> ls)) <> "\n" <>
         "in " <> indentSansFirstLine 3 x
           where
-            assignList :: (String, String) -> String
-            assignList (str, upt) = str <> " = " <> indentSansFirstLine (3 + length str) upt
+            assignList (name, upt) = locatedNameText name <> " = " <> indentSansFirstLine (3 + length (locatedNameText name)) upt
       (ListUPF []) -> "[]"
       (ListUPF [x]) -> "[" <> x <> "]"
       (ListUPF ls) ->
@@ -433,7 +433,7 @@ instance Show PrettyUPT where
               _         -> error "removeFirstComma: input does not start with a comma"
       (AppUPF x y) -> (if (length . words $ x) == 1 then x else "(" <> x <> ")") <> " " <>
                       if (length . words $ y) == 1 then y else "(" <> y <> ")"
-      (LamUPF str y) -> "\\ " <> str <> " -> " <> indentSansFirstLine (6 + length str) y
+      (LamUPF str y) -> "\\ " <> locatedNameText str <> " -> " <> indentSansFirstLine (6 + length (locatedNameText str)) y
       (ChurchUPF x) -> "$" <> show x
       (LeftUPF x) -> "left (" <> indentSansFirstLine 6 x <> ")"
       (RightUPF x) -> "right (" <> indentSansFirstLine 7 x <> ")"
diff --git a/src/Telomare.hs b/src/Telomare.hs
index 46e8972d..ab61aa10 100644
--- a/src/Telomare.hs
+++ b/src/Telomare.hs
@@ -423,14 +423,62 @@ data RecursionSimulationPieces a
   | CheckingWrapper LocTag a a
   deriving (Eq, Ord, Show, NFData, Generic, Functor)
 
+data SourcePosition = SourcePosition
+  { sourcePositionLine   :: Int
+  , sourcePositionColumn :: Int
+  , sourcePositionOffset :: Int
+  }
+  deriving (Eq, Show, Ord, Generic, NFData)
+
+instance Validity SourcePosition
+instance GenValid SourcePosition
+
+data SourceSpan = SourceSpan
+  { sourceSpanFile  :: Maybe FilePath
+  , sourceSpanStart :: SourcePosition
+  , sourceSpanEnd   :: SourcePosition
+  }
+  deriving (Eq, Show, Ord, Generic, NFData)
+
+instance Validity SourceSpan
+instance GenValid SourceSpan
+
 data LocTag
-  = DummyLoc
-  | Loc Int Int
+  = SourceLoc SourceSpan
+  | GeneratedLoc String (Maybe LocTag)
+  | BuiltinLoc String
+  | RuntimeLoc
+  | DecompiledLoc
+  | UnknownLoc
   deriving (Eq, Show, Ord, Generic, NFData)
 
 instance Validity LocTag
 instance GenValid LocTag
 
+locStartLineColumn :: LocTag -> Maybe (Int, Int)
+locStartLineColumn = \case
+  SourceLoc span ->
+    let start = sourceSpanStart span
+    in Just (sourcePositionLine start, sourcePositionColumn start)
+  GeneratedLoc _ parent -> parent >>= locStartLineColumn
+  _ -> Nothing
+
+renderLocTag :: LocTag -> Maybe String
+renderLocTag loc = case locStartLineColumn loc of
+  Just (line, column) -> Just $ "line " <> show line <> ", column " <> show column
+  Nothing             -> Nothing
+
+renderLocTagVerbose :: LocTag -> String
+renderLocTagVerbose loc = case (loc, renderLocTag loc) of
+  (GeneratedLoc reason _, Just rendered) -> rendered <> " (generated by " <> reason <> ")"
+  (GeneratedLoc reason Nothing, _)       -> "generated by " <> reason
+  (BuiltinLoc name, _)                   -> "builtin " <> show name
+  (RuntimeLoc, _)                        -> "runtime value"
+  (DecompiledLoc, _)                     -> "decompiled value"
+  (UnknownLoc, _)                        -> "unknown location"
+  (_, Just rendered)                     -> rendered
+  (_, Nothing)                           -> "unknown location"
+
 newtype FragExprUR =
   FragExprUR { unFragExprUR :: Cofree (FragExprF (RecursionSimulationPieces FragExprUR))
                                       LocTag
@@ -488,8 +536,22 @@ data ResolverError
   | ModuleNotFound String
   | DefinitionCycle [String]
   | MissingDefinitions [String]
+  | MissingDefinitionAt LocTag String
   | ParseError String
-  deriving (Eq, Ord, Show)
+  deriving (Eq, Ord)
+
+instance Show ResolverError where
+  showsPrec d err = showParen (d > 10) $ showString (renderResolverError err)
+
+renderResolverError :: ResolverError -> String
+renderResolverError = \case
+  NoMainFunction moduleName -> "NoMainFunction " <> show moduleName
+  ModuleNotFound moduleName -> "ModuleNotFound " <> show moduleName
+  DefinitionCycle names -> "DefinitionCycle " <> show names
+  MissingDefinitions names -> "MissingDefinitions " <> show names
+  MissingDefinitionAt loc name ->
+    "missing definition " <> show name <> " at " <> renderLocTagVerbose loc
+  ParseError err -> "ParseError " <> show err
 
 data EvalError = RTE RunTimeError
     | TCE TypeCheckError
@@ -932,20 +994,21 @@ instance TelomareLike (ExprT a) where
 telomareToFragmap :: IExpr -> Map FragIndex (Cofree (FragExprF a) LocTag)
 telomareToFragmap expr = Map.insert (FragIndex 0) bf m where
     (bf, (_,m)) = State.runState (convert expr) (FragIndex 1, Map.empty)
+    runtime = RuntimeLoc
     convert = \case
-      Zero -> pure $ DummyLoc :< ZeroFragF
-      Pair a b -> (\x y -> DummyLoc :< PairFragF x y) <$> convert a <*> convert b
-      Env -> pure $ DummyLoc :< EnvFragF
-      SetEnv x -> (\y -> DummyLoc :< SetEnvFragF y) <$> convert x
+      Zero -> pure $ runtime :< ZeroFragF
+      Pair a b -> (\x y -> runtime :< PairFragF x y) <$> convert a <*> convert b
+      Env -> pure $ runtime :< EnvFragF
+      SetEnv x -> (\y -> runtime :< SetEnvFragF y) <$> convert x
       Defer x -> do
         bx <- convert x
         (fi@(FragIndex i), fragMap) <- State.get
         State.put (FragIndex (i + 1), Map.insert fi bx fragMap)
-        pure $ DummyLoc :< DeferFragF fi
-      Gate l r -> (\x y -> DummyLoc :< GateFragF x y) <$> convert l <*> convert r
-      PLeft x -> (\y -> DummyLoc :< LeftFragF y) <$> convert x
-      PRight x -> (\y -> DummyLoc :< RightFragF y) <$> convert x
-      Trace -> pure $ DummyLoc :< TraceFragF
+        pure $ runtime :< DeferFragF fi
+      Gate l r -> (\x y -> runtime :< GateFragF x y) <$> convert l <*> convert r
+      PLeft x -> (\y -> runtime :< LeftFragF y) <$> convert x
+      PRight x -> (\y -> runtime :< RightFragF y) <$> convert x
+      Trace -> pure $ runtime :< TraceFragF
 
 fragmapToTelomare :: Map FragIndex (FragExpr a) -> Maybe IExpr
 fragmapToTelomare fragMap = convert (rootFrag fragMap) where
@@ -1053,17 +1116,29 @@ data Pattern
   | PatternPair Pattern Pattern
   deriving (Show, Eq, Ord)
 
+newtype LocatedName = LocatedName (LocTag, String)
+  deriving (Eq, Ord, Show)
+
+locatedNameLoc :: LocatedName -> LocTag
+locatedNameLoc (LocatedName (loc, _)) = loc
+
+locatedNameText :: LocatedName -> String
+locatedNameText (LocatedName (_, name)) = name
+
+locatedName :: LocTag -> String -> LocatedName
+locatedName loc name = LocatedName (loc, name)
+
 -- |Firstly parsed AST sans location annotations
 data UnprocessedParsedTerm
   = VarUP String
   | ITEUP UnprocessedParsedTerm UnprocessedParsedTerm UnprocessedParsedTerm
-  | LetUP [(String, UnprocessedParsedTerm)] UnprocessedParsedTerm
+  | LetUP [(LocatedName, UnprocessedParsedTerm)] UnprocessedParsedTerm
   | ListUP [UnprocessedParsedTerm]
   | IntUP Int
   | StringUP String
   | PairUP UnprocessedParsedTerm UnprocessedParsedTerm
   | AppUP UnprocessedParsedTerm UnprocessedParsedTerm
-  | LamUP String UnprocessedParsedTerm
+  | LamUP LocatedName UnprocessedParsedTerm
   | ChurchUP Int
   | UnsizedRecursionUP UnprocessedParsedTerm UnprocessedParsedTerm UnprocessedParsedTerm
   | LeftUP UnprocessedParsedTerm
@@ -1080,6 +1155,15 @@ data UnprocessedParsedTerm
 makeBaseFunctor ''UnprocessedParsedTerm -- Functorial version UnprocessedParsedTerm
 makePrisms ''UnprocessedParsedTerm
 
+letBindingName :: (LocatedName, a) -> String
+letBindingName (name, _) = locatedNameText name
+
+letBindingValue :: (LocatedName, a) -> a
+letBindingValue (_, value) = value
+
+letBindingLoc :: (LocatedName, a) -> LocTag
+letBindingLoc (name, _) = locatedNameLoc name
+
 makeBaseFunctor ''Pattern
 
 instance Eq a => Eq (UnprocessedParsedTermF a) where
@@ -1090,7 +1174,7 @@ instance Eq1 UnprocessedParsedTermF where
   liftEq eq (ITEUPF c1 t1 e1) (ITEUPF c2 t2 e2) =
     eq c1 c2 && eq t1 t2 && eq e1 e2
   liftEq eq (LetUPF binds1 body1) (LetUPF binds2 body2) =
-    liftEq (\(s1, t1) (s2, t2) -> s1 == s2 && eq t1 t2) binds1 binds2 && eq body1 body2
+    liftEq (\(s1, t1) (s2, t2) -> locatedNameText s1 == locatedNameText s2 && eq t1 t2) binds1 binds2 && eq body1 body2
   liftEq eq (ListUPF items1) (ListUPF items2) =
     liftEq eq items1 items2
   liftEq eq (IntUPF n1) (IntUPF n2) =
@@ -1102,7 +1186,7 @@ instance Eq1 UnprocessedParsedTermF where
   liftEq eq (AppUPF f1 x1) (AppUPF f2 x2) =
     eq f1 f2 && eq x1 x2
   liftEq eq (LamUPF var1 body1) (LamUPF var2 body2) =
-    var1 == var2 && eq body1 body2
+    locatedNameText var1 == locatedNameText var2 && eq body1 body2
   liftEq eq (ChurchUPF n1) (ChurchUPF n2) =
     n1 == n2
   liftEq eq (UnsizedRecursionUPF a1 b1 c1) (UnsizedRecursionUPF a2 b2 c2) =
@@ -1156,8 +1240,8 @@ instance Show1 UnprocessedParsedTermF where
     ITEUPF c t e -> showString "ITEUPF " . showsPrecFunc 11 c . showChar ' '
                     . showsPrecFunc 11 t . showChar ' ' . showsPrecFunc 11 e
     LetUPF bindings body ->
-      let showBinding (str, x) = showChar '(' . shows str . showString ", "
-                                . showsPrecFunc 11 x . showChar ')'
+      let showBinding (str, x) = showChar '(' . shows (locatedNameText str) . showString ", "
+                                 . showsPrecFunc 11 x . showChar ')'
           showBindings bs = showChar '[' . foldr1 (\a b -> a . showString ", " . b)
                            (fmap showBinding bs) . showChar ']'
       in showString "LetUPF " . showBindings bindings . showChar ' ' . showsPrecFunc 11 body
@@ -1171,7 +1255,7 @@ instance Show1 UnprocessedParsedTermF where
                    . showsPrecFunc 11 b
     AppUPF f x -> showString "AppUPF " . showsPrecFunc 11 f . showChar ' '
                   . showsPrecFunc 11 x
-    LamUPF var body -> showString "LamUPF " . shows var . showChar ' '
+    LamUPF var body -> showString "LamUPF " . shows (locatedNameText var) . showChar ' '
                        . showsPrecFunc 11 body
     ChurchUPF n -> showString "ChurchUPF " . shows n
     UnsizedRecursionUPF a b c -> showString "UnsizedRecursionUPF "
@@ -1192,4 +1276,3 @@ instance Show1 UnprocessedParsedTermF where
                            (fmap showPattern patterns) . showChar ']'
       in showString "CaseUPF " . showsPrecFunc 11 scrutinee . showChar ' '
          . showPatterns patterns
-
diff --git a/src/Telomare/Decompiler.hs b/src/Telomare/Decompiler.hs
index 3ccf2b84..1910ede7 100644
--- a/src/Telomare/Decompiler.hs
+++ b/src/Telomare/Decompiler.hs
@@ -43,15 +43,15 @@ decompileUPT =
           VarUP s -> showS s
           ITEUP i t e -> drawList [showS "if ", draw i, showS " then ", draw t, showS " else ", draw e]
           LetUP ((firstName, firstDef):bindingsXS) in_ -> if null bindingsXS
-            then drawList [showS "let ", showS firstName, showS " = ", draw firstDef, showS " in ", draw in_]
+            then drawList [showS "let ", showS (locatedNameText firstName), showS " = ", draw firstDef, showS " in ", draw in_]
             else do
             startIn <- State.get
             l <- showS "let "
             startBind <- State.get
-            fb <- drawList [showS firstName, showS " = ", draw firstDef, pure "\n"]
+            fb <- drawList [showS (locatedNameText firstName), showS " = ", draw firstDef, pure "\n"]
             let drawOne (name, upt) = do
                   State.put startBind
-                  drawList [drawIndent, showS name, showS " = ", draw upt, pure "\n"]
+                  drawList [drawIndent, showS (locatedNameText name), showS " = ", draw upt, pure "\n"]
             displayedBindings <- mconcat <$> traverse drawOne bindingsXS
             State.put startIn
             mconcat <$> sequence [pure l, pure fb, pure displayedBindings, drawIndent, showS "in ", draw in_]
@@ -64,7 +64,7 @@ decompileUPT =
           PairUP a b -> drawList [showS "(", draw a, showS ",", draw b, showS ")"]
           AppUP f x -> drawList [drawFirstParens f, drawParens x]
           -- TODO flatten nested lambdas
-          LamUP n x -> drawList [showS "\\", showS n, showS " -> ", draw x]
+          LamUP n x -> drawList [showS "\\", showS (locatedNameText n), showS " -> ", draw x]
           ChurchUP n -> drawList [showS "$", showS $ show n]
           UnsizedRecursionUP t r b -> drawList [showS "{", draw t, showS ",", draw r, showS ",", draw b, showS "}"]
           LeftUP x -> drawList [showS "left ", drawParens x]
@@ -105,8 +105,8 @@ decompileTerm1 = \case
   _ :< TLeftF x -> LeftUP (decompileTerm1 x)
   _ :< TRightF x -> RightUP (decompileTerm1 x)
   _ :< TTraceF x -> TraceUP (decompileTerm1 x)
-  _ :< TLamF (Open n) x -> LamUP n (decompileTerm1 x)
-  _ :< TLamF (Closed n) x -> LamUP n (decompileTerm1 x) -- not strictly equivalent
+  loc :< TLamF (Open n) x -> LamUP (locatedName loc n) (decompileTerm1 x)
+  loc :< TLamF (Closed n) x -> LamUP (locatedName loc n) (decompileTerm1 x) -- not strictly equivalent
   _ :< TLimitedRecursionF t r b -> UnsizedRecursionUP (decompileTerm1 t) (decompileTerm1 r) (decompileTerm1 b)
 
 decompileTerm2 :: Term2 -> Term1
@@ -162,13 +162,13 @@ decompileTerm3 (Term3 tm) = decompileFragMap $ Map.map unFragExprUR tm
 
 decompileIExpr :: IExpr -> Term4
 decompileIExpr x = let build = \case
-                         Zero     -> pure . tag DummyLoc $ ZeroFrag
-                         Pair a b -> (\x y -> DummyLoc :< PairFragF x y) <$> build a <*> build b
-                         Env      -> pure . tag DummyLoc $ EnvFrag
-                         SetEnv x -> (DummyLoc :<) . SetEnvFragF <$> build x
-                         Gate l r -> (\x y -> DummyLoc :< GateFragF x y) <$> build l <*> build r
-                         PLeft x  -> (DummyLoc :<) . LeftFragF <$> build x
-                         PRight x -> (DummyLoc :<) . RightFragF <$> build x
-                         Trace    -> pure . tag DummyLoc $ TraceFrag
+                         Zero     -> pure . tag DecompiledLoc $ ZeroFrag
+                         Pair a b -> (\x y -> DecompiledLoc :< PairFragF x y) <$> build a <*> build b
+                         Env      -> pure . tag DecompiledLoc $ EnvFrag
+                         SetEnv x -> (DecompiledLoc :<) . SetEnvFragF <$> build x
+                         Gate l r -> (\x y -> DecompiledLoc :< GateFragF x y) <$> build l <*> build r
+                         PLeft x  -> (DecompiledLoc :<) . LeftFragF <$> build x
+                         PRight x -> (DecompiledLoc :<) . RightFragF <$> build x
+                         Trace    -> pure . tag DecompiledLoc $ TraceFrag
                          Defer x  -> deferF $ build x
-                   in Term4 . buildFragMap $ build x
+                    in Term4 . buildFragMap $ build x
diff --git a/src/Telomare/Eval.hs b/src/Telomare/Eval.hs
index 4ffbd379..52d3bef1 100644
--- a/src/Telomare/Eval.hs
+++ b/src/Telomare/Eval.hs
@@ -16,6 +16,7 @@ import Data.Foldable (fold)
 import Data.List (partition)
 import Data.Map (Map)
 import qualified Data.Map as Map
+import Data.Maybe (isNothing)
 import Data.Semigroup (Max (..), Min (..))
 import Data.Set (Set)
 import qualified Data.Set as Set
@@ -29,14 +30,14 @@ import PrettyPrint
 import Telomare (AbstractRunTime, BreakState, BreakState', EvalError (..),
                  ExprA (..), FragExpr (..), FragExprF (..),
                  FragIndex (FragIndex), IExpr (..), IExprF (..), LocTag (..),
-                 PartialType (..), Pattern, RecursionPieceFrag,
+                 LocatedName, PartialType (..), Pattern, RecursionPieceFrag,
                  RecursionSimulationPieces (..), ResolverError (..),
                  RunTimeError (..), TelomareLike (..), Term2, Term3 (Term3),
                  Term4 (Term4), UnprocessedParsedTerm (..),
                  UnprocessedParsedTermF (..), UnsizedRecursionToken (..), app,
                  appF, convertAbortMessage, deferF, eval, forget, g2s,
-                 innerChurchF, insertAndGetKey, pairF, rootFrag, s2g, setEnvF,
-                 tag, unFragExprUR)
+                 innerChurchF, insertAndGetKey, locStartLineColumn, pairF,
+                 rootFrag, s2g, setEnvF, tag, unFragExprUR)
 import Telomare.Parser (AnnotatedUPT, parseModule, parseOneExprOrTopLevelDefs,
                         parsePrelude)
 import Telomare.Possible (SizingSettings (SizingSettings), abortExprToTerm4,
@@ -119,8 +120,8 @@ removeChecks (Term4 m) =
         x                  -> x
       (ind, newM) = State.runState builder m
       builder = do
-        envDefer <- insertAndGetKey $ DummyLoc :< EnvFragF
-        insertAndGetKey $ DummyLoc :< DeferFragF envDefer
+        envDefer <- insertAndGetKey $ GeneratedLoc "removeChecks" Nothing :< EnvFragF
+        insertAndGetKey $ GeneratedLoc "removeChecks" Nothing :< DeferFragF envDefer
   in Term4 $ Map.map (transform f) newM
 -}
 removeChecks :: Term4 -> Term4
@@ -293,16 +294,16 @@ showSizingInSource prelude s
         unsizedExpr = term3ToUnsizedExpr 256 <$> first RE parsed
         sizedRecursion = unsizedExpr >>= (first RecursionLimitError . getSizesM 256)
         sizeLocs = error "TODO showSizingInSource implement sizeLocs" --Map.toAscList . buildUnsizedLocMap <$> unsizedExpr
-        -- (orphanLocs, lineLocs) = partition ((== DummyLoc) . snd) sizeLocs
+        -- (orphanLocs, lineLocs) = partition (isNothing . locStartLineColumn . snd) sizeLocs
         (orphanLocs, lineLocs) = case sizeLocs of
           Left e   -> error "uh" -- ("Could not size: " <> show e)
-          Right sl -> partition ((== DummyLoc) . snd) sl
+          Right sl -> partition (isNothing . locStartLineColumn . snd) sl
         -- orphanList = map ((<> " ") . show . fst) orphanLocs
         -- orphans = "unsized with no location: " <> foldMap ((<> " ") . show . fst) orphanLocs
         orphans = error "TODO showSizingInSource thing"
-        fromEnum' = \case
-          Loc x _ -> x
-          _ -> error "unexpected DummyLoc"
+        fromEnum' loc = case locStartLineColumn loc of
+          Just (line, _) -> line
+          Nothing        -> error "unexpected source-less location"
         lookupSize x = case sizedRecursion of
           Right (SizedRecursion sm) -> case Map.lookup x sm of
             Just (Just v) -> show v
@@ -325,11 +326,11 @@ showFunctionIndexesInSource prelude s
         -- sizeLocs = (\(fi, t) -> (fi))
         reduceL (a CofreeT.:< x) = let l = fromEnum' a in (Min l, Max l) <> fold x
         sizeLocs = second (unAss . unFragExprUR) <$> Map.toAscList funMap
-        (orphanLocs, lineLocs) = partition ((== DummyLoc) . snd) sizeLocs
+        (orphanLocs, lineLocs) = partition (isNothing . locStartLineColumn . snd) sizeLocs
         orphans = "functions with no location: " <> foldMap ((<> " ") . show . fst) orphanLocs
-        fromEnum' = \case
-          Loc x _ -> x
-          _ -> 0 -- error "unexpected DummyLoc"
+        fromEnum' loc = case locStartLineColumn loc of
+          Just (line, _) -> line
+          Nothing        -> 0 -- source-less generated/runtime location
         getFunMatchingLine x = case filter ((== x) . fromEnum' . snd) lineLocs of
           [] -> ""
           -- l -> ("   # " <>) $ foldMap ((\s -> show (fromEnum s) <> ":" <> lookupSize s <> " ") . fst) l
@@ -377,7 +378,7 @@ eval2IExpr extraModuleBindings str =
         Right x -> case toTelomare x of
           Just ie -> pure ie
           _ -> Left $ "eval2IExpr conversion error back to iexpr:\n" <> prettyPrint x
-      aux = (\str -> Left (DummyLoc :< ImportQualifiedUPF str str)) . fst <$> extraModuleBindings
+      aux = (\str -> Left (GeneratedLoc "eval2IExpr.import" Nothing :< ImportQualifiedUPF str str)) . fst <$> extraModuleBindings
       resolved = resolveAllImports extraModuleBindings aux
 
 tagIExprWithEval :: IExpr -> Cofree IExprF (Int, IExpr)
@@ -434,7 +435,7 @@ tagUPTwithIExpr :: [(String, AnnotatedUPT)]
                 -> Cofree UnprocessedParsedTermF (Int, Either String IExpr)
 tagUPTwithIExpr prelude upt = evalState (para alg upt) 0 where
   upt2iexpr :: UnprocessedParsedTerm -> Either String IExpr
-  upt2iexpr u = first show (process (tag DummyLoc u)) >>= tt . first show . compileUnitTest
+  upt2iexpr u = first show (process (tag UnknownLoc u)) >>= tt . first show . compileUnitTest
   tt = \case
     Left e -> Left e
     Right x -> case toTelomare x of
@@ -463,16 +464,16 @@ tagUPTwithIExpr prelude upt = evalState (para alg upt) 0 where
     LetUPF l (upt0, x) -> do
       i <- State.get
       State.modify (+ 1)
-      let lupt :: [(String, UnprocessedParsedTerm)]
-          lupt = (fmap . fmap) fst l
+      let lupt :: [(LocatedName, UnprocessedParsedTerm)]
+          lupt = (\(name, (upt, _)) -> (name, upt)) <$> l
           slcupt :: State Int
-                     [Cofree UnprocessedParsedTermF (Int, Either String IExpr)]
-          slcupt = mapM snd (snd <$> l)
-          vnames :: [String]
+                       [Cofree UnprocessedParsedTermF (Int, Either String IExpr)]
+          slcupt = mapM (snd . snd) l
+          vnames :: [LocatedName]
           vnames = fst <$> l
       lcupt <- slcupt
       x' <- x
-      pure $ (i, upt2iexpr $ LetUP lupt upt0) :< LetUPF (vnames `zip` lcupt) x'
+      pure $ (i, upt2iexpr $ LetUP lupt upt0) :< LetUPF (zip vnames lcupt) x'
     CaseUPF (upt0, x) l -> do
       i <- State.get
       State.modify (+ 1)
@@ -551,4 +552,3 @@ tagUPTwithIExpr prelude upt = evalState (para alg upt) 0 where
       x' <- x
       y' <- y
       pure $ (i, upt2iexpr $ PairUP upt1 upt2) :< PairUPF x' y'
-
diff --git a/src/Telomare/Parser.hs b/src/Telomare/Parser.hs
index ccf0aa8b..f0019040 100644
--- a/src/Telomare/Parser.hs
+++ b/src/Telomare/Parser.hs
@@ -20,12 +20,11 @@ import PrettyPrint (indentSansFirstLine)
 import qualified System.IO.Strict as Strict
 import Telomare
 import Telomare.TypeChecker (typeCheck)
-import Text.Megaparsec (MonadParsec (eof, notFollowedBy, try), Parsec, Pos,
-                        PosState (pstateSourcePos),
-                        SourcePos (sourceColumn, sourceLine),
-                        State (statePosState), between, choice,
-                        errorBundlePretty, getParserState, many, manyTill,
-                        optional, runParser, sepBy, some, unPos, (<?>), (<|>))
+import Text.Megaparsec (MonadParsec (eof, notFollowedBy, try), ParseErrorBundle,
+                        Parsec, Pos, SourcePos (sourceColumn, sourceLine),
+                        between, choice, errorBundlePretty, getOffset,
+                        getSourcePos, many, manyTill, optional, runParser,
+                        sepBy, some, unPos, (<?>), (<|>))
 import Text.Megaparsec.Char (alphaNumChar, char, letterChar, space1, string)
 import qualified Text.Megaparsec.Char.Lexer as L
 import Text.Megaparsec.Debug (dbg)
@@ -36,18 +35,18 @@ import Text.Show.Deriving (deriveShow1)
 type AnnotatedUPT = Cofree UnprocessedParsedTermF LocTag
 
 data AssignmentEntry
-  = SingleAssignment String AnnotatedUPT
-  | ListAssignment LocTag [String] AnnotatedUPT
+  = SingleAssignment LocatedName AnnotatedUPT
+  | ListAssignment LocTag [LocatedName] AnnotatedUPT
 
 instance Plated UnprocessedParsedTerm where
   plate f = \case
     ITEUP i t e -> ITEUP <$> f i <*> f t <*> f e
-    LetUP l x   -> LetUP <$> traverse (sequenceA . second f) l <*> f x
+    LetUP l x   -> LetUP <$> traverse (traverse f) l <*> f x
     CaseUP x l  -> CaseUP <$> f x <*> traverse (sequenceA . second f) l
     ListUP l    -> ListUP <$> traverse f l
     PairUP a b  -> PairUP <$> f a <*> f b
     AppUP u x   -> AppUP <$> f u <*> f x
-    LamUP s x   -> LamUP s <$> f x
+    LamUP name x -> LamUP name <$> f x
     LeftUP x    -> LeftUP <$> f x
     RightUP x   -> RightUP <$> f x
     TraceUP x   -> TraceUP <$> f x
@@ -62,10 +61,8 @@ type TelomareParser = Parsec Void String
 -- |Parse a variable.
 parseVariable :: TelomareParser AnnotatedUPT
 parseVariable = do
-  s <- getParserState
-  let line = unPos . sourceLine . pstateSourcePos . statePosState $ s
-      column = unPos . sourceColumn . pstateSourcePos . statePosState $ s
-  (\str -> Loc line column :< VarUPF str) <$> identifier
+  (loc, str) <- withSourceSpan identifierRaw
+  pure $ loc :< VarUPF str
 
 -- |Line comments start with "--".
 lineComment :: TelomareParser ()
@@ -108,7 +105,10 @@ rws = ["let", "in", "if", "then", "else", "case", "of", "import"]
 -- |Variable identifiers can consist of alphanumeric characters, underscore,
 -- and must start with an English alphabet letter
 identifier :: TelomareParser String
-identifier = lexeme . try $ p >>= check
+identifier = lexeme identifierRaw
+
+identifierRaw :: TelomareParser String
+identifierRaw = try $ p >>= check
   where
     p = (:) <$> letterChar <*> many (alphaNumChar <|> char '_' <|> char '.' <?> "variable")
     check x = if x `elem` rws
@@ -133,30 +133,57 @@ commaSep p = p `sepBy` symbol ","
 
 -- |Integer TelomareParser used by `parseNumber` and `parseChurch`
 integer :: TelomareParser Integer
-integer = toInteger <$> lexeme L.decimal
-
-getLineColumn = do
-  s <- getParserState
-  let line = unPos . sourceLine . pstateSourcePos . statePosState $ s
-      column = unPos . sourceColumn . pstateSourcePos . statePosState $ s
-  pure $ Loc line column
+integer = lexeme integerRaw
+
+integerRaw :: TelomareParser Integer
+integerRaw = toInteger <$> L.decimal
+
+sourcePositionFromPos :: Int -> SourcePos -> SourcePosition
+sourcePositionFromPos offset pos = SourcePosition
+  { sourcePositionLine = unPos $ sourceLine pos
+  , sourcePositionColumn = unPos $ sourceColumn pos
+  , sourcePositionOffset = offset
+  }
+
+sourceLocFromPositions :: (Int, SourcePos) -> (Int, SourcePos) -> LocTag
+sourceLocFromPositions (startOffset, start) (endOffset, end) = SourceLoc SourceSpan
+  { sourceSpanFile = Nothing
+  , sourceSpanStart = sourcePositionFromPos startOffset start
+  , sourceSpanEnd = sourcePositionFromPos endOffset end
+  }
+
+withSourceSpan :: TelomareParser a -> TelomareParser (LocTag, a)
+withSourceSpan parser = do
+  startOffset <- getOffset
+  start <- getSourcePos
+  x <- parser
+  endOffset <- getOffset
+  end <- getSourcePos
+  sc
+  pure (sourceLocFromPositions (startOffset, start) (endOffset, end), x)
+
+getSourceLoc :: TelomareParser LocTag
+getSourceLoc = do
+  offset <- getOffset
+  pos <- getSourcePos
+  pure $ sourceLocFromPositions (offset, pos) (offset, pos)
 
 -- |Parse string literal.
 parseString :: TelomareParser AnnotatedUPT
 parseString = do
-  x <- getLineColumn
-  (\str -> x :< StringUPF str) <$> (char '"' >> manyTill L.charLiteral (char '"' <* sc))
+  (x, str) <- withSourceSpan (char '"' >> manyTill L.charLiteral (char '"'))
+  pure $ x :< StringUPF str
 
 -- |Parse number (Integer).
 parseNumber :: TelomareParser AnnotatedUPT
 parseNumber = do
-  x <- getLineColumn
-  (\i -> x :< (IntUPF . fromInteger $ i)) <$> integer
+  (x, i) <- withSourceSpan integerRaw
+  pure $ x :< (IntUPF . fromInteger $ i)
 
 -- |Parse a pair.
 parsePair :: TelomareParser AnnotatedUPT
 parsePair = parens $ do
-  x <- getLineColumn
+  x <- getSourceLoc
   a <- scn *> parseLongExpr <* scn
   _ <- symbol "," <* scn
   b <- parseLongExpr <* scn
@@ -165,7 +192,7 @@ parsePair = parens $ do
 -- |Parse unsized recursion triple
 parseUnsizedRecursion :: TelomareParser AnnotatedUPT
 parseUnsizedRecursion = curlies $ do
-  x <- getLineColumn
+  x <- getSourceLoc
   a <- scn *> parseLongExpr <* scn
   _ <- symbol "," <* scn
   b <- parseLongExpr <* scn
@@ -176,7 +203,7 @@ parseUnsizedRecursion = curlies $ do
 -- |Parse a list.
 parseList :: TelomareParser AnnotatedUPT
 parseList = do
-  x <- getLineColumn
+  x <- getSourceLoc
   exprs <- brackets (commaSep (scn *> parseLongExpr <*scn))
   pure $ x :< ListUPF exprs
 
@@ -184,7 +211,7 @@ parseList = do
 -- |Parse ITE (which stands for "if then else").
 parseITE :: TelomareParser AnnotatedUPT
 parseITE = do
-  x <- getLineColumn
+  x <- getSourceLoc
   reserved "if" <* scn
   cond <- (parseLongExpr <|> parseSingleExpr) <* scn
   reserved "then" <* scn
@@ -195,23 +222,29 @@ parseITE = do
 
 parseHash :: TelomareParser AnnotatedUPT
 parseHash = do
-  x <- getLineColumn
+  x <- getSourceLoc
   symbol "#" <* scn
   upt <- parseSingleExpr
   pure $ x :< HashUPF upt
 
 parseListAssignment :: TelomareParser AssignmentEntry
 parseListAssignment = do
-  x <- getLineColumn
-  names :: [String] <- (brackets (commaSep (scn *> identifier <* scn)) <* scn)
-                       <?> "list assignment names"
+  x <- getSourceLoc
+  names <- (brackets (commaSep (scn *> locatedNameParser <* scn)) <* scn)
+           <?> "list assignment names"
   (scn *> symbol "=") <?> "list assignment ="
   expr <- (scn *> parseLongExpr <* scn) <?> "list assignment body"
   pure $ ListAssignment x names expr
 
+locatedIdentifier :: TelomareParser (LocTag, String)
+locatedIdentifier = lexeme $ withSourceSpan identifierRaw
+
+locatedNameParser :: TelomareParser LocatedName
+locatedNameParser = uncurry locatedName <$> locatedIdentifier
+
 parseCase :: TelomareParser AnnotatedUPT
 parseCase = do
-  x <- getLineColumn
+  x <- getSourceLoc
   reserved "case" <* scn
   iexpr <- parseLongExpr <* scn
   reserved "of" <* scn
@@ -227,12 +260,33 @@ parseSingleCase = do
 
 parsePattern :: TelomareParser Pattern
 parsePattern = choice $ try <$> [ parsePatternIgnore
-                                , parsePatternVar
-                                , parsePatternAnnotated
-                                , parsePatternString
-                                , parsePatternInt
-                                , parsePatternPair
-                                ]
+                                 , parsePatternVar
+                                 , parsePatternAnnotated
+                                 , parsePatternString
+                                 , parsePatternInt
+                                 , parsePatternPair
+                                 ]
+
+parseLocatedPattern :: TelomareParser (LocTag, Pattern)
+parseLocatedPattern = choice $ try <$> [ parseLocatedPatternVar
+                                       , parseLocatedPatternOther
+                                       ]
+
+parseLocatedPatternVar :: TelomareParser (LocTag, Pattern)
+parseLocatedPatternVar = do
+  (loc, name) <- locatedIdentifier <* scn
+  pure (loc, PatternVar name)
+
+parseLocatedPatternOther :: TelomareParser (LocTag, Pattern)
+parseLocatedPatternOther = do
+  loc <- getSourceLoc
+  pattern' <- choice $ try <$> [ parsePatternIgnore
+                               , parsePatternAnnotated
+                               , parsePatternString
+                               , parsePatternInt
+                               , parsePatternPair
+                               ]
+  pure (loc, pattern')
 
 parsePatternPair :: TelomareParser Pattern
 parsePatternPair = parens $ do
@@ -287,7 +341,7 @@ parseSingleExpr = choice $ try <$> [ parseHash
 -- |Parse application of functions.
 parseApplied :: TelomareParser AnnotatedUPT
 parseApplied = do
-  x <- getLineColumn
+  x <- getSourceLoc
   fargs <- L.lineFold scn $ \sc' ->
     parseSingleExpr `sepBy` try sc'
   case fargs of
@@ -310,10 +364,10 @@ genPatternVarName = ("generatedVar" <>)
 
 -- |Pick the lambda-bound variable name for a pattern: use the user's name
 -- for a 'PatternVar', otherwise generate one.
-lambdaVarName :: Pattern -> String
-lambdaVarName = \case
-  PatternVar str -> str
-  p              -> genPatternVarName p
+lambdaVarName :: (LocTag, Pattern) -> LocatedName
+lambdaVarName (loc, pattern') = case pattern' of
+  PatternVar str -> locatedName loc str
+  p              -> locatedName (GeneratedLoc "lambda pattern" (Just loc)) (genPatternVarName p)
 
 -- |Build a multi-argument lambda whose destructuring all happens INSIDE
 -- the innermost lambda body. For @\\p1 p2 p3 -> body@ this emits
@@ -328,10 +382,10 @@ lambdaVarName = \case
 -- This avoids putting a function-valued lambda inside a case body, which
 -- would cause the case-rewrite to type-mismatch against the (Pair-typed)
 -- abort fallback.
-buildMultiLambda :: LocTag -> [Pattern] -> AnnotatedUPT -> AnnotatedUPT
+buildMultiLambda :: LocTag -> [(LocTag, Pattern)] -> AnnotatedUPT -> AnnotatedUPT
 buildMultiLambda lt patterns body =
   let varNames = lambdaVarName <$> patterns
-      destructured = foldr applyDestructure body (zip patterns varNames)
+      destructured = foldr applyDestructure body (zip (snd <$> patterns) (locatedNameText <$> varNames))
       lamWrapped = foldr (\v inner -> lt :< LamUPF v inner) destructured varNames
   in lamWrapped
   where
@@ -359,14 +413,14 @@ buildMultiLambda lt patterns body =
 -- Kept as a thin wrapper around 'buildMultiLambda' so existing callers
 -- that work pattern-at-a-time continue to function.
 makeLambda :: LocTag -> Pattern -> AnnotatedUPT -> AnnotatedUPT
-makeLambda lt p = buildMultiLambda lt [p]
+makeLambda lt p = buildMultiLambda lt [(lt, p)]
 
 -- |Parse lambda expression.
 parseLambda :: TelomareParser AnnotatedUPT
 parseLambda = do
-  x <- getLineColumn
+  x <- getSourceLoc
   symbol "\\" <* scn
-  variables <- some parsePattern <* scn
+  variables <- some parseLocatedPattern <* scn
   symbol "->" <* scn
   term1expr <- parseLongExpr <* scn
   pure $ buildMultiLambda x variables term1expr
@@ -382,7 +436,7 @@ parseSameLvl pos parser = do
 -- a specialized list-assignment convention.
 parseLet :: TelomareParser AnnotatedUPT
 parseLet = do
-  x <- getLineColumn
+  x <- getSourceLoc
   reserved "let" <* scn
   lvl <- L.indentLevel
   entries <- manyTill (parseSameLvl lvl parseAssignmentEntry) (reserved "in") <* scn
@@ -403,25 +457,30 @@ parseLongExpr = choice $ try <$> [ parseLet
 -- |Parse church numerals (church numerals are a "$" appended to an integer, without any whitespace separation).
 parseChurch :: TelomareParser AnnotatedUPT
 parseChurch = do
-  x <- getLineColumn
-  (\upt -> x :< ChurchUPF upt) . fromInteger <$> (symbol "$" *> integer)
+  (x, upt) <- withSourceSpan (char '$' *> integerRaw)
+  pure . (x :<) . ChurchUPF $ fromInteger upt
 
 -- |Parse refinement check.
 parseRefinementCheck :: TelomareParser (AnnotatedUPT -> AnnotatedUPT)
 parseRefinementCheck = do
-  x <- getLineColumn
+  x <- getSourceLoc
   (\a b -> x :< CheckUPF a b) <$> (symbol ":" *> parseLongExpr)
 
 -- |Parse assignment add adding binding to ParserState.
 parseAssignment :: TelomareParser (String, AnnotatedUPT)
 parseAssignment = do
-  var <- identifier <* scn
+  (var, expr) <- parseLocatedAssignment
+  pure (locatedNameText var, expr)
+
+parseLocatedAssignment :: TelomareParser (LocatedName, AnnotatedUPT)
+parseLocatedAssignment = do
+  (loc, var) <- locatedIdentifier <* scn
   annotation <- optional . try $ parseRefinementCheck
   scn *> symbol "=" <?> "assignment ="
   expr <- scn *> parseLongExpr <* scn
   case annotation of
-    Just annot -> pure (var, annot expr)
-    _          -> pure (var, expr)
+    Just annot -> pure (locatedName loc var, annot expr)
+    _          -> pure (locatedName loc var, expr)
 
 -- |Parse top level expressions.
 parseTopLevel :: TelomareParser AnnotatedUPT
@@ -429,14 +488,14 @@ parseTopLevel = parseTopLevelWithExtraModuleBindings []
 
 parseImport :: TelomareParser AnnotatedUPT
 parseImport = do
-  x <- getLineColumn
+  x <- getSourceLoc
   reserved "import" <* scn
   var <- identifier <* scn
   pure $ x :< ImportUPF var
 
 parseImportQualified :: TelomareParser AnnotatedUPT
 parseImportQualified = do
-  x <- getLineColumn
+  x <- getSourceLoc
   reserved "import" <* scn
   reserved "qualified" <* scn
   m <- identifier <* scn
@@ -449,12 +508,16 @@ parseImportQualified = do
 -- uppercase-lambda list assignment during expansion.
 parseAssignmentEntry :: TelomareParser AssignmentEntry
 parseAssignmentEntry =
-  (uncurry SingleAssignment <$> parseAssignment)
+  uncurry SingleAssignment <$> parseLocatedAssignment
     <|> parseListAssignment
 
 -- |Parse assignments, expanding list assignments into their per-slot bindings.
 parseAssignmentEntries :: TelomareParser [(String, AnnotatedUPT)]
 parseAssignmentEntries = do
+  fmap (first locatedNameText) <$> parseLocatedAssignmentEntries
+
+parseLocatedAssignmentEntries :: TelomareParser [(LocatedName, AnnotatedUPT)]
+parseLocatedAssignmentEntries = do
   entries <- scn *> many parseAssignmentEntry <* eof
   pure (expandAssignmentEntry =<< entries)
 
@@ -463,18 +526,20 @@ parseAssignmentEntries = do
 parseTopLevelWithExtraModuleBindings :: [(String, AnnotatedUPT)]
                                      -> TelomareParser AnnotatedUPT
 parseTopLevelWithExtraModuleBindings lst = do
-  x <- getLineColumn
-  bindingList <- parseAssignmentEntries
-  case lookup "main" bindingList of
-    Just m  -> pure $ x :< LetUPF (lst <> bindingList) m
+  x <- getSourceLoc
+  bindingList <- parseLocatedAssignmentEntries
+  case lookup "main" $ first locatedNameText <$> bindingList of
+    Just m  -> pure $ x :< LetUPF ((first (locatedName UnknownLoc) <$> lst) <> bindingList) m
     Nothing -> fail "missing 'main' definition"
 
-expandAssignmentEntry :: AssignmentEntry -> [(String, AnnotatedUPT)]
+expandAssignmentEntry :: AssignmentEntry -> [(LocatedName, AnnotatedUPT)]
 expandAssignmentEntry = \case
   SingleAssignment name body -> [(name, body)]
-  ListAssignment loc names body
-    | isUDTAssignment names body -> expandUDT (loc :< UDTUPF names body)
-    | otherwise                 -> expandPlainListAssignment loc names body
+  ListAssignment loc locatedNames body
+    | isUDTAssignment names body -> expandUDTLocated loc locatedNames body
+    | otherwise                 -> expandPlainListAssignment loc locatedNames body
+    where
+      names = locatedNameText <$> locatedNames
 
 isUDTAssignment :: [String] -> AnnotatedUPT -> Bool
 isUDTAssignment (name:_) (_ :< LamUPF _ _) = case name of
@@ -482,19 +547,21 @@ isUDTAssignment (name:_) (_ :< LamUPF _ _) = case name of
   _           -> False
 isUDTAssignment _ _ = False
 
-expandPlainListAssignment :: LocTag -> [String] -> AnnotatedUPT -> [(String, AnnotatedUPT)]
-expandPlainListAssignment loc names body =
+expandPlainListAssignment :: LocTag -> [LocatedName] -> AnnotatedUPT -> [(LocatedName, AnnotatedUPT)]
+expandPlainListAssignment loc locatedNames body =
   case listAssignmentSlots body of
     Just (slots, wrapBody)
-      | length names == length slots -> zip names (wrapBody <$> slots)
+      | length locatedNames == length slots ->
+          zipWith (\name slot -> (name, wrapBody slot)) locatedNames slots
       | otherwise -> error
-        $ "list assignment arity mismatch: " <> show (length names)
+        $ "list assignment arity mismatch: " <> show (length locatedNames)
         <> " names for " <> show (length slots) <> " values"
     Nothing ->
       let intermediate = listAssignmentIntermediate loc
           source = loc :< VarUPF intermediate
           mkAccessorBinding idx name = (name, accessAt loc idx source)
-      in (intermediate, body) : zipWith mkAccessorBinding [0 ..] names
+      in (locatedName (GeneratedLoc "listAssignmentIntermediate" (Just loc)) intermediate, body)
+       : zipWith mkAccessorBinding [0 ..] locatedNames
 
 -- |Find a final list literal in a plain list assignment, preserving lambdas
 -- and lets around each extracted slot. This lets `[f, g] = \x -> [...]`
@@ -511,9 +578,9 @@ listAssignmentSlots = go where
   go _ = Nothing
 
 listAssignmentIntermediate :: LocTag -> String
-listAssignmentIntermediate = \case
-  Loc line column -> "__list_assignment_" <> show line <> "_" <> show column
-  DummyLoc        -> "__list_assignment"
+listAssignmentIntermediate loc = case locStartLineColumn loc of
+  Just (line, column) -> "__list_assignment_" <> show line <> "_" <> show column
+  Nothing             -> "__list_assignment"
 
 accessAt :: LocTag -> Int -> AnnotatedUPT -> AnnotatedUPT
 accessAt loc 0 e = loc :< LeftUPF e
@@ -545,39 +612,54 @@ accessAt loc n e = loc :< LeftUPF (iterate (\x -> loc :< RightUPF x) e !! n)
 -- this fallback is kept for direct/internal callers of 'expandUDT'.
 expandUDT :: AnnotatedUPT -> [(String, AnnotatedUPT)]
 expandUDT (loc :< UDTUPF names@(tname:_) body) =
+  first locatedNameText <$> expandUDTLocated loc (locatedName loc <$> names) body
+expandUDT _ = []
+
+expandUDTLocated :: LocTag -> [LocatedName] -> AnnotatedUPT -> [(LocatedName, AnnotatedUPT)]
+expandUDTLocated loc locatedNames body =
+  case names of
+    tname:_ -> expandUDTLocated' loc locatedNames tname body
+    _       -> []
+  where
+    names = locatedNameText <$> locatedNames
+
+expandUDTLocated' :: LocTag -> [LocatedName] -> String -> AnnotatedUPT -> [(LocatedName, AnnotatedUPT)]
+expandUDTLocated' loc locatedNames tname body =
   case body of
     (_ :< LamUPF hParam inner) ->
       let (slots, wrapBody) = udtSlots tname inner
+          hParamName = locatedNameText hParam
           (coreSlots, hoistedSlots) = splitAt 2 slots
-          coreNames = take (1 + length coreSlots) names
-          hoistedNames = drop (1 + length coreSlots) names
-          validator    = autoValidator loc tname hParam
+          coreNames = take (1 + length coreSlots) locatedNames
+          hoistedNames = drop (1 + length coreSlots) locatedNames
+          validator    = autoValidator loc tname hParamName
           intermediate = "__udt_" <> tname
           hashName     = intermediate <> "_hash"
           hashVar      = loc :< VarUPF hashName
-          coreList     = loc :< ListUPF ((loc :< VarUPF hParam)
+          coreList     = loc :< ListUPF ((loc :< VarUPF hParamName)
                                       : (loc :< VarUPF tname)
                                       : coreSlots)
-          wrappedInner = loc :< LetUPF [(tname, validator)] (wrapBody coreList)
+          wrappedInner = loc :< LetUPF [(locatedName loc tname, validator)] (wrapBody coreList)
           wrapper      = loc :< LamUPF hParam wrappedInner
           udtTuple     = loc :< AppUPF wrapper (loc :< HashUPF wrapper)
-          hashBinding  = (hashName, accessAt loc 0 (loc :< VarUPF intermediate))
+          generated parent name = locatedName (GeneratedLoc name (Just parent)) name
+          hashBinding  = (generated loc hashName, accessAt loc 0 (loc :< VarUPF intermediate))
           mkAccessorBinding idx name =
             (name, accessAt loc idx (loc :< VarUPF intermediate))
           mkHoistedBinding name slot =
             ( name
-            , loc :< LetUPF [ (hParam, hashVar)
-                            , (tname, validator)
+            , loc :< LetUPF [ (locatedName (locatedNameLoc hParam) hParamName, hashVar)
+                            , (locatedName loc tname, validator)
                             ]
                 (wrapBody slot)
             )
-      in (intermediate, udtTuple)
+          intermediateName = generated loc intermediate
+      in (intermediateName, udtTuple)
        : hashBinding
        : zipWith mkAccessorBinding [1 ..] coreNames
-      <> zipWith mkHoistedBinding hoistedNames hoistedSlots
+       <> zipWith mkHoistedBinding hoistedNames hoistedSlots
     _ ->
-      zipWith (\name idx -> (name, accessAt loc idx body)) names [0 ..]
-expandUDT _ = []
+      zipWith (\name idx -> (name, accessAt loc idx body)) locatedNames [0 ..]
 
 -- |Find the final list literal in a UDT body and return a wrapper that
 -- reapplies any surrounding lets. Hoisted methods get the same let
@@ -599,7 +681,7 @@ udtSlots tname = go where
 -- extra ITE.
 autoValidator :: LocTag -> String -> String -> AnnotatedUPT
 autoValidator loc tname hParam =
-  loc :< LamUPF "__udt_v"
+  loc :< LamUPF (locatedName (GeneratedLoc "annotated pattern lambda" (Just loc)) "__udt_v")
     (loc :< ITEUPF
        (loc :< AppUPF
           (loc :< AppUPF
@@ -653,7 +735,7 @@ parseImportOrAssignment = do
       maybeEntry <- optional $ scn *> try parseAssignmentEntry <* scn
       case maybeEntry of
         Nothing    -> fail "Expected either an import statement or an assignment"
-        Just entry -> pure (Right <$> expandAssignmentEntry entry)
+        Just entry -> pure (Right . first locatedNameText <$> expandAssignmentEntry entry)
     Just imp -> pure [Left imp]
 
 parseWithPrelude :: [(String, AnnotatedUPT)]   -- ^Prelude
@@ -662,8 +744,10 @@ parseWithPrelude :: [(String, AnnotatedUPT)]   -- ^Prelude
 parseWithPrelude prelude str = first errorBundlePretty $ runParser (parseTopLevelWithExtraModuleBindings prelude) "" str
 
 parseModule :: String -> Either String [Either AnnotatedUPT (String, AnnotatedUPT)]
-parseModule str = let result = runParser (concat <$> (scn *> many parseImportOrAssignment <* eof)) "" str
-                  in first errorBundlePretty result
+parseModule str = first errorBundlePretty $ parseModuleDetailed str
+
+parseModuleDetailed :: String -> Either (ParseErrorBundle String Void) [Either AnnotatedUPT (String, AnnotatedUPT)]
+parseModuleDetailed = runParser (concat <$> (scn *> many parseImportOrAssignment <* eof)) ""
 
 -- |Parse either a single expression or top level definitions defaulting to the `main` definition.
 --  This function was made for telomare-evaluare
diff --git a/src/Telomare/Possible.hs b/src/Telomare/Possible.hs
index 6cad1a49..f0fc9afd 100644
--- a/src/Telomare/Possible.hs
+++ b/src/Telomare/Possible.hs
@@ -56,7 +56,7 @@ import GHC.Generics (Generic)
 import PrettyPrint
 import Telomare (AbstractRunTime (..), BreakState' (..), FragExpr (..),
                  FragExprF (..), FragExprUR (..), FragIndex, IExpr (..),
-                 IExprF (SetEnvF), LocTag (DummyLoc), PartialType (..),
+                 IExprF (SetEnvF), LocTag (RuntimeLoc), PartialType (..),
                  RecursionPieceFrag, RecursionSimulationPieces (..),
                  RunTimeError (..), TelomareLike (fromTelomare, toTelomare),
                  Term3 (..), Term4 (..),
@@ -1179,7 +1179,7 @@ term4toAbortExpr (Term4 termMap') =
 abortExprToTerm4 :: (Base g ~ f, BasicBase f, StuckBase f, AbortBase f, Foldable f, Recursive g) => g -> Either IExpr Term4
 abortExprToTerm4 x =
   let
-    dl = (DummyLoc :<)
+    dl = (RuntimeLoc :<)
     pv = pure . dl
     findAborted = cata $ \case
       AbortFW (AbortedF e) -> Just e
@@ -1329,7 +1329,7 @@ partiallyAnnotate :: (Base g ~ f, Annotatable1 f, Annotatable g)
 partiallyAnnotate term =
   let runner :: State (PartialType, Set TypeAssociation, Int) (Either TypeCheckError PartialType)
       runner = runExceptT $ anno term
-      initState = (TypeVariable DummyLoc 0, Set.empty, 0)
+      initState = (TypeVariable RuntimeLoc 0, Set.empty, 0)
       (rt, (_, s, _)) = State.runState runner initState
   in (,) <$> rt <*> (flip Map.lookup <$> buildTypeMap s)
 
@@ -1340,7 +1340,7 @@ annotateTree term = do
   let fResolve = fullyResolve resolver
       ca x = anno1 x >>= \a -> pure (fResolve a :< x)
       f = ca <=< sequence
-      initState = (TypeVariable DummyLoc 0, Set.empty, 0)
+      initState = (TypeVariable RuntimeLoc 0, Set.empty, 0)
   flip State.evalState initState . runExceptT $ cata f term
 
 matchType :: PartialType -> PartialType -> Bool
@@ -1356,7 +1356,7 @@ matchType a b = case (a,b) of
 
 matchTypeHead :: (Annotatable1 f, Annotatable g) => PartialType -> f g -> Bool
 matchTypeHead t x =
-  let initState = (TypeVariable DummyLoc 0, Set.empty, 0)
+  let initState = (TypeVariable RuntimeLoc 0, Set.empty, 0)
   in case State.evalState (runExceptT $ anno1 x) initState of
     Left _   -> False
     Right t' -> matchType t' t
@@ -1376,7 +1376,7 @@ instance Validity (Cofree UnsizedExprF PartialType) where
                      ArrTypeP a b -> mv' a <> mv' b
                      PairTypeP a b -> mv' a <> mv' b
                      _ -> Max 0
-                   initState = (TypeVariable DummyLoc startVar, Set.empty, startVar)
+                   initState = (TypeVariable RuntimeLoc startVar, Set.empty, startVar)
                    etb = \case
                      Right True -> True
                      _ -> False
@@ -1416,7 +1416,7 @@ instance GenValidAdj UnsizedExpr where
             resolve = \case
               t@(TypeVariable _ i) -> (fromMaybe t (resolver i))
             f = ca <=< sequence
-            initState = (TypeVariable DummyLoc 0, Set.empty, 0)
+            initState = (TypeVariable RuntimeLoc 0, Set.empty, 0)
         flip State.evalState initState . runExceptT $ cata f term
       ppax = case annoTerm x of
         Left z   -> "toGennable ppax bad: " <> show z
diff --git a/src/Telomare/PossibleData.hs b/src/Telomare/PossibleData.hs
index 79b0b6be..9da267ad 100644
--- a/src/Telomare/PossibleData.hs
+++ b/src/Telomare/PossibleData.hs
@@ -909,8 +909,8 @@ data TypeCheckError
 newPartialType :: AnnotateState PartialType
 newPartialType = do
   (env, typeMap, v) <- State.get
-  State.put (TypeVariable DummyLoc v, typeMap, v + 1)
-  pure $ TypeVariable DummyLoc v
+  State.put (TypeVariable RuntimeLoc v, typeMap, v + 1)
+  pure $ TypeVariable RuntimeLoc v
 
 makeAssociations :: PartialType -> PartialType -> Either TypeCheckError (Set TypeAssociation)
 makeAssociations ta tb = case (ta, tb) of
@@ -971,10 +971,10 @@ instance Annotatable1 PartExprF where
 withNewEnv :: AnnotateState a -> AnnotateState (PartialType, a)
 withNewEnv action = do
   (env, typeMap, v) <- State.get
-  State.put (TypeVariable DummyLoc v, typeMap, v + 1)
+  State.put (TypeVariable RuntimeLoc v, typeMap, v + 1)
   result <- action
   State.modify $ \(_, typeMap, v) -> (env, typeMap, v)
-  pure (TypeVariable DummyLoc v, result)
+  pure (TypeVariable RuntimeLoc v, result)
 
 instance Annotatable1 StuckF where
   liftAnno anno = \case
diff --git a/src/Telomare/Resolver.hs b/src/Telomare/Resolver.hs
index 6b70d650..43a6c421 100644
--- a/src/Telomare/Resolver.hs
+++ b/src/Telomare/Resolver.hs
@@ -101,7 +101,7 @@ fitPatternVarsToCasedUPT p aupt@(anno :< _) = applyVars2UPT varsOnUPT $ pattern2
                 -> AnnotatedUPT
   applyVars2UPT m = \case
     anno :< LamUPF str x ->
-      case Map.lookup str m of
+      case Map.lookup (locatedNameText str) m of
         Just a  -> anno :< AppUPF (anno :< LamUPF str (applyVars2UPT m x)) a
         Nothing -> anno :< LamUPF str x
     x -> x
@@ -111,7 +111,7 @@ varsUPT :: UnprocessedParsedTerm -> Set String
 varsUPT = cata alg where
   alg :: Base UnprocessedParsedTerm (Set String) -> Set String
   alg (VarUPF n)     = Set.singleton n
-  alg (LamUPF str x) = del str x
+  alg (LamUPF str x) = del (locatedNameText str) x
   alg e              = F.fold e
   del :: String -> Set String -> Set String
   del n x = if Set.member n x then Set.delete n x else x
@@ -122,7 +122,7 @@ freeVarsDeep :: UnprocessedParsedTerm -> Set String
 freeVarsDeep = cata alg where
   alg :: Base UnprocessedParsedTerm (Set String) -> Set String
   alg (VarUPF n)           = Set.singleton n
-  alg (LamUPF n body)      = Set.delete n body
+  alg (LamUPF n body)      = Set.delete (locatedNameText n) body
   alg (CaseUPF scrut alts) = scrut <> foldMap (\(p, body) -> patternRefs p <> body) alts <> caseRefs
     where
       caseRefs = Set.fromList ["and", "listEqual", "foldl", "abort"]
@@ -157,7 +157,7 @@ mkLambda4FreeVarUPs aupt@(anno :< _) = tag anno $ go upt freeVars where
   go :: UnprocessedParsedTerm -> [String] -> UnprocessedParsedTerm
   go x = \case
     []     -> x
-    (y:ys) -> LamUP y $ go x ys
+    (y:ys) -> LamUP (locatedName UnknownLoc y) $ go x ys
 
 findPatternVars :: LocTag -> Pattern -> Map String (AnnotatedUPT -> AnnotatedUPT)
 findPatternVars anno = cata alg where
@@ -211,16 +211,16 @@ mkCaseAlternative casedUPT@(anno :< _) caseResult p = appVars2ResultLambdaAlts p
                            -> AnnotatedUPT
   appVars2ResultLambdaAlts m = \case
     lam@(_ :< LamUPF varName upt) ->
-      case Map.lookup varName m of
+      case Map.lookup (locatedNameText varName) m of
         Nothing -> lam
-        Just x -> anno :< AppUPF (anno :< LamUPF varName (appVars2ResultLambdaAlts (Map.delete varName m) upt)) x
+        Just x -> anno :< AppUPF (anno :< LamUPF varName (appVars2ResultLambdaAlts (Map.delete (locatedNameText varName) m) upt)) x
     x -> x
   makeLambdas :: AnnotatedUPT
               -> [String]
               -> AnnotatedUPT
   makeLambdas aupt@(anno' :< _) = \case
     []     -> aupt
-    (x:xs) -> anno' :< LamUPF x (makeLambdas aupt xs)
+    (x:xs) -> anno' :< LamUPF (locatedName anno' x) (makeLambdas aupt xs)
 
 case2annidatedIfs :: AnnotatedUPT -- ^ Term to be pattern matched
                   -> [Pattern] -- ^ All patterns in a case expression
@@ -405,20 +405,20 @@ validateVariables term =
           -- Build dependency graph
           let dependencies :: Map String (Set String)
               dependencies = Map.fromList
-                [(name, Set.fromList $ getDirectDeps def) | (name, def) <- preludeMap]
+                [(locatedNameText name, Set.fromList $ getDirectDeps def) | (name, def) <- preludeMap]
 
               -- Get direct variable dependencies (only those defined in this let block)
               -- Uses Set to properly handle lambda-bound variable shadowing
-              letBindingNames = Set.fromList (fmap fst preludeMap)
+              letBindingNames = Set.fromList (letBindingName <$> preludeMap)
               getDirectDeps :: AnnotatedUPT -> [String]
               getDirectDeps = Set.toList . cata alg where
                 alg :: CofreeF UnprocessedParsedTermF LocTag (Set String) -> Set String
                 alg = \case
                     (_ C.:< VarUPF n) -> if Set.member n letBindingNames then Set.singleton n else Set.empty
-                    (_ C.:< LamUPF v body) -> Set.delete v body
+                    (_ C.:< LamUPF v body) -> Set.delete (locatedNameText v) body
                     (_ C.:< LetUPF binds body) ->
-                      let boundNames = Set.fromList (fmap fst binds)
-                          bindDeps = foldMap snd binds
+                      let boundNames = Set.fromList (letBindingName <$> binds)
+                          bindDeps = foldMap letBindingValue binds
                       in Set.union (bindDeps Set.\\ boundNames) (body Set.\\ boundNames)
                     (_ C.:< ITEUPF i t e) -> i <> t <> e
                     (_ C.:< PairUPF a b) -> a <> b
@@ -433,7 +433,7 @@ validateVariables term =
                     _ -> Set.empty
 
           -- Check if original order works (no forward references)
-          let originalOrder = fmap fst preludeMap
+          let originalOrder = letBindingName <$> preludeMap
               hasForwardRef = any (\(i, name) ->
                 let deps = Map.findWithDefault Set.empty name dependencies
                     laterNames = Set.fromList $ drop (i + 1) originalOrder
@@ -473,8 +473,8 @@ validateVariables term =
               Left cycle -> State.lift . Left $ cycle
               Right sortedNames ->
                 pure [(name, def) | name <- sortedNames,
-                      (name', def) <- preludeMap, name == name']
-            else pure preludeMap  -- Keep original order
+                      (name', def) <- preludeMap, name == locatedNameText name']
+            else pure $ first locatedNameText <$> preludeMap  -- Keep original order
 
           -- Process bindings in order
           forM_ sortedBindings $ \(name, def) -> do
@@ -486,15 +486,15 @@ validateVariables term =
           pure result
         anno :< LamUPF v x -> do
           oldState <- State.get
-          State.modify (Map.insert v (anno :< TVarF v))
+          State.modify (Map.insert (locatedNameText v) (anno :< TVarF (locatedNameText v)))
           result <- validateWithEnvironment x
           State.put oldState
-          pure $ openLambda v result
+          pure $ openLambda (locatedNameText v) result
         anno :< VarUPF n -> do
           definitionsMap <- State.get
           case Map.lookup n definitionsMap of
             Just v -> pure v
-            _      -> State.lift . Left $ MissingDefinitions [n]
+            _      -> State.lift . Left $ MissingDefinitionAt anno n
 
         anno :< ITEUPF i t e -> (\a b c -> anno :< TITEF a b c) <$> validateWithEnvironment i
                                                                 <*> validateWithEnvironment t
@@ -531,11 +531,11 @@ annotateUnsizedCount = capTop . flip evalStateT 0 . cata f where
         lift (Set.singleton n, (anno, 0) :< AppUPF ((anno, 0) :< nur) ((anno, 0) :< VarUPF (':' : show n)))
       LetUPF bindings inner -> (\b i -> (anno, 0) :< LetUPF b i) <$> traverse rebind bindings <*> inner
       x -> ((anno, 0) :<) <$> sequence x
-  rebind (n, x) = cap n $ evalStateT x 0
-  cap n (vs, x@((anno, _) :< _)) = lift (Set.empty, (n, foldr (\v b -> (anno, length vs) :< LamUPF (':' : show v) b) x vs))
+  rebind (n, x) = (\(n', x') -> (n, x')) <$> cap (locatedNameText n) (evalStateT x 0)
+  cap n (vs, x@((anno, _) :< _)) = lift (Set.empty, (n, foldr (\v b -> (anno, length vs) :< LamUPF (locatedName anno (':' : show v)) b) x vs))
   -- HACK vars are just placehorders for next step
   capTop (vs, x@((anno, _) :< _)) =
-    foldr (\v b -> (anno, length vs) :< AppUPF ((anno, 0) :< LamUPF (':' : show v) b) ((anno, 0) :< VarUPF (':' : show v))) x vs
+    foldr (\v b -> (anno, length vs) :< AppUPF ((anno, 0) :< LamUPF (locatedName anno (':' : show v)) b) ((anno, 0) :< VarUPF (':' : show v))) x vs
 
 
 -- convert let bindings to nested lambda/app brackets
@@ -575,23 +575,24 @@ letsToApps term =
       getTransitive' deps = mconcat . fmap (getTransitive deps) . Set.toList
       makeBindingsAsoc (name, def) = case runWriterT def of
         Left s           -> Left s
-        Right (nx, refs) -> pure (name, (nx,refs))
+        Right (nx, refs) -> pure (locatedNameText name, (nx,refs))
       -- f algebra builds Term1 wrapped with metadata (WriterT) of unbound refs (Set String) or ResolverError
       buildRefs :: CofreeF UnprocessedParsedTermF (LocTag, Int) (WriterT (Set String) (Either ResolverError) (Cofree (ParserTermF String String) (LocTag, Int)))
                    -> WriterT (Set String) (Either ResolverError) (Cofree (ParserTermF String String) (LocTag, Int))
       buildRefs ((anno, urC) CofreeT.:< upf) = case upf of
         VarUPF n -> writer ((anno, urC) :< TVarF n, Set.singleton n)
         LamUPF v x -> f (runWriterT x) where
-          f (Right (nx, refs)) = let nrefs = Set.delete v refs in if null nrefs && urC == 0
-            then writer ((anno, urC) :< TLamF (Closed v) nx, nrefs)
-            else writer ((anno, urC) :< TLamF (Open v) nx, nrefs)
+          name = locatedNameText v
+          f (Right (nx, refs)) = let nrefs = Set.delete name refs in if null nrefs && urC == 0
+            then writer ((anno, urC) :< TLamF (Closed name) nx, nrefs)
+            else writer ((anno, urC) :< TLamF (Open name) nx, nrefs)
           f (Left s)           = lift $ Left s
         LetUPF bindings inner -> case runWriterT inner of
           Left s -> lift $ Left s
           Right (nInner, refs) -> WriterT $ do
             -- Build dependency graph
             nBindings <- traverse makeBindingsAsoc bindings
-            let originalOrder = fmap fst bindings
+            let originalOrder = letBindingName <$> bindings
                 dependencies = Map.fromList $ fmap (second snd) nBindings
                 sortedBindings :: Either ResolverError [(String, Cofree (ParserTermF String String) (LocTag, Int))]
                 sortedBindings =
@@ -650,8 +651,8 @@ optimizeBuiltinFunctions = transform optimize where
         VarUPF "left"  -> anno0 :< LeftUPF x
         VarUPF "right" -> anno0 :< RightUPF x
         VarUPF "trace" -> anno0 :< TraceUPF x
-        VarUPF "pair"  -> anno0 :< LamUPF "y" (anno1 :< PairUPF x (anno1 :< VarUPF "y"))
-        VarUPF "app"   -> anno0 :< LamUPF "y" (anno1 :< AppUPF x (anno1 :< VarUPF "y"))
+        VarUPF "pair"  -> anno0 :< LamUPF (locatedName anno0 "y") (anno1 :< PairUPF x (anno1 :< VarUPF "y"))
+        VarUPF "app"   -> anno0 :< LamUPF (locatedName anno0 "y") (anno1 :< AppUPF x (anno1 :< VarUPF "y"))
         _             -> oneApp
         -- VarUP "check" TODO
     x -> x
@@ -673,15 +674,18 @@ generateAllHashes x@(anno :< _) = transform interm x where
     x                      -> x
 
 addBuiltins :: AnnotatedUPT -> AnnotatedUPT
-addBuiltins aupt = DummyLoc :< LetUPF
-  [ ("zero", DummyLoc :< IntUPF 0)
-  , ("left", DummyLoc :< LamUPF "x" (DummyLoc :< LeftUPF (DummyLoc :< VarUPF "x")))
-  , ("right", DummyLoc :< LamUPF "x" (DummyLoc :< RightUPF (DummyLoc :< VarUPF "x")))
-  , ("trace", DummyLoc :< LamUPF "x" (DummyLoc :< TraceUPF (DummyLoc :< VarUPF "x")))
-  , ("pair", DummyLoc :< LamUPF "x" (DummyLoc :< LamUPF "y" (DummyLoc :< PairUPF (DummyLoc :< VarUPF "x") (DummyLoc :< VarUPF "y"))))
-  , ("app", DummyLoc :< LamUPF "x" (DummyLoc :< LamUPF "y" (DummyLoc :< AppUPF (DummyLoc :< VarUPF "x") (DummyLoc :< VarUPF "y"))))
+addBuiltins aupt = GeneratedLoc "addBuiltins" Nothing :< LetUPF
+  [ bind "zero" (builtin "zero" :< IntUPF 0)
+  , bind "left" (builtin "left" :< LamUPF (locatedName (builtin "left") "x") (builtin "left" :< LeftUPF (builtin "left" :< VarUPF "x")))
+  , bind "right" (builtin "right" :< LamUPF (locatedName (builtin "right") "x") (builtin "right" :< RightUPF (builtin "right" :< VarUPF "x")))
+  , bind "trace" (builtin "trace" :< LamUPF (locatedName (builtin "trace") "x") (builtin "trace" :< TraceUPF (builtin "trace" :< VarUPF "x")))
+  , bind "pair" (builtin "pair" :< LamUPF (locatedName (builtin "pair") "x") (builtin "pair" :< LamUPF (locatedName (builtin "pair") "y") (builtin "pair" :< PairUPF (builtin "pair" :< VarUPF "x") (builtin "pair" :< VarUPF "y"))))
+  , bind "app" (builtin "app" :< LamUPF (locatedName (builtin "app") "x") (builtin "app" :< LamUPF (locatedName (builtin "app") "y") (builtin "app" :< AppUPF (builtin "app" :< VarUPF "x") (builtin "app" :< VarUPF "y"))))
   ]
   aupt
+  where
+    builtin = BuiltinLoc
+    bind name value = (locatedName (builtin name) name, value)
 
 -- |Process an `AnnotatedUPT` to a `Term3` with failing capability.
 process :: AnnotatedUPT
@@ -779,7 +783,10 @@ resolveMain allModules mainModule = case lookup mainModule allModules of
                   maybeMain = lookup "main" resolved
               in case maybeMain of
                    Nothing -> Left $ NoMainFunction mainModule
-                   Just x  -> Right $ DummyLoc :< LetUPF (pruneBindings x resolved) x
+                   Just x ->
+                     let loc = case x of loc' :< _ -> loc'
+                         locatedBindings = first (locatedName (GeneratedLoc "resolveMain.binding" (Just loc))) <$> pruneBindings x resolved
+                     in Right $ GeneratedLoc "resolveMain" (Just loc) :< LetUPF locatedBindings x
 
 main2Term3 :: [(String, [Either AnnotatedUPT (String, AnnotatedUPT)])] -- ^Modules: [(ModuleName, [Either Import (VariableName, BindedUPT)])]
            -> String -- ^Module name with main
diff --git a/src/Telomare/TypeChecker.hs b/src/Telomare/TypeChecker.hs
index 02b830ed..70270ef3 100644
--- a/src/Telomare/TypeChecker.hs
+++ b/src/Telomare/TypeChecker.hs
@@ -127,7 +127,10 @@ initState (Term3 termMap) =
   let startVariable = case Set.maxView (Map.keysSet termMap) of
         Nothing               -> 0
         Just (FragIndex i, _) -> (i + 1) * 2
-  in (TypeVariable DummyLoc 0, Set.empty, startVariable)
+      rootLoc = case Map.lookup (FragIndex 0) termMap of
+        Just (FragExprUR (anno :< _)) -> GeneratedLoc "typechecker.root" (Just anno)
+        Nothing                       -> GeneratedLoc "typechecker.root" Nothing
+  in (TypeVariable rootLoc 0, Set.empty, startVariable)
 
 getFragType :: LocTag -> FragIndex -> PartialType
 getFragType anno (FragIndex i) = ArrTypeP (TypeVariable anno $ i * 2) (TypeVariable anno $ i * 2 + 1)
@@ -171,7 +174,10 @@ annotate (Term3 termMap) =
       associateOutType :: LocTag -> FragIndex -> PartialType -> AnnotateState ()
       associateOutType anno fi ot = let (ArrTypeP _ ot2) = getFragType anno fi in associateVar ot ot2
       rootType anno = initInputType anno (FragIndex 0) >> annotate' (unFragExprUR $ rootFrag termMap)
-  in sequence_ (Map.mapWithKey (\k v -> initInputType DummyLoc k >> annotate' (unFragExprUR v) >>= associateOutType DummyLoc k) termMap) >> rootType DummyLoc
+      fragLoc (FragExprUR (anno :< _)) = GeneratedLoc "typechecker.fragment" (Just anno)
+      rootLoc = case rootFrag termMap of
+        FragExprUR (anno :< _) -> GeneratedLoc "typechecker.root" (Just anno)
+  in sequence_ (Map.mapWithKey (\k v -> let loc = fragLoc v in initInputType loc k >> annotate' (unFragExprUR v) >>= associateOutType loc k) termMap) >> rootType rootLoc
 
 partiallyAnnotate :: Term3 -> Either TypeCheckError (PartialType, Int -> Maybe PartialType)
 partiallyAnnotate term =
@@ -188,7 +194,7 @@ typeCheck :: PartialType -> Term3 -> Maybe TypeCheckError
 typeCheck t tm@(Term3 typeMap) = convert (partiallyAnnotate tm >>= associate) where
   associate (ty, resolver) = debugTrace ("COMPARING TYPES " <> show (t, fullyResolve resolver ty) <> "\n" <> debugMap ty resolver)
     . traceAgain $ makeAssociations (fullyResolve resolver ty) t
-  debugMap ty resolver = showTypeDebugInfo (TypeDebugInfo tm (fullyResolve resolver . getFragType DummyLoc)
+  debugMap ty resolver = showTypeDebugInfo (TypeDebugInfo tm (fullyResolve resolver . getFragType (GeneratedLoc "typechecker.debug" Nothing))
                                             (fullyResolve resolver ty))
   traceAgain s = debugTrace ("Resulting thing " <> show s) s
   convert = \case
diff --git a/telomare.cabal b/telomare.cabal
index 17436fc0..84d15644 100644
--- a/telomare.cabal
+++ b/telomare.cabal
@@ -170,16 +170,20 @@ executable telomare-lsp
   hs-source-dirs:      app
 
   build-depends:       base
-                     , containers
-                     , lens
-                     , lsp
-                     , lsp-types
-                     , mtl
-                     , filepath
-                     , stm
-                     , telomare
-                     , text
-                     , aeson
+                      , containers
+                      , directory
+                      , filepath
+                      , free
+                      , lens
+                      , lsp
+                      , lsp-types
+                      , megaparsec
+                      , process
+                      , stm
+                      , telomare
+                      , text
+                      , time
+                      , aeson
 
   default-language:    Haskell2010
   ghc-options:         -Wall
diff --git a/test/CaseTests.hs b/test/CaseTests.hs
index a520014f..1fa581e4 100644
--- a/test/CaseTests.hs
+++ b/test/CaseTests.hs
@@ -30,7 +30,7 @@ caseExprStrWithPattern :: Pattern -> String
 caseExprStrWithPattern p = unlines
   [ "import Prelude"
   , "main ="
-  , "  let toCase = " <> (show . PrettyUPT . forget . pattern2UPT DummyLoc $ p)
+  , "  let toCase = " <> (show . PrettyUPT . forget . pattern2UPT UnknownLoc $ p)
   , "      caseTest ="
   , "        case toCase of"
   , "          " <> (show . PrettyPattern $ p) <> " -> \"True\""
@@ -42,7 +42,7 @@ caseExprStrWithPatternIgnore :: Pattern -> String
 caseExprStrWithPatternIgnore p = unlines
   [ "import Prelude"
   , "main ="
-  , "  let toCase = " <> (show . PrettyUPT . forget . pattern2UPT DummyLoc $ p)
+  , "  let toCase = " <> (show . PrettyUPT . forget . pattern2UPT UnknownLoc $ p)
   , "      caseTest ="
   , "        case toCase of"
   , "          _ -> \"True\""
diff --git a/test/Common.hs b/test/Common.hs
index 1a4c9c99..9893bb5f 100644
--- a/test/Common.hs
+++ b/test/Common.hs
@@ -151,17 +151,17 @@ genTypedTree' :: Maybe DataType -> DataType -> Int -> Gen (BreakState' Recursion
 genTypedTree' ti t i =
   let half = div i 2
       optionEnv = if ti == Just t
-                  then (pure (pure $ DummyLoc :< EnvFragF) :)
+                  then (pure (pure $ UnknownLoc :< EnvFragF) :)
                   else id
       optionGate ti' to = if ti' == ZeroType
-                          then ((liftA2 (\x y -> DummyLoc :< GateFragF x y) <$> genTypedTree' ti to half <*> genTypedTree' ti to half) :)
+                          then ((liftA2 (\x y -> UnknownLoc :< GateFragF x y) <$> genTypedTree' ti to half <*> genTypedTree' ti to half) :)
                           else id
       setEnvOption to = arbitrary >>= makeSetEnv where
-        makeSetEnv ti' = fmap ((DummyLoc :<) . SetEnvFragF) <$> genTypedTree' ti (PairType (ArrType ti' to) ti') (i - 1)
-      leftOption to = arbitrary >>= (\ti' -> fmap ((DummyLoc :<) . LeftFragF) <$> genTypedTree' ti (PairType to ti') (i - 1))
-      rightOption to = arbitrary >>= (\ti' -> fmap ((DummyLoc :<) . RightFragF) <$> genTypedTree' ti (PairType ti' to) (i - 1))
+        makeSetEnv ti' = fmap ((UnknownLoc :<) . SetEnvFragF) <$> genTypedTree' ti (PairType (ArrType ti' to) ti') (i - 1)
+      leftOption to = arbitrary >>= (\ti' -> fmap ((UnknownLoc :<) . LeftFragF) <$> genTypedTree' ti (PairType to ti') (i - 1))
+      rightOption to = arbitrary >>= (\ti' -> fmap ((UnknownLoc :<) . RightFragF) <$> genTypedTree' ti (PairType ti' to) (i - 1))
   in oneof . optionEnv $ case t of
-    ZeroType -> pure (pure $ DummyLoc :< ZeroFragF) :
+    ZeroType -> pure (pure $ UnknownLoc :< ZeroFragF) :
      if i < 1
      then []
      else [ genTypedTree' ti (PairType ZeroType ZeroType) i
@@ -170,7 +170,7 @@ genTypedTree' ti t i =
           , rightOption ZeroType
           ]
     PairType ta tb ->
-      (liftA2 (\x y -> DummyLoc :< PairFragF x y) <$> genTypedTree' ti ta half <*> genTypedTree' ti tb half) :
+      (liftA2 (\x y -> UnknownLoc :< PairFragF x y) <$> genTypedTree' ti ta half <*> genTypedTree' ti tb half) :
       if i < 1
       then []
       else [ setEnvOption (PairType ta tb)
@@ -200,7 +200,7 @@ instance Arbitrary URTestExpr where -- TODO needs to be tested since refactor
       , genTypedTree' Nothing ZeroType
       ]
       where wrapWithUR [t, r, b, i] =
-              appF (unsizedRecursionWrapper DummyLoc t r b) i
+              appF (unsizedRecursionWrapper UnknownLoc t r b) i
 
 
 typeable x = case inferType (fromTelomare $ getIExpr x) of
@@ -263,22 +263,20 @@ instance Arbitrary UnprocessedParsedTerm where
                                    , LeftUP <$> recur (i - 1)
                                    , RightUP <$> recur (i - 1)
                                    , TraceUP <$> recur (i - 1)
-                                   , elements lambdaTerms >>= \var -> LamUP var <$> genTree (var : varList) (i - 1)
+                                    , elements lambdaTerms >>= \var -> LamUP (locatedName UnknownLoc var) <$> genTree (var : varList) (i - 1)
                                    , ITEUP <$> recur third <*> recur third <*> recur third
                                    , UnsizedRecursionUP <$> recur third <*> recur third <*> recur third
                                    , ListUP <$> childList
-                                   , do
-                                      -- listSize <- chooseInt (1, max i 1)
-                                      listSize <- choose (2, max i 2)
-                                      let childShare = div i listSize
-                                      let makeList = \case
-                                            [] -> pure []
-                                            (v:vl) -> do
-                                              newTree <- genTree (v:varList) childShare
-                                              ((v,newTree) :) <$> makeList vl
-                                      vars <- take listSize <$> identifierList
-                                      childList <- makeList vars
-                                      pure $ LetUP (init childList) (snd . last $ childList)
+                                    , do { listSize <- choose (2, max i 2)
+                                         ; let childShare = div i listSize
+                                               makeList [] = pure []
+                                               makeList (v:vl) = do
+                                                  newTree <- genTree (v:varList) childShare
+                                                  ((locatedName UnknownLoc v, newTree) :) <$> makeList vl
+                                         ; vars <- take listSize <$> identifierList
+                                         ; childList <- makeList vars
+                                         ; pure $ LetUP (init childList) (letBindingValue . last $ childList)
+                                         }
                                    , PairUP <$> recur half <*> recur half
                                    , AppUP <$> recur half <*> recur half
                                    ]
@@ -309,7 +307,7 @@ instance Arbitrary UnprocessedParsedTerm where
       _ -> let shrinkBinding (n, v) = map (n,) $ shrink v
            in snd (head l) : LetUP (tail l) i : map (flip LetUP i . second shrink) l
 -}
-    LetUP l i -> let shrinkBinding (n, v) = ((n,) <$> shrink v)
+    LetUP l i -> let shrinkBinding (n, v) = (n,) <$> shrink v
                      removeAt n x = let (f,s) = splitAt n x in (f <> tail s)
                      makeOptions f n [] = error "debugging split here"
                      makeOptions f n x = let (pa,c:pz) = splitAt n x in ((pa ++) . (:pz) <$> f c)
@@ -325,8 +323,8 @@ instance Arbitrary Term1 where
     leaves :: [String] -> Gen Term1
     leaves varList =
       oneof $
-          (if not (null varList) then (((DummyLoc :<) . TVarF <$> elements varList) :) else id)
-          [ pure $ DummyLoc :< TZeroF
+          (if not (null varList) then (((UnknownLoc :<) . TVarF <$> elements varList) :) else id)
+          [ pure $ UnknownLoc :< TZeroF
           ]
     lambdaTerms = ["w", "x", "y", "z"]
     letTerms = fmap (("l" <>) . show) [1..255]
@@ -348,15 +346,15 @@ instance Arbitrary Term1 where
                                  0 -> leaves varList
                                  x -> oneof
                                    [ leaves varList
-                                   , (DummyLoc :<) . THashF <$> recur (i - 1)
-                                   , (DummyLoc :<) . TLeftF <$> recur (i - 1)
-                                   , (DummyLoc :<) . TRightF <$> recur (i - 1)
-                                   , (DummyLoc :<) . TTraceF <$> recur (i - 1)
-                                   , elements lambdaTerms >>= \var -> (DummyLoc :<) . TLamF (Open var) <$> genTree (var : varList) (i - 1)
-                                   , (\a b c -> DummyLoc :< TITEF a b c) <$> recur third <*> recur third <*> recur third
-                                   , (\a b c -> DummyLoc :< TLimitedRecursionF a b c) <$> recur third <*> recur third <*> recur third
-                                   , (\a b -> DummyLoc :< TPairF a b) <$> recur half <*> recur half
-                                   , (\a b -> DummyLoc :< TAppF a b) <$> recur half <*> recur half
+                                   , (UnknownLoc :<) . THashF <$> recur (i - 1)
+                                   , (UnknownLoc :<) . TLeftF <$> recur (i - 1)
+                                   , (UnknownLoc :<) . TRightF <$> recur (i - 1)
+                                   , (UnknownLoc :<) . TTraceF <$> recur (i - 1)
+                                   , elements lambdaTerms >>= \var -> (UnknownLoc :<) . TLamF (Open var) <$> genTree (var : varList) (i - 1)
+                                   , (\a b c -> UnknownLoc :< TITEF a b c) <$> recur third <*> recur third <*> recur third
+                                   , (\a b c -> UnknownLoc :< TLimitedRecursionF a b c) <$> recur third <*> recur third <*> recur third
+                                   , (\a b -> UnknownLoc :< TPairF a b) <$> recur half <*> recur half
+                                   , (\a b -> UnknownLoc :< TAppF a b) <$> recur half <*> recur half
                                    ]
   shrink = \case
     _ :< TZeroF -> []
diff --git a/test/NatUDTTests.hs b/test/NatUDTTests.hs
index ceb47dc3..b81e8c71 100644
--- a/test/NatUDTTests.hs
+++ b/test/NatUDTTests.hs
@@ -58,7 +58,7 @@ evalUDTExpr input = do
   case runParser (parseLongExpr <* eof) "" input of
     Left err -> pure $ Left (errorBundlePretty err)
     Right aupt -> do
-      let term = DummyLoc :< LetUPF (pruneBindings aupt allBindings) aupt
+      let term = UnknownLoc :< LetUPF (first (locatedName UnknownLoc) <$> pruneBindings aupt allBindings) aupt
           compile' :: Term3 -> Either EvalError CompiledExpr
           compile' = compile (DebugSizing (SizingSettings 255 False)) runStaticChecks
       case first RE (process term) >>= compile' of
diff --git a/test/ParserTests.hs b/test/ParserTests.hs
index ed755884..21e06c5a 100644
--- a/test/ParserTests.hs
+++ b/test/ParserTests.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE LambdaCase          #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
 module Main where
@@ -15,6 +16,7 @@ import Data.Bifunctor
 import Data.Either (fromRight)
 import Data.Functor.Foldable
 import Data.List
+import qualified Data.List.NonEmpty as NE
 import Data.Map (Map, fromList, toList)
 import qualified Data.Map as Map
 import Data.Ord
@@ -47,6 +49,47 @@ unitTests = testGroup "Unit tests"
   [ testCase "parse uniqueUP" $ do
       res <- parseSuccessful parseHash "# (\\x -> x)"
       res @?= True
+    -- Keep structured Megaparsec errors available for LSP ranges while
+    -- preserving pretty text for CLI-style diagnostics.
+  , testCase "parseModuleDetailed exposes parse error offsets for diagnostics" $ do
+      case parseModuleDetailed "main = if 0 then 1" of
+        Left bundle -> do
+          errorOffset (NE.head $ bundleErrors bundle) >= 0 @?= True
+          null (errorBundlePretty bundle) @?= False
+        Right _     -> assertFailure "expected parse error"
+    -- Source spans must cover only the token, not whitespace consumed by
+    -- lexeme wrappers, otherwise editor diagnostics underline too much.
+  , testCase "variable source spans exclude trailing whitespace" $ do
+      case runParser parseVariable "" "foo   0" of
+        Left err -> assertFailure $ errorBundlePretty err
+        Right (SourceLoc span :< VarUPF "foo") -> do
+          sourcePositionLine (sourceSpanStart span) @?= 1
+          sourcePositionColumn (sourceSpanStart span) @?= 1
+          sourcePositionLine (sourceSpanEnd span) @?= 1
+          sourcePositionColumn (sourceSpanEnd span) @?= 4
+        Right parsed -> assertFailure $ "unexpected parse result: " <> show parsed
+  , testCase "let binding source spans exclude trailing whitespace" $ do
+      case runParser parseLongExpr "" "let foo   = 0 in foo" of
+        Left err -> assertFailure $ errorBundlePretty err
+        Right (_ :< LetUPF [(name, _)] _) | SourceLoc span <- locatedNameLoc name -> do
+          locatedNameText name @?= "foo"
+          sourcePositionLine (sourceSpanStart span) @?= 1
+          sourcePositionColumn (sourceSpanStart span) @?= 5
+          sourcePositionLine (sourceSpanEnd span) @?= 1
+          sourcePositionColumn (sourceSpanEnd span) @?= 8
+        Right parsed -> assertFailure $ "unexpected parse result: " <> show parsed
+  , testCase "lambda binding source spans exclude trailing whitespace" $ do
+      case runParser parseLongExpr "" "\\foo   -> foo" of
+        Left err -> assertFailure $ errorBundlePretty err
+        Right (_ :< LamUPF binder _) -> case locatedNameLoc binder of
+          SourceLoc span -> do
+            locatedNameText binder @?= "foo"
+            sourcePositionLine (sourceSpanStart span) @?= 1
+            sourcePositionColumn (sourceSpanStart span) @?= 2
+            sourcePositionLine (sourceSpanEnd span) @?= 1
+            sourcePositionColumn (sourceSpanEnd span) @?= 5
+          loc -> assertFailure $ "unexpected lambda binder location: " <> show loc
+        Right parsed -> assertFailure $ "unexpected parse result: " <> show parsed
   , testCase "test function applied to a string that has whitespaces in both sides inside a structure" $ do
       res1 <- parseSuccessful parseLongExpr "(foo \"woops\" , 0)"
       res2 <- parseSuccessful parseLongExpr "(foo \"woops\" )"
@@ -184,7 +227,7 @@ unitTests = testGroup "Unit tests"
       res `compare` False @?= EQ
   , testCase "Case within top level definitions" $ do
       res' <- runTelomareParser parseTopLevel caseExpr0
-      let res = forget res'
+      let res = stripParserLocs $ forget res'
       res @?= caseExpr0UPT
   , testCase "Simple import parsing" $ do
       res' <- runTelomareParser parseImport importExpr0str
@@ -212,15 +255,21 @@ importQualifiedExpr0 = ImportQualifiedUP "F" "Foo"
 importExpr0str = "import Foo"
 importExpr0 = ImportUP "Foo"
 
+stripParserLocs :: UnprocessedParsedTerm -> UnprocessedParsedTerm
+stripParserLocs = cata $ \case
+  LetUPF bindings body -> LetUP ((\(name, value) -> (locatedName UnknownLoc $ locatedNameText name, value)) <$> bindings) body
+  LamUPF name body -> LamUP (locatedName UnknownLoc $ locatedNameText name) body
+  other -> embed other
+
 caseExpr0UPT =
-  LetUP [ ("foo", LamUP "a" (CaseUP (VarUP "a")
+  LetUP [ (locatedName UnknownLoc "foo", LamUP (locatedName UnknownLoc "a") (CaseUP (VarUP "a")
                                [ (PatternInt 0,VarUP "a")
                                , (PatternVar "x",AppUP (VarUP "succ") (VarUP "a"))
                                ]))
-        , ("main", LamUP "i" (PairUP (StringUP "Success")
+        , (locatedName UnknownLoc "main", LamUP (locatedName UnknownLoc "i") (PairUP (StringUP "Success")
                                      (IntUP 0)))
         ]
-        (LamUP "i" (PairUP (StringUP "Success") (IntUP 0)))
+        (LamUP (locatedName UnknownLoc "i") (PairUP (StringUP "Success") (IntUP 0)))
 caseExpr0 = unlines
   [ "foo = \\a -> case a of"
   , "              0 -> a"
diff --git a/test/ResolverTests.hs b/test/ResolverTests.hs
index 68254040..029f9c48 100644
--- a/test/ResolverTests.hs
+++ b/test/ResolverTests.hs
@@ -14,7 +14,7 @@ import Control.Monad.Except (ExceptT, MonadError, catchError, runExceptT,
                              throwError)
 import Data.Algorithm.Diff (getGroupedDiff)
 import Data.Algorithm.DiffOutput (ppDiff)
-import Data.List (isInfixOf, sortOn)
+import Data.List (isInfixOf, isPrefixOf, sortOn)
 import Debug.Trace (trace, traceShow, traceShowId)
 import System.IO
 import qualified System.IO.Strict as Strict
@@ -47,54 +47,52 @@ tests = testGroup "Tests" [unitTests, qcProps, unitTestsCase, qcPropsCase]
 ------ Property Tests
 ---------------------
 qcProps = testGroup "Property tests (QuickCheck)"
-  [ QC.testProperty "Check recursive let work backward" $
-      \() -> withMaxSuccess 16 . QC.idempotentIOProperty $ do
-        assignments <- generate genRecursiveLet
+  [ QC.testProperty "Check recursive let work backward"
+      . withMaxSuccess 16
+      . QC.forAll genRecursiveLet $ \assignments -> QC.idempotentIOProperty $ do
         let dummymodule = wrapRecursiveBackwardLet assignments
             expectedValue = recursiveLetResult assignments <> "\ndone"
         result <- testUserDefAdHocTypes dummymodule
-        pure $ result === expectedValue
-  , QC.testProperty "Check recursive let work forward" $
-      \() -> withMaxSuccess 16 . QC.idempotentIOProperty $ do
-        assignments <- generate genRecursiveLet
+        pure . QC.counterexample dummymodule $ result === expectedValue
+  , QC.testProperty "Check recursive let work forward"
+      . withMaxSuccess 16
+      . QC.forAll genRecursiveLet $ \assignments -> QC.idempotentIOProperty $ do
         let dummymodule = wrapRecursiveForwardLet assignments
             expectedValue = recursiveLetResult assignments <> "\ndone"
         result <- testUserDefAdHocTypes dummymodule
-        pure $ result === expectedValue
-  , QC.testProperty "Check recursive let work" $
-      \() -> withMaxSuccess 16 . QC.idempotentIOProperty $ do
-        assignments <- generate genRecursiveLet
-        shuffleInt  <- generate genInt
+        pure . QC.counterexample dummymodule $ result === expectedValue
+  , QC.testProperty "Check recursive let work"
+      . withMaxSuccess 16
+      . QC.forAll genRecursiveLet $ \assignments -> QC.forAll genInt $ \shuffleInt -> QC.idempotentIOProperty $ do
         let dummymodule   = wrapRecursiveRandomLet assignments shuffleInt
             expectedValue = recursiveLetResult assignments <> "\ndone"
         result <- testUserDefAdHocTypes dummymodule
-        pure $ result === expectedValue
-  , QC.testProperty "Cyclic let backward are stopped to avoid loops" $
-      \() -> withMaxSuccess 16 . QC.idempotentIOProperty $ do
-        assignments <- generate genRecursiveLetWithCycle
+        pure . QC.counterexample dummymodule $ result === expectedValue
+  , QC.testProperty "Cyclic let backward are stopped to avoid loops"
+      . withMaxSuccess 16
+      . QC.forAll genRecursiveLetWithCycle $ \assignments -> QC.idempotentIOProperty $ do
         let dummymodule   = wrapRecursiveBackwardLet assignments
             expectedError = "failed: RE (DefinitionCycle"
         result <- try (testUserDefAdHocTypes dummymodule) :: IO (Either SomeException String)
-        pure $ case result of
+        pure . QC.counterexample dummymodule $ case result of
           Left err  -> expectedError `isInfixOf` show err
           Right res -> expectedError `isInfixOf` show res
-  , QC.testProperty "Cyclic let forward are stopped to avoid loops" $
-      \() -> withMaxSuccess 16 . QC.idempotentIOProperty $ do
-        assignments <- generate genRecursiveLetWithCycle
+  , QC.testProperty "Cyclic let forward are stopped to avoid loops"
+      . withMaxSuccess 16
+      . QC.forAll genRecursiveLetWithCycle $ \assignments -> QC.idempotentIOProperty $ do
         let dummymodule = wrapRecursiveForwardLet assignments
             expectedError = "failed: RE (DefinitionCycle"
         result <- try (testUserDefAdHocTypes dummymodule) :: IO (Either SomeException String)
-        pure $ case result of
+        pure . QC.counterexample dummymodule $ case result of
           Left err  -> expectedError `isInfixOf` show err
           Right res -> expectedError `isInfixOf` show res
-  , QC.testProperty "Cyclic let are stopped to avoid loops" $
-      \() -> withMaxSuccess 16 . QC.idempotentIOProperty $ do
-        assignments <- generate genRecursiveLetWithCycle
-        shuffleInt  <- generate genInt
+  , QC.testProperty "Cyclic let are stopped to avoid loops"
+      . withMaxSuccess 16
+      . QC.forAll genRecursiveLetWithCycle $ \assignments -> QC.forAll genInt $ \shuffleInt -> QC.idempotentIOProperty $ do
         let dummymodule = wrapRecursiveRandomLet assignments shuffleInt
             expectedError = "failed: RE (DefinitionCycle"
         result <- try (testUserDefAdHocTypes dummymodule) :: IO (Either SomeException String)
-        pure $ case result of
+        pure . QC.counterexample dummymodule $ case result of
           Left err  -> expectedError `isInfixOf` show err
           Right res -> expectedError `isInfixOf` show res
   , QC.testProperty "Arbitrary UnprocessedParsedTerm to test hash uniqueness of HashUP's" $
@@ -105,12 +103,12 @@ qcProps = testGroup "Property tests (QuickCheck)"
       \(x' :: Term2) -> withMaxSuccess 16 $
         let x = forget x'
         in containsTHash x QC.==> onlyHashUPsChanged x
-  , QC.testProperty "Check recursive imports work" $
-      \() -> withMaxSuccess 16 . QC.idempotentIOProperty $ do
-        modules <- generate genRecursiveImports
+  , QC.testProperty "Check recursive imports work"
+      . withMaxSuccess 16
+      . QC.forAll genRecursiveImports $ \modules -> QC.idempotentIOProperty $ do
         let expectedValue = recursiveImportsResult modules <> "\ndone"
         result <- runMain_ modules "Main"
-        pure $ result === expectedValue
+        pure . QC.counterexample (ppShow modules) $ result === expectedValue
   ]
 
 recursiveResult :: String -> String
@@ -186,15 +184,20 @@ genRecursiveLetWithCycle = do
 
 -- Variable and Import str generator
 genName :: Gen String
-genName = do
-  firstChar <- elements $ ['a'..'z'] <> ['A'..'Z']
-  len <- choose (3, 15)
-  rest <- vectorOf (len - 1)
-                   (frequency [ (10, elements (['a'..'z'] <> ['A'..'Z'] <> ['0'..'9']))
-                              , (1, pure '_')
-                              , (1, pure '.')
-                              ])
-  pure (firstChar : rest)
+genName = suchThat genNameRaw (not . startsWithReservedWord)
+  where
+    genNameRaw = do
+      firstChar <- elements $ ['a'..'z'] <> ['A'..'Z']
+      len <- choose (3, 15)
+      rest <- vectorOf (len - 1)
+                       (frequency [ (10, elements (['a'..'z'] <> ['A'..'Z'] <> ['0'..'9']))
+                                  , (1, pure '_')
+                                  , (1, pure '.')
+                                  ])
+      pure (firstChar : rest)
+
+    startsWithReservedWord name = any (`isPrefixOf` name)
+      [ "case", "else", "if", "import", "in", "let", "of", "then" ]
 
 genInteger :: Gen Int
 genInteger = choose (0, 100)
@@ -244,7 +247,7 @@ containsTHash = \case
 onlyHashUPsChanged :: Term2' -> Bool
 onlyHashUPsChanged term2 = all (isHash . fst) diffList where
   diffList :: [(Term2', Term2')]
-  diffList = diffTerm2 (term2, forget . generateAllHashes . tag DummyLoc $ term2)
+  diffList = diffTerm2 (term2, forget . generateAllHashes . tag UnknownLoc $ term2)
   isHash :: Term2' -> Bool
   isHash = \case
     THash _ -> True
@@ -260,7 +263,7 @@ noDups = not . f []
 
 allHashesToTerm2 :: Term2' -> [Term2']
 allHashesToTerm2 term2 =
-  let term2WithoutTHash = forget . generateAllHashes . tag DummyLoc $ term2
+  let term2WithoutTHash = forget . generateAllHashes . tag UnknownLoc $ term2
       interm :: (Term2', Term2') -> [Term2']
       interm = \case
         (THash _ , x) -> [x]
@@ -310,6 +313,17 @@ unitTests = testGroup "Unit tests"
       let recursiveRandomLet = wrapRecursiveRandomLet recursiveLet shuffleInt
       res <- testUserDefAdHocTypes recursiveRandomLet
       res @?= "whattt\ndone"
+    -- Missing definitions should point at the unresolved variable so CLI
+    -- messages and LSP diagnostics can direct users to the real source site.
+  , testCase "missing definition error reports source location" $ do
+      case parseWithPrelude [] "main = foo 0" of
+        Left err -> assertFailure err
+        Right term -> case process term of
+          Left err -> do
+            let rendered = renderResolverError err
+            rendered @?= "missing definition \"foo\" at line 1, column 8"
+            show err @?= rendered
+          Right _ -> assertFailure "expected missing definition error"
   , testCase "test backward cycle let" $ do
       let backwardCycleLet = wrapRecursiveBackwardLet cycleLet
       result <- try ( testUserDefAdHocTypes backwardCycleLet ) :: IO (Either SomeException String)
diff --git a/test/UDTTests.hs b/test/UDTTests.hs
index f70ae875..da8a2201 100644
--- a/test/UDTTests.hs
+++ b/test/UDTTests.hs
@@ -63,7 +63,7 @@ evalExprString input = do
   case parseResult of
     Left err -> pure $ Left (errorBundlePretty err)
     Right aupt -> do
-      let term = DummyLoc :< LetUPF (pruneBindings aupt preludeBindings) aupt
+      let term = UnknownLoc :< LetUPF (first (locatedName UnknownLoc) <$> pruneBindings aupt preludeBindings) aupt
           compile' :: Term3 -> Either EvalError CompiledExpr
           compile' = compile (DebugSizing (SizingSettings 255 False)) runStaticChecks
       case first RE (process term) >>= compile' of