From 58359c2d013f2b16f754ac699f7d4883875d31af Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Tue, 7 Jul 2020 22:36:15 +0100
Subject: [PATCH] Leave implicit record fields alone on update

Unless an explicit update is given
---
 src/TTImp/Elab/Record.idr         | 6 +++++-
 tests/Main.idr                    | 2 +-
 tests/idris2/reg032/expected      | 1 +
 tests/idris2/reg032/recupdate.idr | 6 ++++++
 tests/idris2/reg032/run           | 3 +++
 5 files changed, 16 insertions(+), 2 deletions(-)
 create mode 100644 tests/idris2/reg032/expected
 create mode 100644 tests/idris2/reg032/recupdate.idr
 create mode 100755 tests/idris2/reg032/run

diff --git a/src/TTImp/Elab/Record.idr b/src/TTImp/Elab/Record.idr
index 58ccbb53f..f5a76d930 100644
--- a/src/TTImp/Elab/Record.idr
+++ b/src/TTImp/Elab/Record.idr
@@ -125,7 +125,11 @@ findPath loc (p :: ps) full (Just tyn) val (Field mn n v)
     mkArgs ((p, imp, _) :: ps)
         = do fldn <- genFieldName p
              args' <- mkArgs ps
-             pure ((p, Field imp fldn (IVar loc (UN fldn))) :: args')
+             -- If it's an implicit argument, leave it as _ by default
+             let arg = maybe (IVar loc (UN fldn))
+                             (const (Implicit loc False))
+                             imp
+             pure ((p, Field imp fldn arg) :: args')
 
 findPath loc (p :: ps) full tyn val (Constr mn con args)
    = do let Just prec = lookup p args
diff --git a/tests/Main.idr b/tests/Main.idr
index d5ec1b0d4..721dedb0b 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -99,7 +99,7 @@ idrisTests
        "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
        "reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021",
        "reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028",
-       "reg029", "reg030", "reg031",
+       "reg029", "reg030", "reg031", "reg032",
        -- Totality checking
        "total001", "total002", "total003", "total004", "total005",
        "total006", "total007", "total008", "total009",
diff --git a/tests/idris2/reg032/expected b/tests/idris2/reg032/expected
new file mode 100644
index 000000000..f136cb1d4
--- /dev/null
+++ b/tests/idris2/reg032/expected
@@ -0,0 +1 @@
+1/1: Building recupdate (recupdate.idr)
diff --git a/tests/idris2/reg032/recupdate.idr b/tests/idris2/reg032/recupdate.idr
new file mode 100644
index 000000000..d8cf29c96
--- /dev/null
+++ b/tests/idris2/reg032/recupdate.idr
@@ -0,0 +1,6 @@
+record R (a : Type) where
+  constructor MkR
+  x : a
+
+rmap : (a -> b) -> R a -> R b
+rmap f = record { x $= f }
diff --git a/tests/idris2/reg032/run b/tests/idris2/reg032/run
new file mode 100755
index 000000000..7295e347c
--- /dev/null
+++ b/tests/idris2/reg032/run
@@ -0,0 +1,3 @@
+$1 --check recupdate.idr
+
+rm -rf build