[ fix #2095 ] error on duplicated updates

src/Core/Core.idr

@@ -107,6 +107,7 @@ data Error : Type where
      AllFailed : List (Maybe Name, Error) -> Error
      RecordTypeNeeded : {vars : _} ->
                         FC -> Env Term vars -> Error
+     DuplicatedRecordUpdatePath : FC -> List (List String) -> Error
      NotRecordField : FC -> String -> Maybe Name -> Error
      NotRecordType : FC -> Name -> Error
      IncompatibleFieldUpdate : FC -> List String -> Error
@@ -265,6 +266,8 @@ Show Error where
   show (AllFailed ts) = "No successful elaboration: " ++ assert_total (show ts)
   show (RecordTypeNeeded fc env)
       = show fc ++ ":Can't infer type of record to update"
+  show (DuplicatedRecordUpdatePath fc ps)
+      = show fc ++ ":Duplicated record update paths: " ++ show ps
   show (NotRecordField fc fld Nothing)
       = show fc ++ ":" ++ fld ++ " is not part of a record type"
   show (NotRecordField fc fld (Just ty))
@@ -395,6 +398,7 @@ getErrorLoc (AmbiguityTooDeep loc _ _) = Just loc
 getErrorLoc (AllFailed ((_, x) :: _)) = getErrorLoc x
 getErrorLoc (AllFailed []) = Nothing
 getErrorLoc (RecordTypeNeeded loc _) = Just loc
+getErrorLoc (DuplicatedRecordUpdatePath loc _) = Just loc
 getErrorLoc (NotRecordField loc _ _) = Just loc
 getErrorLoc (NotRecordType loc _) = Just loc
 getErrorLoc (IncompatibleFieldUpdate loc _) = Just loc

src/Idris/Error.idr

@@ -354,6 +354,11 @@ perror (AllFailed ts)
     allUndefined _ = Nothing
 perror (RecordTypeNeeded fc _)
     = pure $ errorDesc (reflow "Can't infer type for this record update.") <+> line <+> !(ploc fc)
+perror (DuplicatedRecordUpdatePath fc ps)
+    = pure $ vcat $
+      errorDesc (reflow "Duplicated record update paths:")
+      :: map (indent 2 . concatWith (surround (pretty "->")) . map pretty) ps
+      ++ [line <+> !(ploc fc)]
 perror (NotRecordField fc fld Nothing)
     = pure $ errorDesc (code (pretty fld) <++> reflow "is not part of a record type.") <+> line <+> !(ploc fc)
 perror (NotRecordField fc fld (Just ty))

src/TTImp/Elab/Record.idr

@@ -17,6 +17,7 @@ import TTImp.Elab.Delayed
 import TTImp.TTImp
 
 import Data.List
+import Libraries.Data.SortedSet
 
 %default covering
 
@@ -161,6 +162,16 @@ getAllSides loc [] tyn orig rec = pure rec
 getAllSides loc (u :: upds) tyn orig rec
     = getAllSides loc upds tyn orig !(getSides loc u tyn orig rec)
 
+checkForDuplicates :
+  List IFieldUpdate ->
+  (seen, dups : SortedSet (List String)) ->
+  SortedSet (List String)
+checkForDuplicates [] seen dups = dups
+checkForDuplicates (x :: xs) seen dups
+  = let path = getFieldUpdatePath x
+        dups = ifThenElse (contains path seen) (insert path dups) dups
+    in checkForDuplicates xs (insert path seen) dups
+
 -- Convert the collection of high level field accesses into a case expression
 -- which does the updates all in one go
 export
@@ -174,7 +185,10 @@ recUpdate : {vars : _} ->
             (rec : RawImp) -> (grecty : Glued vars) ->
             Core RawImp
 recUpdate rigc elabinfo iloc nest env flds rec grecty
-      = do defs <- get Ctxt
+      = do let dups = checkForDuplicates flds empty empty
+           unless (null dups) $
+             throw (DuplicatedRecordUpdatePath iloc $ SortedSet.toList dups)
+           defs <- get Ctxt
            rectynf <- getNF grecty
            let Just rectyn = getRecordType env rectynf
                     | Nothing => throw (RecordTypeNeeded iloc env)

tests/Main.idr

@@ -142,7 +142,8 @@ idrisTestsData = MkTestPool "Data and record types" [] Nothing
        "data001",
        -- Records, access and dependent update
        "record001", "record002", "record003", "record004", "record005",
-       "record006", "record007", "record008", "record009", "record010"]
+       "record006", "record007", "record008", "record009", "record010",
+       "record011"]
 
 idrisTestsBuiltin : TestPool
 idrisTestsBuiltin = MkTestPool "Builtin types and functions" [] Nothing

tests/idris2/record011/Issue2095.idr

@@ -0,0 +1,19 @@
+record Foo where
+  constructor MkFoo
+  a : Nat
+  b : Nat
+
+foo1 : Foo
+foo1 = MkFoo
+  { a = 1
+  , a = 2
+  , b = 3
+  }
+
+foo2 : Foo
+foo2 = record
+  { a = 3
+  , a = 4
+  , b = 2
+  , b = 1
+  } foo1

tests/idris2/record011/expected

@@ -0,0 +1,23 @@
+1/1: Building Issue2095 (Issue2095.idr)
+Error: While processing right hand side of foo1. a is not a valid argument in MkFoo 1 3.
+
+Issue2095:7:8--11:4
+ 07 | foo1 = MkFoo
+ 08 |   { a = 1
+ 09 |   , a = 2
+ 10 |   , b = 3
+ 11 |   }
+
+Error: While processing right hand side of foo2. Duplicated record update paths:
+  a
+  b
+
+
+Issue2095:14:8--19:9
+ 14 | foo2 = record
+ 15 |   { a = 3
+ 16 |   , a = 4
+ 17 |   , b = 2
+ 18 |   , b = 1
+ 19 |   } foo1
+

tests/idris2/record011/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner --check Issue2095.idr