Make sure to check that subrange types are not used as type parameters

3 files changed, 88 insertions, 7 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 5f7bf42f..fe219dbc 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -7367,6 +7367,9 @@ namespace Microsoft.Dafny
       if (expr.OptTypeArguments != null) {

         foreach (var ty in expr.OptTypeArguments) {

           ResolveType(expr.tok, ty, opts.codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);

+          if (ty.IsSubrangeType) {

+            Error(expr.tok, "sorry, cannot instantiate type parameter with a subrange type");

+          }

         }

       }

 

@@ -7626,6 +7629,9 @@ namespace Microsoft.Dafny
       if (expr.OptTypeArguments != null) {

         foreach (var ty in expr.OptTypeArguments) {

           ResolveType(expr.tok, ty, opts.codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);

+          if (ty.IsSubrangeType) {

+            Error(expr.tok, "sorry, cannot instantiate type parameter with a subrange type");

+          }

         }

       }

 

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 141e48cb..01c2a0a5 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -114,6 +114,55 @@ method K() {
   var d: MutuallyRecursiveDataType<nat>;  // error: not allowed to instantiate with 'nat'

   var a := new nat[100];  // error: not allowed the type array<nat>

   var b := new nat[100,200];  // error: not allowed the type array2<nat>

+

+  // constructors

+  var ci0 := new Expl_Class.Init<nat>(0, 0);  // error: subrange not allowed here

+  var ci1 := new Expl_Class<nat>;  // error

+  var ci2 := new Expl_Class<nat>.Init(0, 0);  // error

+

+  // collection types (sets are above) and array types

+  var m0: multiset<nat>;  // error

+  var m1: seq<nat>;  // error

+  var m2: map<nat,int>;  // error

+  var m3: map<int,nat>;  // error

+  var n: seq<MutuallyRecursiveDataType<nat>>;  // error

+  var o: array<nat>;  // error

+  var o': array2<nat>;  // error

+

+  // tuple types

+  var tu0: (nat);  // no problem, this just means 'nat'

+  var tu1: (nat,int);  // error

+  var tu2: (int,nat);  // error

+

+  // function types

+  var fn: nat -> int;  // error

+  var gn: int -> nat;  // error

+  var hn: (int,nat) -> int;  // error

+

+  // the following tests test NameSegment and ExprDotName in types:

+  var k: Expl_Class<nat>;  // error

+  var k': Expl_Module.E<nat>;  // error

+

+  // the following tests test NameSegment and ExprDotName in expressions:

+  var e0 := Expl_M<nat>(0);  // error

+  var e1 := Expl_F<nat>(0);  // error

+  var ec := new Expl_Class<int>;

+  ec.Init<nat>(0, 0);  // error

+  Expl_Class.DoIt<nat>(0, 0);  // error

+  Expl_Class<nat>.DoIt(0, 0);  // error

+  Expl_Module.E.N<nat>(0, 0);  // error

+  Expl_Module.E<nat>.N(0, 0);  // error

+}

+method Expl_M<T>(x: T) returns (y: T)

+function method Expl_F<T>(x: T): T

+class Expl_Class<T> {

+  method Init<U>(t: T, u: U)

+  static method DoIt<U>(t: T, u: U)

+}

+module Expl_Module {

+  class E<T> {

+    static method N<U>(t: T, u: U)

+  }

 }

 

 // --------------------- more ghost tests, for assign-such-that statements

diff --git a/Test/dafny0/TypeTests.dfy.expect b/Test/dafny0/TypeTests.dfy.expect
index e40f2c35..500b1af9 100644
--- a/Test/dafny0/TypeTests.dfy.expect
+++ b/Test/dafny0/TypeTests.dfy.expect
@@ -1,6 +1,6 @@
-TypeTests.dfy(156,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)

-TypeTests.dfy(162,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)

-TypeTests.dfy(169,6): Error: RHS (of type set<?>) not assignable to LHS (of type ?)

+TypeTests.dfy(205,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)

+TypeTests.dfy(211,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)

+TypeTests.dfy(218,6): Error: RHS (of type set<?>) not assignable to LHS (of type ?)

 TypeTests.dfy(7,17): Error: type mismatch for argument 0 (function expects C, got D)

 TypeTests.dfy(7,20): Error: type mismatch for argument 1 (function expects D, got C)

 TypeTests.dfy(8,15): Error: type mismatch for argument 0 (function expects C, got int)

@@ -30,8 +30,34 @@ TypeTests.dfy(113,6): Error: sorry, cannot instantiate collection type with a su
 TypeTests.dfy(114,9): Error: sorry, cannot instantiate type parameter 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

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

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

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

+TypeTests.dfy(120,10): Error: new can be applied only to reference types (got Expl_Class<nat>)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 TypeTests.dfy(21,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed

-36 resolution/type errors detected in TypeTests.dfy

+62 resolution/type errors detected in TypeTests.dfy