improvements to type checking of record updates

TODO.md

@@ -135,8 +135,8 @@
 - [x] implement magic nat
 - [ ] Consider splitting desugar/check
   - We can only check physical syntax at the moment, which has been inconvenient in a couple of spots where we want to check generated code. E.g. solutions to auto implicits.
-- [ ] record update can't elaborate if type is unsolved meta
+- [x] record update can't elaborate if type is unsolved meta
-  - need to postpone elab until meta is known. Create fresh meta for the term to return and have postponed elab fill it in later.
+  - The issue actually was a solved meta that wasn't forced
 - [x] drop erased args on types and top level functions
 - [x] can I do some inlining without blowing up code size?
   - [x] Maybe tag some functions as inline

src/Lib/Elab.newt

@@ -1397,6 +1397,12 @@ updateRec ctx fc clauses arg ty = do
     Nothing => RLam fc (BI fc "$ru" Explicit Many) tm
   check ctx tm ty
   where
+    app : FC → Raw → Raw → Raw
+    -- A nested recored update ended up as an RApp of a bare update, essentially
+    -- a beta redux, and it hit `infer` on the RUpdateRec
+    app _ (RUpdateRec fc cl Nothing) u = RUpdateRec fc cl (Just u)
+    app fc t u = (RApp fc t u Explicit)
+
     doClause : List (String × Raw) → UpdateClause → M (List (String × Raw))
     doClause args (ModifyField fc nm tm) = go args
       where
@@ -1404,7 +1410,7 @@ updateRec ctx fc clauses arg ty = do
         go Nil = error fc "\{nm} is not a field of \{show ty}"
         go (x :: xs) = if fst x == nm
         -- need arg in here and apply tm to arg
-          then pure $ (nm, RApp fc tm (snd x) Explicit) :: xs
+          then pure $ (nm, app fc tm (snd x)) :: xs
           else _::_ x <$> go xs
     doClause args (AssignField fc nm tm) = go args
       where
@@ -1425,10 +1431,11 @@ updateRec ctx fc clauses arg ty = do
       let (Just (MkEntry _ _ ty (DCon _ _ _ _) _)) = lookup conname top
         | _ => error fc "\{show conname} not a dcon"
       pure (conname, collect arg ty)
-    --
+    getTele Nothing (VPi _ _ _ _ a b) = do
-    getTele Nothing (VPi _ _ _ _ a b) = getTele (Just $ RVar fc "$ru") a
+      a <- forceType ctx.env a
-    getTele Nothing v = error (getFC v) "Expected a pi type, got \{show v}"
+      getTele (Just $ RVar fc "$ru") a
-    getTele _ v = error (getFC v) "Expected a record type, got \{show v}"
+    getTele Nothing v = error fc "Expected a pi type, got \{show v}"
+    getTele (Just tm) v = error (getFC tm) "Expected a record type, got \{show v}"
 
 infer : Context -> Raw  -> M (Tm × Val)
 

src/Lib/TopContext.newt

@@ -55,7 +55,7 @@ setFlag name fc flag = do
   top <- getTop
   let (Just (MkEntry fc nm ty def flags)) = lookupMap' name top.defs
     | Nothing => error fc "\{show name} not declared"
-  modifyTop $ \ top => [ defs := (updateMap name (MkEntry fc name ty def (flag :: flags)) top.defs) ] top
+  modifyTop [ defs $= (updateMap name (MkEntry fc name ty def (flag :: flags))) ]
 
 setDef : QName -> FC -> Tm -> Def → List EFlag -> M Unit
 setDef name fc ty def flags = do

tests/NestedUpdate.newt

@@ -0,0 +1,12 @@
+module NestedUpdate
+
+import Prelude
+
+record Foo where
+    bar : Int
+
+record Bar where
+    foo : Foo
+
+blah : Bar → Bar
+blah x = [ foo $= [ bar := 1]] x