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.

12 files changed, 160 insertions, 47 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index dfd37954..1ca5e4d9 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -3332,7 +3332,7 @@ namespace Microsoft.Dafny {
   ///    Here, Path may either be of the form C.Init

   ///      -- represents new C.Init(EE)

   ///    or all of Path denotes a type

-  ///      -- represents new C._ctor(EE), where _ctor is the default constructor for class C

+  ///      -- represents new C._ctor(EE), where _ctor is the anonymous constructor for class C

   ///  * TypeRhs(Path, s, EE)

   ///    Here, Path must denote a type and s is a string that denotes the method/constructor Init

   ///      -- represents new Path.s(EE)

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 06e5e640..82d774fc 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -984,7 +984,7 @@ namespace Microsoft.Dafny
                 members.Add(extraName, extraMember);

               }

             } else if (m is Constructor && !((Constructor)m).HasName) {

-              Error(m, "More than one default constructor");

+              Error(m, "More than one anonymous constructor");

             } else {

               Error(m, "Duplicate member name: {0}", m.Name);

             }

@@ -1804,10 +1804,9 @@ namespace Microsoft.Dafny
               }

             }

           }

-        } else if (expr is MapDisplayExpr) {

-          CheckTypeIsDetermined(expr.tok, expr.Type, "map constructor", true);

-        } else if (expr is DisplayExpression) {

-          CheckTypeIsDetermined(expr.tok, expr.Type, "collection constructor", true);

+        } else if (expr is IdentifierExpr) {

+          // by specializing for IdentifierExpr, error messages will be clearer

+          CheckTypeIsDetermined(expr.tok, expr.Type, "variable");

         } else if (CheckTypeIsDetermined(expr.tok, expr.Type, "expression")) {

           var bin = expr as BinaryExpr;

           if (bin != null) {

@@ -1816,12 +1815,14 @@ namespace Microsoft.Dafny
         }

       }

       /// <summary>

-      /// This method checks to see if 'tp' has been determined and returns the result.

-      /// However, if tp denotes an int-based or real-based type, then tp is set to int or real,

-      /// respectively, here.

+      /// This method checks to see if 't' has been determined and returns the result.

+      /// However, if t denotes an int-based or real-based type, then t is set to int or real,

+      /// respectively, here.  Similarly, if t is an unresolved type for "null", then t

+      /// is set to "object".

       /// </summary>

       public static bool IsDetermined(Type t) {

         Contract.Requires(t != null);

+        Contract.Requires(!(t is TypeProxy) || ((TypeProxy)t).T == null);

         // If the type specifies an arbitrary int-based or real-based type, just fill it in with int or real, respectively

         if (t is OperationTypeProxy) {

           var proxy = (OperationTypeProxy)t;

@@ -1832,15 +1833,21 @@ namespace Microsoft.Dafny
             proxy.T = Type.Real;

             return true;

           }

+        } else if (t is ObjectTypeProxy) {

+          var proxy = (ObjectTypeProxy)t;

+          proxy.T = new ObjectType();

+          return true;

         }

         return !(t is TypeProxy);  // all other proxies indicate the type has not yet been determined

       }

-      bool CheckTypeIsDetermined(IToken tok, Type t, string what, bool aggressive = false) {

+      ISet<TypeProxy> UnderspecifiedTypeProxies = new HashSet<TypeProxy>();

+      bool CheckTypeIsDetermined(IToken tok, Type t, string what) {

         Contract.Requires(tok != null);

         Contract.Requires(t != null);

         Contract.Requires(what != null);

         t = t.NormalizeExpand();

-        // If the type specifies an arbitrary int-based or real-based type, just fill it in with int or real, respectively

+        // If the type specifies an arbitrary int-based or real-based type, just fill it in with int or real, respectively;

+        // similarly, if t refers to the type of "null", set its type to be "object".

         if (t is OperationTypeProxy) {

           var proxy = (OperationTypeProxy)t;

           if (proxy.JustInts) {

@@ -1850,18 +1857,29 @@ namespace Microsoft.Dafny
             proxy.T = Type.Real;

             return true;

           }

+        } else if (t is ObjectTypeProxy) {

+          var proxy = (ObjectTypeProxy)t;

+          proxy.T = new ObjectType();

+          return true;

         }

 

-        if (t is TypeProxy && (aggressive || !(t is InferredTypeProxy || t is ParamTypeProxy || t is ObjectTypeProxy))) {

-          Error(tok, "the type of this {0} is underspecified, but it cannot be an opaque type.", what);

+        if (t is TypeProxy) {

+          var proxy = (TypeProxy)t;

+          if (!UnderspecifiedTypeProxies.Contains(proxy)) {

+            // report an error for this TypeProxy only once

+            Error(tok, "the type of this {0} is underspecified", what);

+            UnderspecifiedTypeProxies.Add(proxy);

+          }

           return false;

-        } else if (aggressive && t is MapType) {

-          return CheckTypeIsDetermined(tok, ((MapType)t).Range, what, aggressive) &&

-                 CheckTypeIsDetermined(tok, ((MapType)t).Domain, what, aggressive);

-        } else if (aggressive && t is CollectionType) {

-          return CheckTypeIsDetermined(tok, ((CollectionType)t).Arg, what, aggressive);

-        } else if (aggressive && t is UserDefinedType) {

-          return t.TypeArgs.All(rg => CheckTypeIsDetermined(tok, rg, what, aggressive));

+        }

+        // Recurse on type arguments:

+        if (t is MapType) {

+          return CheckTypeIsDetermined(tok, ((MapType)t).Range, what) &&

+                 CheckTypeIsDetermined(tok, ((MapType)t).Domain, what);

+        } else if (t is CollectionType) {

+          return CheckTypeIsDetermined(tok, ((CollectionType)t).Arg, what);

+        } else if (t is UserDefinedType) {

+          return t.TypeArgs.All(rg => CheckTypeIsDetermined(tok, rg, what));

         } else {

           return true;

         }

@@ -5766,7 +5784,7 @@ namespace Microsoft.Dafny
           var initCallTok = rr.Tok;

           if (rr.OptionalNameComponent == null && rr.Arguments != null) {

             // Resolve rr.EType and do one of three things:

-            // * If rr.EType denotes a type, then set rr.OptionalNameComponent to "_ctor", which sets up a call to the default constructor.

+            // * If rr.EType denotes a type, then set rr.OptionalNameComponent to "_ctor", which sets up a call to the anonymous constructor.

             // * If the all-but-last components of rr.EType denote a type, then do EType,OptionalNameComponent := allButLast(EType),last(EType)

             // * Otherwise, report an error

             var ret = ResolveTypeLenient(stmt.Tok, rr.EType, codeContext, new ResolveTypeOption(ResolveTypeOptionEnum.InferTypeProxies), null, true);

@@ -5856,7 +5874,7 @@ namespace Microsoft.Dafny
 #endif

           var kind = cd is IteratorDecl ? "iterator" : "class";

           if (memberName == "_ctor") {

-            Error(tok, "{0} {1} does not have a default constructor", kind, ctype.Name);

+            Error(tok, "{0} {1} does not have a anonymous constructor", kind, ctype.Name);

           } else {

             Error(tok, "member {0} does not exist in {2} {1}", memberName, ctype.Name, kind);

           }

@@ -6768,7 +6786,7 @@ namespace Microsoft.Dafny
         QuantifierExpr e = (QuantifierExpr)expr;

         int prevErrorCount = ErrorCount;

         bool _val = true;

-        bool typeQuantifier = Attributes.ContainsBool(e.Attributes, "typeQuantifier", ref _val);

+        bool typeQuantifier = Attributes.ContainsBool(e.Attributes, "typeQuantifier", ref _val) && _val;

         allTypeParameters.PushMarker();

         ResolveTypeParameters(e.TypeArgs, true, e);

         scope.PushMarker();

@@ -6776,7 +6794,7 @@ namespace Microsoft.Dafny
           if (!scope.Push(v.Name, v)) {

             Error(v, "Duplicate bound-variable name: {0}", v.Name);

           }

-          var option = typeQuantifier ? new ResolveTypeOption(e) : new ResolveTypeOption(ResolveTypeOptionEnum.DontInfer);

+          var option = typeQuantifier ? new ResolveTypeOption(e) : new ResolveTypeOption(ResolveTypeOptionEnum.InferTypeProxies);

           ResolveType(v.tok, v.Type, opts.codeContext, option, typeQuantifier ? e.TypeArgs : null);

         }

         if (e.TypeArgs.Count > 0 && !typeQuantifier) {

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 21a5dea5..bfd748a2 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -6505,8 +6505,7 @@ namespace Microsoft.Dafny {
       while (true) {

         type = type.NormalizeExpand();

         if (type is TypeProxy) {

-          // unresolved proxy; just treat as ref, since no particular type information is apparently needed for this type

-          return predef.RefType;

+          Contract.Assume(false);  // we assume that all proxies should have been dealt with in the resolver

         }

         var d = type.AsNewtype;

         if (d == null) {

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