Refactored ArrowType's to be resolved with other types. ArrowTypeDecl's are now created by the parser into the system module.

12 files changed, 232 insertions, 176 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 9f13abf6..615ef596 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -172,7 +172,7 @@ namespace Microsoft.Dafny
         return new MapType(CloneType(tt.Domain), CloneType(tt.Range));

       } else if (t is ArrowType) {

         var tt = (ArrowType)t;

-        return new ArrowType(tt.Args.ConvertAll(CloneType), CloneType(tt.Result));

+        return new ArrowType(Tok(tt.tok), tt.Args.ConvertAll(CloneType), CloneType(tt.Result));

       } else if (t is UserDefinedType) {

         var tt = (UserDefinedType)t;

 #if TEST_TYPE_SYNONYM_TRANSPARENCY

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index af9cce11..59fa503e 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -984,18 +984,8 @@ namespace Microsoft.Dafny {
         }

         return name + "]";

       } else if (type is UserDefinedType) {

-        UserDefinedType udt = (UserDefinedType)type;

-        string s = "@" + udt.FullCompileName;

-        if (type is ArrowType) {

-          s = "Func";

-        }

-        if (udt.TypeArgs.Count != 0) {

-          if (udt.TypeArgs.Exists(argType => argType is ObjectType)) {

-            Error("compilation does not support type 'object' as a type parameter; consider introducing a ghost");

-          }

-          s += "<" + TypeNames(udt.TypeArgs) + ">";

-        }

-        return s;

+        var udt = (UserDefinedType)type;

+        return TypeName_UDT(udt.FullCompileName, udt.TypeArgs);

       } else if (type is SetType) {

         Type argType = ((SetType)type).Arg;

         if (argType is ObjectType) {

@@ -1026,6 +1016,19 @@ namespace Microsoft.Dafny {
       }

     }

 

+    string TypeName_UDT(string fullCompileName, List<Type> typeArgs) {

+      Contract.Requires(fullCompileName != null);

+      Contract.Requires(typeArgs != null);

+      string s = "@" + fullCompileName;

+      if (typeArgs.Count != 0) {

+        if (typeArgs.Exists(argType => argType is ObjectType)) {

+          Error("compilation does not support type 'object' as a type parameter; consider introducing a ghost");

+        }

+        s += "<" + TypeNames(typeArgs) + ">";

+      }

+      return s;

+    }

+

     string/*!*/ TypeNames(List<Type/*!*/>/*!*/ types) {

       Contract.Requires(cce.NonNullElements(types));

       Contract.Ensures(Contract.Result<string>() != null);

@@ -2882,7 +2885,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(exprs != null);

       Contract.Requires(bvars.Count == exprs.Count);

       wr.Write("Dafny.Helpers.Id<");

-      wr.Write(TypeName(new ArrowType(bvars.ConvertAll(bv => bv.Type), bodyType)));

+      wr.Write(TypeName_UDT(ArrowType.Arrow_FullCompileName, Util.Snoc(bvars.ConvertAll(bv => bv.Type), bodyType)));

       wr.Write(">((");

       wr.Write(Util.Comma(bvars, bv => "@" + bv.CompileName));

       wr.Write(") => ");

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index bb995c8d..2d3d93d6 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -890,11 +890,13 @@ TypeAndToken<out IToken tok, out Type ty>
     | ReferenceType<out tok, out ty>

   )

   [ (. Type t2; .)

-    "->" Type<out t2>

+    "->"                  (. tok = t; .)

+    Type<out t2>

     (. if (gt == null) {

          gt = new List<Type>{ ty };

        }

-       ty = new ArrowType(gt, t2);

+       ty = new ArrowType(tok, gt, t2);

+       theBuiltIns.CreateArrowTypeDecl(gt.Count);

     .)

   ]

 

@@ -1019,6 +1021,11 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
      }

      f.BodyStartTok = bodyStart;

      f.BodyEndTok = bodyEnd;

+     theBuiltIns.CreateArrowTypeDecl(formals.Count);

+     if (isCoPredicate) {

+       // also create an arrow type for the corresponding prefix predicate

+       theBuiltIns.CreateArrowTypeDecl(formals.Count);

+     }

   .)

   .

 FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/> decreases.>

@@ -2081,6 +2088,7 @@ ParensExpression<out Expression e, bool allowSemi, bool allowLambda>
          }

        }

        e = new LambdaExpr(x, oneShot, bvs, req, reads, body);

+       theBuiltIns.CreateArrowTypeDecl(bvs.Count);

        isLambda = true;

     .)

   ]

@@ -2353,6 +2361,7 @@ DottedIdentifiersAndFunction<out Expression e, bool allowSemi, bool allowLambda>
        }

        BoundVar bv = new BoundVar(id, UnwildIdent(id.val, true),  new InferredTypeProxy());

        e = new LambdaExpr(id, oneShot, new List<BoundVar>{ bv }, req, reads, body);

+       theBuiltIns.CreateArrowTypeDecl(1);

     .)

   ]

   // If it wasn't a lambda expression, then it indeed is an identifier sequence

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 41bbeee4..faf79a30 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -87,16 +87,22 @@ namespace Microsoft.Dafny {
   public class BuiltIns

   {

     public readonly ModuleDefinition SystemModule = new ModuleDefinition(Token.NoToken, "_System", false, false, null, null, null, true);

-    Dictionary<int, ClassDecl> arrayTypeDecls = new Dictionary<int, ClassDecl>();

-    Dictionary<int, TupleTypeDecl> tupleTypeDecls = new Dictionary<int, TupleTypeDecl>();

+    readonly Dictionary<int, ClassDecl> arrayTypeDecls = new Dictionary<int, ClassDecl>();

+    readonly Dictionary<int, ArrowTypeDecl> arrowTypeDecls = new Dictionary<int, ArrowTypeDecl>();

+    readonly Dictionary<int, TupleTypeDecl> tupleTypeDecls = new Dictionary<int, TupleTypeDecl>();

+

     public readonly ClassDecl ObjectDecl;

     public BuiltIns() {

+      SystemModule.Height = -1;  // the system module doesn't get a height assigned later, so we set it here to something below everything else

       // create class 'object'

       ObjectDecl = new ClassDecl(Token.NoToken, "object", SystemModule, new List<TypeParameter>(), new List<MemberDecl>(), DontCompile(), null);

       SystemModule.TopLevelDecls.Add(ObjectDecl);

       // add one-dimensional arrays, since they may arise during type checking

       // Arrays of other dimensions may be added during parsing as the parser detects the need for these

       UserDefinedType tmp = ArrayType(1, Type.Int, true);

+      // Arrow types of other dimensions may be added during parsing as the parser detects the need for these.  For the 0-arity

+      // arrow type, the resolver adds a Valid() predicate for iterators, whose corresponding arrow type is conveniently created here.

+      CreateArrowTypeDecl(0);

       // Note, in addition to these types, the _System module contains tuple types.  These tuple types are added to SystemModule

       // by the parser as the parser detects the need for these.

     }

@@ -106,7 +112,7 @@ namespace Microsoft.Dafny {
       return new Attributes("compile", new List<Attributes.Argument>() { flse }, null);

     }

 

-    public UserDefinedType ArrayType(int dims, Type arg, bool allowCreationOfNewClass = false) {

+    public UserDefinedType ArrayType(int dims, Type arg, bool allowCreationOfNewClass) {

       Contract.Requires(1 <= dims);

       Contract.Requires(arg != null);

       return ArrayType(Token.NoToken, dims, new List<Type>() { arg }, allowCreationOfNewClass);

@@ -142,6 +148,46 @@ namespace Microsoft.Dafny {
       }

     }

 

+    /// <summary>

+    /// Idempotently add an arrow type with arity 'arity' to the system module.

+    /// </summary>

+    public void CreateArrowTypeDecl(int arity) {

+      Contract.Requires(0 <= arity);

+      if (!arrowTypeDecls.ContainsKey(arity)) {

+        IToken tok = Token.NoToken;

+        var tps = Util.Map(Enumerable.Range(0, arity + 1),

+          x => new TypeParameter(tok, "_Fn" + x));

+        var tys = tps.ConvertAll(tp => (Type)(new UserDefinedType(tp)));

+        var args = tys.GetRange(0, arity).ConvertAll(t => new Formal(tok, "x", t, true, false));

+        var argExprs = args.ConvertAll(a =>

+              (Expression)new IdentifierExpr(tok, a.Name) { Var = a, Type = a.Type });

+        var readsIS = new IdentifierSequence(new List<IToken> { tok }, tok, argExprs) {

+          Type = new SetType(new ObjectType()),

+        };

+        var readsFrame = new List<FrameExpression> { new FrameExpression(tok, readsIS, null) };

+        var req = new Function(tok, "requires", false, true,

+          new List<TypeParameter>(), tok, args, Type.Bool,

+          new List<Expression>(), readsFrame, new List<Expression>(),

+          new Specification<Expression>(new List<Expression>(), null),

+          null, new Attributes("axiom", new List<Attributes.Argument>(), null), null);

+        var reads = new Function(tok, "reads", false, true,

+          new List<TypeParameter>(), tok, args, new SetType(new ObjectType()),

+          new List<Expression>(), readsFrame, new List<Expression>(),

+          new Specification<Expression>(new List<Expression>(), null),

+          null, new Attributes("axiom", new List<Attributes.Argument>(), null), null);

+        var readsFexp =

+          new FunctionCallExpr(tok, "reads", new ThisExpr(tok), tok, argExprs) {

+            Function = reads,

+            Type = readsIS.Type,

+            TypeArgumentSubstitutions = Util.Dict(tps, tys)

+          };

+        readsIS.ResolvedExpression = readsFexp;

+        var arrowDecl = new ArrowTypeDecl(tps, req, reads, SystemModule);

+        arrowTypeDecls.Add(arity, arrowDecl);

+        SystemModule.TopLevelDecls.Add(arrowDecl);

+      }

+    }

+

     public TupleTypeDecl TupleType(IToken tok, int dims, bool allowCreationOfNewType) {

       Contract.Requires(tok != null);

       Contract.Requires(0 <= dims);

@@ -412,7 +458,7 @@ namespace Microsoft.Dafny {
         } else {

           var udt = t as UserDefinedType;

           return udt != null && udt.ResolvedParam == null && udt.ResolvedClass is ClassDecl

-            && !(udt.ResolvedClass is ArrowType.ArrowTypeDecl);

+            && !(udt.ResolvedClass is ArrowTypeDecl);

         }

       }

     }

@@ -428,6 +474,15 @@ namespace Microsoft.Dafny {
         return udt == null ? null : udt.ResolvedClass as ArrayClassDecl;

       }

     }

+    public bool IsArrowType {

+      get { return AsArrowType != null; }

+    }

+    public ArrowType AsArrowType {

+      get {

+        var t = NormalizeExpand();

+        return t as ArrowType;

+      }

+    }

     public NewtypeDecl AsNewtype {

       get {

         var udt = NormalizeExpand() as UserDefinedType;

@@ -610,9 +665,31 @@ namespace Microsoft.Dafny {
       get { return TypeArgs.Count - 1; }

     }

 

-    public ArrowType(List<Type> args, Type result) : 

-      base(Token.NoToken, ArrowType.ArrowTypeName(args.Count), Util.Snoc(args, result), null) {

-      ResolvedClass = GetArrowDecl(args.Count);

+    /// <summary>

+    /// Constructs a(n unresolved) arrow type.

+    /// </summary>

+    public ArrowType(IToken tok, List<Type> args, Type result)

+      :  base(tok, ArrowType.ArrowTypeName(args.Count), Util.Snoc(args, result), null) {

+      Contract.Requires(tok != null);

+      Contract.Requires(args != null);

+      Contract.Requires(result != null);

+    }

+    /// <summary>

+    /// Constructs and returns a resolved arrow type.

+    /// </summary>

+    public ArrowType(IToken tok, List<Type> args, Type result, ModuleDefinition systemModule)

+      : this(tok, args, result) {

+      Contract.Requires(tok != null);

+      Contract.Requires(args != null);

+      Contract.Requires(result != null);

+      Contract.Requires(systemModule != null);

+      ResolvedClass = systemModule.TopLevelDecls.Find(d => d.Name == Name);

+      Contract.Assume(ResolvedClass != null);

+    }

+

+    public const string Arrow_FullCompileName = "Func";  // this is the same for all arities

+    public override string FullCompileName {

+      get { return Arrow_FullCompileName; }

     }

 

     public static string ArrowTypeName(int arity) {

@@ -626,7 +703,7 @@ namespace Microsoft.Dafny {
 

     public override string TypeName(ModuleDefinition context) {

       string s = "", closeparen = "";

-      if (Args.Count != 1 || Args[0] is ArrowType) {

+      if (Args.Count != 1 || Args[0].Normalize() is ArrowType) {

         s += "("; closeparen = ")";

       }

       s += Util.Comma(Args, arg => arg.TypeName(context));

@@ -636,69 +713,6 @@ namespace Microsoft.Dafny {
       return s;

     }

    

-    private static ArrowTypeDecl GetArrowDecl(int arity) {

-      ArrowTypeDecl arrowDecl;

-      if (!arrowTypeDecls.TryGetValue(arity, out arrowDecl)) {

-        var tok = Token.NoToken;

-        var tps = Util.Map(Enumerable.Range(0, arity + 1),

-          x => new TypeParameter(tok, "_Fn" + x));

-        var tys = tps.ConvertAll(tp => (Type)(new UserDefinedType(tp)));

-        var args = tys.GetRange(0, arity).ConvertAll(t => new Formal(tok, "x", t, true, false));

-        var argExprs = args.ConvertAll(a => 

-              (Expression)new IdentifierExpr(tok, a.Name) { Var = a, Type = a.Type });

-        var readsIS = new IdentifierSequence(new List<IToken> { tok }, tok, argExprs) {

-          Type = new SetType(new ObjectType()),

-        };

-        var readsFrame = new List<FrameExpression> { new FrameExpression(tok, readsIS, null) };

-        var req = new Function(tok, "requires", false, true,

-          new List<TypeParameter>(), tok, args, Type.Bool,

-          new List<Expression>(), readsFrame, new List<Expression>(),

-          new Specification<Expression>(new List<Expression>(), null),

-          null, null, null); 

-        var reads = new Function(tok, "reads", false, true,

-          new List<TypeParameter>(), tok, args, new SetType(new ObjectType()),

-          new List<Expression>(), readsFrame, new List<Expression>(),

-          new Specification<Expression>(new List<Expression>(), null),

-          null, null, null);

-        var readsFexp =

-          new FunctionCallExpr(tok, "reads", new ThisExpr(tok), tok, argExprs) {

-            Function = reads,

-            Type = readsIS.Type,

-            TypeArgumentSubstitutions = Util.Dict(tps, tys) 

-          };

-        readsIS.ResolvedExpression = readsFexp;

-        arrowDecl = new ArrowTypeDecl(tps, req, reads);

-        arrowTypeDecls[arity] = arrowDecl;

-      }

-      return arrowDecl;

-    }

-

-    private readonly static Dictionary<int, ArrowTypeDecl> arrowTypeDecls = new Dictionary<int, ArrowTypeDecl>();

-    private static readonly ModuleDefinition FunctionModule = new ModuleDefinition(Token.NoToken, "_Fn", false, false, null, null, null, true) { Height = -1 };

-

-    public static IEnumerable<ArrowTypeDecl> ArrowTypeDecls {

-      get {

-        return ArrowType.arrowTypeDecls.Values;

-      }

-    }

-

-    public class ArrowTypeDecl : ClassDecl

-    {

-      public readonly int Arity;

-      public readonly Function Requires;

-      public readonly Function Reads;

-

-      public ArrowTypeDecl(List<TypeParameter> tps, Function req, Function reads) 

-        : base(Token.NoToken, "_Func" + (tps.Count-1), FunctionModule, tps, 

-               new List<MemberDecl>{ req, reads }, null, null) {

-        Arity = tps.Count-1;

-        Requires = req;

-        Reads = reads;

-        Requires.EnclosingClass = this;

-        Reads.EnclosingClass = this;

-      }

-    }

-

     public override bool SupportsEquality {

       get {

         return false;

@@ -848,7 +862,7 @@ namespace Microsoft.Dafny {
     }

 

     string compileName;

-    public string CompileName {

+    string CompileName {

       get {

         if (compileName == null) {

           compileName = NonglobalVariable.CompilerizeName(Name);

@@ -856,7 +870,7 @@ namespace Microsoft.Dafny {
         return compileName;

       }

     }

-    public string FullCompileName {

+    public virtual string FullCompileName {

       get {

         if (ResolvedClass != null && !ResolvedClass.Module.IsDefaultModule) {

           return ResolvedClass.Module.CompileName + ".@" + CompileName;

@@ -1722,6 +1736,27 @@ namespace Microsoft.Dafny {
     }

   }

 

+  public class ArrowTypeDecl : ClassDecl

+  {

+    public readonly int Arity;

+    public readonly Function Requires;

+    public readonly Function Reads;

+

+    public ArrowTypeDecl(List<TypeParameter> tps, Function req, Function reads, ModuleDefinition module)

+      : base(Token.NoToken, "_Func" + (tps.Count - 1), module, tps,

+             new List<MemberDecl> { req, reads }, null, null) {

+      Contract.Requires(tps != null && 1 <= tps.Count);

+      Contract.Requires(req != null);

+      Contract.Requires(reads != null);

+      Contract.Requires(module != null);

+      Arity = tps.Count - 1;

+      Requires = req;

+      Reads = reads;

+      Requires.EnclosingClass = this;

+      Reads.EnclosingClass = this;

+    }

+  }

+

   public abstract class DatatypeDecl : TopLevelDecl

   {

     public readonly List<DatatypeCtor> Ctors;

@@ -2625,7 +2660,8 @@ namespace Microsoft.Dafny {
 

     public Type Type {

       get {

-        return new ArrowType(Formals.ConvertAll(f => f.Type), ResultType);

+        // Note, the following returned type can contain type parameters from the function and its enclosing class

+        return new ArrowType(tok, Formals.ConvertAll(f => f.Type), ResultType);

       }

     }

 

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index a78d90a1..ae998732 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -986,6 +986,11 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		}

 		f.BodyStartTok = bodyStart;

 		f.BodyEndTok = bodyEnd;

+		theBuiltIns.CreateArrowTypeDecl(formals.Count);

+		if (isCoPredicate) {

+		 // also create an arrow type for the corresponding prefix predicate

+		 theBuiltIns.CreateArrowTypeDecl(formals.Count);

+		}

 		

 	}

 

@@ -1380,11 +1385,13 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		if (la.kind == 11) {

 			Type t2; 

 			Get();

+			tok = t; 

 			Type(out t2);

 			if (gt == null) {

 			 gt = new List<Type>{ ty };

 			}

-			ty = new ArrowType(gt, t2);

+			ty = new ArrowType(tok, gt, t2);

+			theBuiltIns.CreateArrowTypeDecl(gt.Count);

 			

 		}

 	}

@@ -3285,6 +3292,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			BoundVar bv = new BoundVar(id, UnwildIdent(id.val, true),  new InferredTypeProxy());

 			e = new LambdaExpr(id, oneShot, new List<BoundVar>{ bv }, req, reads, body);

+			theBuiltIns.CreateArrowTypeDecl(1);

 			

 		}

 		if (e == null) {

@@ -3693,6 +3701,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 }

 			}

 			e = new LambdaExpr(x, oneShot, bvs, req, reads, body);

+			theBuiltIns.CreateArrowTypeDecl(bvs.Count);

 			isLambda = true;

 			

 		}

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 48486698..d0e95248 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -471,7 +471,7 @@ namespace Microsoft.Dafny
     }

 

     public static Expression FrameArrowToObjectSet(Expression e, ref int tmpCounter) {

-      var arrTy = e.Type as ArrowType;

+      var arrTy = e.Type.AsArrowType;

       if (arrTy != null) {

         var bvars = new List<BoundVar>();

         var bexprs = new List<Expression>();

@@ -1175,7 +1175,7 @@ namespace Microsoft.Dafny
         return new MapType(CloneType(tt.Domain), CloneType(tt.Range));

       } else if (t is ArrowType) {

         var tt = (ArrowType)t;

-        return new ArrowType(tt.Args.ConvertAll(CloneType), CloneType(tt.Result));

+        return new ArrowType(tt.tok, tt.Args.ConvertAll(CloneType), CloneType(tt.Result));

       } else if (t is UserDefinedType) {

         var tt = (UserDefinedType)t;

         return new UserDefinedType(tt.tok, tt.Name, tt.TypeArgs.ConvertAll(CloneType), tt.Path.ConvertAll(x => x));

@@ -3523,7 +3523,7 @@ namespace Microsoft.Dafny
       ResolveExpression(fe.E, new ResolveOpts(codeContext, false, true /* yes, this is ghost */));

       Type t = fe.E.Type;

       Contract.Assert(t != null);  // follows from postcondition of ResolveExpression

-      var arrTy = t.NormalizeExpand() as ArrowType;

+      var arrTy = t.AsArrowType;

       if (arrTy != null) {

         t = arrTy.Result;

       }

@@ -4084,7 +4084,7 @@ namespace Microsoft.Dafny
       } else if (type is UserDefinedType) {

         var t = (UserDefinedType)type;

         var isArrow = t is ArrowType;

-        if (!isArrow && (t.ResolvedClass != null || t.ResolvedParam != null)) {

+        if (t.ResolvedClass != null || t.ResolvedParam != null) {

           // Apparently, this type has already been resolved

           return null;

         }

@@ -4094,10 +4094,6 @@ namespace Microsoft.Dafny
             Error(t.tok, "sorry, cannot instantiate type parameter with a subrange type");

           }

         }

-        if (isArrow) {

-          return null;

-          // Done already, all arrow types are resolved at construction time

-        }

         TypeParameter tp = t.Path.Count == 0 ? allTypeParameters.Find(t.Name) : null;

         if (tp != null) {

           if (t.TypeArgs.Count == 0) {

@@ -6162,9 +6158,14 @@ namespace Microsoft.Dafny
       if (ctype != null) {

         var cd = (ClassDecl)ctype.ResolvedClass;  // correctness of cast follows from postcondition of DenotesClass

         Contract.Assert(ctype.TypeArgs.Count == cd.TypeArgs.Count);  // follows from the fact that ctype was resolved

+#if TWO_SEARCHES

         MemberDecl member = cd.Members.Find(md => md.Name == memberName);

         if (member == null && 

           (!classMembers.ContainsKey(cd) || !classMembers[cd].TryGetValue(memberName, out member))) {

+#else

+        MemberDecl member;

+        if (!classMembers[cd].TryGetValue(memberName, out member)) {

+#endif

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

           if (memberName == "_ctor") {

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

@@ -6272,7 +6273,9 @@ namespace Microsoft.Dafny
         }

       } else if (type is ArrowType) {

         var t = (ArrowType)type;

-        return new ArrowType(t.Args.ConvertAll(u => SubstType(u, subst)), SubstType(t.Result, subst));

+        var at = new ArrowType(t.tok, t.Args.ConvertAll(u => SubstType(u, subst)), SubstType(t.Result, subst));

+        at.ResolvedClass = t.ResolvedClass;

+        return at;

       } else if (type is UserDefinedType) {

         var t = (UserDefinedType)type;

         if (t.ResolvedParam != null) {

@@ -6592,7 +6595,7 @@ namespace Microsoft.Dafny
             subst[tp] = prox; 

             e.TypeApplication.Add(prox);

           }

-          e.Type = SubstType(fn.Type, subst);

+          e.Type = new ArrowType(fn.tok, fn.Formals.ConvertAll(f => SubstType(f.Type, subst)), SubstType(fn.ResultType, subst), builtIns.SystemModule);

           AddCallGraphEdge(e, opts.codeContext, fn);

         } else if (member is Field) {

           var field = (Field)member;

@@ -6734,19 +6737,24 @@ namespace Microsoft.Dafny
         ResolveFunctionCallExpr(e, opts, false);

 

       } else if (expr is ApplyExpr) {

-        ApplyExpr e = (ApplyExpr)expr;

+        var e = (ApplyExpr)expr;

         ResolveExpression(e.Function, opts);

         foreach (var arg in e.Args) {

           ResolveExpression(arg, opts);

         }

-        Type tb = new InferredTypeProxy();

-        var targs = e.Args.ConvertAll(arg => arg.Type);

-        Type tc = new ArrowType(targs, tb);

-        if (!UnifyTypes(e.Function.Type, tc)) {

-          Error(e.OpenParen, "cannot apply arguments with types {0} to expression with type {1}", 

-            Util.Comma(targs, x => x.ToString()), e.Function.Type, ", ");

+        var fnType = e.Function.Type.AsArrowType;

+        if (fnType == null) {

+          Error(e.OpenParen, "apply expression requires a function (got {0})", e.Function.Type);

+        } else if (fnType.Arity != e.Args.Count) {

+          Error(e.OpenParen, "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)) {

+              Error(e.Args[i].tok, "type mismatch for argument {0} (function expects {1}, got {2})", i, fnType.Args[i], e.Args[i].Type);

+            }

+          }

         }

-        expr.Type = tb;

+        expr.Type = fnType == null ? new InferredTypeProxy() : fnType.Result;

 

       } else if (expr is OldExpr) {

         OldExpr e = (OldExpr)expr;

@@ -7228,7 +7236,7 @@ namespace Microsoft.Dafny
         ResolveExpression(e.Term, opts);

         Contract.Assert(e.Term.Type != null);

         scope.PopMarker();

-        expr.Type = new ArrowType(Util.Map(e.BoundVars, v => v.Type), e.Body.Type);

+        expr.Type = new ArrowType(e.tok, Util.Map(e.BoundVars, v => v.Type), e.Body.Type, builtIns.SystemModule);

       } else if (expr is WildcardExpr) {

         expr.Type = new SetType(new ObjectType());

       } else if (expr is StmtExpr) {

@@ -7677,7 +7685,7 @@ namespace Microsoft.Dafny
       }

       var field = member as Field;

       if (field != null) {

-        if (field.Type is ArrowType || field.Type.IsTypeParameter) {

+        if (field.Type.IsArrowType || field.Type.IsTypeParameter) {

           return new ApplyExpr(tok, openParen, new ExprDotName(tok, receiver, fn), args);

         } 

       }

@@ -8095,7 +8103,7 @@ namespace Microsoft.Dafny
         }

       } else if (e.Arguments != null) {

         Contract.Assert(p == e.Tokens.Count);

-        if (r.Type is ArrowType || r.Type.IsTypeParameter) {

+        if (r.Type.IsArrowType || r.Type.IsTypeParameter) {

           r = new ApplyExpr(e.tok, e.OpenParen, r, e.Arguments);

           ResolveExpression(r, opts);

         } else {

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 893b72fc..acfcaf22 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -373,12 +373,6 @@ namespace Microsoft.Dafny {
         return new Bpl.Program();

       }

 

-      foreach (var ad in ArrowType.ArrowTypeDecls) {

-        currentDeclaration = ad;

-        GetClassTyCon(ad);

-        AddArrowTypeAxioms(ad);

-      }

-

       foreach (TopLevelDecl d in program.BuiltIns.SystemModule.TopLevelDecls) {

         currentDeclaration = d;

         if (d is OpaqueTypeDecl) {

@@ -387,6 +381,10 @@ namespace Microsoft.Dafny {
           AddTypeDecl((NewtypeDecl)d);

         } else if (d is DatatypeDecl) {

           AddDatatype((DatatypeDecl)d);

+        } else if (d is ArrowTypeDecl) {

+          var ad = (ArrowTypeDecl)d;

+          GetClassTyCon(ad);

+          AddArrowTypeAxioms(ad);

         } else {

           AddClassMembers((ClassDecl)d);

         }

@@ -1718,7 +1716,7 @@ namespace Microsoft.Dafny {
       // TODO(namin) Is checking f.Reads.Count==0 excluding Valid() of BinaryTree in the right way?

       //             I don't see how this in the decreasing clause would help there.

       // danr: Let's create the literal function axioms if there is an arrow type in the signature

-      if (!(f is CoPredicate) && (f.Reads.Count == 0 || f.Formals.Exists(a => a.Type is ArrowType))) {

+      if (!(f is CoPredicate) && (f.Reads.Count == 0 || f.Formals.Exists(a => a.Type.IsArrowType))) {

         var FVs = new HashSet<IVariable>();

         bool usesHeap = false, usesOldHeap = false;

         Type usesThis = null;

@@ -4575,7 +4573,7 @@ namespace Microsoft.Dafny {
       } else if (expr is ApplyExpr) {

         var e = (ApplyExpr)expr;

         int arity = e.Args.Count;

-        var tt = e.Function.Type as ArrowType;

+        var tt = e.Function.Type.AsArrowType;

         Contract.Assert(tt != null);

         Contract.Assert(tt.Arity == arity);

 

@@ -4636,9 +4634,9 @@ namespace Microsoft.Dafny {
         Contract.Assert(e.Function != null);  // follows from the fact that expr has been successfully resolved

         // check well-formedness of receiver

         CheckWellformed(e.Receiver, options, locals, builder, etran);

-        if (!e.Function.IsStatic && !(e.Receiver is ThisExpr) && !(e.Receiver.Type is ArrowType)) {

+        if (!e.Function.IsStatic && !(e.Receiver is ThisExpr) && !e.Receiver.Type.IsArrowType) {

           CheckNonNull(expr.tok, e.Receiver, builder, etran, options.AssertKv);

-        } else if (e.Receiver.Type is ArrowType) {

+        } else if (e.Receiver.Type.IsArrowType) {

           CheckFunctionSelectWF("function specification", builder, etran, e.Receiver, "");

         }

         // check well-formedness of the other parameters

@@ -5228,7 +5226,7 @@ namespace Microsoft.Dafny {
           formals.Add(BplFormalVar(null, predef.LayerType, true));

         }

 

-        var enclosingArrow = f.EnclosingClass as ArrowType.ArrowTypeDecl;

+        var enclosingArrow = f.EnclosingClass as ArrowTypeDecl;

         var fromArrowType = enclosingArrow != null;

 

         Func<List<Bpl.Expr>, List<Bpl.Expr>> SnocSelf = x => x;

@@ -5331,7 +5329,8 @@ namespace Microsoft.Dafny {
       return FunctionCall(tk, name, Bpl.Type.Bool, bvars.ConvertAll(bv => (Bpl.Expr)new Bpl.IdentifierExpr(tk, bv)));

     }

 

-    private void AddArrowTypeAxioms(ArrowType.ArrowTypeDecl ad) {

+    private void AddArrowTypeAxioms(ArrowTypeDecl ad) {

+      Contract.Requires(ad != null);

       var arity = ad.Arity;

       var tok = ad.tok;

 

@@ -5576,7 +5575,7 @@ namespace Microsoft.Dafny {
     private string AddTyAxioms(TopLevelDecl td) {

       IToken tok = td.tok;

       var ty_repr =

-        td is ArrowType.ArrowTypeDecl ? predef.HandleType :

+        td is ArrowTypeDecl ? predef.HandleType :

         td is DatatypeDecl ? predef.DatatypeType :

         predef.RefType;

       var arity = td.TypeArgs.Count;

@@ -6549,7 +6548,7 @@ namespace Microsoft.Dafny {
         return false;

       }

       var res = t.IsTypeParameter;

-      Contract.Assert(t is ArrowType ? !res : true);

+      Contract.Assert(t.IsArrowType ? !res : true);

       return res;

     }

 

@@ -10331,7 +10330,7 @@ namespace Microsoft.Dafny {
         } else if (expr is ApplyExpr) {

           ApplyExpr e = (ApplyExpr)expr;

           int arity = e.Args.Count;

-          var tt = e.Function.Type as ArrowType;

+          var tt = e.Function.Type.AsArrowType;

           Contract.Assert(tt != null);

           Contract.Assert(tt.Arity == arity);

 

@@ -12819,9 +12818,9 @@ namespace Microsoft.Dafny {
 

         } else if (expr is ApplyExpr) {

           ApplyExpr e = (ApplyExpr)expr;

-          Expression receiver = Substitute(e.Function);

+          Expression fn = Substitute(e.Function);

           List<Expression> args = SubstituteExprList(e.Args);

-          newExpr = new ApplyExpr(e.tok, e.OpenParen, receiver, args);

+          newExpr = new ApplyExpr(e.tok, e.OpenParen, fn, args);

 

         } else if (expr is DatatypeValue) {

           DatatypeValue dtv = (DatatypeValue)expr;

diff --git a/Test/dafny0/Modules0.dfy.expect b/Test/dafny0/Modules0.dfy.expect
index 1a06d8f2..e50dc797 100644
--- a/Test/dafny0/Modules0.dfy.expect
+++ b/Test/dafny0/Modules0.dfy.expect
@@ -8,13 +8,10 @@ Modules0.dfy(56,21): Error: Undeclared top-level type or type parameter: MyClass
 Modules0.dfy(57,21): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)

 Modules0.dfy(68,21): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)

 Modules0.dfy(76,9): Error: type MyClass1 does not have a member Down

-Modules0.dfy(76,9): Error: type MyClass1 does not have a member Down

 Modules0.dfy(76,6): Error: expected method call, found expression

 Modules0.dfy(79,9): Error: type MyClass0 does not have a member Down

-Modules0.dfy(79,9): Error: type MyClass0 does not have a member Down

 Modules0.dfy(79,6): Error: expected method call, found expression

 Modules0.dfy(84,8): Error: type MyClassY does not have a member M

-Modules0.dfy(84,8): Error: type MyClassY does not have a member M

 Modules0.dfy(84,6): Error: expected method call, found expression

 Modules0.dfy(92,19): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?)

 Modules0.dfy(224,15): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)

@@ -22,24 +19,19 @@ Modules0.dfy(224,8): Error: new can be applied only to reference types (got X)
 Modules0.dfy(233,13): Error: Undeclared type X in module B

 Modules0.dfy(243,13): Error: unresolved identifier: X

 Modules0.dfy(244,15): Error: member DoesNotExist does not exist in class X

-Modules0.dfy(244,15): Error: member DoesNotExist does not exist in class X

 Modules0.dfy(283,19): Error: Undeclared top-level type or type parameter: D (did you forget to qualify a name?)

 Modules0.dfy(283,12): Error: new can be applied only to reference types (got D)

 Modules0.dfy(286,25): Error: type of the receiver is not fully determined at this program point

-Modules0.dfy(286,25): Error: type of the receiver is not fully determined at this program point

-Modules0.dfy(287,16): Error: type of the receiver is not fully determined at this program point

 Modules0.dfy(287,16): Error: type of the receiver is not fully determined at this program point

 Modules0.dfy(287,6): Error: expected method call, found expression

 Modules0.dfy(288,16): Error: type of the receiver is not fully determined at this program point

-Modules0.dfy(288,16): Error: type of the receiver is not fully determined at this program point

 Modules0.dfy(288,6): Error: expected method call, found expression

 Modules0.dfy(310,24): Error: module Q_Imp does not exist

 Modules0.dfy(102,6): Error: type MyClassY does not have a member M

-Modules0.dfy(102,6): Error: type MyClassY does not have a member M

 Modules0.dfy(102,4): Error: expected method call, found expression

 Modules0.dfy(127,11): Error: ghost variables are allowed only in specification contexts

 Modules0.dfy(141,11): Error: old expressions are allowed only in specification and ghost contexts

 Modules0.dfy(142,11): Error: fresh expressions are allowed only in specification and ghost contexts

 Modules0.dfy(143,11): Error: unresolved identifier: allocated

 Modules0.dfy(146,19): Error: unresolved identifier: allocated

-44 resolution/type errors detected in Modules0.dfy

+36 resolution/type errors detected in Modules0.dfy

diff --git a/Test/dafny0/Newtypes.dfy.expect b/Test/dafny0/Newtypes.dfy.expect
index 0161a713..2678e526 100644
--- a/Test/dafny0/Newtypes.dfy.expect
+++ b/Test/dafny0/Newtypes.dfy.expect
@@ -1,22 +1,22 @@
-DerivedTypes.dfy(74,11): Error: cannot find witness that shows type is inhabited (sorry, for now, only tried 0)

+Newtypes.dfy(74,11): Error: cannot find witness that shows type is inhabited (sorry, for now, only tried 0)

 Execution trace:

     (0,0): anon0

-DerivedTypes.dfy(76,45): Error: possible division by zero

+Newtypes.dfy(76,45): Error: possible division by zero

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-DerivedTypes.dfy(87,14): Error: result of operation might violate newtype constraint

+Newtypes.dfy(87,14): Error: result of operation might violate newtype constraint

 Execution trace:

     (0,0): anon0

-DerivedTypes.dfy(95,12): Error: result of operation might violate newtype constraint

+Newtypes.dfy(95,12): Error: result of operation might violate newtype constraint

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-DerivedTypes.dfy(97,14): Error: result of operation might violate newtype constraint

+Newtypes.dfy(97,14): Error: result of operation might violate newtype constraint

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

-DerivedTypes.dfy(104,16): Error: result of operation might violate newtype constraint

+Newtypes.dfy(104,16): Error: result of operation might violate newtype constraint

 Execution trace:

     (0,0): anon0

 

diff --git a/Test/dafny0/NewtypesResolution.dfy.expect b/Test/dafny0/NewtypesResolution.dfy.expect
index 091ca523..81c43d35 100644
--- a/Test/dafny0/NewtypesResolution.dfy.expect
+++ b/Test/dafny0/NewtypesResolution.dfy.expect
@@ -1,25 +1,25 @@
-DerivedTypesResolution.dfy(5,7): Error: Cycle among redirecting types (newtypes, type synonyms): MySynonym -> MyIntegerType_WellSupposedly -> MyNewType -> MySynonym

-DerivedTypesResolution.dfy(12,10): Error: newtypes must be based on some numeric type (got List<int>)

-DerivedTypesResolution.dfy(38,9): Error: arguments must have the same type (got posReal and real)

-DerivedTypesResolution.dfy(44,9): Error: arguments must have the same type (got int32 and int)

-DerivedTypesResolution.dfy(50,13): Error: arguments must have the same type (got posReal and int32)

-DerivedTypesResolution.dfy(51,13): Error: arguments to <= must have the same type (got posReal and int32)

-DerivedTypesResolution.dfy(52,13): Error: arguments to < must have the same type (got int32 and int)

-DerivedTypesResolution.dfy(53,13): Error: arguments to > must have the same type (got posReal and real)

-DerivedTypesResolution.dfy(57,13): Error: first argument to % must be of type int (instead got posReal)

-DerivedTypesResolution.dfy(57,25): Error: first argument to % must be of type int (instead got real)

-DerivedTypesResolution.dfy(75,8): Error: newtype constraint must be of type bool (instead got SmallInt)

-DerivedTypesResolution.dfy(77,10): Error: unresolved identifier: a

-DerivedTypesResolution.dfy(91,31): Error: old expressions are not allowed in this context

-DerivedTypesResolution.dfy(101,24): Error: Wrong number of type arguments (1 instead of 0) passed to newtype: N

-DerivedTypesResolution.dfy(105,10): Error: recursive dependency involving a newtype: _default.BadLemma -> Cycle

-DerivedTypesResolution.dfy(114,10): Error: recursive dependency involving a newtype: SelfCycle -> SelfCycle

-DerivedTypesResolution.dfy(120,21): Error: name of type ('N9') is used as a variable

-DerivedTypesResolution.dfy(139,6): Error: RHS (of type int) not assignable to LHS (of type Int)

-DerivedTypesResolution.dfy(140,6): Error: RHS (of type AnotherInt) not assignable to LHS (of type Int)

-DerivedTypesResolution.dfy(156,9): Error: name of type ('B') is used as a variable

-DerivedTypesResolution.dfy(157,11): Error: name of type ('Syn') is used as a variable

-DerivedTypesResolution.dfy(162,8): Error: member U does not exist in class Klass

-DerivedTypesResolution.dfy(162,4): Error: expected method call, found expression

-DerivedTypesResolution.dfy(188,39): Error: incorrect type of datatype constructor argument (found Dt<bool>, expected S)

-24 resolution/type errors detected in DerivedTypesResolution.dfy

+NewtypesResolution.dfy(5,7): Error: Cycle among redirecting types (newtypes, type synonyms): MySynonym -> MyIntegerType_WellSupposedly -> MyNewType -> MySynonym

+NewtypesResolution.dfy(12,10): Error: newtypes must be based on some numeric type (got List<int>)

+NewtypesResolution.dfy(38,9): Error: arguments must have the same type (got posReal and real)

+NewtypesResolution.dfy(44,9): Error: arguments must have the same type (got int32 and int)

+NewtypesResolution.dfy(50,13): Error: arguments must have the same type (got posReal and int32)

+NewtypesResolution.dfy(51,13): Error: arguments to <= must have the same type (got posReal and int32)

+NewtypesResolution.dfy(52,13): Error: arguments to < must have the same type (got int32 and int)

+NewtypesResolution.dfy(53,13): Error: arguments to > must have the same type (got posReal and real)

+NewtypesResolution.dfy(57,13): Error: first argument to % must be of type int (instead got posReal)

+NewtypesResolution.dfy(57,25): Error: first argument to % must be of type int (instead got real)

+NewtypesResolution.dfy(75,8): Error: newtype constraint must be of type bool (instead got SmallInt)

+NewtypesResolution.dfy(77,10): Error: unresolved identifier: a

+NewtypesResolution.dfy(91,31): Error: old expressions are not allowed in this context

+NewtypesResolution.dfy(101,24): Error: Wrong number of type arguments (1 instead of 0) passed to newtype: N

+NewtypesResolution.dfy(105,10): Error: recursive dependency involving a newtype: _default.BadLemma -> Cycle

+NewtypesResolution.dfy(114,10): Error: recursive dependency involving a newtype: SelfCycle -> SelfCycle

+NewtypesResolution.dfy(120,21): Error: name of type ('N9') is used as a variable

+NewtypesResolution.dfy(139,6): Error: RHS (of type int) not assignable to LHS (of type Int)

+NewtypesResolution.dfy(140,6): Error: RHS (of type AnotherInt) not assignable to LHS (of type Int)

+NewtypesResolution.dfy(156,9): Error: name of type ('B') is used as a variable

+NewtypesResolution.dfy(157,11): Error: name of type ('Syn') is used as a variable

+NewtypesResolution.dfy(162,8): Error: member U does not exist in class Klass

+NewtypesResolution.dfy(162,4): Error: expected method call, found expression

+NewtypesResolution.dfy(188,39): Error: incorrect type of datatype constructor argument (found Dt<bool>, expected S)

+24 resolution/type errors detected in NewtypesResolution.dfy

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index cf1810e6..3f08e72a 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -60,12 +60,12 @@ ResolutionErrors.dfy(994,7): Error: Duplicate name of top-level declaration: Bad
 ResolutionErrors.dfy(991,17): Error: Wrong number of type arguments (0 instead of 1) passed to class/datatype: List

 ResolutionErrors.dfy(992,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name?)

 ResolutionErrors.dfy(993,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)

-ResolutionErrors.dfy(1000,7): Error: Cycle among redirecting types (derived types, type synonyms): A -> A

-ResolutionErrors.dfy(1003,7): Error: Cycle among redirecting types (derived types, type synonyms): A -> B -> A

-ResolutionErrors.dfy(1007,7): Error: Cycle among redirecting types (derived types, type synonyms): A -> B -> A

+ResolutionErrors.dfy(1000,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> A

+ResolutionErrors.dfy(1003,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A

+ResolutionErrors.dfy(1007,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A

 ResolutionErrors.dfy(1016,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed

-ResolutionErrors.dfy(1019,7): Error: Cycle among redirecting types (derived types, type synonyms): A -> B -> A

-ResolutionErrors.dfy(1024,7): Error: Cycle among redirecting types (derived types, type synonyms): A -> B -> A

+ResolutionErrors.dfy(1019,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A

+ResolutionErrors.dfy(1024,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A

 ResolutionErrors.dfy(1043,21): Error: unresolved identifier: x

 ResolutionErrors.dfy(1050,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P

 ResolutionErrors.dfy(1062,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name?)

diff --git a/Test/hofs/ResolveError.dfy.expect b/Test/hofs/ResolveError.dfy.expect
index 0cb9413c..994d78f2 100644
--- a/Test/hofs/ResolveError.dfy.expect
+++ b/Test/hofs/ResolveError.dfy.expect
@@ -2,8 +2,8 @@ ResolveError.dfy(7,11): Error: the number of left-hand sides (1) and right-hand
 ResolveError.dfy(8,11): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment

 ResolveError.dfy(21,6): Error: LHS of assignment must denote a mutable field

 ResolveError.dfy(31,16): Error: arguments must have the same type (got int and bool)

-ResolveError.dfy(32,12): Error: cannot apply arguments with types int,int to expression with type int -> int

-ResolveError.dfy(33,12): Error: cannot apply arguments with types bool to expression with type int -> int

+ResolveError.dfy(32,12): Error: wrong number of arguments to function application (function type 'int -> int' expects 1, got 2)

+ResolveError.dfy(33,13): Error: type mismatch for argument 0 (function expects int, got bool)

 ResolveError.dfy(34,13): Error: incorrect type of function argument 0 (expected int, got bool)

 ResolveError.dfy(35,25): Error: arguments must have the same type (got bool and int)

 ResolveError.dfy(36,13): Error: wrong number of function arguments (got 2, expected 1)