4 files changed, 1418 insertions, 976 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 7046f9a4..c94c697d 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -550,13 +550,21 @@ namespace Microsoft.Dafny
         r = new ForallStmt(Tok(s.Tok), Tok(s.EndTok), s.BoundVars.ConvertAll(CloneBoundVar), null, CloneExpr(s.Range), s.Ens.ConvertAll(CloneMayBeFreeExpr), CloneStmt(s.Body));
 
       } else if (stmt is CalcStmt) {
-          var s = (CalcStmt)stmt;
-          r = new CalcStmt(Tok(s.Tok), Tok(s.EndTok), CloneCalcOp(s.Op), s.Lines.ConvertAll(CloneExpr), s.Hints.ConvertAll(CloneBlockStmt), s.StepOps.ConvertAll(CloneCalcOp), CloneCalcOp(s.ResultOp), CloneAttributes(s.Attributes));
+        var s = (CalcStmt)stmt;
+        // calc statements have the unusual property that the last line is duplicated.  If that is the case (which
+        // we expect it to be here), we share the clone of that line as well.
+        var lineCount = s.Lines.Count;
+        var lines = new List<Expression>(lineCount);
+        for (int i = 0; i < lineCount; i++) {
+          lines.Add(i == lineCount - 1 && 2 <= lineCount && s.Lines[i] == s.Lines[i - 1] ? lines[i - 1] : CloneExpr(s.Lines[i]));
+        }
+        Contract.Assert(lines.Count == lineCount);
+        r = new CalcStmt(Tok(s.Tok), Tok(s.EndTok), CloneCalcOp(s.Op), lines, s.Hints.ConvertAll(CloneBlockStmt), s.StepOps.ConvertAll(CloneCalcOp), CloneCalcOp(s.ResultOp), CloneAttributes(s.Attributes));
 
       } else if (stmt is MatchStmt) {
         var s = (MatchStmt)stmt;
         r = new MatchStmt(Tok(s.Tok), Tok(s.EndTok), CloneExpr(s.Source),
-          s.Cases.ConvertAll(CloneMatchCaseStmt), s.UsesOptionalBraces);
+        s.Cases.ConvertAll(CloneMatchCaseStmt), s.UsesOptionalBraces);
 
       } else if (stmt is AssignSuchThatStmt) {
         var s = (AssignSuchThatStmt)stmt;
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 123433bc..13381cc7 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1610,6 +1610,9 @@ namespace Microsoft.Dafny {
           if (bound is ComprehensionExpr.BoolBoundedPool) {
             Indent(ind);
             wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);
+          } else if (bound is ComprehensionExpr.CharBoundedPool) {
+            Indent(ind);
+            wr.Write("foreach (var @{0} in Dafny.Helpers.AllChars) {{ ", bv.CompileName);
           } else if (bound is ComprehensionExpr.IntBoundedPool) {
             var b = (ComprehensionExpr.IntBoundedPool)bound;
             Indent(ind);
@@ -1821,6 +1824,8 @@ namespace Microsoft.Dafny {
         Indent(ind);
         if (bound is ComprehensionExpr.BoolBoundedPool) {
           wr.WriteLine("foreach (var {0} in Dafny.Helpers.AllBooleans) {{ @{1} = {0};", tmpVar, bv.CompileName);
+        } else if (bound is ComprehensionExpr.CharBoundedPool) {
+          wr.WriteLine("foreach (var {0} in Dafny.Helpers.AllChars) {{ @{1} = {0};", tmpVar, bv.CompileName);
         } else if (bound is ComprehensionExpr.IntBoundedPool) {
           var b = (ComprehensionExpr.IntBoundedPool)bound;
           if (AsNativeType(bv.Type) != null) {
@@ -2875,6 +2880,8 @@ namespace Microsoft.Dafny {
           // emit:  Dafny.Helpers.QuantX(boundsInformation, isForall, bv => body)
           if (bound is ComprehensionExpr.BoolBoundedPool) {
             wr.Write("Dafny.Helpers.QuantBool(");
+          } else if (bound is ComprehensionExpr.CharBoundedPool) {
+            wr.Write("Dafny.Helpers.QuantChar(");
           } else if (bound is ComprehensionExpr.IntBoundedPool) {
             var b = (ComprehensionExpr.IntBoundedPool)bound;
             wr.Write("Dafny.Helpers.QuantInt(");
@@ -2942,6 +2949,8 @@ namespace Microsoft.Dafny {
           var bv = e.BoundVars[i];
           if (bound is ComprehensionExpr.BoolBoundedPool) {
             wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);
+          } else if (bound is ComprehensionExpr.CharBoundedPool) {
+            wr.Write("foreach (var @{0} in Dafny.Helpers.AllChars) {{ ", bv.CompileName);
           } else if (bound is ComprehensionExpr.IntBoundedPool) {
             var b = (ComprehensionExpr.IntBoundedPool)bound;
             if (AsNativeType(bv.Type) != null) {
@@ -3015,6 +3024,8 @@ namespace Microsoft.Dafny {
         var bv = e.BoundVars[0];
         if (bound is ComprehensionExpr.BoolBoundedPool) {
           wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);
+        } else if (bound is ComprehensionExpr.CharBoundedPool) {
+          wr.Write("foreach (var @{0} in Dafny.Helpers.AllChars) {{ ", bv.CompileName);
         } else if (bound is ComprehensionExpr.IntBoundedPool) {
           var b = (ComprehensionExpr.IntBoundedPool)bound;
           if (AsNativeType(bv.Type) != null) {
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 116b9004..4fc48f2f 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -526,6 +526,27 @@ namespace Microsoft.Dafny {
       }
     }
 
+    public bool HasFinitePossibleValues {
+      get {
+        if (IsBoolType || IsCharType || IsRefType) {
+          return true;
+        }
+        var st = AsSetType;
+        if (st != null && st.Arg.HasFinitePossibleValues) {
+          return true;
+        }
+        var mt = AsMapType;
+        if (mt != null && mt.Domain.HasFinitePossibleValues) {
+          return true;
+        }
+        var dt = AsDatatype;
+        if (dt != null && dt.HasFinitePossibleValues) {
+          return true;
+        }
+        return false;
+      }
+    }
+
     public CollectionType AsCollectionType { get { return NormalizeExpand() as CollectionType; } }
     public SetType AsSetType { get { return NormalizeExpand() as SetType; } }
     public MultiSetType AsMultiSetType { get { return NormalizeExpand() as MultiSetType; } }
@@ -1676,7 +1697,7 @@ namespace Microsoft.Dafny {
                                               // it is abstract). Otherwise, it points to that definition.
     public ModuleSignature CompileSignature = null; // This is the version of the signature that should be used at compile time.
     public ModuleSignature Refines = null;
-    public bool IsGhost = false;
+    public bool IsAbstract = false;
     public ModuleSignature() {}
 
     public bool FindSubmodule(string name, out ModuleSignature pp) {
@@ -2417,6 +2438,48 @@ namespace Microsoft.Dafny {
     }
 
     /// <summary>
+    /// Returns the non-null expressions of this declaration proper (that is, do not include the expressions of substatements).
+    /// Does not include the generated class members.
+    /// </summary>
+    public virtual IEnumerable<Expression> SubExpressions {
+      get {
+        foreach (var e in Attributes.SubExpressions(Attributes)) {
+          yield return e;
+        }
+        foreach (var e in Attributes.SubExpressions(Reads.Attributes)) {
+          yield return e;
+        }
+        foreach (var e in Reads.Expressions) {
+          yield return e.E;
+        }
+        foreach (var e in Attributes.SubExpressions(Modifies.Attributes)) {
+          yield return e;
+        }
+        foreach (var e in Modifies.Expressions) {
+          yield return e.E;
+        }
+        foreach (var e in Attributes.SubExpressions(Decreases.Attributes)) {
+          yield return e;
+        }
+        foreach (var e in Decreases.Expressions) {
+          yield return e;
+        }
+        foreach (var e in Requires) {
+          yield return e.E;
+        }
+        foreach (var e in Ensures) {
+          yield return e.E;
+        }
+        foreach (var e in YieldRequires) {
+          yield return e.E;
+        }
+        foreach (var e in YieldEnsures) {
+          yield return e.E;
+        }
+      }
+    }
+
+    /// <summary>
     /// This Dafny type exists only for the purpose of giving the yield-count variable a type, so
     /// that the type can be recognized during translation of Dafny into Boogie.  It represents
     /// an integer component in a "decreases" clause whose order is (\lambda x,y :: x GREATER y),
@@ -2523,6 +2586,11 @@ namespace Microsoft.Dafny {
         return EnclosingClass.FullCompileName + ".@" + CompileName;
       }
     }
+    public virtual IEnumerable<Expression> SubExpressions {
+      get {
+        yield break;
+      }
+    }
   }
 
   public class Field : MemberDecl {
@@ -3047,6 +3115,26 @@ namespace Microsoft.Dafny {
     public bool IsBuiltin;
     public Function OverriddenFunction;
 
+    public override IEnumerable<Expression> SubExpressions {
+      get {
+        foreach (var e in Req) {
+          yield return e;
+        }
+        foreach (var e in Reads) {
+          yield return e.E;
+        }
+        foreach (var e in Ens) {
+          yield return e;
+        }
+        foreach (var e in Decreases.Expressions) {
+          yield return e;
+        }
+        if (Body != null) {
+          yield return Body;
+        }
+      }
+    }
+
     public Type Type {
       get {
         // Note, the following returned type can contain type parameters from the function and its enclosing class
@@ -3261,6 +3349,24 @@ namespace Microsoft.Dafny {
     public readonly ISet<IVariable> AssignedAssumptionVariables = new HashSet<IVariable>();
     public Method OverriddenMethod;
 
+    public override IEnumerable<Expression> SubExpressions {
+      get {
+        foreach (var e in Req) {
+          yield return e.E;
+        }
+        foreach (var e in Mod.Expressions) {
+          yield return e.E;
+        }
+        foreach (var e in Ens) {
+          yield return e.E;
+        }
+        foreach (var e in Decreases.Expressions) {
+          yield return e;
+        }
+      }
+    }
+
+
     [ContractInvariantMethod]
     void ObjectInvariant() {
       Contract.Invariant(cce.NonNullElements(TypeArgs));
@@ -4100,17 +4206,41 @@ namespace Microsoft.Dafny {
     /// </summary>
     public static bool LhsIsToGhost(Expression lhs) {
       Contract.Requires(lhs != null);
+      return LhsIsToGhost_Which(lhs) == NonGhostKind.IsGhost;
+    }
+    public enum NonGhostKind { IsGhost, Variable, Field, ArrayElement }
+    public static string NonGhostKind_To_String(NonGhostKind gk) {
+      Contract.Requires(gk != NonGhostKind.IsGhost);
+      switch (gk) {
+        case NonGhostKind.Variable: return "non-ghost variable";
+        case NonGhostKind.Field: return "non-ghost field";
+        case NonGhostKind.ArrayElement: return "array element";
+        default:
+          Contract.Assume(false);  // unexpected NonGhostKind
+          throw new cce.UnreachableException();  // please compiler
+      }
+    }
+    /// <summary>
+    /// This method assumes "lhs" has been successfully resolved.
+    /// </summary>
+    public static NonGhostKind LhsIsToGhost_Which(Expression lhs) {
+      Contract.Requires(lhs != null);
       lhs = lhs.Resolved;
       if (lhs is IdentifierExpr) {
         var x = (IdentifierExpr)lhs;
-        return x.Var.IsGhost;
+        if (!x.Var.IsGhost) {
+          return NonGhostKind.Variable;
+        }
       } else if (lhs is MemberSelectExpr) {
         var x = (MemberSelectExpr)lhs;
-        return x.Member.IsGhost;
+        if (!x.Member.IsGhost) {
+          return NonGhostKind.Field;
+        }
       } else {
         // LHS denotes an array element, which is always non-ghost
-        return false;
+        return NonGhostKind.ArrayElement;
       }
+      return NonGhostKind.IsGhost;
     }
   }
 
@@ -4845,18 +4975,32 @@ namespace Microsoft.Dafny {
     }
     public override IEnumerable<Expression> SubExpressions
     {
-      get { // FIXME: This can return duplicates; this could confuse BottomUpVisitors that modify the AST in place
+      get {
         foreach (var e in base.SubExpressions) { yield return e; }
         foreach (var e in Attributes.SubExpressions(Attributes)) { yield return e; }
-        
-        foreach (var l in Lines) {
-          yield return l;
+
+        for (int i = 0; i < Lines.Count - 1; i++) {  // note, we skip the duplicated line at the end
+          yield return Lines[i];
         }
-        foreach (var e in Steps) {
-          yield return e;
+        foreach (var calcop in AllCalcOps) {
+          var o3 = calcop as TernaryCalcOp;
+          if (o3 != null) {
+            yield return o3.Index;
+          }
+        }
+      }
+    }
+
+    IEnumerable<CalcOp> AllCalcOps {
+      get {
+        if (Op != null) {
+          yield return Op;
+        }
+        foreach (var stepop in StepOps) {
+          yield return stepop;
         }
-        if (Result != null) {
-          yield return Result;
+        if (ResultOp != null) {
+          yield return ResultOp;
         }
       }
     }
@@ -6670,7 +6814,7 @@ namespace Microsoft.Dafny {
     public readonly Expression Body;
     public readonly bool Exact;  // Exact==true means a regular let expression; Exact==false means an assign-such-that expression
     public readonly Attributes Attributes;
-    public List<ComprehensionExpr.BoundedPool> Constraint_Bounds;  // initialized and filled in by resolver; null for Exact=true and for a ghost statement
+    public List<ComprehensionExpr.BoundedPool> Constraint_Bounds;  // initialized and filled in by resolver; null for Exact=true and for when expression is in a ghost context
     // invariant Constraint_Bounds == null || Constraint_Bounds.Count == BoundVars.Count;
     public List<IVariable> Constraint_MissingBounds;  // filled in during resolution; remains "null" if Exact==true or if bounds can be found
     // invariant Constraint_Bounds == null || Constraint_MissingBounds == null;
@@ -6823,6 +6967,22 @@ namespace Microsoft.Dafny {
         return 5;
       }
     }
+    public class CharBoundedPool : BoundedPool
+    {
+      public override int Preference() {
+        return 4;
+      }
+    }
+    public class RefBoundedPool : BoundedPool
+    {
+      public Type Type;
+      public RefBoundedPool(Type t) {
+        Type = t;
+      }
+      public override int Preference() {
+        return 2;
+      }
+    }
     public class IntBoundedPool : BoundedPool
     {
       public readonly Expression LowerBound;
@@ -6897,6 +7057,24 @@ namespace Microsoft.Dafny {
     public List<BoundVar> MissingBounds;  // filled in during resolution; remains "null" if bounds can be found
     // invariant Bounds == null || MissingBounds == null;
 
+    public List<BoundVar> UncompilableBoundVars() {
+      var bvs = new List<BoundVar>();
+      if (MissingBounds != null) {
+        bvs.AddRange(MissingBounds);
+      }
+      if (Bounds != null) {
+        Contract.Assert(Bounds.Count == BoundVars.Count);
+        for (int i = 0; i < Bounds.Count; i++) {
+          var bound = Bounds[i];
+          if (bound is RefBoundedPool) {
+            // yes, this is in principle a bound, but it's not one we'd like to compile
+            bvs.Add(BoundVars[i]);
+          }
+        }
+      }
+      return bvs;
+    }
+
     public ComprehensionExpr(IToken tok, List<BoundVar> bvars, Expression range, Expression term, Attributes attrs)
       : base(tok) {
       Contract.Requires(tok != null);
@@ -7798,24 +7976,6 @@ namespace Microsoft.Dafny {
 
   public class BottomUpVisitor
   {
-    public void Visit(Expression expr) {
-      Contract.Requires(expr != null);
-      // recursively visit all subexpressions and all substatements
-      expr.SubExpressions.Iter(Visit);
-      if (expr is StmtExpr) {
-        // a StmtExpr also has a sub-statement
-        var e = (StmtExpr)expr;
-        Visit(e.S);
-      }
-      VisitOneExpr(expr);
-    }
-    public void Visit(Statement stmt) {
-      Contract.Requires(stmt != null);
-      // recursively visit all subexpressions and all substatements
-      stmt.SubExpressions.Iter(Visit);
-      stmt.SubStatements.Iter(Visit);
-      VisitOneStmt(stmt);
-    }
     public void Visit(IEnumerable<Expression> exprs) {
       exprs.Iter(Visit);
     }
@@ -7858,6 +8018,24 @@ namespace Microsoft.Dafny {
       if (function.Body != null) { Visit(function.Body); }
       //TODO More?
     }
+    public void Visit(Expression expr) {
+      Contract.Requires(expr != null);
+      // recursively visit all subexpressions and all substatements
+      expr.SubExpressions.Iter(Visit);
+      if (expr is StmtExpr) {
+        // a StmtExpr also has a sub-statement
+        var e = (StmtExpr)expr;
+        Visit(e.S);
+      }
+      VisitOneExpr(expr);
+    }
+    public void Visit(Statement stmt) {
+      Contract.Requires(stmt != null);
+      // recursively visit all subexpressions and all substatements
+      stmt.SubExpressions.Iter(Visit);
+      stmt.SubStatements.Iter(Visit);
+      VisitOneStmt(stmt);
+    }
     protected virtual void VisitOneExpr(Expression expr) {
       Contract.Requires(expr != null);
       // by default, do nothing
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 210cd4ac..0b0bbf26 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -345,7 +345,7 @@ namespace Microsoft.Dafny
                       "module " + Util.Comma(".", abs.CompilePath, x => x.val) + " must be a refinement of "
                       + Util.Comma(".", abs.Path, x => x.val));
                   }
-                  abs.Signature.IsGhost = compileSig.IsGhost;
+                  abs.Signature.IsAbstract = compileSig.IsAbstract;
                   // always keep the ghost information, to supress a spurious error message when the compile module isn't actually a refinement
                 }
               }
@@ -667,13 +667,17 @@ namespace Microsoft.Dafny
     }
 
     private void ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig) {
+      Contract.Requires(AllTypeConstraints.Count == 0);
+      Contract.Ensures(AllTypeConstraints.Count == 0);
       moduleInfo = MergeSignature(sig, systemNameInfo);
       // resolve
       var datatypeDependencies = new Graph<IndDatatypeDecl>();
       var codatatypeDependencies = new Graph<CoDatatypeDecl>();
       int prevErrorCount = reporter.Count(ErrorLevel.Error);
       ResolveTopLevelDecls_Signatures(m, m.TopLevelDecls, datatypeDependencies, codatatypeDependencies);
+      Contract.Assert(AllTypeConstraints.Count == 0);  // signature resolution does not add any type constraints
       ResolveAttributes(m.Attributes, new ResolveOpts(new NoContext(m.Module), false)); // Must follow ResolveTopLevelDecls_Signatures, in case attributes refer to members
+      SolveAllTypeConstraints();  // solve any type constraints entailed by the attributes
       if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
         ResolveTopLevelDecls_Core(m.TopLevelDecls, datatypeDependencies, codatatypeDependencies);
       }
@@ -831,14 +835,14 @@ namespace Microsoft.Dafny
       foreach (var kv in m.StaticMembers) {
         info.StaticMembers[kv.Key] = kv.Value;
       }
-      info.IsGhost = m.IsGhost;
+      info.IsAbstract = m.IsAbstract;
       return info;
     }
     ModuleSignature RegisterTopLevelDecls(ModuleDefinition moduleDef, bool useImports) {
       Contract.Requires(moduleDef != null);
       var sig = new ModuleSignature();
       sig.ModuleDef = moduleDef;
-      sig.IsGhost = moduleDef.IsAbstract;
+      sig.IsAbstract = moduleDef.IsAbstract;
       List<TopLevelDecl> declarations = moduleDef.TopLevelDecls;
 
       // First go through and add anything from the opened imports
@@ -1260,7 +1264,7 @@ namespace Microsoft.Dafny
       var sig = RegisterTopLevelDecls(mod, false);
       sig.Refines = p.Refines;
       sig.CompileSignature = p;
-      sig.IsGhost = p.IsGhost;
+      sig.IsAbstract = p.IsAbstract;
       sig.ExclusiveRefinement = p.ExclusiveRefinement;
       mods.Add(mod);
       ResolveModuleDefinition(mod, sig);
@@ -1352,7 +1356,7 @@ namespace Microsoft.Dafny
         } else if (d is ModuleDecl) {
           var decl = (ModuleDecl)d;
           if (!def.IsAbstract) {
-            if (decl.Signature.IsGhost)
+            if (decl.Signature.IsAbstract)
               {
                 if (// _module is allowed to contain abstract modules, but not be abstract itself. Note this presents a challenge to
                                             // trusted verification, as toplevels can't be trusted if they invoke abstract module members.
@@ -1390,15 +1394,6 @@ namespace Microsoft.Dafny
       }
     }
 
-    private readonly List<SetComprehension> needFiniteBoundsChecks_SetComprehension = new List<SetComprehension>();
-    private readonly List<LetExpr> needFiniteBoundsChecks_LetSuchThatExpr = new List<LetExpr>();
-    public int NFBC_Count {
-      // provided just for the purpose of conveniently writing contracts for ResolveTopLevelDecl_Meat
-      get {
-        return needFiniteBoundsChecks_SetComprehension.Count + needFiniteBoundsChecks_LetSuchThatExpr.Count;
-      }
-    }
-
     static readonly List<NativeType> NativeTypes = new List<NativeType>() {
       new NativeType("byte", 0, 0x100, "", true),
       new NativeType("sbyte", -0x80, 0x80, "", true),
@@ -1414,11 +1409,18 @@ namespace Microsoft.Dafny
       Contract.Requires(declarations != null);
       Contract.Requires(cce.NonNullElements(datatypeDependencies));
       Contract.Requires(cce.NonNullElements(codatatypeDependencies));
-      Contract.Requires(NFBC_Count == 0);
-      Contract.Ensures(NFBC_Count == 0);
+      Contract.Requires(AllTypeConstraints.Count == 0);
+      Contract.Ensures(AllTypeConstraints.Count == 0);
 
       int prevErrorCount = reporter.Count(ErrorLevel.Error);
 
+      // ---------------------------------- Pass 0 ----------------------------------
+      // This pass resolves names, introduces (and may solve) type constraints, and
+      // builds the module's call graph.
+      // For 'newtype' declarations, it also checks that all types were fully
+      // determined.
+      // ----------------------------------------------------------------------------
+
       // Resolve the meat of classes and iterators, the definitions of type synonyms, and the type parameters of all top-level type declarations
       // First, resolve the newtype declarations and the constraint clauses, including filling in .ResolvedOp fields.  This is needed for the
       // resolution of the other declarations, because those other declarations may invoke DiscoverBounds, which looks at the .Constraint field
@@ -1442,21 +1444,21 @@ namespace Microsoft.Dafny
             var added = scope.Push(dd.Var.Name, dd.Var);
             Contract.Assert(added == Scope<IVariable>.PushResult.Success);
             ResolveType(dd.Var.tok, dd.Var.Type, dd, ResolveTypeOptionEnum.DontInfer, null);
-            ResolveExpression(dd.Constraint, new ResolveOpts(dd, false, true));
+            ResolveExpression(dd.Constraint, new ResolveOpts(dd, false));
             Contract.Assert(dd.Constraint.Type != null);  // follows from postcondition of ResolveExpression
-            if (!UnifyTypes(dd.Constraint.Type, Type.Bool)) {
-              reporter.Error(MessageSource.Resolver, dd.Constraint, "newtype constraint must be of type bool (instead got {0})", dd.Constraint.Type);
-            }
+            ConstrainTypes(dd.Constraint.Type, Type.Bool, dd.Constraint, "newtype constraint must be of type bool (instead got {0})", dd.Constraint.Type);
+            SolveAllTypeConstraints();
             if (!CheckTypeInference_Visitor.IsDetermined(dd.BaseType.NormalizeExpand())) {
               reporter.Error(MessageSource.Resolver, dd.tok, "newtype's base type is not fully determined; add an explicit type for '{0}'", dd.Var.Name);
             }
-            CheckTypeInference(dd.Constraint);
+            CheckTypeInference(dd.Constraint, dd);
             scope.PopMarker();
           }
         }
       }
       // Now, we're ready for the other declarations.
       foreach (TopLevelDecl d in declarations) {
+        Contract.Assert(AllTypeConstraints.Count == 0);
         if (d is TraitDecl && d.TypeArgs.Count > 0) {
           reporter.Error(MessageSource.Resolver, d, "sorry, traits with type parameters are not supported");
         }
@@ -1477,149 +1479,84 @@ namespace Microsoft.Dafny
         allTypeParameters.PopMarker();
       }
 
-      if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
-        foreach (var e in needFiniteBoundsChecks_SetComprehension) {
-          CheckTypeInference(e.Range);  // we need to resolve operators before the call to DiscoverBounds
-          List<BoundVar> missingBounds;
-          e.Bounds = DiscoverBestBounds_MultipleVars(e.BoundVars, e.Range, true, true, out missingBounds);
-          if (missingBounds.Count != 0) {
-            e.MissingBounds = missingBounds;
-            if (e.Finite) {
-              foreach (var bv in e.MissingBounds) {
-              reporter.Error(MessageSource.Resolver, e, "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 '{0}'", bv.Name);
-              }
-            }
-          }
-        }
-        foreach (var e in needFiniteBoundsChecks_LetSuchThatExpr) {
-          Contract.Assert(!e.Exact);  // only let-such-that expressions are ever added to the list
-          Contract.Assert(e.RHSs.Count == 1);  // if we got this far, the resolver will have checked this condition successfully
-          var constraint = e.RHSs[0];
-          CheckTypeInference(constraint);  // we need to resolve operators before the call to DiscoverBounds
-          List<IVariable> missingBounds;
-          var vars = new List<IVariable>(e.BoundVars);
-          var bestBounds = DiscoverBestBounds_MultipleVars(vars, constraint, true, false, out missingBounds);
-          if (missingBounds.Count != 0) {
-            e.Constraint_MissingBounds = missingBounds;
-            foreach (var bv in e.Constraint_MissingBounds) {
-              reporter.Error(MessageSource.Resolver, e, "a non-ghost let-such-that constraint must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
-            }
-          } else {
-            e.Constraint_Bounds = bestBounds;
-          }
-        }
-      }
-      needFiniteBoundsChecks_SetComprehension.Clear();
-      needFiniteBoundsChecks_LetSuchThatExpr.Clear();
+      // ---------------------------------- Pass 1 ----------------------------------
+      // This pass:
+      // * checks that type inference was able to determine all types
+      // * fills in the .ResolvedOp field of binary expressions
+      // * discovers bounds for:
+      //     - forall statements
+      //     - set comprehensions
+      //     - map comprehensions
+      //     - quantifier expressions
+      //     - assign-such-that statements
+      //     - compilable let-such-that expressions
+      //     - newtype constraints
+      // For each statement body that it successfully typed, this pass also:
+      // * computes ghost interests
+      // * determines/checks tail-recursion.
+      // ----------------------------------------------------------------------------
 
       Dictionary<string, NativeType> nativeTypeMap = new Dictionary<string, NativeType>();
       foreach (var nativeType in NativeTypes) {
         nativeTypeMap.Add(nativeType.Name, nativeType);
       }
-
       if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
         // Check that type inference went well everywhere; this will also fill in the .ResolvedOp field in binary expressions
         foreach (TopLevelDecl d in declarations) {
           if (d is IteratorDecl) {
             var iter = (IteratorDecl)d;
+            var prevErrCnt = reporter.Count(ErrorLevel.Error);
             iter.Members.Iter(CheckTypeInference_Member);
+            if (prevErrCnt == reporter.Count(ErrorLevel.Error)) {
+              iter.SubExpressions.Iter(e => CheckExpression(e, this, iter));
+            }
             if (iter.Body != null) {
-              CheckTypeInference(iter.Body);
+              CheckTypeInference(iter.Body, iter);
+              if (prevErrCnt == reporter.Count(ErrorLevel.Error)) {
+                ComputeGhostInterest(iter.Body, false, iter);
+                CheckExpression(iter.Body, this, iter);
+              }
             }
           } else if (d is ClassDecl) {
             var cl = (ClassDecl)d;
-            cl.Members.Iter(CheckTypeInference_Member);
-          } else if (d is NewtypeDecl) {
-            var dd = (NewtypeDecl)d;
-            bool? boolNativeType = null;
-            NativeType stringNativeType = null;
-            object nativeTypeAttr = true;
-            bool hasNativeTypeAttr = Attributes.ContainsMatchingValue(dd.Attributes, "nativeType", ref nativeTypeAttr,
-              new Attributes.MatchingValueOption[] {
-                Attributes.MatchingValueOption.Empty,
-                Attributes.MatchingValueOption.Bool,
-                Attributes.MatchingValueOption.String },
-              err => reporter.Error(MessageSource.Resolver, dd, err));
-            if (hasNativeTypeAttr) {
-              if (nativeTypeAttr is bool) {
-                boolNativeType = (bool)nativeTypeAttr;
-              } else {
-                string keyString = (string)nativeTypeAttr;
-                if (nativeTypeMap.ContainsKey(keyString)) {
-                  stringNativeType = nativeTypeMap[keyString];
-                } else {
-                  reporter.Error(MessageSource.Resolver, dd, "Unsupported nativeType {0}", keyString);
+            foreach (var member in cl.Members) {
+              var prevErrCnt = reporter.Count(ErrorLevel.Error);
+              CheckTypeInference_Member(member);
+              if (prevErrCnt == reporter.Count(ErrorLevel.Error)) {
+                if (member is Method) {
+                  var m = (Method)member;
+                  if (m.Body != null) {
+                    ComputeGhostInterest(m.Body, m.IsGhost, m);
+                    CheckExpression(m.Body, this, m);
+                    DetermineTailRecursion(m);
+                  }
+                } else if (member is Function) {
+                  var f = (Function)member;
+                  if (!f.IsGhost && f.Body != null) {
+                    CheckIsCompilable(f.Body);
+                  }
+                  DetermineTailRecursion(f);
+                }
+                if (prevErrCnt == reporter.Count(ErrorLevel.Error) && member is ICodeContext) {
+                  member.SubExpressions.Iter(e => CheckExpression(e, this, (ICodeContext)member));
                 }
               }
             }
-            if (stringNativeType != null || boolNativeType == true) {
-              if (!dd.BaseType.IsNumericBased(Type.NumericPersuation.Int)) {
-                reporter.Error(MessageSource.Resolver, dd, "nativeType can only be used on integral types");
-              }
-              if (dd.Var == null) {
-                reporter.Error(MessageSource.Resolver, dd, "nativeType can only be used if newtype specifies a constraint");
-              }
-            }
+          } else if (d is NewtypeDecl) {
+            var dd = (NewtypeDecl)d;
             if (dd.Var != null) {
               Contract.Assert(dd.Constraint != null);
-              CheckTypeInference(dd.Constraint);
-
-              Func<Expression, BigInteger?> GetConst = null;
-              GetConst = (Expression e) => {
-                int m = 1;
-                BinaryExpr bin = e as BinaryExpr;
-                if (bin != null && bin.Op == BinaryExpr.Opcode.Sub && GetConst(bin.E0) == BigInteger.Zero) {
-                  m = -1;
-                  e = bin.E1;
-                }
-                LiteralExpr l = e as LiteralExpr;
-                if (l != null && l.Value is BigInteger) {
-                  return m * (BigInteger)l.Value;
-                }
-                return null;
-              };
-              var bounds = DiscoverAllBounds_SingleVar(dd.Var, dd.Constraint);
-              List<NativeType> potentialNativeTypes =
-                (stringNativeType != null) ? new List<NativeType> { stringNativeType } :
-                (boolNativeType == false) ? new List<NativeType>() :
-                NativeTypes;
-              foreach (var nt in potentialNativeTypes) {
-                bool lowerOk = false;
-                bool upperOk = false;
-                foreach (var bound in bounds) {
-                  if (bound is ComprehensionExpr.IntBoundedPool) {
-                    var bnd = (ComprehensionExpr.IntBoundedPool)bound;
-                    if (bnd.LowerBound != null) {
-                      BigInteger? lower = GetConst(bnd.LowerBound);
-                      if (lower != null && nt.LowerBound <= lower) {
-                        lowerOk = true;
-                      }
-                    }
-                    if (bnd.UpperBound != null) {
-                      BigInteger? upper = GetConst(bnd.UpperBound);
-                      if (upper != null && upper <= nt.UpperBound) {
-                        upperOk = true;
-                      }
-                    }
-                  }
-                }
-                if (lowerOk && upperOk) {
-                  dd.NativeType = nt;
-                  break;
-                }
-              }
-              if (dd.NativeType == null && (boolNativeType == true || stringNativeType != null)) {
-                reporter.Error(MessageSource.Resolver, dd, "Dafny's heuristics cannot find a compatible native type.  " +
-                  "Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)'");
-              }
-              if (dd.NativeType != null && stringNativeType == null) {
-                reporter.Info(MessageSource.Resolver, dd.tok, "{:nativeType \"" + dd.NativeType.Name + "\"}");
-              }
+              CheckExpression(dd.Constraint, this, dd);
             }
+            FigureOutNativeType(dd, nativeTypeMap);
           }
         }
       }
 
+      // ---------------------------------- Pass 2 ----------------------------------
+      // This pass fills in various additional information.
+      // ----------------------------------------------------------------------------
+
       if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
         // fill in the postconditions and bodies of prefix lemmas
         foreach (var com in ModuleDefinition.AllFixpointLemmas(declarations)) {
@@ -1944,6 +1881,222 @@ namespace Microsoft.Dafny
       }
     }
 
+    private void FigureOutNativeType(NewtypeDecl dd, Dictionary<string, NativeType> nativeTypeMap) {
+      Contract.Requires(dd != null);
+      Contract.Requires(nativeTypeMap != null);
+      bool? boolNativeType = null;
+      NativeType stringNativeType = null;
+      object nativeTypeAttr = true;
+      bool hasNativeTypeAttr = Attributes.ContainsMatchingValue(dd.Attributes, "nativeType", ref nativeTypeAttr,
+        new Attributes.MatchingValueOption[] {
+                Attributes.MatchingValueOption.Empty,
+                Attributes.MatchingValueOption.Bool,
+                Attributes.MatchingValueOption.String },
+        err => reporter.Error(MessageSource.Resolver, dd, err));
+      if (hasNativeTypeAttr) {
+        if (nativeTypeAttr is bool) {
+          boolNativeType = (bool)nativeTypeAttr;
+        } else {
+          string keyString = (string)nativeTypeAttr;
+          if (nativeTypeMap.ContainsKey(keyString)) {
+            stringNativeType = nativeTypeMap[keyString];
+          } else {
+            reporter.Error(MessageSource.Resolver, dd, "Unsupported nativeType {0}", keyString);
+          }
+        }
+      }
+      if (stringNativeType != null || boolNativeType == true) {
+        if (!dd.BaseType.IsNumericBased(Type.NumericPersuation.Int)) {
+          reporter.Error(MessageSource.Resolver, dd, "nativeType can only be used on integral types");
+        }
+        if (dd.Var == null) {
+          reporter.Error(MessageSource.Resolver, dd, "nativeType can only be used if newtype specifies a constraint");
+        }
+      }
+      if (dd.Var != null) {
+        Func<Expression, BigInteger?> GetConst = null;
+        GetConst = (Expression e) => {
+          int m = 1;
+          BinaryExpr bin = e as BinaryExpr;
+          if (bin != null && bin.Op == BinaryExpr.Opcode.Sub && GetConst(bin.E0) == BigInteger.Zero) {
+            m = -1;
+            e = bin.E1;
+          }
+          LiteralExpr l = e as LiteralExpr;
+          if (l != null && l.Value is BigInteger) {
+            return m * (BigInteger)l.Value;
+          }
+          return null;
+        };
+        var bounds = DiscoverAllBounds_SingleVar(dd.Var, dd.Constraint);
+        List<NativeType> potentialNativeTypes =
+          (stringNativeType != null) ? new List<NativeType> { stringNativeType } :
+          (boolNativeType == false) ? new List<NativeType>() :
+          NativeTypes;
+        foreach (var nt in potentialNativeTypes) {
+          bool lowerOk = false;
+          bool upperOk = false;
+          foreach (var bound in bounds) {
+            if (bound is ComprehensionExpr.IntBoundedPool) {
+              var bnd = (ComprehensionExpr.IntBoundedPool)bound;
+              if (bnd.LowerBound != null) {
+                BigInteger? lower = GetConst(bnd.LowerBound);
+                if (lower != null && nt.LowerBound <= lower) {
+                  lowerOk = true;
+                }
+              }
+              if (bnd.UpperBound != null) {
+                BigInteger? upper = GetConst(bnd.UpperBound);
+                if (upper != null && upper <= nt.UpperBound) {
+                  upperOk = true;
+                }
+              }
+            }
+          }
+          if (lowerOk && upperOk) {
+            dd.NativeType = nt;
+            break;
+          }
+        }
+        if (dd.NativeType == null && (boolNativeType == true || stringNativeType != null)) {
+          reporter.Error(MessageSource.Resolver, dd, "Dafny's heuristics cannot find a compatible native type.  " +
+            "Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)'");
+        }
+        if (dd.NativeType != null && stringNativeType == null) {
+          reporter.Info(MessageSource.Resolver, dd.tok, "{:nativeType \"" + dd.NativeType.Name + "\"}");
+        }
+      }
+    }
+
+    /// <summary>
+    /// Adds the type constraint ty==expected, eventually printing the error message "msg" if this is found to be
+    /// untenable.  If this is immediately known not to be untenable, false is returned.
+    /// </summary>
+    private bool ConstrainTypes(Type ty, Type expected, TopLevelDecl declForToken, string msg, params object[] args) {
+      Contract.Requires(ty != null);
+      Contract.Requires(expected != null);
+      Contract.Requires(declForToken != null);
+      Contract.Requires(msg != null);
+      Contract.Requires(args != null);
+      return ConstrainTypes(ty, expected, declForToken.tok, msg, args);
+    }
+    /// <summary>
+    /// Adds the type constraint ty==expected, eventually printing the error message "msg" if this is found to be
+    /// untenable.  If this is immediately known not to be untenable, false is returned.
+    /// </summary>
+    private bool ConstrainTypes(Type ty, Type expected, MemberDecl declForToken, string msg, params object[] args) {
+      Contract.Requires(ty != null);
+      Contract.Requires(expected != null);
+      Contract.Requires(declForToken != null);
+      Contract.Requires(msg != null);
+      Contract.Requires(args != null);
+      return ConstrainTypes(ty, expected, declForToken.tok, msg, args);
+    }
+    /// <summary>
+    /// Adds the type constraint ty==expected, eventually printing the error message "msg" if this is found to be
+    /// untenable.  If this is immediately known not to be untenable, false is returned.
+    /// </summary>
+    private bool ConstrainTypes(Type ty, Type expected, Statement stmtForToken, string msg, params object[] args) {
+      Contract.Requires(ty != null);
+      Contract.Requires(expected != null);
+      Contract.Requires(stmtForToken != null);
+      Contract.Requires(msg != null);
+      Contract.Requires(args != null);
+      return ConstrainTypes(ty, expected, stmtForToken.Tok, msg, args);
+    }
+    /// <summary>
+    /// Adds the type constraint ty==expected, eventually printing the error message "msg" if this is found to be
+    /// untenable.  If this is immediately known not to be untenable, false is returned.
+    /// </summary>
+    private bool ConstrainTypes(Type ty, Type expected, Expression exprForToken, string msg, params object[] args) {
+      Contract.Requires(ty != null);
+      Contract.Requires(expected != null);
+      Contract.Requires(exprForToken != null);
+      Contract.Requires(msg != null);
+      Contract.Requires(args != null);
+      return ConstrainTypes(ty, expected, exprForToken.tok, msg, args);
+    }
+    /// <summary>
+    /// Adds the type constraint ty==expected, eventually printing the error message "msg" if this is found to be
+    /// untenable.  If this is immediately known not to be untenable, false is returned.
+    /// </summary>
+    private bool ConstrainTypes(Type ty, Type expected, IToken tok, string msg, params object[] args) {
+      Contract.Requires(ty != null);
+      Contract.Requires(expected != null);
+      Contract.Requires(tok != null);
+      Contract.Requires(msg != null);
+      Contract.Requires(args != null);
+#if LAZY_TYPE_CHECKING
+      var c = new TypeConstraint(ty, expected, tok, msg, args);
+      AllTypeConstraints.Add(c);
+      return true;
+#else
+      if (!UnifyTypes(ty, expected)) {
+        reporter.Error(MessageSource.Resolver, tok, msg, args);
+        return false;
+      }
+      return true;
+#endif
+    }
+
+    public List<TypeConstraint> AllTypeConstraints = new List<TypeConstraint>();
+
+    /// <summary>
+    /// Solves or simplifies as many type constraints as possible
+    /// </summary>
+    void PartiallySolveTypeConstraints() {
+      var remainingConstraints = new List<TypeConstraint>();
+      foreach (var constraint in AllTypeConstraints) {
+        if (!constraint.CheckTenable(this)) {
+          remainingConstraints.Add(constraint);
+        }
+      }
+      AllTypeConstraints = remainingConstraints;
+    }
+
+    /// <summary>
+    /// Attempts to fully solve all type constraints.  Upon success, returns "true".
+    /// Upon failure, reports errors and returns "false".
+    /// Clears all constraints.
+    /// </summary>
+    bool SolveAllTypeConstraints() {
+      PartiallySolveTypeConstraints();
+      foreach (var constraint in AllTypeConstraints) {
+        constraint.ReportAsError(reporter);
+      }
+      var success = AllTypeConstraints.Count == 0;
+      AllTypeConstraints.Clear();
+      return success;
+    }
+
+    public class TypeConstraint
+    {
+      readonly Type Ty;
+      readonly Type Expected;
+      readonly IToken Tok;
+      readonly string Msg;
+      readonly object[] MsgArgs;
+      public TypeConstraint(Type ty, Type expected, IToken tok, string msg, object[] msgArgs) {
+        Ty = ty;
+        Expected = expected;
+        Tok = tok;
+        Msg = msg;
+        MsgArgs = msgArgs;
+      }
+      /// <summary>
+      /// Returns "true" if constraint is tenable, "false" otherwise.
+      /// </summary>
+      /// <returns></returns>
+      public bool CheckTenable(Resolver resolver) {
+        Contract.Requires(resolver != null);
+        return resolver.UnifyTypes(Ty, Expected);
+      }
+      public void ReportAsError(ErrorReporter reporter) {
+        Contract.Requires(reporter != null);
+        reporter.Error(MessageSource.Resolver, Tok, Msg, MsgArgs);
+      }
+    }
+
     // ------------------------------------------------------------------------------------------------------
     // ----- Visitors ---------------------------------------------------------------------------------------
     // ------------------------------------------------------------------------------------------------------
@@ -1973,49 +2126,22 @@ namespace Microsoft.Dafny
     private void CheckTypeInference_Member(MemberDecl member) {
       if (member is Method) {
         var m = (Method)member;
-        m.Req.Iter(CheckTypeInference_MaybeFreeExpression);
-        m.Ens.Iter(CheckTypeInference_MaybeFreeExpression);
-        CheckTypeInference_Specification_FrameExpr(m.Mod);
-        CheckTypeInference_Specification_Expr(m.Decreases);
+        m.Req.Iter(mfe => CheckTypeInference_MaybeFreeExpression(mfe, m));
+        m.Ens.Iter(mfe => CheckTypeInference_MaybeFreeExpression(mfe, m));
+        CheckTypeInference_Specification_FrameExpr(m.Mod, m);
+        CheckTypeInference_Specification_Expr(m.Decreases, m);
         if (m.Body != null) {
-          CheckTypeInference(m.Body);
-          bool tail = true;
-          bool hasTailRecursionPreference = Attributes.ContainsBool(m.Attributes, "tailrecursion", ref tail);
-          if (hasTailRecursionPreference && !tail) {
-            // the user specifically requested no tail recursion, so do nothing else
-          } else if (hasTailRecursionPreference && tail && m.IsGhost) {
-            reporter.Error(MessageSource.Resolver, m.tok, "tail recursion can be specified only for methods that will be compiled, not for ghost methods");
-          } else {
-            var module = m.EnclosingClass.Module;
-            var sccSize = module.CallGraph.GetSCCSize(m);
-            if (hasTailRecursionPreference && 2 <= sccSize) {
-              reporter.Error(MessageSource.Resolver, m.tok, "sorry, tail-call optimizations are not supported for mutually recursive methods");
-            } else if (hasTailRecursionPreference || sccSize == 1) {
-              CallStmt tailCall = null;
-              var status = CheckTailRecursive(m.Body.Body, m, ref tailCall, hasTailRecursionPreference);
-              if (status != TailRecursionStatus.NotTailRecursive) {
-                m.IsTailRecursive = true;
-                if (tailCall != null) {
-                  // this means there was at least one recursive call
-                  reporter.Info(MessageSource.Resolver, m.tok, "tail recursive");
-                }
-              }
-            }
-          }
+          CheckTypeInference(m.Body, m);
         }
       } else if (member is Function) {
         var f = (Function)member;
         var errorCount = reporter.Count(ErrorLevel.Error);
-        f.Req.Iter(CheckTypeInference);
-        f.Ens.Iter(CheckTypeInference);
-        f.Reads.Iter(fe => CheckTypeInference(fe.E));
-        CheckTypeInference_Specification_Expr(f.Decreases);
+        f.Req.Iter(e => CheckTypeInference(e, f));
+        f.Ens.Iter(e => CheckTypeInference(e, f));
+        f.Reads.Iter(fe => CheckTypeInference(fe.E, f));
+        CheckTypeInference_Specification_Expr(f.Decreases, f);
         if (f.Body != null) {
-          CheckTypeInference(f.Body);
-          bool tail = true;
-          if (Attributes.ContainsBool(f.Attributes, "tailrecursion", ref tail) && tail) {
-            reporter.Error(MessageSource.Resolver, f.tok, "sorry, tail-call functions are not supported");
-          }
+          CheckTypeInference(f.Body, f);
         }
         if (errorCount == reporter.Count(ErrorLevel.Error) && f is FixpointPredicate) {
           var cop = (FixpointPredicate)f;
@@ -2023,42 +2149,52 @@ namespace Microsoft.Dafny
         }
       }
     }
-    private void CheckTypeInference_MaybeFreeExpression(MaybeFreeExpression mfe) {
+
+    private void CheckTypeInference_MaybeFreeExpression(MaybeFreeExpression mfe, ICodeContext codeContext) {
       Contract.Requires(mfe != null);
+      Contract.Requires(codeContext != null);
       foreach (var e in Attributes.SubExpressions(mfe.Attributes)) {
-        CheckTypeInference(e);
+        CheckTypeInference(e, codeContext);
       }
-      CheckTypeInference(mfe.E);
+      CheckTypeInference(mfe.E, codeContext);
     }
-    private void CheckTypeInference_Specification_Expr(Specification<Expression> spec) {
+    private void CheckTypeInference_Specification_Expr(Specification<Expression> spec, ICodeContext codeContext) {
       Contract.Requires(spec != null);
+      Contract.Requires(codeContext != null);
       foreach (var e in Attributes.SubExpressions(spec.Attributes)) {
-        CheckTypeInference(e);
+        CheckTypeInference(e, codeContext);
       }
-      spec.Expressions.Iter(CheckTypeInference);
+      spec.Expressions.Iter(e => CheckTypeInference(e, codeContext));
     }
-    private void CheckTypeInference_Specification_FrameExpr(Specification<FrameExpression> spec) {
+    private void CheckTypeInference_Specification_FrameExpr(Specification<FrameExpression> spec, ICodeContext codeContext) {
       Contract.Requires(spec != null);
+      Contract.Requires(codeContext != null);
       foreach (var e in Attributes.SubExpressions(spec.Attributes)) {
-        CheckTypeInference(e);
+        CheckTypeInference(e, codeContext);
       }
-      spec.Expressions.Iter(fe => CheckTypeInference(fe.E));
+      spec.Expressions.Iter(fe => CheckTypeInference(fe.E, codeContext));
     }
-    void CheckTypeInference(Expression expr) {
+    void CheckTypeInference(Expression expr, ICodeContext codeContext) {
       Contract.Requires(expr != null);
-      var c = new CheckTypeInference_Visitor(this);
+      Contract.Requires(codeContext != null);
+      PartiallySolveTypeConstraints();
+      var c = new CheckTypeInference_Visitor(this, codeContext);
       c.Visit(expr);
     }
-    void CheckTypeInference(Statement stmt) {
+    void CheckTypeInference(Statement stmt, ICodeContext codeContext) {
       Contract.Requires(stmt != null);
-      var c = new CheckTypeInference_Visitor(this);
+      Contract.Requires(codeContext != null);
+      var c = new CheckTypeInference_Visitor(this, codeContext);
       c.Visit(stmt);
     }
     class CheckTypeInference_Visitor : ResolverBottomUpVisitor
     {
-      public CheckTypeInference_Visitor(Resolver resolver)
+      readonly ICodeContext codeContext;
+      public CheckTypeInference_Visitor(Resolver resolver, ICodeContext codeContext)
         : base(resolver) {
         Contract.Requires(resolver != null);
+        Contract.Requires(codeContext != null);
+        this.codeContext = codeContext;
       }
       protected override void VisitOneStmt(Statement stmt) {
         if (stmt is VarDeclStmt) {
@@ -2069,19 +2205,94 @@ namespace Microsoft.Dafny
         } else if (stmt is ForallStmt) {
           var s = (ForallStmt)stmt;
           s.BoundVars.Iter(bv => CheckTypeIsDetermined(bv.tok, bv.Type, "bound variable"));
+          List<BoundVar> missingBounds;
+          s.Bounds = DiscoverBestBounds_MultipleVars(s.BoundVars, s.Range, true, true, out missingBounds);
+
+        } else if (stmt is AssignSuchThatStmt) {
+          var s = (AssignSuchThatStmt)stmt;
+          if (s.AssumeToken == null) {
+            var varLhss = new List<IVariable>();
+            foreach (var lhs in s.Lhss) {
+              var ide = (IdentifierExpr)lhs.Resolved;  // successful resolution implies all LHS's are IdentifierExpr's
+              varLhss.Add(ide.Var);
+            }
+            List<IVariable> missingBounds;
+            var bestBounds = DiscoverBestBounds_MultipleVars(varLhss, s.Expr, true, false, out missingBounds);
+            if (missingBounds.Count != 0) {
+              s.MissingBounds = missingBounds;  // so that an error message can be produced during compilation
+            } else {
+              Contract.Assert(bestBounds != null);
+              s.Bounds = bestBounds;
+            }
+          }
+        } else if (stmt is CalcStmt) {
+          var s = (CalcStmt)stmt;
+          // The resolution of the calc statement builds up .Steps and .Result, which are of the form E0 OP E1, where
+          // E0 and E1 are expressions from .Lines.  These additional expressions still need to have their .ResolvedOp
+          // fields filled in, so we visit them (but not their subexpressions) here.
+          foreach (var e in s.Steps) {
+            VisitOneExpr(e);
+          }
+          VisitOneExpr(s.Result);
         }
       }
       protected override void VisitOneExpr(Expression expr) {
         if (expr is ComprehensionExpr) {
           var e = (ComprehensionExpr)expr;
-          if (e != null) {
-            foreach (var bv in e.BoundVars) {
-              if (!IsDetermined(bv.Type.Normalize())) {
-                resolver.reporter.Error(MessageSource.Resolver, bv.tok, "type of bound variable '{0}' could not be determined; please specify the type explicitly",
-                  bv.Name);
+          foreach (var bv in e.BoundVars) {
+            if (!IsDetermined(bv.Type.Normalize())) {
+              resolver.reporter.Error(MessageSource.Resolver, bv.tok, "type of bound variable '{0}' could not be determined; please specify the type explicitly", bv.Name);
+            }
+          }
+          // apply bounds discovery to quantifiers, finite sets, and finite maps
+          string what = null;
+          Expression whereToLookForBounds = null;
+          bool polarity = true;
+          if (e is QuantifierExpr) {
+            what = "quantifier";
+            whereToLookForBounds = ((QuantifierExpr)e).LogicalBody();
+            polarity = e is ExistsExpr;
+          } else if (e is SetComprehension && ((SetComprehension)e).Finite) {
+            what = "set comprehension";
+            whereToLookForBounds = e.Range;
+          } else if (e is MapComprehension && ((MapComprehension)e).Finite) {
+            what = "map comprehension";
+            whereToLookForBounds = e.Range;
+          }
+          if (whereToLookForBounds != null) {
+            List<BoundVar> missingBounds;
+            e.Bounds = DiscoverBestBounds_MultipleVars(e.BoundVars, whereToLookForBounds, polarity, true, out missingBounds);
+            if (missingBounds.Count != 0) {
+              e.MissingBounds = missingBounds;
+
+              if ((e is SetComprehension && !((SetComprehension)e).Finite) || (e is MapComprehension && !((MapComprehension)e).Finite)) {
+                // a possibly infinite set/map has no restrictions on its range
+              } else if (e is QuantifierExpr) {
+                // don't report any errors at this time (instead, wait to see if the quantifier is used in a non-ghost context)
+              } else if (e is SetComprehension && e.Type.HasFinitePossibleValues) {
+                // This means the set is finite, regardless of if the Range is bounded.  So, we don't give any error here.
+                // However, if this expression is used in a non-ghost context (which is not yet known at this stage of
+                // resolution), the resolver will generate an error about that later.
+              } else {
+                // we cannot be sure that the set/map really is finite
+                foreach (var bv in missingBounds) {
+                  resolver.reporter.Error(MessageSource.Resolver, e, "a {0} must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{1}'", what, bv.Name);
+                }
+              }
+            }
+            if (codeContext is Function && e.Bounds != null) {
+              // functions are not allowed to depend on the set of allocated objects
+              Contract.Assert(e.Bounds.Count == e.BoundVars.Count);
+              for (int i = 0; i < e.Bounds.Count; i++) {
+                var bound = e.Bounds[i] as ComprehensionExpr.RefBoundedPool;
+                if (bound != null) {
+                  var bv = e.BoundVars[i];
+                  resolver.reporter.Error(MessageSource.Resolver, expr, "a {0} involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of '{1}'", what, bv.Name);
+                }
               }
             }
           }
+
         } else if (expr is MemberSelectExpr) {
           var e = (MemberSelectExpr)expr;
           if (e.Member is Function || e.Member is Method) {
@@ -2118,6 +2329,7 @@ namespace Microsoft.Dafny
           var bin = expr as BinaryExpr;
           if (bin != null) {
             bin.ResolvedOp = ResolveOp(bin.Op, bin.E1.Type);
+          
           }
         }
       }
@@ -2196,6 +2408,58 @@ namespace Microsoft.Dafny
     #endregion CheckTypeInference
 
     // ------------------------------------------------------------------------------------------------------
+    // ----- CheckExpression --------------------------------------------------------------------------------
+    // ------------------------------------------------------------------------------------------------------
+    #region CheckExpression
+    /// <summary>
+    /// This method computes ghost interests in the statement portion of StmtExpr's and
+    /// checks for hint restrictions in any CalcStmt.
+    /// </summary>
+    void CheckExpression(Expression expr, Resolver resolver, ICodeContext codeContext) {
+      Contract.Requires(expr != null);
+      Contract.Requires(resolver != null);
+      Contract.Requires(codeContext != null);
+      var v = new CheckExpression_Visitor(resolver, codeContext);
+      v.Visit(expr);
+    }
+    /// <summary>
+    /// This method computes ghost interests in the statement portion of StmtExpr's and
+    /// checks for hint restrictions in any CalcStmt.
+    /// </summary>
+    void CheckExpression(Statement stmt, Resolver resolver, ICodeContext codeContext) {
+      Contract.Requires(stmt != null);
+      Contract.Requires(resolver != null);
+      Contract.Requires(codeContext != null);
+      var v = new CheckExpression_Visitor(resolver, codeContext);
+      v.Visit(stmt);
+    }
+    class CheckExpression_Visitor : ResolverBottomUpVisitor
+    {
+      readonly ICodeContext CodeContext;
+      public CheckExpression_Visitor(Resolver resolver, ICodeContext codeContext)
+        : base(resolver) {
+        Contract.Requires(resolver != null);
+        Contract.Requires(codeContext != null);
+        CodeContext = codeContext;
+      }
+      protected override void VisitOneExpr(Expression expr) {
+        if (expr is StmtExpr) {
+          var e = (StmtExpr)expr;
+          resolver.ComputeGhostInterest(e.S, true, CodeContext);
+        }
+      }
+      protected override void VisitOneStmt(Statement stmt) {
+        if (stmt is CalcStmt) {
+          var s = (CalcStmt)stmt;
+          foreach (var h in s.Hints) {
+            resolver.CheckHintRestrictions(h, new HashSet<LocalVariable>());
+          }
+        }
+      }
+    }
+    #endregion
+
+    // ------------------------------------------------------------------------------------------------------
     // ----- CheckTailRecursive -----------------------------------------------------------------------------
     // ------------------------------------------------------------------------------------------------------
     #region CheckTailRecursive
@@ -2244,6 +2508,41 @@ namespace Microsoft.Dafny
       return status;
     }
 
+    void DetermineTailRecursion(Function f) {
+      Contract.Requires(f != null);
+      bool tail = true;
+      if (Attributes.ContainsBool(f.Attributes, "tailrecursion", ref tail) && tail) {
+        reporter.Error(MessageSource.Resolver, f.tok, "sorry, tail-call functions are not supported");
+      }
+    }
+
+    void DetermineTailRecursion(Method m) {
+      Contract.Requires(m != null);
+      bool tail = true;
+      bool hasTailRecursionPreference = Attributes.ContainsBool(m.Attributes, "tailrecursion", ref tail);
+      if (hasTailRecursionPreference && !tail) {
+        // the user specifically requested no tail recursion, so do nothing else
+      } else if (hasTailRecursionPreference && tail && m.IsGhost) {
+        reporter.Error(MessageSource.Resolver, m.tok, "tail recursion can be specified only for methods that will be compiled, not for ghost methods");
+      } else {
+        var module = m.EnclosingClass.Module;
+        var sccSize = module.CallGraph.GetSCCSize(m);
+        if (hasTailRecursionPreference && 2 <= sccSize) {
+          reporter.Error(MessageSource.Resolver, m.tok, "sorry, tail-call optimizations are not supported for mutually recursive methods");
+        } else if (hasTailRecursionPreference || sccSize == 1) {
+          CallStmt tailCall = null;
+          var status = CheckTailRecursive(m.Body.Body, m, ref tailCall, hasTailRecursionPreference);
+          if (status != TailRecursionStatus.NotTailRecursive) {
+            m.IsTailRecursive = true;
+            if (tailCall != null) {
+              // this means there was at least one recursive call
+              reporter.Info(MessageSource.Resolver, m.tok, "tail recursive");
+            }
+          }
+        }
+      }
+    }
+
     /// <summary>
     /// See CheckTailRecursive(List Statement, ...), including its description of "tailCall".
     /// In the current implementation, "enclosingMethod" is not allowed to be a mutually recursive method.
@@ -2917,6 +3216,312 @@ namespace Microsoft.Dafny
     #endregion CheckEqualityTypes
 
     // ------------------------------------------------------------------------------------------------------
+    // ----- ComputeGhostInterest ---------------------------------------------------------------------------
+    // ------------------------------------------------------------------------------------------------------
+    #region ComputeGhostInterest
+    public void ComputeGhostInterest(Statement stmt, bool mustBeErasable, ICodeContext codeContext) {
+      Contract.Requires(stmt != null);
+      Contract.Requires(codeContext != null);
+      var visitor = new GhostInterest_Visitor(codeContext, this);
+      visitor.Visit(stmt, mustBeErasable);
+    }
+    class GhostInterest_Visitor
+    {
+      readonly ICodeContext codeContext;
+      readonly Resolver resolver;
+      public GhostInterest_Visitor(ICodeContext codeContext, Resolver resolver) {
+        Contract.Requires(codeContext != null);
+        Contract.Requires(resolver != null);
+        this.codeContext = codeContext;
+        this.resolver = resolver;
+      }
+      protected void Error(Statement stmt, string msg, params object[] msgArgs) {
+        Contract.Requires(stmt != null);
+        Contract.Requires(msg != null);
+        Contract.Requires(msgArgs != null);
+        resolver.reporter.Error(MessageSource.Resolver, stmt, msg, msgArgs);
+      }
+      protected void Error(Expression expr, string msg, params object[] msgArgs) {
+        Contract.Requires(expr != null);
+        Contract.Requires(msg != null);
+        Contract.Requires(msgArgs != null);
+        resolver.reporter.Error(MessageSource.Resolver, expr, msg, msgArgs);
+      }
+      protected void Error(IToken tok, string msg, params object[] msgArgs) {
+        Contract.Requires(tok != null);
+        Contract.Requires(msg != null);
+        Contract.Requires(msgArgs != null);
+        resolver.reporter.Error(MessageSource.Resolver, tok, msg, msgArgs);
+      }
+      /// <summary>
+      /// This method does three things, in order:
+      /// 0. Sets .IsGhost to "true" if the statement is ghost.  This often depends on some guard of the statement
+      ///    (like the guard of an "if" statement) or the LHS of the statement (if it is an assignment).
+      ///    Note, if "mustBeErasable", then the statement is already in a ghost context.
+      ///    statement itself is ghost) or and the statement assigns to a non-ghost field
+      /// 1. Determines if the statement and all its subparts are legal under its computed .IsGhost setting.
+      /// 2. ``Upgrades'' .IsGhost to "true" if, after investigation of the substatements of the statement, it
+      ///    turns out that the statement can be erased during compilation.
+      /// Notes:
+      /// * Both step (0) and step (2) sets the .IsGhost field.  What step (0) does affects only the
+      ///   rules of resolution, whereas step (2) makes a note for the later compilation phase.
+      /// * It is important to do step (0) before step (1)--that is, it is important to set the statement's ghost
+      ///   status before descending into its sub-statements--because break statements look at the ghost status of
+      ///   its enclosing statements.
+      /// * The method called by a StmtExpr must be ghost; however, this is checked elsewhere.  For
+      ///   this reason, it is not necessary to visit all subexpressions, unless the subexpression
+      ///   matter for the ghost checking/recording of "stmt".
+      /// </summary>
+      public void Visit(Statement stmt, bool mustBeErasable) {
+        Contract.Requires(stmt != null);
+        Contract.Assume(!codeContext.IsGhost || mustBeErasable);  // (this is really a precondition) codeContext.IsGhost ==> mustBeErasable
+
+        if (stmt is PredicateStmt) {
+          stmt.IsGhost = true;
+
+        } else if (stmt is PrintStmt) {
+          var s = (PrintStmt)stmt;
+          if (mustBeErasable) {
+            Error(stmt, "print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
+          } else {
+            s.Args.Iter(resolver.CheckIsCompilable);
+          }
+
+        } else if (stmt is BreakStmt) {
+          var s = (BreakStmt)stmt;
+          s.IsGhost = mustBeErasable;
+          if (s.IsGhost && !s.TargetStmt.IsGhost) {
+            var targetIsLoop = s.TargetStmt is WhileStmt || s.TargetStmt is AlternativeLoopStmt;
+            Error(stmt, "ghost-context break statement is not allowed to break out of non-ghost " + (targetIsLoop ? "loop" : "structure"));
+          }
+
+        } else if (stmt is ProduceStmt) {
+          var s = (ProduceStmt)stmt;
+          var kind = stmt is YieldStmt ? "yield" : "return";
+          if (mustBeErasable && !codeContext.IsGhost) {
+            Error(stmt, "{0} statement is not allowed in this context (because it is guarded by a specification-only expression)", kind);
+          }
+          if (s.hiddenUpdate != null) {
+            Visit(s.hiddenUpdate, mustBeErasable);
+          }
+
+        } else if (stmt is AssignSuchThatStmt) {
+          var s = (AssignSuchThatStmt)stmt;
+          s.IsGhost = mustBeErasable || s.AssumeToken != null || s.Lhss.Any(AssignStmt.LhsIsToGhost);
+          if (mustBeErasable && !codeContext.IsGhost) {
+            foreach (var lhs in s.Lhss) {
+              var gk = AssignStmt.LhsIsToGhost_Which(lhs);
+              if (gk != AssignStmt.NonGhostKind.IsGhost) {
+                Error(lhs, "cannot assign to {0} in a ghost context", AssignStmt.NonGhostKind_To_String(gk));
+              }
+            }
+          } else if (!mustBeErasable && s.AssumeToken == null && resolver.UsesSpecFeatures(s.Expr)) {
+            foreach (var lhs in s.Lhss) {
+              var gk = AssignStmt.LhsIsToGhost_Which(lhs);
+              if (gk != AssignStmt.NonGhostKind.IsGhost) {
+                Error(lhs, "{0} cannot be assigned a value that depends on a ghost", AssignStmt.NonGhostKind_To_String(gk));
+              }
+            }
+          }
+
+        } else if (stmt is UpdateStmt) {
+          var s = (UpdateStmt)stmt;
+          s.ResolvedStatements.Iter(ss => Visit(ss, mustBeErasable));
+          s.IsGhost = s.ResolvedStatements.All(ss => ss.IsGhost);
+
+        } else if (stmt is VarDeclStmt) {
+          var s = (VarDeclStmt)stmt;
+          if (mustBeErasable) {
+            foreach (var local in s.Locals) {
+              // a local variable in a specification-only context might as well be ghost
+              local.IsGhost = true;
+            }
+          }
+          s.IsGhost = (s.Update == null || s.Update.IsGhost) && s.Locals.All(v => v.IsGhost);
+          if (s.Update != null) {
+            Visit(s.Update, mustBeErasable);
+          }
+
+        } else if (stmt is AssignStmt) {
+          var s = (AssignStmt)stmt;
+          var lhs = s.Lhs.Resolved;
+          var gk = AssignStmt.LhsIsToGhost_Which(lhs);
+          if (gk == AssignStmt.NonGhostKind.IsGhost) {
+            s.IsGhost = true;
+            if (s.Rhs is TypeRhs) {
+              Error(s.Rhs.Tok, "'new' is not allowed in ghost contexts");
+            }
+          } else if (gk == AssignStmt.NonGhostKind.Variable && codeContext.IsGhost) {
+            // cool
+          } else if (mustBeErasable) {
+            Error(stmt, "Assignment to {0} is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)",
+              AssignStmt.NonGhostKind_To_String(gk));
+          } else if (s.Rhs is ExprRhs) {
+            var rhs = (ExprRhs)s.Rhs;
+            resolver.CheckIsCompilable(rhs.Expr);
+          } else if (s.Rhs is HavocRhs) {
+            // cool
+          } else {
+            var rhs = (TypeRhs)s.Rhs;
+            if (rhs.ArrayDimensions != null) {
+              foreach (var dim in rhs.ArrayDimensions) {
+                resolver.CheckIsCompilable(dim);
+              }
+            }
+            if (rhs.InitCall != null) {
+              foreach (var arg in rhs.InitCall.Args) {
+                resolver.CheckIsCompilable(arg);
+              }
+            }
+          }
+
+        } else if (stmt is CallStmt) {
+          var s = (CallStmt)stmt;
+          var callee = s.Method;
+          Contract.Assert(callee != null);  // follows from the invariant of CallStmt
+          s.IsGhost = callee.IsGhost;
+          // check in-parameters
+          if (mustBeErasable) {
+            if (!s.IsGhost) {
+              Error(s, "only ghost methods can be called from this context");
+            }
+          } else {
+            resolver.CheckIsCompilable(s.Receiver);
+            int j;
+            if (!callee.IsGhost) {
+              j = 0;
+              foreach (var e in s.Args) {
+                Contract.Assume(j < callee.Ins.Count);  // this should have already been checked by the resolver
+                if (!callee.Ins[j].IsGhost) {
+                  resolver.CheckIsCompilable(e);
+                }
+                j++;
+              }
+            }
+            j = 0;
+            foreach (var e in s.Lhs) {
+              var resolvedLhs = e.Resolved;
+              if (callee.IsGhost || callee.Outs[j].IsGhost) {
+                // LHS must denote a ghost
+                if (resolvedLhs is IdentifierExpr) {
+                  var ll = (IdentifierExpr)resolvedLhs;
+                  if (!ll.Var.IsGhost) {
+                    if (ll is AutoGhostIdentifierExpr && ll.Var is LocalVariable) {
+                      // the variable was actually declared in this statement, so auto-declare it as ghost
+                      ((LocalVariable)ll.Var).MakeGhost();
+                    } else {
+                      Error(s, "actual out-parameter {0} is required to be a ghost variable", j);
+                    }
+                  }
+                } else if (resolvedLhs is MemberSelectExpr) {
+                  var ll = (MemberSelectExpr)resolvedLhs;
+                  if (!ll.Member.IsGhost) {
+                    Error(s, "actual out-parameter {0} is required to be a ghost field", j);
+                  }
+                } else {
+                  // this is an array update, and arrays are always non-ghost
+                  Error(s, "actual out-parameter {0} is required to be a ghost variable", j);
+                }
+              }
+              j++;
+            }
+          }
+
+        } else if (stmt is BlockStmt) {
+          var s = (BlockStmt)stmt;
+          s.IsGhost = mustBeErasable;  // set .IsGhost before descending into substatements (since substatements may do a 'break' out of this block)
+          s.Body.Iter(ss => Visit(ss, mustBeErasable));
+          s.IsGhost = s.IsGhost || s.Body.All(ss => ss.IsGhost);  // mark the block statement as ghost if all its substatements are ghost
+
+        } else if (stmt is IfStmt) {
+          var s = (IfStmt)stmt;
+          s.IsGhost = mustBeErasable || (s.Guard != null && resolver.UsesSpecFeatures(s.Guard));
+          Visit(s.Thn, s.IsGhost);
+          if (s.Els != null) {
+            Visit(s.Els, s.IsGhost);
+          }
+          // if both branches were all ghost, then we can mark the enclosing statement as ghost as well
+          s.IsGhost = s.IsGhost || (s.Thn.IsGhost && (s.Els == null || s.Els.IsGhost));
+
+        } else if (stmt is AlternativeStmt) {
+          var s = (AlternativeStmt)stmt;
+          s.IsGhost = mustBeErasable || s.Alternatives.Exists(alt => resolver.UsesSpecFeatures(alt.Guard));
+          s.Alternatives.Iter(alt => alt.Body.Iter(ss => Visit(ss, s.IsGhost)));
+          s.IsGhost = s.IsGhost || s.Alternatives.All(alt => alt.Body.All(ss => ss.IsGhost));
+
+        } else if (stmt is WhileStmt) {
+          var s = (WhileStmt)stmt;
+          s.IsGhost = mustBeErasable || (s.Guard != null && resolver.UsesSpecFeatures(s.Guard));
+          if (s.IsGhost && s.Decreases.Expressions.Exists(e => e is WildcardExpr)) {
+            Error(s, "'decreases *' is not allowed on ghost loops");
+          }
+          if (s.IsGhost && s.Mod.Expressions != null) {
+            s.Mod.Expressions.Iter(resolver.DisallowNonGhostFieldSpecifiers);
+          }
+          if (s.Body != null) {
+            Visit(s.Body, s.IsGhost);
+          }
+          s.IsGhost = s.IsGhost || s.Body == null || (!s.Decreases.Expressions.Exists(e => e is WildcardExpr) && s.Body.IsGhost);
+
+        } else if (stmt is AlternativeLoopStmt) {
+          var s = (AlternativeLoopStmt)stmt;
+          s.IsGhost = mustBeErasable || s.Alternatives.Exists(alt => resolver.UsesSpecFeatures(alt.Guard));
+          if (s.IsGhost && s.Decreases.Expressions.Exists(e => e is WildcardExpr)) {
+            Error(s, "'decreases *' is not allowed on ghost loops");
+          }
+          if (s.IsGhost && s.Mod.Expressions != null) {
+            s.Mod.Expressions.Iter(resolver.DisallowNonGhostFieldSpecifiers);
+          }
+          s.Alternatives.Iter(alt => alt.Body.Iter(ss => Visit(ss, s.IsGhost)));
+          s.IsGhost = s.IsGhost || (!s.Decreases.Expressions.Exists(e => e is WildcardExpr) && s.Alternatives.All(alt => alt.Body.All(ss => ss.IsGhost)));
+
+        } else if (stmt is ForallStmt) {
+          var s = (ForallStmt)stmt;
+          s.IsGhost = mustBeErasable || s.Kind != ForallStmt.ParBodyKind.Assign || resolver.UsesSpecFeatures(s.Range);
+          if (s.Body != null) {
+            Visit(s.Body, s.IsGhost);
+          }
+          s.IsGhost = s.IsGhost || s.Body == null || s.Body.IsGhost;
+
+        } else if (stmt is ModifyStmt) {
+          var s = (ModifyStmt)stmt;
+          s.IsGhost = mustBeErasable;
+          if (s.IsGhost) {
+            s.Mod.Expressions.Iter(resolver.DisallowNonGhostFieldSpecifiers);
+          }
+          if (s.Body != null) {
+            Visit(s.Body, mustBeErasable);
+          }
+
+        } else if (stmt is CalcStmt) {
+          var s = (CalcStmt)stmt;
+          s.IsGhost = true;
+          foreach (var h in s.Hints) {
+            Visit(h, true);
+          }
+
+        } else if (stmt is MatchStmt) {
+          var s = (MatchStmt)stmt;
+          s.IsGhost = mustBeErasable || resolver.UsesSpecFeatures(s.Source);
+          s.Cases.Iter(kase => kase.Body.Iter(ss => Visit(ss, s.IsGhost)));
+          s.IsGhost = s.IsGhost || s.Cases.All(kase => kase.Body.All(ss => ss.IsGhost));
+
+        } else if (stmt is SkeletonStatement) {
+          var s = (SkeletonStatement)stmt;
+          s.IsGhost = mustBeErasable;
+          if (s.S != null) {
+            Visit(s.S, mustBeErasable);
+            s.IsGhost = s.IsGhost || s.S.IsGhost;
+          }
+
+        } else {
+          Contract.Assert(false); throw new cce.UnreachableException();
+        }
+      }
+    }
+    #endregion
+
+    // ------------------------------------------------------------------------------------------------------
     // ----- FillInDefaultLoopDecreases ---------------------------------------------------------------------
     // ------------------------------------------------------------------------------------------------------
     #region FillInDefaultLoopDecreases
@@ -3030,7 +3635,6 @@ namespace Microsoft.Dafny
     readonly Scope<IVariable>/*!*/ scope = new Scope<IVariable>();
     Scope<Statement>/*!*/ labeledStatements = new Scope<Statement>();
     List<Statement> loopStack = new List<Statement>();  // the enclosing loops (from which it is possible to break out)
-    readonly Dictionary<Statement, bool> inSpecOnlyContext = new Dictionary<Statement, bool>();  // invariant: domain contain union of the domains of "labeledStatements" and "loopStack"
 
     /// <summary>
     /// This method resolves the types that have been given after the 'extends' keyword.  Then, it populates
@@ -3541,26 +4145,17 @@ namespace Microsoft.Dafny
 
     void ResolveAttributes(Attributes attrs, ResolveOpts opts) {
       Contract.Requires(opts != null);
-      Contract.Requires(opts.DontCareAboutCompilation);  // attributes are never compiled
       // order does not matter much for resolution, so resolve them in reverse order
       foreach (var attr in attrs.AsEnumerable()) {
         if (attr.Args != null) {
-          ResolveAttributeArgs(attr.Args, opts, true);
-        }
-      }
-    }
-
-    void ResolveAttributeArgs(List<Expression> args, ResolveOpts opts, bool allowGhosts) {
-      Contract.Requires(args != null);
-      foreach (var arg in args) {
-        Contract.Assert(arg != null);
-        int prevErrors = reporter.Count(ErrorLevel.Error);
-        ResolveExpression(arg, opts);
-        if (!allowGhosts) {
-          CheckIsNonGhost(arg);
-        }
-        if (prevErrors == reporter.Count(ErrorLevel.Error)) {
-          CheckTypeInference(arg);
+          foreach (var arg in attr.Args) {
+            Contract.Assert(arg != null);
+            int prevErrors = reporter.Count(ErrorLevel.Error);
+            ResolveExpression(arg, opts);
+            if (prevErrors == reporter.Count(ErrorLevel.Error)) {
+              CheckTypeInference(arg, opts.codeContext);
+            }
+          }
         }
       }
     }
@@ -3643,39 +4238,32 @@ namespace Microsoft.Dafny
       foreach (Formal p in f.Formals) {
         scope.Push(p.Name, p);
       }
-      ResolveAttributes(f.Attributes, new ResolveOpts(f, false, true));
+      ResolveAttributes(f.Attributes, new ResolveOpts(f, false));
       foreach (Expression r in f.Req) {
-        ResolveExpression(r, new ResolveOpts(f, false, true));
+        ResolveExpression(r, new ResolveOpts(f, false));
         Contract.Assert(r.Type != null);  // follows from postcondition of ResolveExpression
-        if (!UnifyTypes(r.Type, Type.Bool)) {
-          reporter.Error(MessageSource.Resolver, r, "Precondition must be a boolean (got {0})", r.Type);
-        }
+        ConstrainTypes(r.Type, Type.Bool, r, "Precondition must be a boolean (got {0})", r.Type);
       }
       foreach (FrameExpression fr in f.Reads) {
-        ResolveFrameExpression(fr, true, f.IsGhost, f);
+        ResolveFrameExpression(fr, true, f);
       }
       foreach (Expression r in f.Ens) {
-        ResolveExpression(r, new ResolveOpts(f, false, true));  // since this is a function, the postcondition is still a one-state predicate
+        ResolveExpression(r, new ResolveOpts(f, false));  // since this is a function, the postcondition is still a one-state predicate
         Contract.Assert(r.Type != null);  // follows from postcondition of ResolveExpression
-        if (!UnifyTypes(r.Type, Type.Bool)) {
-          reporter.Error(MessageSource.Resolver, r, "Postcondition must be a boolean (got {0})", r.Type);
-        }
+        ConstrainTypes(r.Type, Type.Bool, r, "Postcondition must be a boolean (got {0})", r.Type);
       }
-      ResolveAttributes(f.Decreases.Attributes, new ResolveOpts(f, false, true));
+      ResolveAttributes(f.Decreases.Attributes, new ResolveOpts(f, false));
       foreach (Expression r in f.Decreases.Expressions) {
-        ResolveExpression(r, new ResolveOpts(f, false, true));
+        ResolveExpression(r, new ResolveOpts(f, false));
         // any type is fine
       }
+      SolveAllTypeConstraints();
       if (f.Body != null) {
         var prevErrorCount = reporter.Count(ErrorLevel.Error);
         ResolveExpression(f.Body, new ResolveOpts(f, false));
-        if (!f.IsGhost && prevErrorCount == reporter.Count(ErrorLevel.Error)) {
-          CheckIsNonGhost(f.Body);
-        }
+        SolveAllTypeConstraints();
         Contract.Assert(f.Body.Type != null);  // follows from postcondition of ResolveExpression
-        if (!UnifyTypes(f.Body.Type, f.ResultType)) {
-          reporter.Error(MessageSource.Resolver, f, "Function body type mismatch (expected {0}, got {1})", f.ResultType, f.Body.Type);
-        }
+        ConstrainTypes(f.Body.Type, f.ResultType, f, "Function body type mismatch (expected {0}, got {1})", f.ResultType, f.Body.Type);
       }
       scope.PopMarker();
     }
@@ -3683,14 +4271,11 @@ namespace Microsoft.Dafny
     /// <summary>
     /// 
     /// </summary>
-    /// <param name="fe"></param>
     /// <param name="readsFrame">True indicates "reads", false indicates "modifies".</param>
-    /// <param name="isGhostContext"></param>
-    /// <param name="codeContext"></param>
-    void ResolveFrameExpression(FrameExpression fe, bool readsFrame, bool isGhostContext, ICodeContext codeContext) {
+    void ResolveFrameExpression(FrameExpression fe, bool readsFrame, ICodeContext codeContext) {
       Contract.Requires(fe != null);
       Contract.Requires(codeContext != null);
-      ResolveExpression(fe.E, new ResolveOpts(codeContext, false, true /* yes, this is ghost */));
+      ResolveExpression(fe.E, new ResolveOpts(codeContext, false));
       Type t = fe.E.Type;
       Contract.Assert(t != null);  // follows from postcondition of ResolveExpression
       var arrTy = t.AsArrowType;
@@ -3701,8 +4286,7 @@ namespace Microsoft.Dafny
       if (collType != null) {
         t = collType.Arg;
       }
-      if (!UnifyTypes(t, new ObjectType())) {
-        reporter.Error(MessageSource.Resolver, fe.E, "a {0}-clause expression must denote an object or a collection of objects (instead got {1})", readsFrame ? "reads" : "modifies", fe.E.Type);
+      if (!ConstrainTypes(t, new ObjectType(), fe.E, "a {0}-clause expression must denote an object or a collection of objects (instead got {1})", readsFrame ? "reads" : "modifies", fe.E.Type)) {
       } else if (fe.FieldName != null) {
         NonProxyType nptype;
         MemberDecl member = ResolveMember(fe.E.tok, t, fe.FieldName, out nptype);
@@ -3711,8 +4295,6 @@ namespace Microsoft.Dafny
           // error has already been reported by ResolveMember
         } else if (!(member is Field)) {
           reporter.Error(MessageSource.Resolver, fe.E, "member {0} in type {1} does not refer to a field", fe.FieldName, ctype.Name);
-        } else if (!readsFrame && isGhostContext && !member.IsGhost) {
-          reporter.Error(MessageSource.Resolver, fe.E, "in a ghost context, only ghost fields can be mentioned as modifies frame targets ({0})", fe.FieldName);
         } else {
           Contract.Assert(ctype != null && ctype.ResolvedClass != null);  // follows from postcondition of ResolveMember
           fe.Field = (Field)member;
@@ -3721,6 +4303,17 @@ namespace Microsoft.Dafny
     }
 
     /// <summary>
+    /// This method can be called even if the resolution of "fe" failed; in that case, this method will
+    /// not issue any error message.
+    /// </summary>
+    void DisallowNonGhostFieldSpecifiers(FrameExpression fe) {
+      Contract.Requires(fe != null);
+      if (fe.Field != null && !fe.Field.IsGhost) {
+        reporter.Error(MessageSource.Resolver, fe.E, "in a ghost context, only ghost fields can be mentioned as modifies frame targets ({0})", fe.FieldName);
+      }
+    }
+
+    /// <summary>
     /// Assumes type parameters have already been pushed
     /// </summary>
     void ResolveMethodSignature(Method m) {
@@ -3764,27 +4357,24 @@ namespace Microsoft.Dafny
 
         // Start resolving specification...
         foreach (MaybeFreeExpression e in m.Req) {
-          ResolveAttributes(e.Attributes, new ResolveOpts(m, false, true));
-          ResolveExpression(e.E, new ResolveOpts(m, false, true));
+          ResolveAttributes(e.Attributes, new ResolveOpts(m, false));
+          ResolveExpression(e.E, new ResolveOpts(m, false));
           Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression
-          if (!UnifyTypes(e.E.Type, Type.Bool)) {
-            reporter.Error(MessageSource.Resolver, e.E, "Precondition must be a boolean (got {0})", e.E.Type);
-          }
+          ConstrainTypes(e.E.Type, Type.Bool, e.E, "Precondition must be a boolean (got {0})", e.E.Type);
         }
-        ResolveAttributes(m.Mod.Attributes, new ResolveOpts(m, false, true));
+        ResolveAttributes(m.Mod.Attributes, new ResolveOpts(m, false));
         foreach (FrameExpression fe in m.Mod.Expressions) {
-          ResolveFrameExpression(fe, false, m.IsGhost, m);
+          ResolveFrameExpression(fe, false, m);
           if (m is Lemma || m is FixpointLemma) {
             reporter.Error(MessageSource.Resolver, fe.tok, "{0}s are not allowed to have modifies clauses", m.WhatKind);
+          } else if (m.IsGhost) {
+            DisallowNonGhostFieldSpecifiers(fe);
           }
         }
-        ResolveAttributes(m.Decreases.Attributes, new ResolveOpts(m, false, true));
+        ResolveAttributes(m.Decreases.Attributes, new ResolveOpts(m, false));
         foreach (Expression e in m.Decreases.Expressions) {
-          ResolveExpression(e, new ResolveOpts(m, false, true));
+          ResolveExpression(e, new ResolveOpts(m, false));
           // any type is fine
-          if (m.IsGhost && e is WildcardExpr) {
-            reporter.Error(MessageSource.Resolver, e, "'decreases *' is not allowed on ghost methods");
-          }
         }
 
         // Add out-parameters to a new scope that will also include the outermost-level locals of the body
@@ -3800,13 +4390,12 @@ namespace Microsoft.Dafny
 
         // ... continue resolving specification
         foreach (MaybeFreeExpression e in m.Ens) {
-          ResolveAttributes(e.Attributes, new ResolveOpts(m, true, true));
-          ResolveExpression(e.E, new ResolveOpts(m, true, true));
+          ResolveAttributes(e.Attributes, new ResolveOpts(m, true));
+          ResolveExpression(e.E, new ResolveOpts(m, true));
           Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression
-          if (!UnifyTypes(e.E.Type, Type.Bool)) {
-            reporter.Error(MessageSource.Resolver, e.E, "Postcondition must be a boolean (got {0})", e.E.Type);
-          }
+          ConstrainTypes(e.E.Type, Type.Bool, e.E, "Postcondition must be a boolean (got {0})", e.E.Type);
         }
+        SolveAllTypeConstraints();
 
         // Resolve body
         if (m.Body != null) {
@@ -3817,12 +4406,16 @@ namespace Microsoft.Dafny
             var k = com.PrefixLemma.Ins[0];
             scope.Push(k.Name, k);  // we expect no name conflict for _k
           }
-          var codeContext = m;
-          ResolveBlockStatement(m.Body, m.IsGhost, codeContext);
+          var prevErrorCount = reporter.Count(ErrorLevel.Error);
+          ResolveBlockStatement(m.Body, m);
+          SolveAllTypeConstraints();
+          if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
+//KRML            ComputeGhostInterest(m.Body, m);
+          }
         }
 
         // attributes are allowed to mention both in- and out-parameters (including the implicit _k, for colemmas)
-        ResolveAttributes(m.Attributes, new ResolveOpts(m, false, true));
+        ResolveAttributes(m.Attributes, new ResolveOpts(m, false));
 
         scope.PopMarker();  // for the out-parameters and outermost-level locals
         scope.PopMarker();  // for the in-parameters
@@ -3888,26 +4481,22 @@ namespace Microsoft.Dafny
       Contract.Assert(iter.Decreases.Expressions.Count == iter.DecreasesFields.Count);
       for (int i = 0; i < iter.Decreases.Expressions.Count; i++) {
         var e = iter.Decreases.Expressions[i];
-        ResolveExpression(e, new ResolveOpts(iter, false, true));
+        ResolveExpression(e, new ResolveOpts(iter, false));
         // any type is fine, but associate this type with the corresponding _decreases<n> field
         var d = iter.DecreasesFields[i];
-        if (!UnifyTypes(d.Type, e.Type)) {
-          // bummer, there was a use--and a bad use--of the field before, so this won't be the best of error messages
-          reporter.Error(MessageSource.Resolver, e, "type of field {0} is {1}, but has been constrained elsewhere to be of type {2}", d.Name, e.Type, d.Type);
-        }
+        // If the following type constraint does not hold, then: Bummer, there was a use--and a bad use--of the field before, so this won't be the best of error messages
+        ConstrainTypes(d.Type, e.Type, e, "type of field {0} is {1}, but has been constrained elsewhere to be of type {2}", d.Name, e.Type, d.Type);
       }
       foreach (FrameExpression fe in iter.Reads.Expressions) {
-        ResolveFrameExpression(fe, true, false, iter);
+        ResolveFrameExpression(fe, true, iter);
       }
       foreach (FrameExpression fe in iter.Modifies.Expressions) {
-        ResolveFrameExpression(fe, false, false, iter);
+        ResolveFrameExpression(fe, false, iter);
       }
       foreach (MaybeFreeExpression e in iter.Requires) {
-        ResolveExpression(e.E, new ResolveOpts(iter, false, true));
+        ResolveExpression(e.E, new ResolveOpts(iter, false));
         Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression
-        if (!UnifyTypes(e.E.Type, Type.Bool)) {
-          reporter.Error(MessageSource.Resolver, e.E, "Precondition must be a boolean (got {0})", e.E.Type);
-        }
+        ConstrainTypes(e.E.Type, Type.Bool, e.E, "Precondition must be a boolean (got {0})", e.E.Type);
       }
 
       scope.PopMarker();  // for the in-parameters
@@ -3919,34 +4508,31 @@ namespace Microsoft.Dafny
       Contract.Assert(scope.AllowInstance);
 
       foreach (MaybeFreeExpression e in iter.YieldRequires) {
-        ResolveExpression(e.E, new ResolveOpts(iter, false, true));
+        ResolveExpression(e.E, new ResolveOpts(iter, false));
         Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression
-        if (!UnifyTypes(e.E.Type, Type.Bool)) {
-          reporter.Error(MessageSource.Resolver, e.E, "Yield precondition must be a boolean (got {0})", e.E.Type);
-        }
+        ConstrainTypes(e.E.Type, Type.Bool, e.E, "Yield precondition must be a boolean (got {0})", e.E.Type);
       }
       foreach (MaybeFreeExpression e in iter.YieldEnsures) {
-        ResolveExpression(e.E, new ResolveOpts(iter, true, true));
+        ResolveExpression(e.E, new ResolveOpts(iter, true));
         Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression
-        if (!UnifyTypes(e.E.Type, Type.Bool)) {
-          reporter.Error(MessageSource.Resolver, e.E, "Yield postcondition must be a boolean (got {0})", e.E.Type);
-        }
+        ConstrainTypes(e.E.Type, Type.Bool, e.E, "Yield postcondition must be a boolean (got {0})", e.E.Type);
       }
       foreach (MaybeFreeExpression e in iter.Ensures) {
-        ResolveExpression(e.E, new ResolveOpts(iter, true, true));
+        ResolveExpression(e.E, new ResolveOpts(iter, true));
         Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression
-        if (!UnifyTypes(e.E.Type, Type.Bool)) {
-          reporter.Error(MessageSource.Resolver, e.E, "Postcondition must be a boolean (got {0})", e.E.Type);
-        }
+        ConstrainTypes(e.E.Type, Type.Bool, e.E, "Postcondition must be a boolean (got {0})", e.E.Type);
       }
 
-      ResolveAttributes(iter.Attributes, new ResolveOpts(iter, false, true));
+      ResolveAttributes(iter.Attributes, new ResolveOpts(iter, false));
 
       var postSpecErrorCount = reporter.Count(ErrorLevel.Error);
 
       // Resolve body
       if (iter.Body != null) {
-        ResolveBlockStatement(iter.Body, false, iter);
+        ResolveBlockStatement(iter.Body, iter);
+        if (reporter.Count(ErrorLevel.Error) == postSpecErrorCount) {
+          //KRML          ComputeGhostInterest(iter.Body, iter);
+        }
       }
 
       currentClass = null;
@@ -4251,13 +4837,13 @@ namespace Microsoft.Dafny
         }
         var prevErrorCount = reporter.Count(ErrorLevel.Error);
         if (t.NamePath is ExprDotName) {
-          var ret = ResolveDotSuffix_Type((ExprDotName)t.NamePath, new ResolveOpts(context, true, true), allowDanglingDotName, option, defaultTypeArguments);
+          var ret = ResolveDotSuffix_Type((ExprDotName)t.NamePath, new ResolveOpts(context, true), allowDanglingDotName, option, defaultTypeArguments);
           if (ret != null) {
             return ret;
           }
         } else {
           var s = (NameSegment)t.NamePath;
-          ResolveNameSegment_Type(s, new ResolveOpts(context, true, true), option, defaultTypeArguments);
+          ResolveNameSegment_Type(s, new ResolveOpts(context, true), option, defaultTypeArguments);
         }
         if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
           var r = t.NamePath.Resolved as Resolver_IdentifierExpr;
@@ -4818,31 +5404,22 @@ namespace Microsoft.Dafny
       return at;
     }
 
-    /// <summary>
-    /// "specContextOnly" means that the statement must be erasable, that is, it should be okay to omit it
-    /// at run time.  That means it must not have any side effects on non-ghost variables, for example.
-    /// </summary>
-    public void ResolveStatement(Statement stmt, bool specContextOnly, ICodeContext codeContext) {
+    public void ResolveStatement(Statement stmt, ICodeContext codeContext) {
       Contract.Requires(stmt != null);
       Contract.Requires(codeContext != null);
       if (!(stmt is ForallStmt)) {  // forall statements do their own attribute resolution below
-        ResolveAttributes(stmt.Attributes, new ResolveOpts(codeContext, true, true));
+        ResolveAttributes(stmt.Attributes, new ResolveOpts(codeContext, true));
       }
       if (stmt is PredicateStmt) {
         PredicateStmt s = (PredicateStmt)stmt;
-        s.IsGhost = true;
-        ResolveExpression(s.Expr, new ResolveOpts(codeContext, true, true));
+        ResolveExpression(s.Expr, new ResolveOpts(codeContext, true));
         Contract.Assert(s.Expr.Type != null);  // follows from postcondition of ResolveExpression
-        if (!UnifyTypes(s.Expr.Type, Type.Bool)) {
-          reporter.Error(MessageSource.Resolver, s.Expr, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Expr.Type);
-        }
+        ConstrainTypes(s.Expr.Type, Type.Bool, s.Expr, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Expr.Type);
 
       } else if (stmt is PrintStmt) {
-        PrintStmt s = (PrintStmt)stmt;
-        ResolveAttributeArgs(s.Args, new ResolveOpts(codeContext, false, specContextOnly), false);
-        if (specContextOnly) {
-          reporter.Error(MessageSource.Resolver, stmt, "print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
-        }
+        var s = (PrintStmt)stmt;
+        var opts = new ResolveOpts(codeContext, false);
+        s.Args.Iter(e => ResolveExpression(e, opts));
 
       } else if (stmt is BreakStmt) {
         var s = (BreakStmt)stmt;
@@ -4852,10 +5429,6 @@ namespace Microsoft.Dafny
             reporter.Error(MessageSource.Resolver, s, "break label is undefined or not in scope: {0}", s.TargetLabel);
           } else {
             s.TargetStmt = target;
-            bool targetIsLoop = target is WhileStmt || target is AlternativeLoopStmt;
-            if (specContextOnly && !s.TargetStmt.IsGhost && !inSpecOnlyContext[s.TargetStmt]) {
-              reporter.Error(MessageSource.Resolver, stmt, "ghost-context break statement is not allowed to break out of non-ghost " + (targetIsLoop ? "loop" : "structure"));
-            }
           }
         } else {
           if (loopStack.Count < s.BreakCount) {
@@ -4867,9 +5440,6 @@ namespace Microsoft.Dafny
               target.Labels = new LList<Label>(new Label(target.Tok, null), null);
             }
             s.TargetStmt = target;
-            if (specContextOnly && !target.IsGhost && !inSpecOnlyContext[target]) {
-              reporter.Error(MessageSource.Resolver, stmt, "ghost-context break statement is not allowed to break out of non-ghost loop");
-            }
           }
         }
 
@@ -4879,8 +5449,6 @@ namespace Microsoft.Dafny
           reporter.Error(MessageSource.Resolver, stmt, "yield statement is allowed only in iterators");
         } else if (stmt is ReturnStmt && !(codeContext is Method)) {
           reporter.Error(MessageSource.Resolver, stmt, "return statement is allowed only in method");
-        } else if (specContextOnly && !codeContext.IsGhost) {
-          reporter.Error(MessageSource.Resolver, stmt, "{0} statement is not allowed in this context (because it is guarded by a specification-only expression)", kind);
         }
         var s = (ProduceStmt)stmt;
         if (s.rhss != null) {
@@ -4911,13 +5479,13 @@ namespace Microsoft.Dafny
             }
             s.hiddenUpdate = new UpdateStmt(s.Tok, s.EndTok, formals, s.rhss, true);
             // resolving the update statement will check for return/yield statement specifics.
-            ResolveStatement(s.hiddenUpdate, specContextOnly, codeContext);
+            ResolveStatement(s.hiddenUpdate, codeContext);
           }
         } else {// this is a regular return/yield statement.
           s.hiddenUpdate = null;
         }
       } else if (stmt is ConcreteUpdateStatement) {
-        ResolveConcreteUpdateStmt((ConcreteUpdateStatement)stmt, specContextOnly, codeContext);
+        ResolveConcreteUpdateStmt((ConcreteUpdateStatement)stmt, codeContext);
       } else if (stmt is VarDeclStmt) {
         var s = (VarDeclStmt)stmt;
         // We have three cases.
@@ -4939,10 +5507,6 @@ namespace Microsoft.Dafny
         foreach (var local in s.Locals) {
           ResolveType(local.Tok, local.OptionalType, codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
           local.type = local.OptionalType;
-          if (specContextOnly) {
-            // a local variable in a specification-only context might as well be ghost
-            local.IsGhost = true;
-          }
         }
         // Resolve the UpdateStmt, if any
         if (s.Update is UpdateStmt) {
@@ -4957,7 +5521,7 @@ namespace Microsoft.Dafny
             lhs.Type = local.Type;
           }
           // resolve the whole thing
-          ResolveConcreteUpdateStmt(s.Update, specContextOnly, codeContext);
+          ResolveConcreteUpdateStmt(s.Update, codeContext);
         }
         // Add the locals to the scope
         foreach (var local in s.Locals) {
@@ -4965,16 +5529,13 @@ namespace Microsoft.Dafny
         }
         // With the new locals in scope, it's now time to resolve the attributes on all the locals
         foreach (var local in s.Locals) {
-          ResolveAttributes(local.Attributes, new ResolveOpts(codeContext, true, true));
+          ResolveAttributes(local.Attributes, new ResolveOpts(codeContext, true));
         }
         // Resolve the AssignSuchThatStmt, if any
         if (s.Update is AssignSuchThatStmt) {
-          ResolveConcreteUpdateStmt(s.Update, specContextOnly, codeContext);
+          ResolveConcreteUpdateStmt(s.Update, codeContext);
         }
         // Update the VarDeclStmt's ghost status according to its components
-        if (!s.IsGhost) {
-          s.IsGhost = (s.Update == null || s.Update.IsGhost) && s.Locals.All(v => v.IsGhost);
-        }
         foreach (var local in s.Locals)
         {
           if (Attributes.Contains(local.Attributes, "assumption"))
@@ -4983,13 +5544,12 @@ namespace Microsoft.Dafny
             {
               reporter.Error(MessageSource.Resolver, local.Tok, "assumption variable can only be declared in a method");
             }
-            if (!local.IsGhost)
-            {
-              reporter.Error(MessageSource.Resolver, local.Tok, "assumption variable must be ghost");
-            }
             if (!(local.Type.IsBoolType))
             {
-              reporter.Error(MessageSource.Resolver, s, "assumption variable must be of type 'bool'");
+              reporter.Error(MessageSource.Resolver, local.Tok, "assumption variable must be of type 'bool'");
+            }
+            if (!local.IsGhost) {
+              reporter.Error(MessageSource.Resolver, local.Tok, "assumption variable must be ghost");
             }
           }
         }
@@ -4997,22 +5557,17 @@ namespace Microsoft.Dafny
       } else if (stmt is AssignStmt) {
         AssignStmt s = (AssignStmt)stmt;
         int prevErrorCount = reporter.Count(ErrorLevel.Error);
-        ResolveExpression(s.Lhs, new ResolveOpts(codeContext, true, specContextOnly));  // allow ghosts for now, tighted up below
+        ResolveExpression(s.Lhs, new ResolveOpts(codeContext, true));  // allow ghosts for now, tighted up below
         bool lhsResolvedSuccessfully = reporter.Count(ErrorLevel.Error) == prevErrorCount;
         Contract.Assert(s.Lhs.Type != null);  // follows from postcondition of ResolveExpression
         // check that LHS denotes a mutable variable or a field
-        bool lvalueIsGhost = false;
         var lhs = s.Lhs.Resolved;
         if (lhs is IdentifierExpr) {
           IVariable var = ((IdentifierExpr)lhs).Var;
           if (var == null) {
             // the LHS didn't resolve correctly; some error would already have been reported
           } else {
-            lvalueIsGhost = var.IsGhost || codeContext.IsGhost;
             CheckIsLvalue(lhs, codeContext);
-            if (!lvalueIsGhost && specContextOnly) {
-              reporter.Error(MessageSource.Resolver, stmt, "Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
-            }
 
             var localVar = var as LocalVariable;
             if (localVar != null && currentMethod != null && Attributes.Contains(localVar.Attributes, "assumption"))
@@ -5037,18 +5592,6 @@ namespace Microsoft.Dafny
         } else if (lhs is MemberSelectExpr) {
           var fse = (MemberSelectExpr)lhs;
           if (fse.Member != null) {  // otherwise, an error was reported above
-            lvalueIsGhost = fse.Member.IsGhost;
-            if (!lvalueIsGhost) {
-              if (specContextOnly) {
-                reporter.Error(MessageSource.Resolver, stmt, "Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
-              } else {
-                // It is now that we wish we would have resolved s.Lhs to not allow ghosts.  Too late, so we do
-                // the next best thing.
-                if (lhsResolvedSuccessfully && UsesSpecFeatures(fse.Obj)) {
-                  reporter.Error(MessageSource.Resolver, stmt, "Assignment to non-ghost field is not allowed to use specification-only expressions in the receiver");
-                }
-              }
-            }
             CheckIsLvalue(fse, codeContext);
           }
         } else if (lhs is SeqSelectExpr) {
@@ -5056,52 +5599,26 @@ namespace Microsoft.Dafny
           // LHS is fine, provided the "sequence" is really an array
           if (lhsResolvedSuccessfully) {
             Contract.Assert(slhs.Seq.Type != null);
-            if (specContextOnly) {
-              reporter.Error(MessageSource.Resolver, stmt, "Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
-            }
             CheckIsLvalue(slhs, codeContext);
           }
 
         } else if (lhs is MultiSelectExpr) {
-          if (specContextOnly) {
-            reporter.Error(MessageSource.Resolver, stmt, "Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
-          }
           CheckIsLvalue(lhs, codeContext);
 
         } else {
           CheckIsLvalue(lhs, codeContext);
         }
 
-        s.IsGhost = lvalueIsGhost;
         Type lhsType = s.Lhs.Type;
         if (s.Rhs is ExprRhs) {
           ExprRhs rr = (ExprRhs)s.Rhs;
-          ResolveExpression(rr.Expr, new ResolveOpts(codeContext, true, specContextOnly));
-          if (!lvalueIsGhost) {
-            CheckIsNonGhost(rr.Expr);
-          }
+          ResolveExpression(rr.Expr, new ResolveOpts(codeContext, true));
           Contract.Assert(rr.Expr.Type != null);  // follows from postcondition of ResolveExpression
-          if (!UnifyTypes(lhsType, rr.Expr.Type)) {
-            reporter.Error(MessageSource.Resolver, stmt, "RHS (of type {0}) not assignable to LHS (of type {1})", rr.Expr.Type, lhsType);
-          }
+          ConstrainTypes(lhsType, rr.Expr.Type, stmt, "RHS (of type {0}) not assignable to LHS (of type {1})", rr.Expr.Type, lhsType);
         } else if (s.Rhs is TypeRhs) {
           TypeRhs rr = (TypeRhs)s.Rhs;
-          Type t = ResolveTypeRhs(rr, stmt, lvalueIsGhost, codeContext);
-          if (!lvalueIsGhost) {
-            if (rr.ArrayDimensions != null) {
-              foreach (var dim in rr.ArrayDimensions) {
-                CheckIsNonGhost(dim);
-              }
-            }
-            if (rr.InitCall != null) {
-              foreach (var arg in rr.InitCall.Args) {
-                CheckIsNonGhost(arg);
-              }
-            }
-          }
-          if (!UnifyTypes(lhsType, t)) {
-            reporter.Error(MessageSource.Resolver, stmt, "type {0} is not assignable to LHS (of type {1})", t, lhsType);
-          }
+          Type t = ResolveTypeRhs(rr, stmt, codeContext);
+          ConstrainTypes(lhsType, t, stmt, "type {0} is not assignable to LHS (of type {1})", t, lhsType);
         } else if (s.Rhs is HavocRhs) {
           // nothing else to do
         } else {
@@ -5110,105 +5627,45 @@ namespace Microsoft.Dafny
 
       } else if (stmt is CallStmt) {
         CallStmt s = (CallStmt)stmt;
-        ResolveCallStmt(s, specContextOnly, codeContext, null);
+        ResolveCallStmt(s, codeContext, null);
 
       } else if (stmt is BlockStmt) {
         var s = (BlockStmt)stmt;
         scope.PushMarker();
-        ResolveBlockStatement(s, specContextOnly, codeContext);
-        if (!s.IsGhost) {
-          s.IsGhost = s.Body.All(ss => ss.IsGhost);  // mark the block statement as ghost if all its substatements are ghost
-        }
+        ResolveBlockStatement(s, codeContext);
         scope.PopMarker();
 
       } else if (stmt is IfStmt) {
         IfStmt s = (IfStmt)stmt;
-        bool branchesAreSpecOnly = specContextOnly;
         if (s.Guard != null) {
-          int prevErrorCount = reporter.Count(ErrorLevel.Error);
-          ResolveExpression(s.Guard, new ResolveOpts(codeContext, true, specContextOnly));
+          ResolveExpression(s.Guard, new ResolveOpts(codeContext, true));
           Contract.Assert(s.Guard.Type != null);  // follows from postcondition of ResolveExpression
-          bool successfullyResolved = reporter.Count(ErrorLevel.Error) == prevErrorCount;
-          if (!UnifyTypes(s.Guard.Type, Type.Bool)) {
-            reporter.Error(MessageSource.Resolver, s.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Guard.Type);
-          }
-          if (!specContextOnly && successfullyResolved) {
-            branchesAreSpecOnly = UsesSpecFeatures(s.Guard);
-          }
+          ConstrainTypes(s.Guard.Type, Type.Bool, s.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Guard.Type);
         }
-        s.IsGhost = branchesAreSpecOnly;
-        ResolveStatement(s.Thn, branchesAreSpecOnly, codeContext);
+        ResolveStatement(s.Thn, codeContext);
         if (s.Els != null) {
-          ResolveStatement(s.Els, branchesAreSpecOnly, codeContext);
-        }
-        if (!s.IsGhost && s.Thn.IsGhost && (s.Els == null || s.Els.IsGhost)) {
-          // mark the entire 'if' statement as ghost if its branches are ghost
-          s.IsGhost = true;
+          ResolveStatement(s.Els, codeContext);
         }
 
       } else if (stmt is AlternativeStmt) {
         var s = (AlternativeStmt)stmt;
-        s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, null, codeContext);
-        if (!s.IsGhost) {
-          s.IsGhost = s.Alternatives.All(alt => alt.Body.All(ss => ss.IsGhost));
-        }
+        ResolveAlternatives(s.Alternatives, null, codeContext);
 
       } else if (stmt is WhileStmt) {
         WhileStmt s = (WhileStmt)stmt;
-        bool bodyMustBeSpecOnly = specContextOnly;
         var fvs = new HashSet<IVariable>();
         if (s.Guard != null) {
-          int prevErrorCount = reporter.Count(ErrorLevel.Error);
-          ResolveExpression(s.Guard, new ResolveOpts(codeContext, true, specContextOnly));
+          ResolveExpression(s.Guard, new ResolveOpts(codeContext, true));
           Contract.Assert(s.Guard.Type != null);  // follows from postcondition of ResolveExpression
-          bool successfullyResolved = reporter.Count(ErrorLevel.Error) == prevErrorCount;
           Translator.ComputeFreeVariables(s.Guard, fvs);
-          if (!UnifyTypes(s.Guard.Type, Type.Bool)) {
-            reporter.Error(MessageSource.Resolver, s.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Guard.Type);
-          }
-          if (!specContextOnly && successfullyResolved) {
-            bodyMustBeSpecOnly = UsesSpecFeatures(s.Guard);
-          }
+          ConstrainTypes(s.Guard.Type, Type.Bool, s.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Guard.Type);
         }
 
-        foreach (MaybeFreeExpression inv in s.Invariants) {
-          ResolveAttributes(inv.Attributes, new ResolveOpts(codeContext, true, true));
-          ResolveExpression(inv.E, new ResolveOpts(codeContext, true, true));
-          Contract.Assert(inv.E.Type != null);  // follows from postcondition of ResolveExpression
-          Translator.ComputeFreeVariables(inv.E, fvs);
-          if (!UnifyTypes(inv.E.Type, Type.Bool)) {
-            reporter.Error(MessageSource.Resolver, inv.E, "invariant is expected to be of type {0}, but is {1}", Type.Bool, inv.E.Type);
-          }
-        }
+        ResolveLoopSpecificationComponents(s.Invariants, s.Decreases, s.Mod, codeContext, fvs);
 
-        ResolveAttributes(s.Decreases.Attributes, new ResolveOpts(codeContext, true, true));
-        foreach (Expression e in s.Decreases.Expressions) {
-          ResolveExpression(e, new ResolveOpts(codeContext, true, true));
-          if (e is WildcardExpr) {
-            if (bodyMustBeSpecOnly) {
-              reporter.Error(MessageSource.Resolver, e, "'decreases *' is not allowed on ghost loops");
-            } else if (!codeContext.AllowsNontermination && !DafnyOptions.O.Dafnycc) {
-              reporter.Error(MessageSource.Resolver, e, "a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating");
-            }
-          }
-          // any type is fine
-        }
-
-        if (s.Mod.Expressions != null) {
-          ResolveAttributes(s.Mod.Attributes, new ResolveOpts(codeContext, true, true));
-          foreach (FrameExpression fe in s.Mod.Expressions) {
-            ResolveFrameExpression(fe, false, bodyMustBeSpecOnly, codeContext);
-            Translator.ComputeFreeVariables(fe.E, fvs);
-          }
-        }
-        s.IsGhost = s.Body == null || bodyMustBeSpecOnly;
         if (s.Body != null) {
           loopStack.Add(s);  // push
-          if (s.Labels == null) {  // otherwise, "s" is already in "inSpecOnlyContext" map
-            inSpecOnlyContext.Add(s, specContextOnly);
-          }
-
-          ResolveStatement(s.Body, bodyMustBeSpecOnly, codeContext);
+          ResolveStatement(s.Body, codeContext);
           loopStack.RemoveAt(loopStack.Count - 1);  // pop
         } else {
           string text = "havoc {" + Util.Comma(", ", fvs, fv => fv.Name) + "};";  // always terminate with a semi-colon
@@ -5217,26 +5674,8 @@ namespace Microsoft.Dafny
 
       } else if (stmt is AlternativeLoopStmt) {
         var s = (AlternativeLoopStmt)stmt;
-        s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, s, codeContext);
-        foreach (MaybeFreeExpression inv in s.Invariants) {
-          ResolveExpression(inv.E, new ResolveOpts(codeContext, true, true));
-          Contract.Assert(inv.E.Type != null);  // follows from postcondition of ResolveExpression
-          if (!UnifyTypes(inv.E.Type, Type.Bool)) {
-            reporter.Error(MessageSource.Resolver, inv.E, "invariant is expected to be of type {0}, but is {1}", Type.Bool, inv.E.Type);
-          }
-        }
-
-        foreach (Expression e in s.Decreases.Expressions) {
-          ResolveExpression(e, new ResolveOpts(codeContext, true, true));
-          if (e is WildcardExpr) {
-            if (s.IsGhost) {
-              reporter.Error(MessageSource.Resolver, e, "'decreases *' is not allowed on ghost loops");
-            } else if (!codeContext.AllowsNontermination && !DafnyOptions.O.Dafnycc) {
-              reporter.Error(MessageSource.Resolver, e, "a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating");
-            }
-          }
-          // any type is fine
-        }
+        ResolveAlternatives(s.Alternatives, s, codeContext);
+        ResolveLoopSpecificationComponents(s.Invariants, s.Decreases, s.Mod, codeContext, null);
 
       } else if (stmt is ForallStmt) {
         var s = (ForallStmt)stmt;
@@ -5247,32 +5686,17 @@ namespace Microsoft.Dafny
           ScopePushAndReport(scope, v, "local-variable");
           ResolveType(v.tok, v.Type, codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
         }
-        ResolveExpression(s.Range, new ResolveOpts(codeContext, true, specContextOnly));
+        ResolveExpression(s.Range, new ResolveOpts(codeContext, true));
         Contract.Assert(s.Range.Type != null);  // follows from postcondition of ResolveExpression
-        if (!UnifyTypes(s.Range.Type, Type.Bool)) {
-          reporter.Error(MessageSource.Resolver, stmt, "range restriction in forall statement must be of type bool (instead got {0})", s.Range.Type);
-        }
+        ConstrainTypes(s.Range.Type, Type.Bool, stmt, "range restriction in forall statement must be of type bool (instead got {0})", s.Range.Type);
         foreach (var ens in s.Ens) {
-          ResolveExpression(ens.E, new ResolveOpts(codeContext, true, true));
+          ResolveExpression(ens.E, new ResolveOpts(codeContext, true));
           Contract.Assert(ens.E.Type != null);  // follows from postcondition of ResolveExpression
-          if (!UnifyTypes(ens.E.Type, Type.Bool)) {
-            reporter.Error(MessageSource.Resolver, ens.E, "ensures condition is expected to be of type {0}, but is {1}", Type.Bool, ens.E.Type);
-          }
+          ConstrainTypes(ens.E.Type, Type.Bool, ens.E, "ensures condition is expected to be of type {0}, but is {1}", Type.Bool, ens.E.Type);
         }
         // Since the range and postconditions are more likely to infer the types of the bound variables, resolve them
         // first (above) and only then resolve the attributes (below).
-        ResolveAttributes(s.Attributes, new ResolveOpts(codeContext, true, true));
-
-        bool bodyMustBeSpecOnly = specContextOnly || (prevErrorCount == reporter.Count(ErrorLevel.Error) && UsesSpecFeatures(s.Range));
-        if (!bodyMustBeSpecOnly && prevErrorCount == reporter.Count(ErrorLevel.Error)) {
-          CheckTypeInference(s.Range);  // we need to resolve operators before the call to DiscoverBounds
-          List<BoundVar> missingBounds;
-          s.Bounds = DiscoverBestBounds_MultipleVars(s.BoundVars, s.Range, true, true, out missingBounds);
-          if (missingBounds.Count != 0) {
-            bodyMustBeSpecOnly = true;
-          }
-        }
-        s.IsGhost = s.Body == null || bodyMustBeSpecOnly;
+        ResolveAttributes(s.Attributes, new ResolveOpts(codeContext, true));
 
         if (s.Body != null) {
           // clear the labels for the duration of checking the body, because break statements are not allowed to leave a forall statement
@@ -5280,7 +5704,7 @@ namespace Microsoft.Dafny
           var prevLoopStack = loopStack;
           labeledStatements = new Scope<Statement>();
           loopStack = new List<Statement>();
-          ResolveStatement(s.Body, bodyMustBeSpecOnly, codeContext);
+          ResolveStatement(s.Body, codeContext);
           labeledStatements = prevLblStmts;
           loopStack = prevLoopStack;
         }
@@ -5327,34 +5751,30 @@ namespace Microsoft.Dafny
 
       } else if (stmt is ModifyStmt) {
         var s = (ModifyStmt)stmt;
-        ResolveAttributes(s.Mod.Attributes, new ResolveOpts(codeContext, true, true));
+        ResolveAttributes(s.Mod.Attributes, new ResolveOpts(codeContext, true));
         foreach (FrameExpression fe in s.Mod.Expressions) {
-          // (yes, say "modifies", not "modify", in the next line -- it seems to give a more readable error message
-          ResolveFrameExpression(fe, false, specContextOnly, codeContext);
+          ResolveFrameExpression(fe, false, codeContext);
         }
         if (s.Body != null) {
-          ResolveBlockStatement(s.Body, specContextOnly, codeContext);
+          ResolveBlockStatement(s.Body, codeContext);
         }
-        s.IsGhost = specContextOnly;
 
       } else if (stmt is CalcStmt) {
         var prevErrorCount = reporter.Count(ErrorLevel.Error);
         CalcStmt s = (CalcStmt)stmt;
-        s.IsGhost = true;
         if (s.Lines.Count > 0) {
           var e0 = s.Lines.First();
-          ResolveExpression(e0, new ResolveOpts(codeContext, true, true));
+          ResolveExpression(e0, new ResolveOpts(codeContext, true));
           Contract.Assert(e0.Type != null);  // follows from postcondition of ResolveExpression
           for (int i = 1; i < s.Lines.Count; i++) {
             if (i < s.Lines.Count - 1 || prevErrorCount == reporter.Count(ErrorLevel.Error)) { // do not resolve the dummy step if there were errors, it might generate more errors
               var e1 = s.Lines[i];
-              ResolveExpression(e1, new ResolveOpts(codeContext, true, true));
+              ResolveExpression(e1, new ResolveOpts(codeContext, true));
               Contract.Assert(e1.Type != null);  // follows from postcondition of ResolveExpression
-              if (!UnifyTypes(e0.Type, e1.Type)) {
-                reporter.Error(MessageSource.Resolver, e1, "all lines in a calculation must have the same type (got {0} after {1})", e1.Type, e0.Type);
+              if (!ConstrainTypes(e0.Type, e1.Type, e1, "all lines in a calculation must have the same type (got {0} after {1})", e1.Type, e0.Type)) {
               } else {
                 var step = s.StepOps[i - 1].StepExpr(e0, e1); // Use custom line operator
-                ResolveExpression(step, new ResolveOpts(codeContext, true, true));
+                ResolveExpression(step, new ResolveOpts(codeContext, true));
                 s.Steps.Add(step);
               }
               e0 = e1;
@@ -5367,8 +5787,7 @@ namespace Microsoft.Dafny
           labeledStatements = new Scope<Statement>();
           loopStack = new List<Statement>();
           foreach (var h in s.Hints) {
-            ResolveStatement(h, true, codeContext);
-            CheckHintRestrictions(h);
+            ResolveStatement(h, codeContext);
           }
           labeledStatements = prevLblStmts;
           loopStack = prevLoopStack;
@@ -5380,36 +5799,68 @@ namespace Microsoft.Dafny
         } else {
           s.Result = CalcStmt.DefaultOp.StepExpr(Expression.CreateIntLiteral(s.Tok, 0), Expression.CreateIntLiteral(s.Tok, 0));
         }
-        ResolveExpression(s.Result, new ResolveOpts(codeContext, true, true));
+        ResolveExpression(s.Result, new ResolveOpts(codeContext, true));
         Contract.Assert(s.Result != null);
         Contract.Assert(prevErrorCount != reporter.Count(ErrorLevel.Error) || s.Steps.Count == s.Hints.Count);
 
       } else if (stmt is MatchStmt) {
-        ResolveMatchStmt(stmt, specContextOnly, codeContext);
+        ResolveMatchStmt(stmt, codeContext);
       } else if (stmt is SkeletonStatement) {
         var s = (SkeletonStatement)stmt;
         reporter.Error(MessageSource.Resolver, s.Tok, "skeleton statements are allowed only in refining methods");
         // nevertheless, resolve the underlying statement; hey, why not
         if (s.S != null) {
-          ResolveStatement(s.S, specContextOnly, codeContext);
+          ResolveStatement(s.S, codeContext);
         }
       } else {
         Contract.Assert(false); throw new cce.UnreachableException();
       }
     }
 
-    void ResolveMatchStmt(Statement stmt, bool specContextOnly, ICodeContext codeContext) {
+    private void ResolveLoopSpecificationComponents(List<MaybeFreeExpression> invariants, Specification<Expression> decreases, Specification<FrameExpression> modifies, ICodeContext codeContext, HashSet<IVariable> fvs) {
+      Contract.Requires(invariants != null);
+      Contract.Requires(decreases != null);
+      Contract.Requires(modifies != null);
+      Contract.Requires(codeContext != null);
+
+      foreach (MaybeFreeExpression inv in invariants) {
+        ResolveAttributes(inv.Attributes, new ResolveOpts(codeContext, true));
+        ResolveExpression(inv.E, new ResolveOpts(codeContext, true));
+        Contract.Assert(inv.E.Type != null);  // follows from postcondition of ResolveExpression
+        if (fvs != null) {
+          Translator.ComputeFreeVariables(inv.E, fvs);
+        }
+        ConstrainTypes(inv.E.Type, Type.Bool, inv.E, "invariant is expected to be of type {0}, but is {1}", Type.Bool, inv.E.Type);
+      }
+
+      ResolveAttributes(decreases.Attributes, new ResolveOpts(codeContext, true));
+      foreach (Expression e in decreases.Expressions) {
+        ResolveExpression(e, new ResolveOpts(codeContext, true));
+        if (e is WildcardExpr) {
+          if (!codeContext.AllowsNontermination && !DafnyOptions.O.Dafnycc) {
+            reporter.Error(MessageSource.Resolver, e, "a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating");
+          }
+        }
+        // any type is fine
+      }
+
+      ResolveAttributes(modifies.Attributes, new ResolveOpts(codeContext, true));
+      if (modifies.Expressions != null) {
+        foreach (FrameExpression fe in modifies.Expressions) {
+          ResolveFrameExpression(fe, false, codeContext);
+          if (fvs != null) {
+            Translator.ComputeFreeVariables(fe.E, fvs);
+          }
+        }
+      }
+    }
+
+    void ResolveMatchStmt(Statement stmt, ICodeContext codeContext) {
       MatchStmt s = (MatchStmt)stmt;
       DesugarMatchStmtWithTupleExpression(s);
 
-      bool bodyIsSpecOnly = specContextOnly;
-      int prevErrorCount = reporter.Count(ErrorLevel.Error);
-      ResolveExpression(s.Source, new ResolveOpts(codeContext, true, specContextOnly));
+      ResolveExpression(s.Source, new ResolveOpts(codeContext, true));
       Contract.Assert(s.Source.Type != null);  // follows from postcondition of ResolveExpression
-      bool successfullyResolved = reporter.Count(ErrorLevel.Error) == prevErrorCount;
-      if (!specContextOnly && successfullyResolved) {
-        bodyIsSpecOnly = UsesSpecFeatures(s.Source);
-      }
       UserDefinedType sourceType = null;
       DatatypeDecl dtd = null;
       if (s.Source.Type.IsDatatype) {
@@ -5431,7 +5882,6 @@ namespace Microsoft.Dafny
           subst.Add(dtd.TypeArgs[i], sourceType.TypeArgs[i]);
         }
       }
-      s.IsGhost = bodyIsSpecOnly;
 
       // convert CasePattern in MatchCaseExpr to BoundVar and flatten the MatchCaseExpr.
       Type type = new InferredTypeProxy();
@@ -5472,16 +5922,14 @@ namespace Microsoft.Dafny
             if (ctor != null && i < ctor.Formals.Count) {
               Formal formal = ctor.Formals[i];
               Type st = SubstType(formal.Type, subst);
-              if (!UnifyTypes(v.Type, st)) {
-                reporter.Error(MessageSource.Resolver, stmt, "the declared type of the formal ({0}) does not agree with the corresponding type in the constructor's signature ({1})", v.Type, st);
-              }
+              ConstrainTypes(v.Type, st, stmt, "the declared type of the formal ({0}) does not agree with the corresponding type in the constructor's signature ({1})", v.Type, st);
               v.IsGhost = formal.IsGhost;
 
               // update the type of the boundvars in the MatchCaseToken
               if (v.tok is MatchCaseToken) {
                 MatchCaseToken mt = (MatchCaseToken)v.tok;
                 foreach (Tuple<IToken, BoundVar, bool> entry in mt.varList) {
-                  UnifyTypes(entry.Item2.Type, v.Type);
+                  UnifyTypes(entry.Item2.Type, v.Type);  // TODO: What if this unification fails? Can it?  --KRML
                 }
               }
             }
@@ -5489,7 +5937,7 @@ namespace Microsoft.Dafny
           }
         }
         foreach (Statement ss in mc.Body) {
-          ResolveStatement(ss, bodyIsSpecOnly, codeContext);
+          ResolveStatement(ss, codeContext);
         }
         // substitute body to replace the case pat with v. This needs to happen
         // after the body is resolved so we can scope the bv correctly.
@@ -5499,7 +5947,7 @@ namespace Microsoft.Dafny
           foreach (Statement ss in mc.Body) {
             Statement clone = cloner.CloneStmt(ss);
             // resolve it again since we just cloned it.
-            ResolveStatement(clone, bodyIsSpecOnly, codeContext);
+            ResolveStatement(clone, codeContext);
             list.Add(clone);
           }
           mc.UpdateBody(list);
@@ -5519,9 +5967,6 @@ namespace Microsoft.Dafny
         }
         Contract.Assert(memberNamesUsed.Count + s.MissingCases.Count == dtd.Ctors.Count);
       }
-      if (!s.IsGhost) {
-        s.IsGhost = s.Cases.All(cs => cs.Body.All(ss => ss.IsGhost));
-      }
     }
 
     /*
@@ -5920,7 +6365,7 @@ namespace Microsoft.Dafny
         reporter.Info(MessageSource.Resolver, loopStmt.Tok, s);
       }
     }
-    private void ResolveConcreteUpdateStmt(ConcreteUpdateStatement s, bool specContextOnly, ICodeContext codeContext) {
+    private void ResolveConcreteUpdateStmt(ConcreteUpdateStatement s, ICodeContext codeContext) {
       Contract.Requires(codeContext != null);
 
       // First, resolve all LHS's and expression-looking RHS's.
@@ -5930,11 +6375,8 @@ namespace Microsoft.Dafny
       var lhsNameSet = new HashSet<string>();  // used to check for duplicate identifiers on the left (full duplication checking for references and the like is done during verification)
       foreach (var lhs in s.Lhss) {
         var ec = reporter.Count(ErrorLevel.Error);
-        ResolveExpression(lhs, new ResolveOpts(codeContext, true, specContextOnly));
+        ResolveExpression(lhs, new ResolveOpts(codeContext, true));
         if (ec == reporter.Count(ErrorLevel.Error)) {
-          if (update == null && specContextOnly && !AssignStmt.LhsIsToGhost(lhs) && !codeContext.IsGhost) {
-            reporter.Error(MessageSource.Resolver, lhs, "cannot assign to non-ghost variable in a ghost context");
-          }
           if (lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne) {
             reporter.Error(MessageSource.Resolver, lhs, "cannot assign to a range of array elements (try the 'forall' statement)");
           }
@@ -5944,18 +6386,18 @@ namespace Microsoft.Dafny
       // Resolve RHSs
       if (update == null) {
         var suchThat = (AssignSuchThatStmt)s;  // this is the other possible subclass
-        ResolveAssignSuchThatStmt(suchThat, specContextOnly, codeContext);
+        ResolveAssignSuchThatStmt(suchThat, codeContext);
       } else {
-        ResolveUpdateStmt(update, specContextOnly, codeContext, errorCountBeforeCheckingLhs);
+        ResolveUpdateStmt(update, codeContext, errorCountBeforeCheckingLhs);
       }
-      ResolveAttributes(s.Attributes, new ResolveOpts(codeContext, true, true));
+      ResolveAttributes(s.Attributes, new ResolveOpts(codeContext, true));
     }
     /// <summary>
     /// Resolve the RHSs and entire UpdateStmt (LHSs should already have been checked by the caller).
     /// errorCountBeforeCheckingLhs is passed in so that this method can determined if any resolution errors were found during
     /// LHS or RHS checking, because only if no errors were found is update.ResolvedStmt changed.
     /// </summary>
-    private void ResolveUpdateStmt(UpdateStmt update, bool specContextOnly, ICodeContext codeContext, int errorCountBeforeCheckingLhs) {
+    private void ResolveUpdateStmt(UpdateStmt update, ICodeContext codeContext, int errorCountBeforeCheckingLhs) {
       Contract.Requires(update != null);
       Contract.Requires(codeContext != null);
       IToken firstEffectfulRhs = null;
@@ -5965,7 +6407,7 @@ namespace Microsoft.Dafny
         bool isEffectful;
         if (rhs is TypeRhs) {
           var tr = (TypeRhs)rhs;
-          ResolveTypeRhs(tr, update, specContextOnly, codeContext);
+          ResolveTypeRhs(tr, update, codeContext);
           isEffectful = tr.InitCall != null;
         } else if (rhs is HavocRhs) {
           isEffectful = false;
@@ -5973,17 +6415,11 @@ namespace Microsoft.Dafny
           var er = (ExprRhs)rhs;
           if (er.Expr is ApplySuffix) {
             var a = (ApplySuffix)er.Expr;
-            // Note, in the following line, the dontCareAboutCompilation could be more precise. It could be computed as in the else
-            // branch if the ApplySuffix is really just the RHS of an assignment. However, if "update" is really a call statement,
-            // then we should not let the LHS influence  the call to ResolveApplySuffix. Unfortunately, we don't know which case
-            // we're in until ResolveApplySuffix has returned (where a non-null cRhs indicates that "update" is a call statement).
-            // So, we'll be conservative and will simply pass in specContextOnly here.
-            var cRhs = ResolveApplySuffix(a, new ResolveOpts(codeContext, true, specContextOnly/*see note on previous line*/), true);
+            var cRhs = ResolveApplySuffix(a, new ResolveOpts(codeContext, true), true);
             isEffectful = cRhs != null;
             methodCallInfo = methodCallInfo ?? cRhs;
           } else {
-            var dontCareAboutCompilation = specContextOnly || (j < update.Lhss.Count && AssignStmt.LhsIsToGhost(update.Lhss[j]));
-            ResolveExpression(er.Expr, new ResolveOpts(codeContext, true, dontCareAboutCompilation));
+            ResolveExpression(er.Expr, new ResolveOpts(codeContext, true));
             isEffectful = false;
           }
         }
@@ -6054,12 +6490,11 @@ namespace Microsoft.Dafny
       }
 
       foreach (var a in update.ResolvedStatements) {
-        ResolveStatement(a, specContextOnly, codeContext);
+        ResolveStatement(a, codeContext);
       }
-      update.IsGhost = update.ResolvedStatements.TrueForAll(ss => ss.IsGhost);
     }
 
-    private void ResolveAssignSuchThatStmt(AssignSuchThatStmt s, bool specContextOnly, ICodeContext codeContext) {
+    private void ResolveAssignSuchThatStmt(AssignSuchThatStmt s, ICodeContext codeContext) {
       Contract.Requires(s != null);
       Contract.Requires(codeContext != null);
 
@@ -6076,71 +6511,44 @@ namespace Microsoft.Dafny
         }
       }
 
-      s.IsGhost = s.Lhss.TrueForAll(AssignStmt.LhsIsToGhost);
       var ec = reporter.Count(ErrorLevel.Error);
-      ResolveExpression(s.Expr, new ResolveOpts(codeContext, true, specContextOnly));
-      if (!UnifyTypes(s.Expr.Type, Type.Bool)) {
-        reporter.Error(MessageSource.Resolver, s.Expr, "type of RHS of assign-such-that statement must be boolean (got {0})", s.Expr.Type);
-      }
-      if (ec == reporter.Count(ErrorLevel.Error) && !s.IsGhost && s.AssumeToken == null && !specContextOnly) {
-        CheckIsNonGhost(s.Expr);
-
-        CheckTypeInference(s.Expr);  // we need to resolve operators before the call to DiscoverBoundsAux
-        List<IVariable> missingBounds;
-        var bestBounds = DiscoverBestBounds_MultipleVars(varLhss, s.Expr, true, false, out missingBounds);
-        if (missingBounds.Count != 0) {
-          s.MissingBounds = missingBounds;  // so that an error message can be produced during compilation
-        } else {
-          Contract.Assert(bestBounds != null);
-          s.Bounds = bestBounds;
-        }
-      }
+      ResolveExpression(s.Expr, new ResolveOpts(codeContext, true));
+      ConstrainTypes(s.Expr.Type, Type.Bool, s.Expr, "type of RHS of assign-such-that statement must be boolean (got {0})", s.Expr.Type);
     }
 
-    bool ResolveAlternatives(List<GuardedAlternative> alternatives, bool specContextOnly, AlternativeLoopStmt loopToCatchBreaks, ICodeContext codeContext) {
+    void ResolveAlternatives(List<GuardedAlternative> alternatives, AlternativeLoopStmt loopToCatchBreaks, ICodeContext codeContext) {
       Contract.Requires(alternatives != null);
       Contract.Requires(codeContext != null);
 
-      bool isGhost = specContextOnly;
       // first, resolve the guards, which tells us whether or not the entire statement is a ghost statement
       foreach (var alternative in alternatives) {
         int prevErrorCount = reporter.Count(ErrorLevel.Error);
-        ResolveExpression(alternative.Guard, new ResolveOpts(codeContext, true, specContextOnly));
+        ResolveExpression(alternative.Guard, new ResolveOpts(codeContext, true));
         Contract.Assert(alternative.Guard.Type != null);  // follows from postcondition of ResolveExpression
         bool successfullyResolved = reporter.Count(ErrorLevel.Error) == prevErrorCount;
-        if (!UnifyTypes(alternative.Guard.Type, Type.Bool)) {
-          reporter.Error(MessageSource.Resolver, alternative.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, alternative.Guard.Type);
-        }
-        if (!specContextOnly && successfullyResolved) {
-          isGhost = isGhost || UsesSpecFeatures(alternative.Guard);
-        }
+        ConstrainTypes(alternative.Guard.Type, Type.Bool, alternative.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, alternative.Guard.Type);
       }
 
       if (loopToCatchBreaks != null) {
         loopStack.Add(loopToCatchBreaks);  // push
-        if (loopToCatchBreaks.Labels == null) {  // otherwise, "loopToCatchBreak" is already in "inSpecOnlyContext" map
-          inSpecOnlyContext.Add(loopToCatchBreaks, specContextOnly);
-        }
       }
       foreach (var alternative in alternatives) {
         scope.PushMarker();
         foreach (Statement ss in alternative.Body) {
-          ResolveStatement(ss, isGhost, codeContext);
+          ResolveStatement(ss, codeContext);
         }
         scope.PopMarker();
       }
       if (loopToCatchBreaks != null) {
         loopStack.RemoveAt(loopStack.Count - 1);  // pop
       }
-
-      return isGhost;
     }
 
     /// <summary>
     /// Resolves the given call statement.
     /// Assumes all LHSs have already been resolved (and checked for mutability).
     /// </summary>
-    void ResolveCallStmt(CallStmt s, bool specContextOnly, ICodeContext codeContext, Type receiverType) {
+    void ResolveCallStmt(CallStmt s, ICodeContext codeContext, Type receiverType) {
       Contract.Requires(s != null);
       Contract.Requires(codeContext != null);
       bool isInitCall = receiverType != null;
@@ -6150,27 +6558,15 @@ namespace Microsoft.Dafny
       if (!isInitCall && callee is Constructor) {
         reporter.Error(MessageSource.Resolver, s, "a constructor is allowed to be called only when an object is being allocated");
       }
-      s.IsGhost = callee.IsGhost;
-      if (specContextOnly && !callee.IsGhost) {
-        reporter.Error(MessageSource.Resolver, s, "only ghost methods can be called from this context");
-      }
 
       // resolve left-hand sides
       foreach (var lhs in s.Lhs) {
         Contract.Assume(lhs.Type != null);  // a sanity check that LHSs have already been resolved
       }
       // resolve arguments
-      if (!s.IsGhost && s.Receiver.WasResolved()) {
-        CheckIsNonGhost(s.Receiver);
-      }
       int j = 0;
       foreach (Expression e in s.Args) {
-        bool allowGhost = s.IsGhost || callee.Ins.Count <= j || callee.Ins[j].IsGhost;
-        var ec = reporter.Count(ErrorLevel.Error);
-        ResolveExpression(e, new ResolveOpts(codeContext, true, allowGhost));
-        if (ec == reporter.Count(ErrorLevel.Error) && !allowGhost) {
-          CheckIsNonGhost(e);
-        }
+        ResolveExpression(e, new ResolveOpts(codeContext, true));
         j++;
       }
 
@@ -6200,39 +6596,14 @@ namespace Microsoft.Dafny
         // type check the arguments
         for (int i = 0; i < callee.Ins.Count; i++) {
           Type st = SubstType(callee.Ins[i].Type, s.MethodSelect.TypeArgumentSubstitutions());
-          if (!UnifyTypes(cce.NonNull(s.Args[i].Type), st)) {
-            reporter.Error(MessageSource.Resolver, s, "incorrect type of method in-parameter {0} (expected {1}, got {2})", i, st, s.Args[i].Type);
-          }
+          ConstrainTypes(s.Args[i].Type, st, s, "incorrect type of method in-parameter {0} (expected {1}, got {2})", i, st, s.Args[i].Type);
         }
         for (int i = 0; i < callee.Outs.Count; i++) {
           Type st = SubstType(callee.Outs[i].Type, s.MethodSelect.TypeArgumentSubstitutions());
           var lhs = s.Lhs[i];
-          if (!UnifyTypes(cce.NonNull(lhs.Type), st)) {
-            reporter.Error(MessageSource.Resolver, s, "incorrect type of method out-parameter {0} (expected {1}, got {2})", i, st, lhs.Type);
+          if (!ConstrainTypes(lhs.Type, st, s, "incorrect type of method out-parameter {0} (expected {1}, got {2})", i, st, lhs.Type)) {
           } else {
             var resolvedLhs = lhs.Resolved;
-            if (!specContextOnly && (s.IsGhost || callee.Outs[i].IsGhost)) {
-              // LHS must denote a ghost
-              if (resolvedLhs is IdentifierExpr) {
-                var ll = (IdentifierExpr)resolvedLhs;
-                if (!ll.Var.IsGhost) {
-                  if (ll is AutoGhostIdentifierExpr && ll.Var is LocalVariable) {
-                    // the variable was actually declared in this statement, so auto-declare it as ghost
-                    ((LocalVariable)ll.Var).MakeGhost();
-                  } else {
-                    reporter.Error(MessageSource.Resolver, s, "actual out-parameter {0} is required to be a ghost variable", i);
-                  }
-                }
-              } else if (resolvedLhs is MemberSelectExpr) {
-                var ll = (MemberSelectExpr)resolvedLhs;
-                if (!ll.Member.IsGhost) {
-                  reporter.Error(MessageSource.Resolver, s, "actual out-parameter {0} is required to be a ghost field", i);
-                }
-              } else {
-                // this is an array update, and arrays are always non-ghost
-                reporter.Error(MessageSource.Resolver, s, "actual out-parameter {0} is required to be a ghost variable", i);
-              }
-            }
             // LHS must denote a mutable field.
             CheckIsLvalue(resolvedLhs, codeContext);
           }
@@ -6282,9 +6653,7 @@ namespace Microsoft.Dafny
         }
       } else if (lhs is SeqSelectExpr) {
         var ll = (SeqSelectExpr)lhs;
-        if (!UnifyTypes(ll.Seq.Type, ResolvedArrayType(ll.Seq.tok, 1, new InferredTypeProxy(), codeContext))) {
-          reporter.Error(MessageSource.Resolver, ll.Seq, "LHS of array assignment must denote an array element (found {0})", ll.Seq.Type);
-        }
+        ConstrainTypes(ll.Seq.Type, ResolvedArrayType(ll.Seq.tok, 1, new InferredTypeProxy(), codeContext), ll.Seq, "LHS of array assignment must denote an array element (found {0})", ll.Seq.Type);
         if (!ll.SelectOne) {
           reporter.Error(MessageSource.Resolver, ll.Seq, "cannot assign to a range of array elements (try the 'forall' statement)");
         }
@@ -6295,7 +6664,7 @@ namespace Microsoft.Dafny
       }
     }
 
-    void ResolveBlockStatement(BlockStmt blockStmt, bool specContextOnly, ICodeContext codeContext) {
+    void ResolveBlockStatement(BlockStmt blockStmt, ICodeContext codeContext) {
       Contract.Requires(blockStmt != null);
       Contract.Requires(codeContext != null);
 
@@ -6313,12 +6682,9 @@ namespace Microsoft.Dafny
           } else {
             var r = labeledStatements.Push(lnode.Name, ss);
             Contract.Assert(r == Scope<Statement>.PushResult.Success);  // since we just checked for duplicates, we expect the Push to succeed
-            if (l == ss.Labels) {  // add it only once
-              inSpecOnlyContext.Add(ss, specContextOnly);
-            }
           }
         }
-        ResolveStatement(ss, specContextOnly, codeContext);
+        ResolveStatement(ss, codeContext);
         labeledStatements.PopMarker();
       }
     }
@@ -6471,8 +6837,9 @@ namespace Microsoft.Dafny
     /// Check that a statment is a valid hint for a calculation.
     /// ToDo: generalize the part for compound statements to take a delegate?
     /// </summary>
-    public void CheckHintRestrictions(Statement stmt) {
+    public void CheckHintRestrictions(Statement stmt, ISet<LocalVariable> localsAllowedInUpdates) {
       Contract.Requires(stmt != null);
+      Contract.Requires(localsAllowedInUpdates != null);
       if (stmt is PredicateStmt) {
         // cool
       } else if (stmt is PrintStmt) {
@@ -6486,11 +6853,11 @@ namespace Microsoft.Dafny
       } else if (stmt is AssignSuchThatStmt) {
         var s = (AssignSuchThatStmt)stmt;
         foreach (var lhs in s.Lhss) {
-          CheckHintLhs(s.Tok, lhs.Resolved);
+          CheckHintLhs(s.Tok, lhs.Resolved, localsAllowedInUpdates);
         }
       } else if (stmt is AssignStmt) {
         var s = (AssignStmt)stmt;
-        CheckHintLhs(s.Tok, s.Lhs.Resolved);
+        CheckHintLhs(s.Tok, s.Lhs.Resolved, localsAllowedInUpdates);
       } else if (stmt is CallStmt) {
         var s = (CallStmt)stmt;
         if (s.Method.Mod.Expressions.Count != 0) {
@@ -6499,33 +6866,33 @@ namespace Microsoft.Dafny
       } else if (stmt is UpdateStmt) {
         var s = (UpdateStmt)stmt;
         foreach (var ss in s.ResolvedStatements) {
-          CheckHintRestrictions(ss);
+          CheckHintRestrictions(ss, localsAllowedInUpdates);
         }
       } else if (stmt is VarDeclStmt) {
         var s = (VarDeclStmt)stmt;
+        s.Locals.Iter(local => localsAllowedInUpdates.Add(local));
         if (s.Update != null) {
-          CheckHintRestrictions(s.Update);
+          CheckHintRestrictions(s.Update, localsAllowedInUpdates);
         }
       } else if (stmt is BlockStmt) {
         var s = (BlockStmt)stmt;
-        scope.PushMarker();
+        var newScopeForLocals = new HashSet<LocalVariable>(localsAllowedInUpdates);
         foreach (var ss in s.Body) {
-          CheckHintRestrictions(ss);
+          CheckHintRestrictions(ss, newScopeForLocals);
         }
-        scope.PopMarker();
 
       } else if (stmt is IfStmt) {
         var s = (IfStmt)stmt;
-        CheckHintRestrictions(s.Thn);
+        CheckHintRestrictions(s.Thn, localsAllowedInUpdates);
         if (s.Els != null) {
-          CheckHintRestrictions(s.Els);
+          CheckHintRestrictions(s.Els, localsAllowedInUpdates);
         }
 
       } else if (stmt is AlternativeStmt) {
         var s = (AlternativeStmt)stmt;
         foreach (var alt in s.Alternatives) {
           foreach (var ss in alt.Body) {
-            CheckHintRestrictions(ss);
+            CheckHintRestrictions(ss, localsAllowedInUpdates);
           }
         }
 
@@ -6535,14 +6902,14 @@ namespace Microsoft.Dafny
           reporter.Error(MessageSource.Resolver, s.Mod.Expressions[0].tok, "a while statement used inside a hint is not allowed to have a modifies clause");
         }
         if (s.Body != null) {
-          CheckHintRestrictions(s.Body);
+          CheckHintRestrictions(s.Body, localsAllowedInUpdates);
         }
 
       } else if (stmt is AlternativeLoopStmt) {
         var s = (AlternativeLoopStmt)stmt;
         foreach (var alt in s.Alternatives) {
           foreach (var ss in alt.Body) {
-            CheckHintRestrictions(ss);
+            CheckHintRestrictions(ss, localsAllowedInUpdates);
           }
         }
 
@@ -6564,14 +6931,14 @@ namespace Microsoft.Dafny
       } else if (stmt is CalcStmt) {
         var s = (CalcStmt)stmt;
         foreach (var h in s.Hints) {
-          CheckHintRestrictions(h);
+          CheckHintRestrictions(h, new HashSet<LocalVariable>());
         }
 
       } else if (stmt is MatchStmt) {
         var s = (MatchStmt)stmt;
         foreach (var kase in s.Cases) {
           foreach (var ss in kase.Body) {
-            CheckHintRestrictions(ss);
+            CheckHintRestrictions(ss, localsAllowedInUpdates);
           }
         }
 
@@ -6580,25 +6947,24 @@ namespace Microsoft.Dafny
       }
     }
 
-    void CheckHintLhs(IToken tok, Expression lhs) {
+    void CheckHintLhs(IToken tok, Expression lhs, ISet<LocalVariable> localsAllowedInUpdates) {
+      Contract.Requires(tok != null);
+      Contract.Requires(lhs != null);
+      Contract.Requires(localsAllowedInUpdates != null);
       var idExpr = lhs as IdentifierExpr;
       if (idExpr == null) {
         reporter.Error(MessageSource.Resolver, tok, "a hint is not allowed to update heap locations");
-      } else if (scope.ContainsDecl(idExpr.Var)) {
+      } else if (!localsAllowedInUpdates.Contains(idExpr.Var)) {
         reporter.Error(MessageSource.Resolver, tok, "a hint is not allowed to update a variable declared outside the hint");
       }
     }
 
-    Type ResolveTypeRhs(TypeRhs rr, Statement stmt, bool specContextOnly, ICodeContext codeContext) {
+    Type ResolveTypeRhs(TypeRhs rr, Statement stmt, ICodeContext codeContext) {
       Contract.Requires(rr != null);
       Contract.Requires(stmt != null);
       Contract.Requires(codeContext != null);
       Contract.Ensures(Contract.Result<Type>() != null);
 
-      // "new" is not allowed in ghost contexts
-      if (specContextOnly) {
-        reporter.Error(MessageSource.Resolver, rr.Tok, "'new' is not allowed in ghost contexts");
-      }
       if (rr.Type == null) {
         if (rr.ArrayDimensions != null) {
           // ---------- new T[EE]
@@ -6608,9 +6974,7 @@ namespace Microsoft.Dafny
           foreach (Expression dim in rr.ArrayDimensions) {
             Contract.Assert(dim != null);
             ResolveExpression(dim, new ResolveOpts(codeContext, true));
-            if (!UnifyTypes(dim.Type, new OperationTypeProxy(true, false, false, false, false, false))) {
-              reporter.Error(MessageSource.Resolver, stmt, "new must use an integer-based expression for the array size (got {0} for index {1})", dim.Type, i);
-            }
+            ConstrainTypes(dim.Type, new OperationTypeProxy(true, false, false, false, false, false), stmt, "new must use an integer-based expression for the array size (got {0} for index {1})", dim.Type, i);
             i++;
           }
           rr.Type = ResolvedArrayType(stmt.Tok, rr.ArrayDimensions.Count, rr.EType, codeContext);
@@ -6652,13 +7016,13 @@ namespace Microsoft.Dafny
               // type, create an dot-suffix expression around this receiver, and then resolve it in the usual way for dot-suffix expressions.
               var lhs = new ImplicitThisExpr(initCallTok) { Type = rr.EType };
               var callLhs = new ExprDotName(initCallTok, lhs, initCallName, ret == null ? null : ret.LastComponent.OptTypeArguments);
-              ResolveDotSuffix(callLhs, true, rr.Arguments, new ResolveOpts(codeContext, true, specContextOnly), true);
+              ResolveDotSuffix(callLhs, true, rr.Arguments, new ResolveOpts(codeContext, true), true);
               if (prevErrorCount == reporter.Count(ErrorLevel.Error)) {
                 Contract.Assert(callLhs.ResolvedExpression is MemberSelectExpr);  // since ResolveApplySuffix succeeded and call.Lhs denotes an expression (not a module or a type)
                 var methodSel = (MemberSelectExpr)callLhs.ResolvedExpression;
                 if (methodSel.Member is Method) {
                   rr.InitCall = new CallStmt(initCallTok, stmt.EndTok, new List<Expression>(), methodSel, rr.Arguments);
-                  ResolveCallStmt(rr.InitCall, specContextOnly, codeContext, rr.EType);
+                  ResolveCallStmt(rr.InitCall, codeContext, rr.EType);
                   if (rr.InitCall.Method is Constructor) {
                     callsConstructor = true;
                   }
@@ -6692,6 +7056,8 @@ namespace Microsoft.Dafny
       Contract.Requires(memberName != null);
       Contract.Ensures(Contract.Result<MemberDecl>() == null || Contract.ValueAtReturn(out nptype) != null);
 
+      PartiallySolveTypeConstraints();  // so that we can try to pick up the type of the receiver
+
       nptype = null;  // prepare for the worst
       receiverType = receiverType.NormalizeExpand();
       var opProxy = receiverType as OperationTypeProxy;
@@ -6932,24 +7298,10 @@ namespace Microsoft.Dafny
     {
       public readonly ICodeContext codeContext;
       public readonly bool twoState;
-      public readonly bool DontCareAboutCompilation;
       public ResolveOpts(ICodeContext codeContext, bool twoState) {
         Contract.Requires(codeContext != null);
         this.codeContext = codeContext;
         this.twoState = twoState;
-        DontCareAboutCompilation = codeContext.IsGhost;
-      }
-      public ResolveOpts(ICodeContext codeContext, bool twoState, bool dontCareAboutCompilation) {
-        Contract.Requires(codeContext != null);
-        this.codeContext = codeContext;
-        this.twoState = twoState;
-        this.DontCareAboutCompilation = dontCareAboutCompilation;
-      }
-      public ResolveOpts(ResolveOpts r, bool dontCareAboutCompilation) {
-        Contract.Requires(r != null);
-        this.codeContext = r.codeContext;
-        this.twoState = r.twoState;
-        this.DontCareAboutCompilation = dontCareAboutCompilation;
       }
     }
 
@@ -7083,9 +7435,7 @@ namespace Microsoft.Dafny
         foreach (Expression ee in e.Elements) {
           ResolveExpression(ee, opts);
           Contract.Assert(ee.Type != null);  // follows from postcondition of ResolveExpression
-          if (!UnifyTypes(elementType, ee.Type)) {
-            reporter.Error(MessageSource.Resolver, ee, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", ee.Type, elementType);
-          }
+          ConstrainTypes(elementType, ee.Type, ee, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", ee.Type, elementType);
         }
         if (expr is SetDisplayExpr) {
           var se = (SetDisplayExpr)expr;
@@ -7102,14 +7452,10 @@ namespace Microsoft.Dafny
         foreach (ExpressionPair p in e.Elements) {
           ResolveExpression(p.A, opts);
           Contract.Assert(p.A.Type != null);  // follows from postcondition of ResolveExpression
-          if (!UnifyTypes(domainType, p.A.Type)) {
-            reporter.Error(MessageSource.Resolver, p.A, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", p.A.Type, domainType);
-          }
+          ConstrainTypes(domainType, p.A.Type, p.A, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", p.A.Type, domainType);
           ResolveExpression(p.B, opts);
           Contract.Assert(p.B.Type != null);  // follows from postcondition of ResolveExpression
-          if (!UnifyTypes(rangeType, p.B.Type)) {
-            reporter.Error(MessageSource.Resolver, p.B, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", p.B.Type, rangeType);
-          }
+          ConstrainTypes(rangeType, p.B.Type, p.B, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", p.B.Type, rangeType);
         }
         expr.Type = new MapType(e.Finite, domainType, rangeType);
       } else if (expr is NameSegment) {
@@ -7192,17 +7538,13 @@ namespace Microsoft.Dafny
         ResolveExpression(e.Array, opts);
         Contract.Assert(e.Array.Type != null);  // follows from postcondition of ResolveExpression
         Type elementType = new InferredTypeProxy();
-        if (!UnifyTypes(e.Array.Type, ResolvedArrayType(e.Array.tok, e.Indices.Count, elementType, opts.codeContext))) {
-          reporter.Error(MessageSource.Resolver, e.Array, "array selection requires an array{0} (got {1})", e.Indices.Count, e.Array.Type);
-        }
+        ConstrainTypes(e.Array.Type, ResolvedArrayType(e.Array.tok, e.Indices.Count, elementType, opts.codeContext), e.Array, "array selection requires an array{0} (got {1})", e.Indices.Count, e.Array.Type);
         int i = 0;
         foreach (Expression idx in e.Indices) {
           Contract.Assert(idx != null);
           ResolveExpression(idx, opts);
           Contract.Assert(idx.Type != null);  // follows from postcondition of ResolveExpression
-          if (!UnifyTypes(idx.Type, new OperationTypeProxy(true, false, false, false, false, false))) {
-            reporter.Error(MessageSource.Resolver, idx, "array selection requires integer-based numeric indices (got {0} for index {1})", idx.Type, i);
-          }
+          ConstrainTypes(idx.Type, new OperationTypeProxy(true, false, false, false, false, false), idx, "array selection requires integer-based numeric indices (got {0} for index {1})", idx.Type, i);
           i++;
         }
         e.Type = elementType;
@@ -7217,44 +7559,28 @@ namespace Microsoft.Dafny
         if (UnifyTypes(e.Seq.Type, new SeqType(elementType))) {
           ResolveExpression(e.Index, opts);
           Contract.Assert(e.Index.Type != null);  // follows from postcondition of ResolveExpression
-          if (!UnifyTypes(e.Index.Type, Type.Int)) {
-            reporter.Error(MessageSource.Resolver, e.Index, "sequence update requires integer index (got {0})", e.Index.Type);
-          }
+          ConstrainTypes(e.Index.Type, Type.Int, e.Index, "sequence update requires integer index (got {0})", e.Index.Type);
           ResolveExpression(e.Value, opts);
           Contract.Assert(e.Value.Type != null);  // follows from postcondition of ResolveExpression
-          if (!UnifyTypes(e.Value.Type, elementType)) {
-            reporter.Error(MessageSource.Resolver, e.Value, "sequence update requires the value to have the element type of the sequence (got {0})", e.Value.Type);
-          }
+          ConstrainTypes(e.Value.Type, elementType, e.Value, "sequence update requires the value to have the element type of the sequence (got {0})", e.Value.Type);
           expr.Type = e.Seq.Type;
         } else if (UnifyTypes(e.Seq.Type, new MapType(true, domainType, rangeType))) {
           ResolveExpression(e.Index, opts);
-          if (!UnifyTypes(e.Index.Type, domainType)) {
-            reporter.Error(MessageSource.Resolver, e.Index, "map update requires domain element to be of type {0} (got {1})", domainType, e.Index.Type);
-          }
+          ConstrainTypes(e.Index.Type, domainType, e.Index, "map update requires domain element to be of type {0} (got {1})", domainType, e.Index.Type);
           ResolveExpression(e.Value, opts);
-          if (!UnifyTypes(e.Value.Type, rangeType)) {
-            reporter.Error(MessageSource.Resolver, e.Value, "map update requires the value to have the range type {0} (got {1})", rangeType, e.Value.Type);
-          }
+          ConstrainTypes(e.Value.Type, rangeType, e.Value, "map update requires the value to have the range type {0} (got {1})", rangeType, e.Value.Type);
           expr.Type = e.Seq.Type;
         } else if (UnifyTypes(e.Seq.Type, new MapType(false, domainType, rangeType))) {
           ResolveExpression(e.Index, opts);
-          if (!UnifyTypes(e.Index.Type, domainType)) {
-            reporter.Error(MessageSource.Resolver, e.Index, "imap update requires domain element to be of type {0} (got {1})", domainType, e.Index.Type);
-          }
+          ConstrainTypes(e.Index.Type, domainType, e.Index, "imap update requires domain element to be of type {0} (got {1})", domainType, e.Index.Type);
           ResolveExpression(e.Value, opts);
-          if (!UnifyTypes(e.Value.Type, rangeType)) {
-            reporter.Error(MessageSource.Resolver, e.Value, "imap update requires the value to have the range type {0} (got {1})", rangeType, e.Value.Type);
-          }
+          ConstrainTypes(e.Value.Type, rangeType, e.Value, "imap update requires the value to have the range type {0} (got {1})", rangeType, e.Value.Type);
           expr.Type = e.Seq.Type;
         } else if (UnifyTypes(e.Seq.Type, new MultiSetType(elementType))) {
           ResolveExpression(e.Index, opts);
-          if (!UnifyTypes(e.Index.Type, elementType)) {
-            reporter.Error(MessageSource.Resolver, e.Index, "multiset update requires domain element to be of type {0} (got {1})", elementType, e.Index.Type);
-          }
+          ConstrainTypes(e.Index.Type, elementType, e.Index, "multiset update requires domain element to be of type {0} (got {1})", elementType, e.Index.Type);
           ResolveExpression(e.Value, opts);
-          if (!UnifyTypes(e.Value.Type, new OperationTypeProxy(true, false, false, false, false, false))) {
-            reporter.Error(MessageSource.Resolver, e.Value, "multiset update requires integer-based numeric value (got {0})", e.Value.Type);
-          }
+          ConstrainTypes(e.Value.Type, new OperationTypeProxy(true, false, false, false, false, false), e.Value, "multiset update requires integer-based numeric value (got {0})", e.Value.Type);
           expr.Type = e.Seq.Type;
 
         } else if (e.Seq.Type.IsDatatype) {
@@ -7363,9 +7689,7 @@ namespace Microsoft.Dafny
           reporter.Error(MessageSource.Resolver, e.tok, "wrong number of arguments to function application (function type '{0}' expects {1}, got {2})", fnType, fnType.Arity, e.Args.Count);
         } else {
           for (var i = 0; i < fnType.Arity; i++) {
-            if (!UnifyTypes(fnType.Args[i], e.Args[i].Type)) {
-              reporter.Error(MessageSource.Resolver, e.Args[i].tok, "type mismatch for argument {0} (function expects {1}, got {2})", i, fnType.Args[i], e.Args[i].Type);
-            }
+            ConstrainTypes(fnType.Args[i], e.Args[i].Type, e.Args[i].tok, "type mismatch for argument {0} (function expects {1}, got {2})", i, fnType.Args[i], e.Args[i].Type);
           }
         }
         expr.Type = fnType == null ? new InferredTypeProxy() : fnType.Result;
@@ -7392,15 +7716,11 @@ namespace Microsoft.Dafny
         Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression
         switch (e.Op) {
           case UnaryOpExpr.Opcode.Not:
-            if (!UnifyTypes(e.E.Type, Type.Bool)) {
-              reporter.Error(MessageSource.Resolver, expr, "logical negation expects a boolean argument (instead got {0})", e.E.Type);
-            }
+            ConstrainTypes(e.E.Type, Type.Bool, expr, "logical negation expects a boolean argument (instead got {0})", e.E.Type);
             expr.Type = Type.Bool;
             break;
           case UnaryOpExpr.Opcode.Cardinality:
-            if (!UnifyTypes(e.E.Type, new CollectionTypeProxy(new InferredTypeProxy(), false, false))) {
-              reporter.Error(MessageSource.Resolver, expr, "size operator expects a collection argument (instead got {0})", e.E.Type);
-            }
+            ConstrainTypes(e.E.Type, new CollectionTypeProxy(new InferredTypeProxy(), false, false), expr, "size operator expects a collection argument (instead got {0})", e.E.Type);
             expr.Type = Type.Int;
             break;
           case UnaryOpExpr.Opcode.Fresh:
@@ -7433,13 +7753,9 @@ namespace Microsoft.Dafny
         ResolveType(e.tok, e.ToType, opts.codeContext, new ResolveTypeOption(ResolveTypeOptionEnum.DontInfer), null);
         ResolveExpression(e.E, opts);
         if (e.ToType.IsNumericBased(Type.NumericPersuation.Int)) {
-          if (!UnifyTypes(e.E.Type, new OperationTypeProxy(true, true, false, false, false, false))) {
-            reporter.Error(MessageSource.Resolver, expr, "type conversion to an int-based type is allowed only from numeric types (got {0})", e.E.Type);
-          }
+          ConstrainTypes(e.E.Type, new OperationTypeProxy(true, true, false, false, false, false), expr, "type conversion to an int-based type is allowed only from numeric types (got {0})", e.E.Type);
         } else if (e.ToType.IsNumericBased(Type.NumericPersuation.Real)) {
-          if (!UnifyTypes(e.E.Type, new OperationTypeProxy(true, true, false, false, false, false))) {
-            reporter.Error(MessageSource.Resolver, expr, "type conversion to a real-based type is allowed only from numeric types (got {0})", e.E.Type);
-          }
+          ConstrainTypes(e.E.Type, new OperationTypeProxy(true, true, false, false, false, false), expr, "type conversion to a real-based type is allowed only from numeric types (got {0})", e.E.Type);
         } else {
           reporter.Error(MessageSource.Resolver, expr, "type conversions are not supported to this type (got {0})", e.ToType);
         }
@@ -7457,12 +7773,8 @@ namespace Microsoft.Dafny
           case BinaryExpr.Opcode.Exp:
           case BinaryExpr.Opcode.And:
           case BinaryExpr.Opcode.Or:
-            if (!UnifyTypes(e.E0.Type, Type.Bool)) {
-              reporter.Error(MessageSource.Resolver, expr, "first argument to {0} must be of type bool (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
-            }
-            if (!UnifyTypes(e.E1.Type, Type.Bool)) {
-              reporter.Error(MessageSource.Resolver, expr, "second argument to {0} must be of type bool (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E1.Type);
-            }
+            ConstrainTypes(e.E0.Type, Type.Bool, expr, "first argument to {0} must be of type bool (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
+            ConstrainTypes(e.E1.Type, Type.Bool, expr, "second argument to {0} must be of type bool (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E1.Type);
             expr.Type = Type.Bool;
             break;
 
@@ -7489,9 +7801,7 @@ namespace Microsoft.Dafny
 
           case BinaryExpr.Opcode.Disjoint:
             // TODO: the error messages are backwards from what (ideally) they should be. this is necessary because UnifyTypes can't backtrack.
-            if (!UnifyTypes(e.E0.Type, e.E1.Type)) {
-              reporter.Error(MessageSource.Resolver, expr, "arguments must have the same type (got {0} and {1})", e.E0.Type, e.E1.Type);
-            }
+            ConstrainTypes(e.E0.Type, e.E1.Type, expr, "arguments must have the same type (got {0} and {1})", e.E0.Type, e.E1.Type);
             if (!UnifyTypes(e.E0.Type, new SetType(true, new InferredTypeProxy())) &&
                 !UnifyTypes(e.E0.Type, new MultiSetType(new InferredTypeProxy())) &&
                 !UnifyTypes(e.E0.Type, new MapType(true, new InferredTypeProxy(), new InferredTypeProxy()))) {
@@ -7504,34 +7814,25 @@ namespace Microsoft.Dafny
           case BinaryExpr.Opcode.Le:
           case BinaryExpr.Opcode.Add: {
               if (e.Op == BinaryExpr.Opcode.Lt && (e.E0.Type.NormalizeExpand().IsIndDatatype || e.E0.Type.IsTypeParameter)) {
-                if (UnifyTypes(e.E1.Type, new DatatypeProxy(false, false))) {
+                if (ConstrainTypes(e.E1.Type, new DatatypeProxy(false, false), expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type)) {
                   e.ResolvedOp = BinaryExpr.ResolvedOpcode.RankLt;
-                } else {
-                  reporter.Error(MessageSource.Resolver, expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);
                 }
                 expr.Type = Type.Bool;
               } else if (e.Op == BinaryExpr.Opcode.Lt && e.E1.Type.NormalizeExpand().IsIndDatatype) {
-                if (UnifyTypes(e.E0.Type, new DatatypeProxy(false, true))) {
+                if (ConstrainTypes(e.E0.Type, new DatatypeProxy(false, true), expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E0.Type)) {
                   e.ResolvedOp = BinaryExpr.ResolvedOpcode.RankLt;
-                } else {
-                  reporter.Error(MessageSource.Resolver, expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E0.Type);
                 }
                 expr.Type = Type.Bool;
               } else {
-                bool err = false;
                 bool isComparison = e.Op != BinaryExpr.Opcode.Add;
-                if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true, true, isComparison, true, true, true))) {
-                  reporter.Error(MessageSource.Resolver, expr, "arguments to {0} must be of a numeric type{2} or a collection type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type,
-                    isComparison ? ", char," : "");
-                  err = true;
-                }
-                if (!UnifyTypes(e.E1.Type, e.E0.Type)) {
-                  reporter.Error(MessageSource.Resolver, expr, "arguments to {0} must have the same type (got {1} and {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);
-                  err = true;
-                }
+                var good0 = ConstrainTypes(e.E0.Type, new OperationTypeProxy(true, true, isComparison, true, true, true),
+                  expr, "arguments to {0} must be of a numeric type{2} or a collection type (instead got {1})",
+                  BinaryExpr.OpcodeString(e.Op), e.E0.Type, isComparison ? ", char," : "");
+                var good1 = ConstrainTypes(e.E1.Type, e.E0.Type,
+                  expr, "arguments to {0} must have the same type (got {1} and {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);
                 if (isComparison) {
                   expr.Type = Type.Bool;
-                } else if (!err) {
+                } else if (good0 && good1) {
                   expr.Type = e.E0.Type;
                 }
               }
@@ -7543,34 +7844,24 @@ namespace Microsoft.Dafny
           case BinaryExpr.Opcode.Gt:
           case BinaryExpr.Opcode.Ge: {
               if (e.Op == BinaryExpr.Opcode.Gt && e.E0.Type.NormalizeExpand().IsIndDatatype) {
-                if (UnifyTypes(e.E1.Type, new DatatypeProxy(false, true))) {
+                if (ConstrainTypes(e.E1.Type, new DatatypeProxy(false, true), expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type)) {
                   e.ResolvedOp = BinaryExpr.ResolvedOpcode.RankGt;
-                } else {
-                  reporter.Error(MessageSource.Resolver, expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);
                 }
                 expr.Type = Type.Bool;
               } else if (e.Op == BinaryExpr.Opcode.Gt && (e.E1.Type.NormalizeExpand().IsIndDatatype || e.E1.Type.IsTypeParameter)) {
-                if (UnifyTypes(e.E0.Type, new DatatypeProxy(false, false))) {
+                if (ConstrainTypes(e.E0.Type, new DatatypeProxy(false, false), expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E0.Type)) {
                   e.ResolvedOp = BinaryExpr.ResolvedOpcode.RankGt;
-                } else {
-                  reporter.Error(MessageSource.Resolver, expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E0.Type);
                 }
                 expr.Type = Type.Bool;
               } else {
-                bool err = false;
                 bool isComparison = e.Op == BinaryExpr.Opcode.Gt || e.Op == BinaryExpr.Opcode.Ge;
-                if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true, true, isComparison, false, true, true))) {
-                  reporter.Error(MessageSource.Resolver, expr, "arguments to {0} must be of a numeric type{2} or a set type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type,
-                    isComparison ? ", char, " : "");
-                  err = true;
-                }
-                if (!UnifyTypes(e.E1.Type, e.E0.Type)) {
-                  reporter.Error(MessageSource.Resolver, expr, "arguments to {0} must have the same type (got {1} and {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);
-                  err = true;
-                }
+                var good0 = ConstrainTypes(e.E0.Type, new OperationTypeProxy(true, true, isComparison, false, true, true),
+                  expr, "arguments to {0} must be of a numeric type{2} or a set type (instead got {1})",
+                  BinaryExpr.OpcodeString(e.Op), e.E0.Type, isComparison ? ", char, " : "");
+                var good1 = ConstrainTypes(e.E1.Type, e.E0.Type, expr, "arguments to {0} must have the same type (got {1} and {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);
                 if (isComparison) {
                   expr.Type = Type.Bool;
-                } else if (!err) {
+                } else if (good0 && good1) {
                   expr.Type = e.E0.Type;
                 }
               }
@@ -7579,29 +7870,23 @@ namespace Microsoft.Dafny
 
           case BinaryExpr.Opcode.In:
           case BinaryExpr.Opcode.NotIn:
-            if (!UnifyTypes(e.E1.Type, new CollectionTypeProxy(e.E0.Type, true, true))) {
-              reporter.Error(MessageSource.Resolver, expr, "second argument to \"{0}\" must be a set, multiset, or sequence with elements of type {1}, or a map with domain {1} (instead got {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);
-            }
+            ConstrainTypes(e.E1.Type, new CollectionTypeProxy(e.E0.Type, true, true), expr, "second argument to \"{0}\" must be a set, multiset, or sequence with elements of type {1}, or a map with domain {1} (instead got {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);
             expr.Type = Type.Bool;
             break;
 
           case BinaryExpr.Opcode.Div:
-            if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true, true, false, false, false, false))) {
-              reporter.Error(MessageSource.Resolver, expr, "first argument to {0} must be of numeric type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
-            }
-            if (!UnifyTypes(e.E1.Type, e.E0.Type)) {
-              reporter.Error(MessageSource.Resolver, expr, "arguments to {0} must have the same type (got {1} and {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);
-            }
+            ConstrainTypes(e.E0.Type, new OperationTypeProxy(true, true, false, false, false, false),
+              expr, "first argument to {0} must be of numeric type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
+            ConstrainTypes(e.E1.Type, e.E0.Type,
+              expr, "arguments to {0} must have the same type (got {1} and {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);
             expr.Type = e.E0.Type;
             break;
 
           case BinaryExpr.Opcode.Mod:
-            if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true, false, false, false, false, false))) {
-              reporter.Error(MessageSource.Resolver, expr, "first argument to {0} must be of type int (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
-            }
-            if (!UnifyTypes(e.E1.Type, e.E0.Type)) {
-              reporter.Error(MessageSource.Resolver, expr, "second argument to {0} must be of type int (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E1.Type);
-            }
+            ConstrainTypes(e.E0.Type, new OperationTypeProxy(true, false, false, false, false, false),
+              expr, "first argument to {0} must be of type int (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
+            ConstrainTypes(e.E1.Type, e.E0.Type,
+              expr, "second argument to {0} must be of type int (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E1.Type);
             expr.Type = e.E0.Type;
             break;
 
@@ -7619,15 +7904,12 @@ namespace Microsoft.Dafny
         switch (e.Op) {
           case TernaryExpr.Opcode.PrefixEqOp:
           case TernaryExpr.Opcode.PrefixNeqOp:
-            if (!UnifyTypes(e.E0.Type, Type.Int)) {
-              reporter.Error(MessageSource.Resolver, e.E0, "prefix-equality limit argument must be an integer expression (got {0})", e.E0.Type);
-            }
-            if (!UnifyTypes(e.E1.Type, new DatatypeProxy(true))) {
-              reporter.Error(MessageSource.Resolver, expr, "arguments to prefix equality must be codatatypes (instead of {0})", e.E1.Type);
-            }
-            if (!UnifyTypes(e.E1.Type, e.E2.Type)) {
-              reporter.Error(MessageSource.Resolver, expr, "arguments must have the same type (got {0} and {1})", e.E1.Type, e.E2.Type);
-            }
+            ConstrainTypes(e.E0.Type, Type.Int,
+              e.E0, "prefix-equality limit argument must be an integer expression (got {0})", e.E0.Type);
+            ConstrainTypes(e.E1.Type, new DatatypeProxy(true),
+              expr, "arguments to prefix equality must be codatatypes (instead of {0})", e.E1.Type);
+            ConstrainTypes(e.E1.Type, e.E2.Type,
+              expr, "arguments must have the same type (got {0} and {1})", e.E1.Type, e.E2.Type);
             expr.Type = Type.Bool;
             break;
           default:
@@ -7676,16 +7958,11 @@ namespace Microsoft.Dafny
           }
           foreach (var rhs in e.RHSs) {
             ResolveExpression(rhs, opts);
-            if (!UnifyTypes(rhs.Type, Type.Bool)) {
-              reporter.Error(MessageSource.Resolver, rhs.tok, "type of RHS of let-such-that expression must be boolean (got {0})", rhs.Type);
-            }
-          }
-          if (!opts.DontCareAboutCompilation && !e.BoundVars.All(bv => bv.IsGhost)) {
-            needFiniteBoundsChecks_LetSuchThatExpr.Add(e);
+            ConstrainTypes(rhs.Type, Type.Bool, rhs.tok, "type of RHS of let-such-that expression must be boolean (got {0})", rhs.Type);
           }
         }
         ResolveExpression(e.Body, opts);
-        ResolveAttributes(e.Attributes, new ResolveOpts(opts, true));
+        ResolveAttributes(e.Attributes, opts);
         scope.PopMarker();
         expr.Type = e.Body.Type;
 
@@ -7712,47 +7989,20 @@ namespace Microsoft.Dafny
           reporter.Error(MessageSource.Resolver, expr, "a quantifier cannot quantify over types. Possible fix: use the experimental attribute :typeQuantifier");
         }
         if (e.Range != null) {
-          ResolveExpression(e.Range, new ResolveOpts(opts, true));
+          ResolveExpression(e.Range, opts);
           Contract.Assert(e.Range.Type != null);  // follows from postcondition of ResolveExpression
-          if (!UnifyTypes(e.Range.Type, Type.Bool)) {
-            reporter.Error(MessageSource.Resolver, expr, "range of quantifier must be of type bool (instead got {0})", e.Range.Type);
-          }
+          ConstrainTypes(e.Range.Type, Type.Bool, expr, "range of quantifier must be of type bool (instead got {0})", e.Range.Type);
         }
-        ResolveExpression(e.Term, new ResolveOpts(opts, true));
+        ResolveExpression(e.Term, opts);
         Contract.Assert(e.Term.Type != null);  // follows from postcondition of ResolveExpression
-        if (!UnifyTypes(e.Term.Type, Type.Bool)) {
-          reporter.Error(MessageSource.Resolver, expr, "body of quantifier must be of type bool (instead got {0})", e.Term.Type);
-        }
+        ConstrainTypes(e.Term.Type, Type.Bool, expr, "body of quantifier must be of type bool (instead got {0})", e.Term.Type);
         // Since the body is more likely to infer the types of the bound variables, resolve it
         // first (above) and only then resolve the attributes (below).
-        ResolveAttributes(e.Attributes, new ResolveOpts(opts, true));
+        ResolveAttributes(e.Attributes, opts);
         scope.PopMarker();
         allTypeParameters.PopMarker();
         expr.Type = Type.Bool;
 
-        if (prevErrorCount == reporter.Count(ErrorLevel.Error)) {
-          CheckTypeInference(e.LogicalBody());  // we need to resolve operators before the call to DiscoverBounds
-          List<BoundVar> missingBounds;
-          e.Bounds = DiscoverBestBounds_MultipleVars(e.BoundVars, e.LogicalBody(), e is ExistsExpr, true, out missingBounds);
-          if (missingBounds.Count != 0) {
-            // Report errors here about quantifications that depend on the allocation state.
-            var mb = missingBounds;
-            if (opts.codeContext is Function) {
-              mb = new List<BoundVar>();  // (who cares if we allocate another array; this happens only in the case of a resolution error anyhow)
-              foreach (var bv in missingBounds) {
-                if (bv.Type.IsRefType) {
-                  reporter.Error(MessageSource.Resolver, expr, "a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of '{0}'", bv.Name);
-                } else {
-                  mb.Add(bv);
-                }
-              }
-            }
-            if (mb.Count != 0) {
-              e.MissingBounds = mb;
-            }
-          }
-        }
-
       } else if (expr is SetComprehension) {
         var e = (SetComprehension)expr;
         int prevErrorCount = reporter.Count(ErrorLevel.Error);
@@ -7763,22 +8013,14 @@ namespace Microsoft.Dafny
         }
         ResolveExpression(e.Range, opts);
         Contract.Assert(e.Range.Type != null);  // follows from postcondition of ResolveExpression
-        if (!UnifyTypes(e.Range.Type, Type.Bool)) {
-          reporter.Error(MessageSource.Resolver, expr, "range of comprehension must be of type bool (instead got {0})", e.Range.Type);
-        }
+        ConstrainTypes(e.Range.Type, Type.Bool, expr, "range of comprehension must be of type bool (instead got {0})", e.Range.Type);
         ResolveExpression(e.Term, opts);
         Contract.Assert(e.Term.Type != null);  // follows from postcondition of ResolveExpression
 
-        ResolveAttributes(e.Attributes, new ResolveOpts(opts, true));
+        ResolveAttributes(e.Attributes, opts);
         scope.PopMarker();
         expr.Type = new SetType(e.Finite, e.Term.Type);
 
-        if (opts.DontCareAboutCompilation && (e.Term.Type.IsRefType || e.Term.Type.IsBoolType) || e.Term.Type.IsCharType) {
-          // ok, term type is finite and we're in a ghost context
-        } else {
-          needFiniteBoundsChecks_SetComprehension.Add(e);
-        }
-
       } else if (expr is MapComprehension) {
         var e = (MapComprehension)expr;
         int prevErrorCount = reporter.Count(ErrorLevel.Error);
@@ -7792,29 +8034,14 @@ namespace Microsoft.Dafny
         }
         ResolveExpression(e.Range, opts);
         Contract.Assert(e.Range.Type != null);  // follows from postcondition of ResolveExpression
-        if (!UnifyTypes(e.Range.Type, Type.Bool)) {
-          reporter.Error(MessageSource.Resolver, expr, "range of comprehension must be of type bool (instead got {0})", e.Range.Type);
-        }
+        ConstrainTypes(e.Range.Type, Type.Bool, expr, "range of comprehension must be of type bool (instead got {0})", e.Range.Type);
         ResolveExpression(e.Term, opts);
         Contract.Assert(e.Term.Type != null);  // follows from postcondition of ResolveExpression
 
-        ResolveAttributes(e.Attributes, new ResolveOpts(opts, true));
+        ResolveAttributes(e.Attributes, opts);
         scope.PopMarker();
         expr.Type = new MapType(e.Finite, e.BoundVars[0].Type, e.Term.Type);
 
-        if (prevErrorCount == reporter.Count(ErrorLevel.Error)) {
-          CheckTypeInference(e.Range);  // we need to resolve operators before the call to DiscoverBounds
-          List<BoundVar> missingBounds;
-          e.Bounds = DiscoverBestBounds_MultipleVars(e.BoundVars, e.Range, true, true, out missingBounds);
-          if (missingBounds.Count != 0) {
-            e.MissingBounds = missingBounds;
-            if (e.Finite) {
-              foreach (var bv in e.MissingBounds) {
-                reporter.Error(MessageSource.Resolver, expr, "a map comprehension must produce a finite domain, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
-              }
-            }
-          }
-        }
       } else if (expr is LambdaExpr) {
         var e = (LambdaExpr)expr;
         int prevErrorCount = reporter.Count(ErrorLevel.Error);
@@ -7827,13 +8054,11 @@ namespace Microsoft.Dafny
         if (e.Range != null) {
           ResolveExpression(e.Range, opts);
           Contract.Assert(e.Range.Type != null);  // follows from postcondition of ResolveExpression
-          if (!UnifyTypes(e.Range.Type, Type.Bool)) {
-            reporter.Error(MessageSource.Resolver, expr, "Precondition must be boolean (got {0})", e.Range.Type);
-          }
+          ConstrainTypes(e.Range.Type, Type.Bool, expr, "Precondition must be boolean (got {0})", e.Range.Type);
         }
 
         foreach (var read in e.Reads) {
-          ResolveFrameExpression(read, true, false, opts.codeContext);
+          ResolveFrameExpression(read, true, opts.codeContext);
         }
 
         ResolveExpression(e.Term, opts);
@@ -7845,7 +8070,7 @@ namespace Microsoft.Dafny
       } else if (expr is StmtExpr) {
         var e = (StmtExpr)expr;
         int prevErrorCount = reporter.Count(ErrorLevel.Error);
-        ResolveStatement(e.S, true, opts.codeContext);
+        ResolveStatement(e.S, opts.codeContext);
         if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
           var r = e.S as UpdateStmt;
           if (r != null && r.ResolvedStatements.Count == 1) {
@@ -7867,13 +8092,9 @@ namespace Microsoft.Dafny
         Contract.Assert(e.Thn.Type != null);  // follows from postcondition of ResolveExpression
         ResolveExpression(e.Els, opts);
         Contract.Assert(e.Els.Type != null);  // follows from postcondition of ResolveExpression
-        if (!UnifyTypes(e.Test.Type, Type.Bool)) {
-          reporter.Error(MessageSource.Resolver, expr, "guard condition in if-then-else expression must be a boolean (instead got {0})", e.Test.Type);
-        }
-        if (UnifyTypes(e.Thn.Type, e.Els.Type)) {
+        ConstrainTypes(e.Test.Type, Type.Bool, expr, "guard condition in if-then-else expression must be a boolean (instead got {0})", e.Test.Type);
+        if (ConstrainTypes(e.Thn.Type, e.Els.Type, expr, "the two branches of an if-then-else expression must have the same type (got {0} and {1})", e.Thn.Type, e.Els.Type)) {
           expr.Type = e.Thn.Type;
-        } else {
-          reporter.Error(MessageSource.Resolver, expr, "the two branches of an if-then-else expression must have the same type (got {0} and {1})", e.Thn.Type, e.Els.Type);
         }
 
       } else if (expr is MatchExpr) {
@@ -7955,16 +8176,15 @@ namespace Microsoft.Dafny
             if (ctor != null && i < ctor.Formals.Count) {
               Formal formal = ctor.Formals[i];
               Type st = SubstType(formal.Type, subst);
-              if (!UnifyTypes(v.Type, st)) {
-                reporter.Error(MessageSource.Resolver, expr, "the declared type of the formal ({0}) does not agree with the corresponding type in the constructor's signature ({1})", v.Type, st);
-              }
+              ConstrainTypes(v.Type, st,
+                expr, "the declared type of the formal ({0}) does not agree with the corresponding type in the constructor's signature ({1})", v.Type, st);
               v.IsGhost = formal.IsGhost;
 
               // update the type of the boundvars in the MatchCaseToken
               if (v.tok is MatchCaseToken) {
                 MatchCaseToken mt = (MatchCaseToken)v.tok;
                 foreach (Tuple<IToken, BoundVar, bool> entry in mt.varList) {
-                  UnifyTypes(entry.Item2.Type, v.Type);
+                  UnifyTypes(entry.Item2.Type, v.Type);  // TODO: What to do if this unification fails? Or can it?  --KRML
                 }
               }
             }
@@ -7982,9 +8202,7 @@ namespace Microsoft.Dafny
         }
 
         Contract.Assert(mc.Body.Type != null);  // follows from postcondition of ResolveExpression
-        if (!UnifyTypes(expr.Type, mc.Body.Type)) {
-          reporter.Error(MessageSource.Resolver, mc.Body.tok, "type of case bodies do not agree (found {0}, previous types {1})", mc.Body.Type, expr.Type);
-        }
+        ConstrainTypes(expr.Type, mc.Body.Type, mc.Body.tok, "type of case bodies do not agree (found {0}, previous types {1})", mc.Body.Type, expr.Type);
         scope.PopMarker();
       }
       if (dtd != null && memberNamesUsed.Count != dtd.Ctors.Count) {
@@ -8318,9 +8536,7 @@ namespace Microsoft.Dafny
         // this is a simple resolution
         var v = pat.Var;
         ResolveType(v.tok, v.Type, context, ResolveTypeOptionEnum.InferTypeProxies, null);
-        if (!UnifyTypes(v.Type, sourceType)) {
-          reporter.Error(MessageSource.Resolver, v.tok, "type of corresponding source/RHS ({0}) does not match type of bound variable ({1})", sourceType, v.Type);
-        }
+        ConstrainTypes(v.Type, sourceType, v.tok, "type of corresponding source/RHS ({0}) does not match type of bound variable ({1})", sourceType, v.Type);
         pat.AssembleExpr(null);
       } else if (dtd == null) {
         reporter.Error(MessageSource.Resolver, pat.tok, "to use a pattern, the type of the source/RHS expression must be a datatype (instead found {0})", sourceType);
@@ -9038,9 +9254,8 @@ namespace Microsoft.Dafny
             reporter.Error(MessageSource.Resolver, e.tok, "wrong number of arguments to function application ({0} expects {1}, got {2})", what, fnType.Arity, e.Args.Count);
           } else {
             for (var i = 0; i < fnType.Arity; i++) {
-              if (!UnifyTypes(fnType.Args[i], e.Args[i].Type)) {
-                reporter.Error(MessageSource.Resolver, e.Args[i].tok, "type mismatch for argument {0} (function expects {1}, got {2})", i, fnType.Args[i], e.Args[i].Type);
-              }
+              ConstrainTypes(fnType.Args[i], e.Args[i].Type,
+                e.Args[i].tok, "type mismatch for argument {0} (function expects {1}, got {2})", i, fnType.Args[i], e.Args[i].Type);
             }
             if (errorCount != reporter.Count(ErrorLevel.Error)) {
               // do nothing else; error has been reported
@@ -9066,9 +9281,7 @@ namespace Microsoft.Dafny
                 ResolveExpression(farg, opts);
                 Contract.Assert(farg.Type != null);  // follows from postcondition of ResolveExpression
                 Type s = SubstType(callee.Formals[i].Type, rr.TypeArgumentSubstitutions);
-                if (!UnifyTypes(farg.Type, s)) {
-                  reporter.Error(MessageSource.Resolver, rr, "incorrect type of function argument {0} (expected {1}, got {2})", i, s, farg.Type);
-                }
+                ConstrainTypes(farg.Type, s, rr, "incorrect type of function argument {0} (expected {1}, got {2})", i, s, farg.Type);
               }
               rr.Type = SubstType(callee.ResultType, rr.TypeArgumentSubstitutions);
               // further bookkeeping
@@ -9124,9 +9337,7 @@ namespace Microsoft.Dafny
         Contract.Assert(arg.Type != null);  // follows from postcondition of ResolveExpression
         if (formal != null) {
           Type st = SubstType(formal.Type, subst);
-          if (!UnifyTypes(arg.Type, st)) {
-            reporter.Error(MessageSource.Resolver, arg.tok, "incorrect type of datatype constructor argument (found {0}, expected {1})", arg.Type, st);
-          }
+          ConstrainTypes(arg.Type, st, arg.tok, "incorrect type of datatype constructor argument (found {0}, expected {1})", arg.Type, st);
         }
         j++;
       }
@@ -9162,7 +9373,7 @@ namespace Microsoft.Dafny
     /// Generate an error for every non-ghost feature used in "expr".
     /// Requires "expr" to have been successfully resolved.
     /// </summary>
-    void CheckIsNonGhost(Expression expr) {
+    void CheckIsCompilable(Expression expr) {
       Contract.Requires(expr != null);
       Contract.Requires(expr.WasResolved());  // this check approximates the requirement that "expr" be resolved
 
@@ -9188,10 +9399,10 @@ namespace Microsoft.Dafny
             return;
           }
           // function is okay, so check all NON-ghost arguments
-          CheckIsNonGhost(e.Receiver);
+          CheckIsCompilable(e.Receiver);
           for (int i = 0; i < e.Function.Formals.Count; i++) {
             if (!e.Function.Formals[i].IsGhost) {
-              CheckIsNonGhost(e.Args[i]);
+              CheckIsCompilable(e.Args[i]);
             }
           }
         }
@@ -9203,7 +9414,7 @@ namespace Microsoft.Dafny
         // note that if resolution is successful, then |e.Arguments| == |e.Ctor.Formals|
         for (int i = 0; i < e.Arguments.Count; i++) {
           if (!e.Ctor.Formals[i].IsGhost) {
-            CheckIsNonGhost(e.Arguments[i]);
+            CheckIsCompilable(e.Arguments[i]);
           }
         }
         return;
@@ -9222,7 +9433,7 @@ namespace Microsoft.Dafny
       } else if (expr is StmtExpr) {
         var e = (StmtExpr)expr;
         // ignore the statement
-        CheckIsNonGhost(e.E);
+        CheckIsCompilable(e.E);
         return;
 
       } else if (expr is BinaryExpr) {
@@ -9253,29 +9464,59 @@ namespace Microsoft.Dafny
           var i = 0;
           foreach (var ee in e.RHSs) {
             if (!e.LHSs[i].Vars.All(bv => bv.IsGhost)) {
-              CheckIsNonGhost(ee);
+              CheckIsCompilable(ee);
             }
             i++;
           }
-          CheckIsNonGhost(e.Body);
+          CheckIsCompilable(e.Body);
         } else {
           Contract.Assert(e.RHSs.Count == 1);
           var lhsVarsAreAllGhost = e.BoundVars.All(bv => bv.IsGhost);
           if (!lhsVarsAreAllGhost) {
-            CheckIsNonGhost(e.RHSs[0]);
+            CheckIsCompilable(e.RHSs[0]);
+          }
+          CheckIsCompilable(e.Body);
+
+          // fill in bounds for this to-be-compiled let-such-that expression
+          Contract.Assert(e.RHSs.Count == 1);  // if we got this far, the resolver will have checked this condition successfully
+          var constraint = e.RHSs[0];
+          List<IVariable> missingBounds;
+          var vars = new List<IVariable>(e.BoundVars);
+          var bestBounds = DiscoverBestBounds_MultipleVars(vars, constraint, true, false, out missingBounds);
+          if (missingBounds.Count != 0) {
+            e.Constraint_MissingBounds = missingBounds;
+            foreach (var bv in e.Constraint_MissingBounds) {
+              reporter.Error(MessageSource.Resolver, e, "a non-ghost let-such-that constraint must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
+            }
+          } else {
+            e.Constraint_Bounds = bestBounds;
           }
-          CheckIsNonGhost(e.Body);
         }
         return;
-      } else if (expr is QuantifierExpr) {
-        var e = (QuantifierExpr)expr;
-        Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution
-        if (e.MissingBounds != null) {
-          foreach (var bv in e.MissingBounds) {
-            reporter.Error(MessageSource.Resolver, expr, "quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
+      } else if (expr is LambdaExpr) {
+        var e = expr as LambdaExpr;
+        CheckIsCompilable(e.Body);
+        return;
+      } else if (expr is ComprehensionExpr) {
+        var e = (ComprehensionExpr)expr;
+        var uncompilableBoundVars = e.UncompilableBoundVars();
+        if (uncompilableBoundVars.Count != 0) {
+          string what;
+          if (e is SetComprehension) {
+            what = "set comprehensions";
+          } else if (e is MapComprehension) {
+            what = "map comprehensions";
+          } else {
+            Contract.Assume(e is QuantifierExpr);  // otherwise, unexpected ComprehensionExpr (since LambdaExpr is handled separately above)
+            Contract.Assert(((QuantifierExpr)e).SplitQuantifier == null); // No split quantifiers during resolution
+            what = "quantifiers";
+          }
+          foreach (var bv in uncompilableBoundVars) {
+            reporter.Error(MessageSource.Resolver, expr, "{0} in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for '{1}'", what, bv.Name);
           }
           return;
         }
+
       } else if (expr is MapComprehension) {
         var e = (MapComprehension)expr;
         if (e.MissingBounds != null && !e.Finite) {
@@ -9285,23 +9526,19 @@ namespace Microsoft.Dafny
           return;
         }
       } else if (expr is NamedExpr) {
-        if (!moduleInfo.IsGhost)
-          CheckIsNonGhost(((NamedExpr)expr).Body);
+        if (!moduleInfo.IsAbstract)
+          CheckIsCompilable(((NamedExpr)expr).Body);
         return;
       } else if (expr is ChainingExpression) {
         // We don't care about the different operators; we only want the operands, so let's get them directly from
         // the chaining expression
         var e = (ChainingExpression)expr;
-        e.Operands.ForEach(CheckIsNonGhost);
-        return;
-      } else if (expr is LambdaExpr) {
-        var e = expr as LambdaExpr;
-        CheckIsNonGhost(e.Body);
+        e.Operands.ForEach(CheckIsCompilable);
         return;
       }
 
       foreach (var ee in expr.SubExpressions) {
-        CheckIsNonGhost(ee);
+        CheckIsCompilable(ee);
       }
     }
 
@@ -9361,9 +9598,7 @@ namespace Microsoft.Dafny
             ResolveExpression(farg, opts);
             Contract.Assert(farg.Type != null);  // follows from postcondition of ResolveExpression
             Type s = SubstType(function.Formals[i].Type, e.TypeArgumentSubstitutions);
-            if (!UnifyTypes(farg.Type, s)) {
-              reporter.Error(MessageSource.Resolver, e, "incorrect type of function argument {0} (expected {1}, got {2})", i, s, farg.Type);
-            }
+            ConstrainTypes(farg.Type, s, e, "incorrect type of function argument {0} (expected {1}, got {2})", i, s, farg.Type);
           }
           e.Type = SubstType(function.ResultType, e.TypeArgumentSubstitutions);
         }
@@ -9416,7 +9651,7 @@ namespace Microsoft.Dafny
     /// </summary>
     public static List<ComprehensionExpr.BoundedPool> DiscoverBestBounds_MultipleVars<VT>(List<VT> bvars, Expression expr, bool polarity, bool onlyFiniteBounds, out List<VT> missingBounds) where VT : IVariable {
       foreach (var bv in bvars) {
-        var c = TypeConstraint(bv, bv.Type, null);
+        var c = GetImpliedTypeConstraint(bv, bv.Type, null);
         expr = polarity ? Expression.CreateAnd(c, expr) : Expression.CreateImplies(c, expr);
       }
       var all = DiscoverAllBounds_Aux_MultipleVars(bvars, expr, polarity);
@@ -9431,7 +9666,7 @@ namespace Microsoft.Dafny
     }
 
     public static List<ComprehensionExpr.BoundedPool> DiscoverAllBounds_SingleVar<VT>(VT v, Expression expr) where VT : IVariable {
-      expr = Expression.CreateAnd(TypeConstraint(v, v.Type, null), expr);
+      expr = Expression.CreateAnd(GetImpliedTypeConstraint(v, v.Type, null), expr);
       return DiscoverAllBounds_Aux_SingleVar(new List<VT> { v }, 0, expr, true);
     }
 
@@ -9458,8 +9693,11 @@ namespace Microsoft.Dafny
 
       // Maybe the type itself gives a bound
       if (bv.Type.IsBoolType) {
-        // easy
         bounds.Add(new ComprehensionExpr.BoolBoundedPool());
+      } else if (bv.Type.IsCharType) {
+        bounds.Add(new ComprehensionExpr.CharBoundedPool());
+      } else if (bv.Type.IsRefType) {
+        bounds.Add(new ComprehensionExpr.RefBoundedPool(bv.Type));
       } else if (bv.Type.IsIndDatatype && bv.Type.AsIndDatatype.HasFinitePossibleValues) {
         bounds.Add(new ComprehensionExpr.DatatypeBoundedPool(bv.Type.AsIndDatatype));
       } else if (bv.Type.IsNumericBased(Type.NumericPersuation.Int)) {
@@ -9545,13 +9783,13 @@ namespace Microsoft.Dafny
       return bounds;
     }
 
-    static Expression TypeConstraint(IVariable bv, Type ty, ErrorReporter reporter) {
+    static Expression GetImpliedTypeConstraint(IVariable bv, Type ty, ErrorReporter reporter) {
       Contract.Requires(bv != null);
       Contract.Requires(ty != null);
       ty = ty.NormalizeExpand();
       var dd = ty.AsNewtype;
       if (dd != null) {
-        var c = TypeConstraint(bv, dd.BaseType, reporter);
+        var c = GetImpliedTypeConstraint(bv, dd.BaseType, reporter);
         if (dd.Var != null) {
           c = Expression.CreateAnd(c, new Translator(reporter).Substitute(dd.Constraint, dd.Var, Expression.CreateIdentExpr(bv)));
         }
@@ -9898,17 +10136,14 @@ namespace Microsoft.Dafny
       Type argType = new InferredTypeProxy();
 
       IndexableTypeProxy expectedType = new IndexableTypeProxy(domainType, elementType, argType, true, true, true);
-      if (!UnifyTypes(e.Seq.Type, expectedType)) {
-        reporter.Error(MessageSource.Resolver, e, "sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got {0})", e.Seq.Type);
+      if (!ConstrainTypes(e.Seq.Type, expectedType, e, "sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got {0})", e.Seq.Type)) {
         seqErr = true;
       }
       if (!e.SelectOne)  // require sequence or array
       {
         if (!allowNonUnitArraySelection) {
           // require seq
-          if (!UnifyTypes(expectedType, new SeqType(new InferredTypeProxy()))) {
-            reporter.Error(MessageSource.Resolver, e, "selection requires a sequence (got {0})", e.Seq.Type);
-          }
+          ConstrainTypes(expectedType, new SeqType(new InferredTypeProxy()), e, "selection requires a sequence (got {0})", e.Seq.Type);
         } else {
           if (UnifyTypes(expectedType, new MapType(true, new InferredTypeProxy(), new InferredTypeProxy()))) {
             reporter.Error(MessageSource.Resolver, e, "cannot multiselect a map (got {0} as map type)", e.Seq.Type);
@@ -9920,17 +10155,13 @@ namespace Microsoft.Dafny
       if (e.E0 != null) {
         ResolveExpression(e.E0, opts);
         Contract.Assert(e.E0.Type != null);  // follows from postcondition of ResolveExpression
-        if (!UnifyTypes(e.E0.Type, domainType)) {
-          reporter.Error(MessageSource.Resolver, e.E0, "sequence/array/multiset/map selection requires {1} indices (got {0})", e.E0.Type, domainType);
-        }
+        ConstrainTypes(e.E0.Type, domainType, e.E0, "sequence/array/multiset/map selection requires {1} indices (got {0})", e.E0.Type, domainType);
       }
       if (e.E1 != null) {
         ResolveExpression(e.E1, opts);
         Contract.Assert(e.E1.Type != null);  // follows from postcondition of ResolveExpression
         var domType = e.E0 == null ? domainType : new OperationTypeProxy(true, false, false, false, false, false);  // reuse 'domainType' if .E0 did not use it; otherwise, create a new proxy to allow .E1 to be any integer-based numeric type, independent of the integer-based numeric type used by .E0
-        if (!UnifyTypes(e.E1.Type, domType)) {
-          reporter.Error(MessageSource.Resolver, e.E1, "sequence/array/multiset/map selection requires {1} indices (got {0})", e.E1.Type, domType);
-        }
+        ConstrainTypes(e.E1.Type, domType, e.E1, "sequence/array/multiset/map selection requires {1} indices (got {0})", e.E1.Type, domType);
       }
       if (!seqErr) {
         if (e.SelectOne) {
@@ -10106,8 +10337,15 @@ namespace Microsoft.Dafny
         IdentifierExpr e = (IdentifierExpr)expr;
         return cce.NonNull(e.Var).IsGhost;
       } else if (expr is DatatypeValue) {
-        DatatypeValue dtv = (DatatypeValue)expr;
-        return dtv.Arguments.Exists(arg => UsesSpecFeatures(arg));
+        var e = (DatatypeValue)expr;
+        // check all NON-ghost arguments
+        // note that if resolution is successful, then |e.Arguments| == |e.Ctor.Formals|
+        for (int i = 0; i < e.Arguments.Count; i++) {
+          if (!e.Ctor.Formals[i].IsGhost && UsesSpecFeatures(e.Arguments[i])) {
+            return true;
+          }
+        }
+        return false;
       } else if (expr is DisplayExpression) {
         DisplayExpression e = (DisplayExpression)expr;
         return e.Elements.Exists(ee => UsesSpecFeatures(ee));
@@ -10135,11 +10373,20 @@ namespace Microsoft.Dafny
                UsesSpecFeatures(e.Index) ||
                UsesSpecFeatures(e.Value);
       } else if (expr is FunctionCallExpr) {
-        FunctionCallExpr e = (FunctionCallExpr)expr;
-        if (cce.NonNull(e.Function).IsGhost) {
+        var e = (FunctionCallExpr)expr;
+        if (e.Function.IsGhost) {
           return true;
         }
-        return e.Args.Exists(arg => UsesSpecFeatures(arg));
+        // check all NON-ghost arguments
+        if (UsesSpecFeatures(e.Receiver)) {
+          return true;
+        }
+        for (int i = 0; i < e.Function.Formals.Count; i++) {
+          if (!e.Function.Formals[i].IsGhost && UsesSpecFeatures(e.Args[i])) {
+            return true;
+          }
+        }
+        return false;
       } else if (expr is ApplyExpr) {
         ApplyExpr e = (ApplyExpr)expr;
         return UsesSpecFeatures(e.Function) || e.Args.Exists(UsesSpecFeatures);
@@ -10180,22 +10427,20 @@ namespace Microsoft.Dafny
           return true;  // let-such-that is always ghost
         }
       } else if (expr is NamedExpr) {
-        return moduleInfo.IsGhost ? false : UsesSpecFeatures(((NamedExpr)expr).Body);
-      } else if (expr is ComprehensionExpr) {
-        var q = expr as QuantifierExpr;
-        Contract.Assert(q == null || q.SplitQuantifier == null); // No split quantifiers during resolution
-        if (q != null && q.Bounds.Contains(null)) {
-          return true;  // the quantifier cannot be compiled if the resolver found no bounds
-        }
-        return Contract.Exists(expr.SubExpressions, se => UsesSpecFeatures(se));
+        return moduleInfo.IsAbstract ? false : UsesSpecFeatures(((NamedExpr)expr).Body);
+      } else if (expr is QuantifierExpr) {
+        var e = (QuantifierExpr)expr;
+        Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution
+        return e.UncompilableBoundVars().Count != 0;
       } else if (expr is SetComprehension) {
         var e = (SetComprehension)expr;
-        return (e.Range != null && UsesSpecFeatures(e.Range)) || (e.Term != null && UsesSpecFeatures(e.Term));
+        return !e.Finite || e.UncompilableBoundVars().Count != 0 || (e.Range != null && UsesSpecFeatures(e.Range)) || (e.Term != null && UsesSpecFeatures(e.Term));
       } else if (expr is MapComprehension) {
         var e = (MapComprehension)expr;
-        return (UsesSpecFeatures(e.Range)) || (UsesSpecFeatures(e.Term));
+        return !e.Finite || e.UncompilableBoundVars().Count != 0 || UsesSpecFeatures(e.Range) || UsesSpecFeatures(e.Term);
       } else if (expr is LambdaExpr) {
-        return Contract.Exists(expr.SubExpressions, UsesSpecFeatures);
+        var e = (LambdaExpr)expr;
+        return UsesSpecFeatures(e.Term);
       } else if (expr is WildcardExpr) {
         return false;
       } else if (expr is StmtExpr) {