Fix: Crash using subset type dafny-lang#4724 (dafny-lang#4825)

### Description
Fix for issue dafny-lang#4724 

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

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 {

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
+}

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

docs/dev/news/4724.fix

@@ -0,0 +1 @@
+fix: correction of type inference for default expressions