diff --git a/Source/DafnyCore/Resolver.cs b/Source/DafnyCore/Resolver.cs
index 9452daa777c..ab8df7984c9 100644
--- a/Source/DafnyCore/Resolver.cs
+++ b/Source/DafnyCore/Resolver.cs
@@ -15075,8 +15075,11 @@ public void ResolveExpressionX(Expression expr, ResolutionContext resolutionCont
         ResolveExpression(e.Index, resolutionContext);
         ResolveExpression(e.Value, resolutionContext);
         AddXConstraint(expr.tok, "SeqUpdatable", e.Seq.Type, e.Index, e.Value, "update requires a sequence, map, or multiset (got {0})");
-        expr.Type = e.Seq.Type;
-
+        expr.Type = new InferredTypeProxy(); // drop type constraints
+        ConstrainSubtypeRelation(
+          super: expr.Type, sub: e.Seq.Type, // expr.Type generalizes e.Seq.Type by dropping constraints
+          exprForToken: expr,
+          msg: "Update expression used with type '{0}'", e.Seq.Type);
       } else if (expr is DatatypeUpdateExpr) {
         var e = (DatatypeUpdateExpr)expr;
         ResolveExpression(e.Root, resolutionContext);
diff --git a/Test/git-issues/git-issue-3059.dfy b/Test/git-issues/git-issue-3059.dfy
new file mode 100644
index 00000000000..7eae9737c4f
--- /dev/null
+++ b/Test/git-issues/git-issue-3059.dfy
@@ -0,0 +1,59 @@
+// RUN: %dafny_0 /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+type seq0 = s: seq<int> | forall n <- s :: n == 0
+
+function ReplaceInSeq0_Rejects(s: seq0): seq0
+  requires |s| > 0
+  ensures false
+{
+  var s' := s[0 := 1];
+  assert s'[0] != 0;
+  s'
+}
+
+function ReplaceInSeq0_Accepts(s: seq0): seq<int>
+  requires |s| > 0
+{
+  var s' := s[0 := 1];
+  assert s'[0] != 0;
+  s'
+}
+
+type map0 = m: map<int, int> | forall k <- m :: m[k] == 0
+
+function AddInMap0_Rejects(m: map0): map0
+  ensures false
+{
+  m[0 := 1]
+}
+
+function AddInMap0_Accepts(m: map0): map<int, int>
+{
+  m[0 := 1]
+}
+
+function RecoverType<T>(a: T): T { a }
+
+method AddInMap0_Proxy_Rejects() returns (r: map0)
+  ensures false
+{
+  var m; // The type of m is to be inferred, but that won't happen until
+         // after type inference has processed the assignment to r.
+  r := m[1 := 7];
+  // To trigger the unsoundness, the verifier needs to be reminded that
+  // r is a variable of type map0. That is done by the following little
+  // trick:
+  ghost var u := RecoverType<map0>(r);
+}
+
+method AddInMap0_Proxy_Accepts() returns (r: map<int, int>)
+{
+  var m; // The type of m is to be inferred, but that won't happen until
+         // after type inference has processed the assignment to r.
+  r := m[1 := 7];
+  // To trigger the unsoundness, the verifier needs to be reminded that
+  // r is a variable of type map0. That is done by the following little
+  // trick:
+  ghost var u := RecoverType<map<int, int>>(r);
+}
diff --git a/Test/git-issues/git-issue-3059.dfy.expect b/Test/git-issues/git-issue-3059.dfy.expect
new file mode 100644
index 00000000000..90a9984aca4
--- /dev/null
+++ b/Test/git-issues/git-issue-3059.dfy.expect
@@ -0,0 +1,5 @@
+git-issue-3059.dfy(12,2): Error: value does not satisfy the subset constraints of 'seq0'
+git-issue-3059.dfy(28,3): Error: value does not satisfy the subset constraints of 'map0'
+git-issue-3059.dfy(43,8): Error: value does not satisfy the subset constraints of 'map0'
+
+Dafny program verifier finished with 3 verified, 3 errors
diff --git a/docs/dev/news/3059.fix b/docs/dev/news/3059.fix
new file mode 100644
index 00000000000..9d155788913
--- /dev/null
+++ b/docs/dev/news/3059.fix
@@ -0,0 +1 @@
+Use correct type for map update expression
\ No newline at end of file