Fixed bug Issue 37: expand type synonyms in more (hopefully all) places in the resolver and translator

6 files changed, 17 insertions, 9 deletions

diff --git a/Test/dafny0/EqualityTypes.dfy.expect b/Test/dafny0/EqualityTypes.dfy.expect
index 410e4507..70e46ff0 100644
--- a/Test/dafny0/EqualityTypes.dfy.expect
+++ b/Test/dafny0/EqualityTypes.dfy.expect
@@ -5,7 +5,7 @@ EqualityTypes.dfy(41,8): Error: opaque type 'Y' is not allowed to be replaced by
 EqualityTypes.dfy(45,11): Error: type 'X' is used to refine an opaque type with equality support, but 'X' does not support equality

 EqualityTypes.dfy(46,11): Error: type 'Y' is used to refine an opaque type with equality support, but 'Y' does not support equality

 EqualityTypes.dfy(66,7): Error: == can only be applied to expressions of types that support equality (got Dt<T>)

-EqualityTypes.dfy(85,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0)

+EqualityTypes.dfy(85,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0) (perhaps try declaring type parameter '_T0' on line 81 as '_T0(==)', which says it can only be instantiated with a type that supports equality)

 EqualityTypes.dfy(109,7): Error: == can only be applied to expressions of types that support equality (got D)

 EqualityTypes.dfy(114,13): Error: == can only be applied to expressions of types that support equality (got D)

 EqualityTypes.dfy(118,16): Error: == can only be applied to expressions of types that support equality (got D)

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 520b2e38..aaf1291c 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -1007,20 +1007,20 @@ module CycleError2 {
   type A = B  // error: cycle: A -> B -> A

   type B = set<A>

 }

-module Good0 {

+module CycleErrors3 {

   type A = (B, D<bool>)

   type B = C

   class C {

     var a: A;  // this is fine

   }

-  datatype D<X> = Make(A, B, C)  // this is fine, too

+  datatype D<X> = Make(A, B, C)  // error: cannot construct a D<X>

 }

-module CycleError3 {

+module CycleError4 {

   type A = B  // error: cycle: A -> B -> A

   type B = C<A>

   class C<T> { }

 }

-module CycleError4 {

+module CycleError5 {

   type A = B  // error: cycle: A -> B -> A

   type B = Dt<A>

   datatype Dt<T> = Make(T)

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 49cfe650..d5d12eb9 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -63,6 +63,7 @@ ResolutionErrors.dfy(993,22): Error: Undeclared top-level type or type parameter
 ResolutionErrors.dfy(1000,7): Error: Cycle among type synonyms: A -> A

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

 ResolutionErrors.dfy(1007,7): Error: Cycle among 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 type synonyms: A -> B -> A

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

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

@@ -171,4 +172,4 @@ ResolutionErrors.dfy(956,10): Error: second argument to % must be of type int (i
 ResolutionErrors.dfy(960,7): Error: type conversion to real is allowed only from int (got real)

 ResolutionErrors.dfy(961,7): Error: type conversion to int is allowed only from real (got int)

 ResolutionErrors.dfy(962,7): Error: type conversion to int is allowed only from real (got nat)

-173 resolution/type errors detected in ResolutionErrors.dfy

+174 resolution/type errors detected in ResolutionErrors.dfy

diff --git a/Test/dafny0/TypeSynonyms.dfy b/Test/dafny0/TypeSynonyms.dfy
index 4bec5253..85beb340 100644
--- a/Test/dafny0/TypeSynonyms.dfy
+++ b/Test/dafny0/TypeSynonyms.dfy
@@ -44,3 +44,10 @@ function Skip(s: Synonym3): Synonym0
   case Nil => Nil

   case Cons(_, tail) => tail

 }

+

+type MyMap = map<int, map<real, bool>>

+

+predicate MyMapProperty(m: MyMap, x: int)

+{

+  x in m && real(x) in m[x] && m[x][real(x)]

+}

diff --git a/Test/dafny0/TypeSynonyms.dfy.expect b/Test/dafny0/TypeSynonyms.dfy.expect
index 4ef2de53..76f19e0d 100644
--- a/Test/dafny0/TypeSynonyms.dfy.expect
+++ b/Test/dafny0/TypeSynonyms.dfy.expect
@@ -1,2 +1,2 @@
 

-Dafny program verifier finished with 6 verified, 0 errors

+Dafny program verifier finished with 7 verified, 0 errors

diff --git a/Test/dafny0/TypeTests.dfy.expect b/Test/dafny0/TypeTests.dfy.expect
index 62e41019..5d78fe16 100644
--- a/Test/dafny0/TypeTests.dfy.expect
+++ b/Test/dafny0/TypeTests.dfy.expect
@@ -25,8 +25,8 @@ TypeTests.dfy(106,3): Error: cannot assign to a range of array elements (try the
 TypeTests.dfy(107,3): Error: cannot assign to a range of array elements (try the 'forall' statement)

 TypeTests.dfy(113,6): Error: sorry, cannot instantiate collection type with a subrange type

 TypeTests.dfy(114,9): Error: sorry, cannot instantiate type parameter with a subrange type

-TypeTests.dfy(115,8): Error: sorry, cannot instantiate 'array' type with a subrange type

-TypeTests.dfy(116,8): Error: sorry, cannot instantiate 'array' type with a subrange type

+TypeTests.dfy(115,8): Error: sorry, cannot instantiate type parameter with a subrange type

+TypeTests.dfy(116,8): Error: sorry, cannot instantiate type parameter with a subrange type

 TypeTests.dfy(128,15): Error: ghost variables are allowed only in specification contexts

 TypeTests.dfy(138,4): Error: cannot assign to non-ghost variable in a ghost context

 TypeTests.dfy(139,7): Error: cannot assign to non-ghost variable in a ghost context