Stricter rules about that types need to be completely resolved.

Renamed "default constructor" to "anonymous constructor" (since there's really nothing "default" about it).
If the type of literal "null" is unresolved, make the type "object".
The need to translate unresolved proxies is now assumed to be gone.

9 files changed, 117 insertions, 21 deletions

diff --git a/Test/dafny0/CoResolution.dfy.expect b/Test/dafny0/CoResolution.dfy.expect
index 196b3faa..9acb5a58 100644
--- a/Test/dafny0/CoResolution.dfy.expect
+++ b/Test/dafny0/CoResolution.dfy.expect
@@ -20,5 +20,6 @@ CoResolution.dfy(149,4): Error: a recursive call from a copredicate can go only
 CoResolution.dfy(151,4): Error: a recursive call from a copredicate can go only to other copredicates

 CoResolution.dfy(167,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

 CoResolution.dfy(202,12): Error: type variable '_T0' in the function call to 'A' could not be determined

+CoResolution.dfy(202,12): Error: the type of this expression is underspecified

 CoResolution.dfy(202,19): Error: type variable '_T0' in the function call to 'S' could not be determined

-23 resolution/type errors detected in CoResolution.dfy

+24 resolution/type errors detected in CoResolution.dfy

diff --git a/Test/dafny0/DisplayExpressions.dfy b/Test/dafny0/DisplayExpressions.dfy
index 767cfcdb..ef7d4062 100644
--- a/Test/dafny0/DisplayExpressions.dfy
+++ b/Test/dafny0/DisplayExpressions.dfy
@@ -2,20 +2,25 @@
 // RUN: %diff "%s.expect" "%t"

 method M()

 {

-  var m := map[];

+  var m := map[];  // error: underspecified type

 }

 

 method N()

 {

-  var n := multiset{};

+  var n := multiset{};  // error: underspecified type

 }

 

 method O()

 {

-  var o := [];

+  var o := [];  // error: underspecified type

 }

 

 method P()

 {

-  var p := {};

+  var p := {};  // error: underspecified type

+}

+

+method Q()

+{

+  assert (((map[]))) == (((((map[])))));  // error (but not 10 errors)

 }

diff --git a/Test/dafny0/DisplayExpressions.dfy.expect b/Test/dafny0/DisplayExpressions.dfy.expect
index 7374db2a..e12353f7 100644
--- a/Test/dafny0/DisplayExpressions.dfy.expect
+++ b/Test/dafny0/DisplayExpressions.dfy.expect
@@ -1,5 +1,6 @@
-DisplayExpressions.dfy(5,11): Error: the type of this map constructor is underspecified, but it cannot be an opaque type.

-DisplayExpressions.dfy(10,11): Error: the type of this collection constructor is underspecified, but it cannot be an opaque type.

-DisplayExpressions.dfy(15,11): Error: the type of this collection constructor is underspecified, but it cannot be an opaque type.

-DisplayExpressions.dfy(20,11): Error: the type of this collection constructor is underspecified, but it cannot be an opaque type.

-4 resolution/type errors detected in DisplayExpressions.dfy

+DisplayExpressions.dfy(5,6): Error: the type of this variable is underspecified

+DisplayExpressions.dfy(10,6): Error: the type of this variable is underspecified

+DisplayExpressions.dfy(15,6): Error: the type of this variable is underspecified

+DisplayExpressions.dfy(20,6): Error: the type of this variable is underspecified

+DisplayExpressions.dfy(25,12): Error: the type of this expression is underspecified

+5 resolution/type errors detected in DisplayExpressions.dfy

diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy
index 9a76777a..d343a84d 100644
--- a/Test/dafny0/Parallel.dfy
+++ b/Test/dafny0/Parallel.dfy
@@ -196,7 +196,7 @@ ghost method DontDoMuch(x: int)
 }

 

 method OmittedRange() {

-  forall (x) { }

+  forall (x: int) { }  // a type is still needed for the bound variable

   forall (x) {

     DontDoMuch(x);

   }

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 38f2f9c2..79e7ac57 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -555,8 +555,8 @@ module NonInferredType {
   method NonInferredType0(x: int)

   {

     var t;

-    assume forall z :: P(z) && z == t;

-    assume t == x;  // this statement determined the type of z

+    assume forall z :: P(z) && z == t;  // It would be nice to allow the following example, but the implementation calls DiscoverBounds before CheckInference for quantifiers.

+    assume t == x;  // this statement determines the type of t and z

   }

 

   method NonInferredType1(x: int)

@@ -1159,3 +1159,84 @@ method NonTermination_D()
     n := n + 1;

   }

 }

+

+// ------------ type variables whose values are not inferred ----------

+

+module NonInferredTypeVariables {

+  class C<CT> {

+    var f: CT;

+  }

+

+  predicate method P<PT>(x: int)

+  {

+    x < 100

+  }

+  function Q<QT>(x: int): QT

+  {

+    var qt :| true; qt

+  }

+  method M<MT>(n: nat)

+  {

+    var a := new MT[n];

+  }

+  method N<NT>(n: nat) returns (x: NT)

+  {

+    var a := new NT[10];

+    x := a[3];

+  }

+

+  method DeterminedClient(n: nat)

+  {

+    ghost var q := Q(n);

+    var x := N(n);

+    var a := new array;

+    var c := new C;

+    var s: set;

+    var ss := new set[15];

+

+    q := 3.14;  // this will determine the type parameter of Q to be 'real'

+    x := 3.14;  // this will determine the type parameter of N to be 'real'

+    if a.Length != 0 {

+      a[0] := 3.14;  // this will determine the type parameter of 'array' to be 'real'

+    }

+    c.f := 3.14;  // this will determine the type parameter of 'C' to be 'real'

+    var containsPi := 3.14 in s;  // this will determine the type parameter of 'set' to be 'real'

+    ss[12] := s;  // this will determine the type parameter of 'array<set< _ >>' to be 'real'

+  }

+  method BadClient(n: nat)

+  {

+    var p := P(n);  // error: cannot infer the type argument for P

+    ghost var q := Q(n);  // error: cannot infer the type argument for Q

+    M(n);  // error: cannot infer the type argument for M

+    var x := N(n);  // error: cannot infer the type argument for N

+    var a := new array;  // error: cannot infer the type argument for 'array'

+    var c := new C;  // error: cannot infer the type argument for 'C'

+    var s: set;  // type argument for 'set' 

+    var ss := new set[15];  // error: cannot infer the type argument in 'array<set< _ >>'

+    var what;  // error: the type of this local variable in underspecified

+  }

+  method MoreBadClient()

+  {

+    var b0 := forall s :: s <= {} ==> s == {};  // error: type of s underspecified

+    var b1 := forall s: set :: s <= {} ==> s == {};  // error: type of s underspecified

+    var b2 := forall c: C :: c in {null} ==> c == null;  // error: type of s underspecified

+

+    // In the following, the type of the bound variable is completely determined.

+    var S: set<set<int>>;

+    ghost var d0 := forall s :: s == {7} ==> s != {};

+    var d1 := forall s: set :: s in S ==> s == {};

+    var ggcc0: C;

+    var ggcc1: C;

+    ghost var d2 := forall c: C :: c != null ==> c.f == 10;

+    ghost var d2' := forall c :: c == ggcc0 && c != null ==> c.f == 10;

+    ghost var d2'' := forall c :: c == ggcc1 && c != null ==> c.f == c.f; // error: here, type of c is not determined

+

+    /* TODO: Dafny's heuristic that looks for bounds should look for equality to

+     *       accept these.

+    var d0' := forall s :: s == {7} ==> s != {};

+    var d0'' := forall s :: s <= {7} ==> s == {};

+    var ggcc2: C;

+    var d2''' := forall c :: c == ggcc2 && c != null ==> c.f == 10;

+     */

+  }

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 3f08e72a..1b802687 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -2,7 +2,9 @@ ResolutionErrors.dfy(499,7): Error: RHS (of type List<A>) not assignable to LHS
 ResolutionErrors.dfy(504,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)

 ResolutionErrors.dfy(518,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)

 ResolutionErrors.dfy(530,24): Error: Wrong number of type arguments (0 instead of 2) passed to class/datatype: Tree

+ResolutionErrors.dfy(558,25): Error: the type of this variable is underspecified

 ResolutionErrors.dfy(558,23): Error: type variable 'T' in the function call to 'P' could not be determined

+ResolutionErrors.dfy(565,25): Error: the type of this variable is underspecified

 ResolutionErrors.dfy(565,23): Error: type variable 'T' in the function call to 'P' could not be determined

 ResolutionErrors.dfy(578,13): Error: 'new' is not allowed in ghost contexts

 ResolutionErrors.dfy(579,9): Error: 'new' is not allowed in ghost contexts

@@ -16,8 +18,7 @@ ResolutionErrors.dfy(608,10): Error: ghost variables are allowed only in specifi
 ResolutionErrors.dfy(617,17): Error: 'new' is not allowed in ghost contexts

 ResolutionErrors.dfy(619,20): Error: only ghost methods can be called from this context

 ResolutionErrors.dfy(621,8): Error: calls to methods with side-effects are not allowed inside a hint

-ResolutionErrors.dfy(639,21): Error: the type of this expression is underspecified, but it cannot be an opaque type.

-ResolutionErrors.dfy(639,21): Error: the type of this expression is underspecified, but it cannot be an opaque type.

+ResolutionErrors.dfy(639,21): Error: the type of this variable is underspecified

 ResolutionErrors.dfy(676,8): Error: calls to methods with side-effects are not allowed inside a hint

 ResolutionErrors.dfy(686,8): Error: only ghost methods can be called from this context

 ResolutionErrors.dfy(689,20): Error: 'decreases *' is not allowed on ghost loops

@@ -78,7 +79,11 @@ ResolutionErrors.dfy(1089,13): Error: arguments must have the same type (got P<b
 ResolutionErrors.dfy(1090,13): Error: arguments must have the same type (got P<int> and P<bool>)

 ResolutionErrors.dfy(1113,38): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'

 ResolutionErrors.dfy(1115,24): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'

-ResolutionErrors.dfy(429,2): Error: More than one default constructor

+ResolutionErrors.dfy(1220,26): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1221,31): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1222,29): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1232,34): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(429,2): Error: More than one anonymous constructor

 ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context

 ResolutionErrors.dfy(111,9): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(112,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

@@ -99,7 +104,7 @@ ResolutionErrors.dfy(240,8): Error: return statement is not allowed in this cont
 ResolutionErrors.dfy(435,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called

 ResolutionErrors.dfy(440,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called

 ResolutionErrors.dfy(441,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called

-ResolutionErrors.dfy(443,9): Error: class Lamb does not have a default constructor

+ResolutionErrors.dfy(443,9): Error: class Lamb does not have a anonymous constructor

 ResolutionErrors.dfy(839,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int)

 ResolutionErrors.dfy(843,14): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)

 ResolutionErrors.dfy(846,12): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)

@@ -175,4 +180,4 @@ ResolutionErrors.dfy(1101,8): Error: new cannot be applied to a trait
 ResolutionErrors.dfy(1122,13): Error: first argument to / must be of numeric type (instead got set<bool>)

 ResolutionErrors.dfy(1129,2): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating

 ResolutionErrors.dfy(1144,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating

-177 resolution/type errors detected in ResolutionErrors.dfy

+182 resolution/type errors detected in ResolutionErrors.dfy

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index a208b1b6..d6658671 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -512,7 +512,7 @@ class AttributeTests {
 

 static method TestAttributesVarDecls()

 {

-  var {:foo} foo;

+  var {:foo} foo := null;

   var {:bar} bar := 0;

   var {:foo} {:bar} foobar : set<int> := {};

   var {:baz} baz, {:foobaz} foobaz := true, false;

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 31819dcc..6086fcf1 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -68,7 +68,7 @@ method DuplicateVarName(x: int) returns (y: int)
 method ScopeTests()

 {

   var x := x;  // error: the 'x' in the RHS is not in scope

-  var y :| y == y;  // fine, 'y' is in scope in the RHS

+  var y: real :| y == y;  // fine, 'y' is in scope in the RHS

   var z := DuplicateVarName(z);  // error: the 'z' in the RHS is not in scope

   var w0, w1 := IntTransform(w1), IntTransform(w0);  // errors two

   var c := new MyClass.Init(null);  // fine

diff --git a/Test/hofs/Underspecified.dfy.expect b/Test/hofs/Underspecified.dfy.expect
index 04394d78..a5970830 100644
--- a/Test/hofs/Underspecified.dfy.expect
+++ b/Test/hofs/Underspecified.dfy.expect
@@ -1,5 +1,8 @@
+Underspecified.dfy(6,6): Error: the type of this variable is underspecified

 Underspecified.dfy(6,11): Error: type of bound variable '_v0' could not be determined; please specify the type explicitly

+Underspecified.dfy(7,6): Error: the type of this variable is underspecified

 Underspecified.dfy(7,12): Error: type of bound variable '_v1' could not be determined; please specify the type explicitly

 Underspecified.dfy(7,15): Error: type of bound variable '_v2' could not be determined; please specify the type explicitly

+Underspecified.dfy(8,6): Error: the type of this variable is underspecified

 Underspecified.dfy(8,11): Error: type of bound variable 'a' could not be determined; please specify the type explicitly

-4 resolution/type errors detected in Underspecified.dfy

+7 resolution/type errors detected in Underspecified.dfy