Ho node manager types (#1203)

* Remove restrictions about function types

* Introduce notion of first-class type, improve assertions, add comment on equality type rule.

* Update comment

1 files changed, 2 insertions, 4 deletions

diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 370e5d348..777f6e57f 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -77,10 +77,7 @@ class EqualityTypeRule {
     if( check ) {
       TypeNode lhsType = n[0].getType(check);
       TypeNode rhsType = n[1].getType(check);
-
-      // TODO : we may want to limit cases where we have equalities between terms of different types 
-      //   equalities between (Set Int) and (Set Real) already cause strange issues in theory solver for sets
-      //   one possibility is to only allow this for Int/Real
+      
       if ( TypeNode::leastCommonTypeNode(lhsType, rhsType).isNull() ) {
         std::stringstream ss;
         ss << "Subexpressions must have a common base type:" << std::endl;
@@ -90,6 +87,7 @@ class EqualityTypeRule {
 
         throw TypeCheckingExceptionPrivate(n, ss.str());
       }
+      // TODO : check isFirstClass for these types? (github issue #1202)
     }
     return booleanType;
   }