Add test case and release notes for 3333 fix (#3334)

Fixes #3333

The actual fix was already accidentally made in
#2734, this PR is just adding a
test case and a release note, and removing some obsolete code.

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

@@ -67,12 +67,6 @@ public void Resolve(Resolver resolver, ResolutionContext resolutionContext) {
  return;
  }
 
- var dtd = sourceType.AsDatatype;
- var subst = new Dictionary<TypeParameter, Type>();
- if (dtd != null) {
- subst = TypeParameter.SubstitutionMap(dtd.TypeArgs, sourceType.TypeArgs);
- }
-
  Type = new InferredTypeProxy();
  foreach (var kase in Cases) {
  resolver.scope.PushMarker();

Test/git-issues/git-issue-3333.dfy

@@ -0,0 +1,13 @@
+// RUN: %exits-with 2 %baredafny verify %args "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+newtype uint16 = x: int | 0 <= x < 0x1_0000
+
+datatype Datatype = A | B
+{
+ function method Foo(): uint16 {
+ match this
+ case A => 1
+ case B => 2
+ }
+}

Test/git-issues/git-issue-3333.dfy.expect

@@ -0,0 +1,2 @@
+git-issue-3333.dfy(8,18): Error: Function body type mismatch (expected uint16, got int)
+1 resolution/type errors detected in git-issue-3333.dfy

docs/dev/news/3333.fix

@@ -0,0 +1 @@
+Match expressions no longer incorrectly convert between newtypes and their basetype