diff options
| author |  Rustan Leino <unknown> | 2015-08-20 11:49:24 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2015-08-20 11:49:24 -0700 |
| commit | 270b34fc36dcfc781e8f49df5339cb2e10e69828 (patch) | |
| tree | fdf0ff7860d19e01b806f1fe0a4db54d71654c11 /Source/Dafny/Resolver.cs | |
| parent | eb146ddaa09123f57b963fd85845c944a73a23cb (diff) | |
Fixed bug in type unification
Diffstat (limited to 'Source/Dafny/Resolver.cs')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 58984b9b..2f2b5a54 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -4574,8 +4574,11 @@ namespace Microsoft.Dafny } else if (a is CollectionTypeProxy) {
if (b is CollectionTypeProxy) {
- a.T = b;
- return UnifyTypes(((CollectionTypeProxy)a).Arg, ((CollectionTypeProxy)b).Arg);
+ var argUnificationSuccess = UnifyTypes(((CollectionTypeProxy)a).Arg, ((CollectionTypeProxy)b).Arg);
+ if (argUnificationSuccess) {
+ a.T = b;
+ }
+ return argUnificationSuccess;
} else if (b is OperationTypeProxy) {
var proxy = (OperationTypeProxy)b;
if (proxy.AllowSeq && proxy.AllowSetVarieties && proxy.AllowISet) {
|