diff options
| author |  Dan Rosén <danr@chalmers.se> | 2014-08-14 17:43:01 -0700 |
|---|---|---|
| committer | Dan Rosén <danr@chalmers.se> | 2014-08-14 17:43:01 -0700 |
| commit | 4ab6c9f4cfa6295369fde54084f3e1f4ed70d5e4 (patch) | |
| tree | 77e930de4ae3b762e9efeefa9796738e4976049f /Source | |
| parent | d5911a6efb781c089a067c9931302622fcc52a5b (diff) | |
Fix bug in type substitution for type variables
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 148dded7..35086275 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -6073,12 +6073,18 @@ namespace Microsoft.Dafny } else if (type is UserDefinedType) {
var t = (UserDefinedType)type;
if (t.ResolvedParam != null) {
- Contract.Assert(t.TypeArgs.Count == 0);
Type s;
if (subst.TryGetValue(t.ResolvedParam, out s)) {
+ Contract.Assert(t.TypeArgs.Count == 0); // what to do?
return cce.NonNull(s);
} else {
- return type;
+ if (t.TypeArgs.Count == 0) {
+ return type;
+ } else {
+ return new UserDefinedType(t.ResolvedParam) {
+ TypeArgs = t.TypeArgs.ConvertAll(u => SubstType(u, subst))
+ };
+ }
}
} else if (t.ResolvedClass != null) {
List<Type> newArgs = null; // allocate it lazily
|