From adff28ea0ffc9cb7b8e5f4c5274929fd6cdadd40 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sun, 15 Feb 2026 21:51:16 -0800
Subject: [PATCH] Remove some workarounds for record update issues

---
 src/LSP.newt      |  8 +++-----
 src/Lib/Elab.newt | 16 ++++++++++------
 2 files changed, 13 insertions(+), 11 deletions(-)

diff --git a/src/LSP.newt b/src/LSP.newt
index 276ed7a..cda9355 100644
--- a/src/LSP.newt
+++ b/src/LSP.newt
@@ -65,7 +65,7 @@ lspFileSource = MkFileSource $ \fc fn => do
 updateFile : String → String → Unit
 updateFile fn src = unsafePerformIO $ do
     st <- readIORef state
-    modifyIORef state $ \a => [ files $= updateMap fn src ] a
+    modifyIORef state [ files $= updateMap fn src ]
     let st = the LSPState $ [ files $= updateMap fn src ] st
     -- module relative to base
 
@@ -75,9 +75,7 @@ updateFile fn src = unsafePerformIO $ do
 
     Right (ctx,_) <- (invalidateModule modName).runM st.topContext
         | _ => writeIORef state st
-    -- TODO It doesn't have record type, but eta expanding resolves this.  See if there is a quick fix.
-    -- modifyIORef state [ topContext := ctx ]
-    modifyIORef state $ \a => [ topContext := ctx ] a
+    modifyIORef state [ topContext := ctx ]
 
 
 fcToRange : FC → Json
@@ -139,7 +137,7 @@ checkFile fn = unsafePerformIO $ do
             putStrLn $ showError "" err
             pure $ jsonToJObject $ JsonArray $ errorToDiag err :: Nil
     -- Cache loaded modules
-    modifyIORef state $ \a => [ topContext := top ] a
+    modifyIORef state $ [ topContext := top ]
     pure $ jsonToJObject $ JsonArray json
 
 -- This seems like a hack, but it works.
diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt
index fff0c48..36751c0 100644
--- a/src/Lib/Elab.newt
+++ b/src/Lib/Elab.newt
@@ -118,8 +118,8 @@ isCandidate ty (App fc t u) = isCandidate ty t
 isCandidate _ _ = False
 
 setMetaMode : MetaMode → M Unit
--- ideally we could do metaCtx.mcmode := CheckFirst
-setMetaMode mcmode = modifyTop $ \top => [ metaCtx := [mcmode := mcmode] (top.metaCtx) ] top
+-- ideally we would support dotted paths like metaCtx.mcmode := CheckFirst
+setMetaMode mcmode = modifyTop [ metaCtx $= [mcmode := mcmode] ]
 
 findMatches : Context -> Val -> List (QName × Tm) -> M (List QName)
 findMatches ctx ty Nil = pure Nil
@@ -632,7 +632,7 @@ freshMeta ctx fc ty kind = do
   let autos = case kind of
       AutoSolve => qn :: mc.autos
       _ => mc.autos
-  modifyTop $ \top => [metaCtx := MC (updateMap qn newmeta mc.metas) autos (1 + mc.next) mc.mcmode ] top
+  modifyTop [metaCtx := MC (updateMap qn newmeta mc.metas) autos (1 + mc.next) mc.mcmode ]
   -- I tried checking Auto immediately if CheckAll, but there isn't enough information yet.
   pure $ applyBDs 0 (Meta fc qn) ctx.bds
   where
@@ -1384,9 +1384,13 @@ undo prev ((DoArrow fc left right alts) :: xs) = do
     (RLam fc (BI fc nm Explicit Many) rest) Explicit
 
 
--- REVIEW do we want to let arg?
--- collect fields and default assignment
--- subst in real assignment
+-- REVIEW should `arg` be assigned to a variable with `RLet`?
+-- REVIEW a case statement to destruct the record instead of projections
+-- would make less work for the compiler / inliner.
+
+-- updateRec makes a list of fields and a term for the current value (collect), swaps in
+-- any updates present in the code (doClause), and generates an application of the
+-- constructor.
 updateRec : Context → FC → List UpdateClause → Maybe Raw → Val → M Tm
 updateRec ctx fc clauses arg ty = do
   ((QN _ conname), args) <- getTele arg ty