Make arrow types not look like reference types for the resolver

3 files changed, 11 insertions, 2 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 7c2c5759..61b5ccff 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -4240,7 +4240,9 @@ namespace Microsoft.Dafny
         }

 

       } else if (proxy is ObjectTypeProxy) {

-        if (t is ObjectType || UserDefinedType.DenotesClass(t) != null) {

+        if (t is ArrowType) {

+          return false;

+        } else if (t is ObjectType || UserDefinedType.DenotesClass(t) != null) {

           // all is fine, proxy can be redirected to t

         } else {

           return false;

diff --git a/Test/hofs/ResolveError.dfy b/Test/hofs/ResolveError.dfy
index 1e389f04..31de9424 100644
--- a/Test/hofs/ResolveError.dfy
+++ b/Test/hofs/ResolveError.dfy
@@ -56,3 +56,8 @@ method Bla() {
   assert Bool;
 }
 
+method Pli(f : A -> B) requires f != null;
+{
+  var o : object;
+  assert f != o;
+}
diff --git a/Test/hofs/ResolveError.dfy.expect b/Test/hofs/ResolveError.dfy.expect
index a95d9bac..d7de049a 100644
--- a/Test/hofs/ResolveError.dfy.expect
+++ b/Test/hofs/ResolveError.dfy.expect
@@ -13,4 +13,6 @@ ResolveError.dfy(39,13): Error: wrong number of function arguments (got 2, expec
 ResolveError.dfy(46,15): Error: a reads-clause expression must denote an object or a collection of objects (instead got int)

 ResolveError.dfy(47,7): Error: Precondition must be boolean (got int)

 ResolveError.dfy(56,9): Error: condition is expected to be of type bool, but is () -> bool

-15 resolution/type errors detected in ResolveError.dfy

+ResolveError.dfy(59,34): Error: arguments must have the same type (got A -> B and ?)

+ResolveError.dfy(62,11): Error: arguments must have the same type (got A -> B and object)

+17 resolution/type errors detected in ResolveError.dfy