From ea733181c5a30713e05d607525f6c4dabff2a8b3 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sat, 12 Nov 2022 21:58:23 -0800
Subject: [PATCH] [ error ] Add an FC to record constructors for better error
 messages (#2769)

---
 src/TTImp/ProcessRecord.idr          | 2 +-
 tests/Main.idr                       | 2 +-
 tests/idris2/perror020/Issue2769.idr | 5 +++++
 tests/idris2/perror020/expected      | 8 ++++++++
 tests/idris2/perror020/run           | 3 +++
 5 files changed, 18 insertions(+), 2 deletions(-)
 create mode 100644 tests/idris2/perror020/Issue2769.idr
 create mode 100644 tests/idris2/perror020/expected
 create mode 100644 tests/idris2/perror020/run

diff --git a/src/TTImp/ProcessRecord.idr b/src/TTImp/ProcessRecord.idr
index 9e26560b6..884ba1669 100644
--- a/src/TTImp/ProcessRecord.idr
+++ b/src/TTImp/ProcessRecord.idr
@@ -129,7 +129,7 @@ elabRecord {vars} eopts fc env nest newns vis mbtot tn_in params opts conName_in
              let conty = mkTy paramTelescope $
                          mkTy (map farg fields) (recTy tn)
              let boundNames = paramNames ++ map fname fields ++ vars
-             let con = MkImpTy EmptyFC EmptyFC cname
+             let con = MkImpTy (virtualiseFC fc) EmptyFC cname
                        !(bindTypeNames fc [] boundNames conty)
              let dt = MkImpData fc tn !(bindTypeNames fc [] boundNames (mkDataTy fc params)) opts [con]
              log "declare.record" 5 $ "Record data type " ++ show dt
diff --git a/tests/Main.idr b/tests/Main.idr
index 2a87a585f..b2e9e830d 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -93,7 +93,7 @@ idrisTestsError = MkTestPool "Error messages" [] Nothing
        "perror001", "perror002", "perror003", "perror004", "perror005",
        "perror006", "perror007", "perror008", "perror009", "perror010",
        "perror011", "perror012", "perror013", "perror014", "perror015",
-       "perror016", "perror017", "perror018", "perror019"]
+       "perror016", "perror017", "perror018", "perror019", "perror020"]
 
 idrisTestsInteractive : TestPool
 idrisTestsInteractive = MkTestPool "Interactive editing" [] Nothing
diff --git a/tests/idris2/perror020/Issue2769.idr b/tests/idris2/perror020/Issue2769.idr
new file mode 100644
index 000000000..a16a56908
--- /dev/null
+++ b/tests/idris2/perror020/Issue2769.idr
@@ -0,0 +1,5 @@
+module Issue2769
+
+record SomeRecord where
+  constructor SomeRecord
+  field : Int
diff --git a/tests/idris2/perror020/expected b/tests/idris2/perror020/expected
new file mode 100644
index 000000000..a2f0de569
--- /dev/null
+++ b/tests/idris2/perror020/expected
@@ -0,0 +1,8 @@
+1/1: Building Issue2769 (Issue2769.idr)
+Error: Issue2769.SomeRecord is already defined.
+
+Issue2769:3:1--5:14
+ 3 | record SomeRecord where
+ 4 |   constructor SomeRecord
+ 5 |   field : Int
+
diff --git a/tests/idris2/perror020/run b/tests/idris2/perror020/run
new file mode 100644
index 000000000..a004cd035
--- /dev/null
+++ b/tests/idris2/perror020/run
@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-banner --no-color --console-width 0 --check Issue2769.idr