Improve error messages about variance and cardinality preservation

RELEASE_NOTES.md

@@ -7,6 +7,7 @@
 - fix: Use the right comparison operators for bitvectors in Javascript (https://github.com/dafny-lang/dafny/pull/2716)
 - fix: Retain non-method-body block statements when cloning abstract signatures (https://github.com/dafny-lang/dafny/pull/2731)
 - fix: Correctly substitute variables introduced by a binding guard (https://github.com/dafny-lang/dafny/pull/2745)
+- fix: Improved hints and error messages regarding variance/cardinality preservation (https://github.com/dafny-lang/dafny/pull/2774)
 
 # 3.8.1
 

Source/DafnyCore/Resolver.cs

@@ -14652,7 +14652,7 @@ public void CheckVariance(Type type, ICallable enclosingTypeDefinition, TypePara
           } else if (tp.StrictVariance && lax) {
             string hint;
             if (tp.VarianceSyntax == TypeParameter.TPVarianceSyntax.NonVariant_Strict) {
-              hint = string.Format(" (perhaps try declaring '{0}' as '!{0}')", tp.Name);
+              hint = string.Format(" (perhaps try declaring '{0}' as '-{0}' or '!{0}')", tp.Name);
             } else {
               Contract.Assert(tp.VarianceSyntax == TypeParameter.TPVarianceSyntax.Covariant_Strict);
               hint = string.Format(" (perhaps try changing the declaration from '+{0}' to '*{0}')", tp.Name);
@@ -14668,7 +14668,7 @@ public void CheckVariance(Type type, ICallable enclosingTypeDefinition, TypePara
             var cg = enclosingTypeDefinition.EnclosingModule.CallGraph;
             var t0 = resolvedClass as ICallable;
             if (t0 != null && cg.GetSCCRepresentative(t0) == cg.GetSCCRepresentative(enclosingTypeDefinition)) {
-              reporter.Error(MessageSource.Resolver, t.tok, "using the type being defined ('{0}') here violates strict positivity, that is, it would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)", resolvedClass.Name);
+              reporter.Error(MessageSource.Resolver, t.tok, "using the type being defined ('{0}') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)", resolvedClass.Name);
             }
           }
           for (int i = 0; i < t.TypeArgs.Count; i++) {

Test/dafny0/TypeTests.dfy.expect

@@ -33,10 +33,10 @@ TypeTests.dfy(222,9): Error: assignment to array element is not allowed in this
 TypeTests.dfy(229,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'A' can be constructed
 TypeTests.dfy(230,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'B' can be constructed
 TypeTests.dfy(232,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Cycle' can be constructed
-TypeTests.dfy(237,20): Error: using the type being defined ('A') here violates strict positivity, that is, it would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
-TypeTests.dfy(238,20): Error: using the type being defined ('B') here violates strict positivity, that is, it would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
-TypeTests.dfy(243,20): Error: using the type being defined ('E') here violates strict positivity, that is, it would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
-TypeTests.dfy(244,20): Error: using the type being defined ('F') here violates strict positivity, that is, it would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
-TypeTests.dfy(245,20): Error: using the type being defined ('G') here violates strict positivity, that is, it would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
+TypeTests.dfy(237,20): Error: using the type being defined ('A') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
+TypeTests.dfy(238,20): Error: using the type being defined ('B') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
+TypeTests.dfy(243,20): Error: using the type being defined ('E') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
+TypeTests.dfy(244,20): Error: using the type being defined ('F') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
+TypeTests.dfy(245,20): Error: using the type being defined ('G') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
 TypeTests.dfy(250,7): Error: recursive constraint dependency involving a subset type: CycW -> W -> CycleW -> CycW
 41 resolution/type errors detected in TypeTests.dfy

Test/dafny0/Variance.dfy.expect

@@ -127,9 +127,9 @@ module MoreDependencyCycles1 {
 }
 Variance.dfy(10,12): Error: formal type parameter 'E' is not used according to its variance specification
 Variance.dfy(12,33): Error: formal type parameter 'Y' is not used according to its variance specification
-Variance.dfy(12,36): Error: formal type parameter 'Z' is not used according to its variance specification (it is used left of an arrow) (perhaps try declaring 'Z' as '!Z')
-Variance.dfy(12,42): Error: formal type parameter 'Z' is not used according to its variance specification (it is used left of an arrow) (perhaps try declaring 'Z' as '!Z')
-Variance.dfy(13,37): Error: formal type parameter 'M' is not used according to its variance specification (it is used left of an arrow) (perhaps try declaring 'M' as '!M')
+Variance.dfy(12,36): Error: formal type parameter 'Z' is not used according to its variance specification (it is used left of an arrow) (perhaps try declaring 'Z' as '-Z' or '!Z')
+Variance.dfy(12,42): Error: formal type parameter 'Z' is not used according to its variance specification (it is used left of an arrow) (perhaps try declaring 'Z' as '-Z' or '!Z')
+Variance.dfy(13,37): Error: formal type parameter 'M' is not used according to its variance specification (it is used left of an arrow) (perhaps try declaring 'M' as '-M' or '!M')
 Variance.dfy(13,40): Error: formal type parameter 'N' is not used according to its variance specification
 Variance.dfy(13,50): Error: formal type parameter 'N' is not used according to its variance specification
 Variance.dfy(13,53): Error: formal type parameter 'N' is not used according to its variance specification
@@ -144,35 +144,35 @@ Variance.dfy(30,35): Error: formal type parameter 'A' is not used according to i
 Variance.dfy(33,29): Error: formal type parameter 'B' is not used according to its variance specification
 Variance.dfy(34,33): Error: formal type parameter 'B' is not used according to its variance specification
 Variance.dfy(35,37): Error: formal type parameter 'B' is not used according to its variance specification
-Variance.dfy(42,28): Error: formal type parameter 'D' is not used according to its variance specification (it is used left of an arrow) (perhaps try declaring 'D' as '!D')
-Variance.dfy(43,32): Error: formal type parameter 'D' is not used according to its variance specification (it is used left of an arrow) (perhaps try declaring 'D' as '!D')
-Variance.dfy(45,40): Error: formal type parameter 'D' is not used according to its variance specification (it is used left of an arrow) (perhaps try declaring 'D' as '!D')
+Variance.dfy(42,28): Error: formal type parameter 'D' is not used according to its variance specification (it is used left of an arrow) (perhaps try declaring 'D' as '-D' or '!D')
+Variance.dfy(43,32): Error: formal type parameter 'D' is not used according to its variance specification (it is used left of an arrow) (perhaps try declaring 'D' as '-D' or '!D')
+Variance.dfy(45,40): Error: formal type parameter 'D' is not used according to its variance specification (it is used left of an arrow) (perhaps try declaring 'D' as '-D' or '!D')
 Variance.dfy(46,21): Error: formal type parameter 'E' is not used according to its variance specification
 Variance.dfy(47,25): Error: formal type parameter 'E' is not used according to its variance specification
 Variance.dfy(48,29): Error: formal type parameter 'E' is not used according to its variance specification
 Variance.dfy(49,33): Error: formal type parameter 'E' is not used according to its variance specification
 Variance.dfy(51,17): Error: formal type parameter 'A' is not used according to its variance specification (it is used left of an arrow) (perhaps try changing the declaration from '+A' to '*A')
-Variance.dfy(54,17): Error: formal type parameter 'D' is not used according to its variance specification (it is used left of an arrow) (perhaps try declaring 'D' as '!D')
+Variance.dfy(54,17): Error: formal type parameter 'D' is not used according to its variance specification (it is used left of an arrow) (perhaps try declaring 'D' as '-D' or '!D')
 Variance.dfy(55,17): Error: formal type parameter 'E' is not used according to its variance specification
 Variance.dfy(60,15): Error: formal type parameter 'E' is not used according to its variance specification
 Variance.dfy(61,18): Error: formal type parameter 'A' is not used according to its variance specification (it is used left of an arrow) (perhaps try changing the declaration from '+A' to '*A')
 Variance.dfy(62,21): Error: formal type parameter 'E' is not used according to its variance specification
-Variance.dfy(64,18): Error: formal type parameter 'D' is not used according to its variance specification (it is used left of an arrow) (perhaps try declaring 'D' as '!D')
-Variance.dfy(69,17): Error: using the type being defined ('CheckRec') here violates strict positivity, that is, it would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
-Variance.dfy(71,16): Error: using the type being defined ('CheckRec') here violates strict positivity, that is, it would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
-Variance.dfy(74,22): Error: using the type being defined ('CheckRec') here violates strict positivity, that is, it would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
-Variance.dfy(75,27): Error: using the type being defined ('CheckRec') here violates strict positivity, that is, it would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
-Variance.dfy(77,37): Error: using the type being defined ('CheckRec') here violates strict positivity, that is, it would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
-Variance.dfy(80,13): Error: using the type being defined ('CheckRec2') here violates strict positivity, that is, it would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
+Variance.dfy(64,18): Error: formal type parameter 'D' is not used according to its variance specification (it is used left of an arrow) (perhaps try declaring 'D' as '-D' or '!D')
+Variance.dfy(69,17): Error: using the type being defined ('CheckRec') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
+Variance.dfy(71,16): Error: using the type being defined ('CheckRec') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
+Variance.dfy(74,22): Error: using the type being defined ('CheckRec') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
+Variance.dfy(75,27): Error: using the type being defined ('CheckRec') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
+Variance.dfy(77,37): Error: using the type being defined ('CheckRec') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
+Variance.dfy(80,13): Error: using the type being defined ('CheckRec2') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
 Variance.dfy(83,28): Error: class declarations only support non-variant type parameters
 Variance.dfy(83,38): Error: class declarations only support non-variant type parameters
 Variance.dfy(91,30): Error: iterator declarations only support non-variant type parameters
 Variance.dfy(91,40): Error: iterator declarations only support non-variant type parameters
-Variance.dfy(95,21): Error: using the type being defined ('Dt') here violates strict positivity, that is, it would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
-Variance.dfy(99,26): Error: using the type being defined ('U2') here violates strict positivity, that is, it would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
-Variance.dfy(101,21): Error: using the type being defined ('R2') here violates strict positivity, that is, it would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
-Variance.dfy(108,21): Error: using the type being defined ('W0') here violates strict positivity, that is, it would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
-Variance.dfy(110,21): Error: using the type being defined ('Z2') here violates strict positivity, that is, it would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
+Variance.dfy(95,21): Error: using the type being defined ('Dt') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
+Variance.dfy(99,26): Error: using the type being defined ('U2') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
+Variance.dfy(101,21): Error: using the type being defined ('R2') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
+Variance.dfy(108,21): Error: using the type being defined ('W0') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
+Variance.dfy(110,21): Error: using the type being defined ('Z2') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
 Variance.dfy(116,7): Error: recursive constraint dependency involving a subset type: V0 -> V2 -> V1 -> V0
 Variance.dfy(122,7): Error: recursive constraint dependency involving a subset type: A -> B -> F -> A
 Variance.dfy(130,7): Error: recursive constraint dependency involving a subset type: R -> S -> G -> Q -> R

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

@@ -57,8 +57,8 @@ module GeneralFunction1 {
     assert !f(dd);
   }
 }
-git-issue-1219.dfy(5,39): Error: using the type being defined ('CheckRussell') here violates strict positivity, that is, it would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
-git-issue-1219.dfy(21,11): Error: using the type being defined ('DD') here violates strict positivity, that is, it would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
-git-issue-1219.dfy(36,23): Error: using the type being defined ('DD') here violates strict positivity, that is, it would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
-git-issue-1219.dfy(49,23): Error: using the type being defined ('D') here violates strict positivity, that is, it would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
+git-issue-1219.dfy(5,39): Error: using the type being defined ('CheckRussell') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
+git-issue-1219.dfy(21,11): Error: using the type being defined ('DD') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
+git-issue-1219.dfy(36,23): Error: using the type being defined ('DD') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
+git-issue-1219.dfy(49,23): Error: using the type being defined ('D') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
 4 resolution/type errors detected in git-issue-1219.dfy