Add test and fix bug for 3797 (dafny-lang#3800)

Fixes dafny-lang#3797

<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/NestedMatchStmt.cs

@@ -103,8 +103,6 @@ public NestedMatchStmt(RangeToken rangeToken, Expression source, [Captured] List
  _case.Resolve(resolver, resolutionContext, subst, sourceType);
  resolver.scope.PopMarker();
  }
-
- resolver.SolveAllTypeConstraints();
  }
 
  public void CheckLinearNestedMatchStmt(Type dtd, ResolutionContext resolutionContext, Resolver resolver) {

Test/git-issues/git-issue-283g.dfy.expect

@@ -1,4 +1,4 @@
 git-issue-283g.dfy(20,21): Error: the type of the pattern (int) does not agree with the match expression (string)
-git-issue-283g.dfy(35,7): Error: incorrect argument type for datatype constructor parameter 'value' (expected int, found real)
+git-issue-283g.dfy(32,14): Error: the type of the pattern (int) does not agree with the match expression (real)
 git-issue-283g.dfy(41,14): Error: the type of the pattern (int) does not agree with the match expression (real)
 3 resolution/type errors detected in git-issue-283g.dfy

Test/git-issues/github-issue-3797.dfy

@@ -0,0 +1,14 @@
+// RUN: %verify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+newtype uint16 = x | 0 <= x < 0x1_0000
+datatype D = A | B
+
+method M(x: D, u: uint16) returns (r: uint16) {
+ var v := 5;
+ match x {
+ case A => r := 12;
+ case B => r := 13;
+ }
+ r := v;
+}

Test/git-issues/github-issue-3797.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 2 verified, 0 errors