diff --git a/Source/DafnyCore/AST/Expressions/DefaultValueExpression.cs b/Source/DafnyCore/AST/Expressions/DefaultValueExpression.cs
index e85656e56f0..0eeed8b32a9 100644
--- a/Source/DafnyCore/AST/Expressions/DefaultValueExpression.cs
+++ b/Source/DafnyCore/AST/Expressions/DefaultValueExpression.cs
@@ -73,8 +73,6 @@ public void FillIn(ModuleResolver resolver, Dictionary<DefaultValueExpression, W
     var s = new DefaultValueSubstituter(resolver, visited, this.receiver, this.substMap, typeMap);
     this.ResolvedExpression = s.Substitute(this.formal.DefaultValue);
     visited[this] = WorkProgress.Done;
-
-    this.ResolvedExpression.Type = this.Type;
   }
 
   class DefaultValueSubstituter : Substituter {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4724.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4724.dfy
new file mode 100644
index 00000000000..ccf59ee20d9
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4724.dfy
@@ -0,0 +1,9 @@
+// RUN: %exits-with 4 %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+type seq31<T> = x: seq<T> | |x| <= 31
+
+method TakeThis(x: seq31<int> := []) 
+{
+  TakeThis(); // Error: cannot prove termination; try supplying a decreases clause
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4724.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4724.dfy.expect
new file mode 100644
index 00000000000..61cfed51234
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4724.dfy.expect
@@ -0,0 +1,3 @@
+git-issue-4724.dfy(8,10): Error: cannot prove termination; try supplying a decreases clause
+
+Dafny program verifier finished with 2 verified, 1 error
diff --git a/docs/dev/news/4724.fix b/docs/dev/news/4724.fix
new file mode 100644
index 00000000000..404c0704326
--- /dev/null
+++ b/docs/dev/news/4724.fix
@@ -0,0 +1 @@
+fix: correction of type inference for default expressions 
\ No newline at end of file