diff --git a/Source/DafnyCore/AST/Expressions/NestedMatchExpr.cs b/Source/DafnyCore/AST/Expressions/NestedMatchExpr.cs index a095c553cdf..5631075e21d 100644 --- a/Source/DafnyCore/AST/Expressions/NestedMatchExpr.cs +++ b/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(); - if (dtd != null) { - subst = TypeParameter.SubstitutionMap(dtd.TypeArgs, sourceType.TypeArgs); - } - Type = new InferredTypeProxy(); foreach (var kase in Cases) { resolver.scope.PushMarker(); diff --git a/Test/git-issues/git-issue-3333.dfy b/Test/git-issues/git-issue-3333.dfy new file mode 100644 index 00000000000..2a8f1d345fc --- /dev/null +++ b/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 + } +} diff --git a/Test/git-issues/git-issue-3333.dfy.expect b/Test/git-issues/git-issue-3333.dfy.expect new file mode 100644 index 00000000000..a3b0d948c38 --- /dev/null +++ b/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 diff --git a/docs/dev/news/3333.fix b/docs/dev/news/3333.fix new file mode 100644 index 00000000000..c8e9bcf2df0 --- /dev/null +++ b/docs/dev/news/3333.fix @@ -0,0 +1 @@ +Match expressions no longer incorrectly convert between newtypes and their basetype