diff options
| author |  Rustan Leino <unknown> | 2014-07-15 16:44:00 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-07-15 16:44:00 -0700 |
| commit | 30cd666db7142297b7cd627cad34243b76e7291a (patch) | |
| tree | 7d3155ede7a8ea29b4d5cb552fcbab64deabb374 /Test/dafny0/ResolutionErrors.dfy | |
| parent | 3d81de6e45e1a82931cd09442cb88458c86094e8 (diff) | |
Allow an arbitrary-type to take type parameters
Diffstat (limited to 'Test/dafny0/ResolutionErrors.dfy')
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 48 |
1 files changed, 48 insertions, 0 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 823fbe29..520b2e38 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -1042,3 +1042,51 @@ type {:myAttribute x} Synonym = int // error: x does not refer to anything module {:myAttribute x} Modulette { // error: x does not refer to anything
}
+
+// --- opaque types with type parameters ---
+
+module OpaqueTypes0 {
+ type P<AA>
+ method M<B>(p: P<B>) returns (q: P<B,B>) // error: wrong param count
+ {
+ q := p;
+ }
+}
+
+module OpaqueTypes1 {
+ type P<A>
+
+ method M0<B>(p: P<B>) returns (q: P<B>)
+ {
+ q := p;
+ var m: P<BX>; // error: BX undefined
+ }
+
+ method M1<B>(p: P<B>) returns (q: P) // type parameter of q's type inferred
+ {
+ q := p;
+ }
+
+ method M2(p: P<int>) returns (q: P<bool>)
+ {
+ q := p; // error: cannot assign P<bool> to P<int>
+ }
+
+ method M3<A,B>(p: P<A>) returns (q: P<B>)
+ {
+ q := p; // error: cannot assign P<A> to P<B>
+ }
+
+ method M4<A>() returns (p: P<A>, q: P<int>)
+ {
+ q := p; // error: cannot assign P<A> to P<int>
+ p := q; // error: cannot assign P<int> to P<A>
+ }
+
+ method EqualityTests<X>(p: P<int>, q: P<bool>, r: P<X>)
+ {
+ assert p != r; // error: types must be the same in order to do compare
+ assert q != r; // error: types must be the same in order to do compare
+ assert p != q; // error: types must be the same in order to do compare
+ }
+}
|