Type parameters in method/function signatures are no longer auto-declared. Although

convenient and concise, the auto-declare behavior has on many occasions caused
confusion when a type name has accidentally been mistyped (and Dafny had then
accepted and auto-declared the name).
Note, the behavior of filling in missing type parameters is still supported.  This
mode, although unusual (even original?) in languages, is different from the auto-
declare behavior.  For auto-declare, identifiers could be used in the program
without having a declaration.  For fill-in parameters, the implicitly declared
type parameters remain anonymous.

1 files changed, 0 insertions, 6 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 29e36ccd..7c78c1e2 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -8469,12 +8469,6 @@ namespace Microsoft.Dafny
           r = ResolveExprDotCall(expr.tok, receiver, member, expr.OptTypeArguments, opts.codeContext, allowMethodCall);

         }

 #endif

-      } else if (option.Opt == ResolveTypeOptionEnum.AllowPrefixExtend && expr.OptTypeArguments == null) {

-        // it woulc plausibly be a type parameter, but isn't; we will declare it automatically

-        tp = new TypeParameter(expr.tok, expr.Name, defaultTypeArguments.Count, option.Parent);

-        defaultTypeArguments.Add(tp);

-        r = new Resolver_IdentifierExpr(expr.tok, tp);

-        allTypeParameters.Push(expr.Name, tp);

       } else {

         // ----- None of the above

         Error(expr.tok, "Undeclared top-level type or type parameter: {0} (did you forget to qualify a name?)", expr.Name);