Improve error message locations for function calls and call arguments (…

…#6009) ### What was changed? Added a method for updating test expect files based on CI output. This is contained in the C# project `Scripts` #### Call arguments Errors that relate to call arguments are reported on the argument, instead of on the `(`. Example: ```dafny r := new C<char>.Orig('h'); // error incorrect argument type for constructor // in-parameter 'x' (expected X, found char) ^ new location ^ old location ``` #### Function calls Errors that relate to function or method calls are now consistently reported on the `(`. This was already done for method calls, while for function calls the error was reported on the center of the callee expression. It's better to report on the `(`, to distinguish from errors in computing the callee, which are reported on the center of the callee expression. Example: ```dafny ghost const objs: set<object> := getObjs() ^ new location ^ old location // Error: insufficient reads clause to invoke function ``` #### Assertions Currently, errors about assertions (assert/ensure/invariant) are reported on the center of the condition. Since this PR changes the center of expressions that call functions, the locations for 'assertion might not hold' can change as well. Example: ```dafny assert !Even(N(17)); ^^^^|^^^^^^ new origin |^^^ previous origin // Error: assertion might not hold ``` Another example: ```dafny ensures Pos(UpIList(n)) ^ new location ^ old location // Related location: this is the postcondition that could not be proved ``` ### How has this been tested? - Updated existing tests <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>
dafny-lang · Jan 11, 2025 · b8fad27 · b8fad27
1 parent c42b706
commit b8fad27
Show file tree

Hide file tree

Showing 150 changed files with 797 additions and 688 deletions.
diff --git a/Source/Dafny.sln b/Source/Dafny.sln
@@ -43,6 +43,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyDriver.Test", "DafnyDr
 EndProject
 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyCore.Test", "DafnyCore.Test\DafnyCore.Test.csproj", "{33C29F26-A27B-474D-B436-83EA615B09FC}"
 EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Scripts", "Scripts\Scripts.csproj", "{3FAB051A-1745-497B-B4C0-D49194BB5D32}"
+EndProject
 EndProject
 Global
 	GlobalSection(SolutionConfigurationPlatforms) = preSolution
@@ -130,6 +132,10 @@ Global
 		{96B8ADA8-6190-49F7-8C38-CDA60DC92293}.Debug|Any CPU.Build.0 = Debug|Any CPU
 		{96B8ADA8-6190-49F7-8C38-CDA60DC92293}.Release|Any CPU.ActiveCfg = Release|Any CPU
 		{96B8ADA8-6190-49F7-8C38-CDA60DC92293}.Release|Any CPU.Build.0 = Release|Any CPU
+		{3FAB051A-1745-497B-B4C0-D49194BB5D32}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+		{3FAB051A-1745-497B-B4C0-D49194BB5D32}.Debug|Any CPU.Build.0 = Debug|Any CPU
+		{3FAB051A-1745-497B-B4C0-D49194BB5D32}.Release|Any CPU.ActiveCfg = Release|Any CPU
+		{3FAB051A-1745-497B-B4C0-D49194BB5D32}.Release|Any CPU.Build.0 = Release|Any CPU
 	EndGlobalSection
 	GlobalSection(SolutionProperties) = preSolution
 		HideSolutionNode = FALSE

diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs
@@ -3327,7 +3327,7 @@ internal void ResolveActualParameters(ActualBindings bindings, List<Formal> form
             whatKind + (context is Method ? " in-parameter" : " parameter"));
 
           AddAssignableConstraint(
-            callTok /* TODO should be b.Actual.Origin */, formal.Type.Subst(typeMap), b.Actual.Type,
+            b.Actual.Origin, formal.Type.Subst(typeMap), b.Actual.Type,
             $"incorrect argument type {what} (expected {{0}}, found {{1}})");
         } else if (formal.DefaultValue != null) {
           // Note, in the following line, "substMap" is passed in, but it hasn't been fully filled in until the
@@ -5916,8 +5916,7 @@ public MethodCallInformation ResolveApplySuffix(ApplySuffix e, ResolutionContext
           }
           if (callee != null) {
             // produce a FunctionCallExpr instead of an ApplyExpr(MemberSelectExpr)
-            // TODO use e.Origin instead of e.Lhs.Origin
-            var rr = new FunctionCallExpr(new OverrideCenter(e.Origin, e.Lhs.Origin.Center), mse.MemberNameNode, mse.Obj, e.Origin, e.CloseParen, e.Bindings, atLabel) {
+            var rr = new FunctionCallExpr(e.Origin, mse.MemberNameNode, mse.Obj, e.Origin, e.CloseParen, e.Bindings, atLabel) {
               Function = callee,
               TypeApplication_AtEnclosingClass = mse.TypeApplicationAtEnclosingClass,
               TypeApplication_JustFunction = mse.TypeApplicationJustMember

diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs
@@ -127,7 +127,7 @@ internal void ResolveActualParameters(ActualBindings bindings, List<Formal> form
             whatKind + (context is Method ? " in-parameter" : " parameter"));
 
           Constraints.AddSubtypeConstraint(
-            formal.PreType.Substitute(typeMap), b.Actual.PreType, callTok /* TODO should be b.Actual.Origin */,
+            formal.PreType.Substitute(typeMap), b.Actual.PreType, b.Actual.Origin,
             $"incorrect argument type {what} (expected {{0}}, found {{1}})");
         } else if (formal.DefaultValue != null) {
           // Note, in the following line, "substMap" is passed in, but it hasn't been fully filled in until the

diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs
@@ -1756,8 +1756,7 @@ public MethodCallInformation ResolveApplySuffix(ApplySuffix e, ResolutionContext
           }
           if (callee != null) {
             // resolve as a FunctionCallExpr instead of as an ApplyExpr(MemberSelectExpr)
-            // TODO use e.Origin instead of e.Lhs.Origin
-            var rr = new FunctionCallExpr(e.Lhs.Origin, mse.MemberNameNode, mse.Obj, e.Origin, e.CloseParen, e.Bindings, atLabel) {
+            var rr = new FunctionCallExpr(e.Origin, mse.MemberNameNode, mse.Obj, e.Origin, e.CloseParen, e.Bindings, atLabel) {
               Function = callee,
               PreTypeApplication_AtEnclosingClass = mse.PreTypeApplicationAtEnclosingClass,
               PreTypeApplication_JustFunction = mse.PreTypeApplicationJustMember

diff --git a/...les/LitTests/LitTest/HigherOrderIntrinsicSpecification/ReadPreconditionBypass1.dfy.expect b/...les/LitTests/LitTest/HigherOrderIntrinsicSpecification/ReadPreconditionBypass1.dfy.expect
@@ -1,3 +1,3 @@
-ReadPreconditionBypass1.dfy(23,20): Error: function precondition could not be proved
+ReadPreconditionBypass1.dfy(23,25): Error: function precondition could not be proved
 
 Dafny program verifier finished with 1 verified, 1 error
diff --git a/.../IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect b/.../IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect
@@ -17,7 +17,7 @@ at-attributes-typos.dfy(5,0): Error: @AutoContracts attribute cannot be applied
 at-attributes-typos.dfy(58,9): Error: the parameter named 'low' is already given positionally
 at-attributes-typos.dfy(56,14): Error: Argument to attribute Compile must be a literal
 at-attributes-typos.dfy(55,0): Error: wrong number of arguments (got 2, but attribute 'Compile' expects at most 1: (0: bool))
-at-attributes-typos.dfy(54,0): Error: incorrect argument type for attribute parameter '0' (expected bool, found string)
+at-attributes-typos.dfy(54,9): Error: incorrect argument type for attribute parameter '0' (expected bool, found string)
 at-attributes-typos.dfy(82,0): Error: @Transparent attribute cannot be applied to method
 at-attributes-typos.dfy(80,0): Error: wrong number of arguments (got 1, but attribute 'IsolateAssertions' expects 0)
 at-attributes-typos.dfy(49,0): Error: @Synthesize attribute cannot be applied to module definition
@@ -33,7 +33,7 @@ at-attributes-typos.dfy(40,0): Error: @Verify attribute cannot be applied to mod
 at-attributes-typos.dfy(39,0): Error: @TimeLimitMultiplier attribute cannot be applied to module definition
 at-attributes-typos.dfy(38,0): Error: @TimeLimit attribute cannot be applied to module definition
 at-attributes-typos.dfy(37,0): Error: @ResourceLimit attribute cannot be applied to module definition
-at-attributes-typos.dfy(37,0): Error: incorrect argument type for attribute parameter '0' (expected seq<char>, found int)
+at-attributes-typos.dfy(37,15): Error: incorrect argument type for attribute parameter '0' (expected seq<char>, found int)
 at-attributes-typos.dfy(36,0): Error: @Priority attribute cannot be applied to module definition
 at-attributes-typos.dfy(35,0): Error: @Print attribute cannot be applied to module definition
 at-attributes-typos.dfy(34,0): Error: @VerifyOnly attribute cannot be applied to module definition

diff --git a/...grationTests/TestFiles/LitTests/LitTest/autoRevealDependencies/func-depth-fail.dfy.expect b/...grationTests/TestFiles/LitTests/LitTest/autoRevealDependencies/func-depth-fail.dfy.expect
@@ -1,4 +1,4 @@
-func-depth-fail.dfy(12,2): Error: a postcondition could not be proved on this return path
+func-depth-fail.dfy(12,3): Error: a postcondition could not be proved on this return path
 func-depth-fail.dfy(10,10): Related location: this is the postcondition that could not be proved
 
 Dafny program verifier finished with 3 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AsIs-Resolve.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AsIs-Resolve.dfy.expect
@@ -54,7 +54,7 @@ AsIs-Resolve.dfy(212,11): Error: type test for type 'int -> real' must be from a
 AsIs-Resolve.dfy(213,11): Error: type test for type 'int -> Odd' must be from an expression assignable to it (got 'int -> nat') (covariant type parameter 1 would require nat <: Odd)
 AsIs-Resolve.dfy(220,11): Error: type test for type 'int ~> real' must be from an expression assignable to it (got 'int ~> nat') (covariant type parameter 1 would require nat <: real)
 AsIs-Resolve.dfy(185,11): Error: type cast to reference type 'C<(int, real)>' must be from an expression assignable to it (got 'M<string>') (non-variant type parameter would require (int, real) = (string, string)) (covariant type parameter 0 would require string <: int)
-AsIs-Resolve.dfy(196,9): Error: incorrect argument type at index 0 for datatype constructor parameter (expected real, found int)
+AsIs-Resolve.dfy(196,14): Error: incorrect argument type at index 0 for datatype constructor parameter (expected real, found int)
 AsIs-Resolve.dfy(229,15): Error: type test for type 'object' must be from an expression assignable to it (got 'T')
 AsIs-Resolve.dfy(230,18): Error: type test for type 'array<object>' must be from an expression assignable to it (got 'array<T>') (nonvariance for type parameter expects object = T)
 AsIs-Resolve.dfy(231,18): Error: type test for type 'array<int>' must be from an expression assignable to it (got 'array<T>') (nonvariance for type parameter expects int = T)

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AutoReq.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AutoReq.dfy.expect
@@ -1,21 +1,21 @@
-AutoReq.dfy(13,2): Error: function precondition could not be proved
+AutoReq.dfy(13,3): Error: function precondition could not be proved
 AutoReq.dfy(5,13): Related location: this proposition could not be proved
-AutoReq.dfy(25,2): Error: function precondition could not be proved
+AutoReq.dfy(25,3): Error: function precondition could not be proved
 AutoReq.dfy(5,13): Related location: this proposition could not be proved
-AutoReq.dfy(38,11): Error: function precondition could not be proved
+AutoReq.dfy(38,12): Error: function precondition could not be proved
 AutoReq.dfy(5,13): Related location: this proposition could not be proved
-AutoReq.dfy(38,11): Error: assertion might not hold
-AutoReq.dfy(31,12): Related location: this proposition could not be proved
+AutoReq.dfy(38,12): Error: assertion might not hold
+AutoReq.dfy(31,13): Related location: this proposition could not be proved
 AutoReq.dfy(7,4): Related location: this proposition could not be proved
-AutoReq.dfy(40,11): Error: function precondition could not be proved
+AutoReq.dfy(40,12): Error: function precondition could not be proved
 AutoReq.dfy(5,13): Related location: this proposition could not be proved
-AutoReq.dfy(40,11): Error: assertion might not hold
-AutoReq.dfy(31,26): Related location: this proposition could not be proved
+AutoReq.dfy(40,12): Error: assertion might not hold
+AutoReq.dfy(31,27): Related location: this proposition could not be proved
 AutoReq.dfy(7,4): Related location: this proposition could not be proved
-AutoReq.dfy(45,11): Error: assertion might not hold
-AutoReq.dfy(31,12): Related location: this proposition could not be proved
+AutoReq.dfy(45,12): Error: assertion might not hold
+AutoReq.dfy(31,13): Related location: this proposition could not be proved
 AutoReq.dfy(7,4): Related location: this proposition could not be proved
-AutoReq.dfy(247,4): Error: function precondition could not be proved
+AutoReq.dfy(247,6): Error: function precondition could not be proved
 AutoReq.dfy(239,13): Related location: this proposition could not be proved
 
 Dafny program verifier finished with 30 verified, 8 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Backticks.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Backticks.dfy.expect
@@ -1,4 +1,4 @@
-Backticks.dfy(38,4): Error: insufficient reads clause to invoke function
+Backticks.dfy(38,5): Error: insufficient reads clause to invoke function
 Backticks.dfy(77,7): Error: call might violate context's modifies clause
 
 Dafny program verifier finished with 12 verified, 2 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BadFunction.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BadFunction.dfy.expect
@@ -1,3 +1,3 @@
-BadFunction.dfy(9,2): Error: decreases clause might not decrease
+BadFunction.dfy(9,3): Error: decreases clause might not decrease
 
 Dafny program verifier finished with 1 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BindingGuards.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BindingGuards.dfy.expect
@@ -304,7 +304,7 @@ method AltSyntax9(x: int, y: int, c: Color)
 datatype Color = Red | Green | Blue
 BindingGuards.dfy(85,10): Error: a postcondition could not be proved on this return path
 BindingGuards.dfy(71,12): Related location: this is the postcondition that could not be proved
-BindingGuards.dfy(134,9): Error: assertion might not hold
+BindingGuards.dfy(134,10): Error: assertion might not hold
 BindingGuards.dfy(6,8): Related location: this proposition could not be proved
 BindingGuards.dfy(139,2): Error: alternative cases fail to cover all possibilities
 BindingGuards.dfy(147,2): Error: alternative cases fail to cover all possibilities

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BindingGuardsResolution.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BindingGuardsResolution.dfy.expect
@@ -164,5 +164,5 @@ BindingGuardsResolution.dfy(132,8): Error: assignment to non-ghost variable is n
 BindingGuardsResolution.dfy(140,8): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression
 BindingGuardsResolution.dfy(142,8): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression
 BindingGuardsResolution.dfy(146,8): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression
-BindingGuardsResolution.dfy(149,37): Error: a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword)
+BindingGuardsResolution.dfy(149,38): Error: a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword)
 11 resolution/type errors detected in BindingGuardsResolution.dfy
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BitvectorResolution.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BitvectorResolution.dfy.expect
@@ -8,8 +8,8 @@ BitvectorResolution.dfy(38,6): Error: RHS (of type bv67) not assignable to LHS (
 BitvectorResolution.dfy(39,6): Error: RHS (of type bv67) not assignable to LHS (of type int)
 BitvectorResolution.dfy(40,15): Error: type of right argument to << (real) must be an integer-numeric or bitvector type
 BitvectorResolution.dfy(41,15): Error: type of right argument to << (SmallReal) must be an integer-numeric or bitvector type
-BitvectorResolution.dfy(42,25): Error: incorrect argument type for function parameter 'w' (expected nat, found real)
-BitvectorResolution.dfy(43,25): Error: incorrect argument type for function parameter 'w' (expected nat, found SmallReal)
+BitvectorResolution.dfy(42,26): Error: incorrect argument type for function parameter 'w' (expected nat, found real)
+BitvectorResolution.dfy(43,26): Error: incorrect argument type for function parameter 'w' (expected nat, found SmallReal)
 BitvectorResolution.dfy(94,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
 BitvectorResolution.dfy(95,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
 BitvectorResolution.dfy(96,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BitvectorsMore.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BitvectorsMore.dfy.expect
@@ -490,7 +490,7 @@ BitvectorsMore.dfy(168,33): Error: when converting shift amount to a bit vector,
 BitvectorsMore.dfy(169,33): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv0
 BitvectorsMore.dfy(170,33): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv0
 BitvectorsMore.dfy(171,33): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv0
-BitvectorsMore.dfy(193,26): Error: rotate amount must not exceed the width of the result (5)
-BitvectorsMore.dfy(194,26): Error: rotate amount must not exceed the width of the result (5)
+BitvectorsMore.dfy(193,36): Error: rotate amount must not exceed the width of the result (5)
+BitvectorsMore.dfy(194,37): Error: rotate amount must not exceed the width of the result (5)
 
 Dafny program verifier finished with 9 verified, 41 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BitvectorsMore.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BitvectorsMore.dfy.refresh.expect
@@ -550,7 +550,7 @@ BitvectorsMore.dfy(168,33): Error: when converting shift amount to a bit vector,
 BitvectorsMore.dfy(169,33): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv0
 BitvectorsMore.dfy(170,33): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv0
 BitvectorsMore.dfy(171,33): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv0
-BitvectorsMore.dfy(193,26): Error: rotate amount must not exceed the width of the result (5)
-BitvectorsMore.dfy(194,26): Error: rotate amount must not exceed the width of the result (5)
+BitvectorsMore.dfy(193,36): Error: rotate amount must not exceed the width of the result (5)
+BitvectorsMore.dfy(194,37): Error: rotate amount must not exceed the width of the result (5)
 
 Dafny program verifier finished with 9 verified, 41 errors
diff --git a/...tegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismResolution.dfy.expect b/...tegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismResolution.dfy.expect
@@ -65,7 +65,7 @@ BoundedPolymorphismResolution.dfy(216,23): Error: type parameter 'A' of type 'To
 BoundedPolymorphismResolution.dfy(218,24): Error: type bound for type parameter 'A' of class 'ToBeReplaced5' is different from the corresponding type bound of the corresponding type parameter of the corresponding class in the module it refines (expected 'Trait', found 'object')
 BoundedPolymorphismResolution.dfy(218,10): Error: type parameter ('A') passed to type 'ToBeReplaced5' must meet type bound 'object' (got 'A')
 BoundedPolymorphismResolution.dfy(251,12): Error: type parameter ('Y') passed to method 'MyMethod' must meet type bound 'Trait<string>' (got 'RandomClass<real>')
-BoundedPolymorphismResolution.dfy(254,13): Error: type parameter ('Y') passed to function 'MyFunction' must meet type bound 'Trait<string>' (got 'RandomClass<char>')
+BoundedPolymorphismResolution.dfy(254,23): Error: type parameter ('Y') passed to function 'MyFunction' must meet type bound 'Trait<string>' (got 'RandomClass<char>')
 BoundedPolymorphismResolution.dfy(257,18): Error: type parameter ('Y') passed to type 'MyClass' must meet type bound 'Trait<string>' (got 'RandomClass<int>')
 BoundedPolymorphismResolution.dfy(257,18): Error: type parameter ('Y') passed to type 'MyClass' must meet type bound 'Trait<string>' (got 'RandomClass<int>')
 BoundedPolymorphismResolution.dfy(268,15): Error: type parameter 'X' of function 'F' is declared with a different number of type bounds than in the function it overrides (expected 1, found 2)
@@ -93,7 +93,7 @@ BoundedPolymorphismResolution.dfy(355,39): Error: type bound for type parameter
 BoundedPolymorphismResolution.dfy(378,15): Error: type parameters are not allowed to be renamed from the names given in the datatype in the module being refined (expected 'X', found 'Y')
 BoundedPolymorphismResolution.dfy(399,11): Error: type parameters are not allowed to be renamed from the names given in the type in the module being refined (expected 'X', found 'Z')
 BoundedPolymorphismResolution.dfy(401,12): Error: type parameters are not allowed to be renamed from the names given in the class in the module being refined (expected 'X', found 'Y')
-BoundedPolymorphismResolution.dfy[YY](394,23): Error: incorrect argument type for constructor in-parameter 'x' (expected X, found char)
+BoundedPolymorphismResolution.dfy[YY](394,28): Error: incorrect argument type for constructor in-parameter 'x' (expected X, found char)
 BoundedPolymorphismResolution.dfy(425,5): Error: type parameter ('G') passed to method 'M' must meet type bound 'GoodTrait' (got 'real')
 BoundedPolymorphismResolution.dfy(426,5): Error: type parameter ('G') passed to method 'M' must meet type bound 'GoodTrait' (got 'nat')
 BoundedPolymorphismResolution.dfy(440,5): Error: type parameter 2 ('T') passed to method 'P' must meet type bound 'ConstrainedReferenceTrait' (got 'ReferenceTrait')