Do not allow implicit arguments in definitions

src/cmd_parser.cpp

@@ -428,11 +428,27 @@ bool CmdParser::parseNextCommand()
     case Token::DEFINE:
     {
       d_state.pushScope();
-      //d_state.checkThatLogicIsSet();
       std::string name = d_eparser.parseSymbol();
       //d_state.checkUserSymbol(name);
+      std::vector<Expr> impls;
       std::vector<Expr> vars =
-          d_eparser.parseAndBindSortedVarList();
+          d_eparser.parseAndBindSortedVarList(impls);
+      if (!impls.empty())
+      {
+        // If there were implicit variables, we go back and refine what is
+        // bound in the body to only include the explicit arguments. This
+        // ensures that `T` is not parsable in the body of a definition like:
+        //   (define test ((T Type :implicit) (x T)) T)
+        // It should not be parsable since it is not bound when test is applied,
+        // which prevents users from generating definitions that lead to
+        // unexpected unbound arguments.
+        d_state.popScope();
+        d_state.pushScope();
+        for (const Expr& e : vars)
+        {
+          d_state.bind(e.getSymbol(), e);
+        }
+      }
       Expr ret;
       if (tok == Token::DEFINE_FUN)
       {

src/expr_parser.cpp

@@ -668,6 +668,13 @@ std::vector<Expr> ExprParser::parseExprPairList()
 }
 
 std::vector<Expr> ExprParser::parseAndBindSortedVarList(bool isLookup)
+{
+  std::vector<Expr> impls;
+  return parseAndBindSortedVarList(impls, isLookup);
+}
+
+std::vector<Expr> ExprParser::parseAndBindSortedVarList(
+                     std::vector<Expr>& impls, bool isLookup)
 {
   std::vector<Expr> varList;
   d_lex.eatToken(Token::LPAREN);
@@ -700,6 +707,7 @@ std::vector<Expr> ExprParser::parseAndBindSortedVarList(bool isLookup)
       {
         attrs.erase(Attr::IMPLICIT);
         isImplicit = true;
+        impls.push_back(v);
       }
       if (processAttributeMap(attrs, ck, cons))
       {

src/expr_parser.h

@@ -51,6 +51,13 @@ class ExprParser
    * variables and throw an error if a variable does not match.
    */
   std::vector<Expr> parseAndBindSortedVarList(bool isLookup=false);
+  /**
+   * Same as above, but tracks implicit variables. All variables marked
+   * :implicit that were parsed and not added to the return value of this
+   * method are added to impls.
+   */
+  std::vector<Expr> parseAndBindSortedVarList(std::vector<Expr>& impls,
+                                              bool isLookup=false);
   /**
    * Parse symbol, which returns the string of the parsed symbol if the next
    * token is a valid smt2 symbol.