avoid sortedness errors with polymorphically let-bound constants

Kernel/Signature.cpp

@@ -61,6 +61,7 @@ Signature::Symbol::Symbol(const vstring& nm, unsigned arity, bool interpreted, b
     _skipCongruence(0),
     _tuple(0),
     _computable(1),
+    _letBound(0),
     _prox(NOT_PROXY),
     _comb(NOT_COMB)
 {

Kernel/Signature.hpp

@@ -157,6 +157,8 @@ class Signature
     unsigned _tuple : 1;
     /** if allowed in answer literals */
     unsigned _computable : 1;
+    /** name that is bound by a $let-binder */
+    unsigned _letBound : 1;
     /** proxy type */
     Proxy _prox;
     /** combinator type */
@@ -195,6 +197,8 @@ class Signature
     void markTermAlgebraDest() { _termAlgebraDest=1; }
     /** mark the symbol as uncomputable and hence not allowed in answer literals */
     void markUncomputable() { _computable = 0; }
+    /** mark the symbol as let-bound */
+    void markLetBound() { _letBound = 1; }
 
     /** return true iff symbol is marked as skip for the purpose of symbol elimination */
     bool skip() const { return _skip; }
@@ -245,6 +249,8 @@ class Signature
     inline bool termAlgebraDest() const { return _termAlgebraDest; }
     /** Return true iff symbol is considered computable */
     inline bool computable() const { return _computable; }
+    /** if bound by a $let-binder */
+    inline bool letBound() const { return _letBound; }
 
     /** Increase the usage count of this symbol **/
     inline void incUsageCnt(){ _usageCount++; }

Kernel/SortHelper.cpp

@@ -92,7 +92,27 @@ TermList SortHelper::getResultSort(const Term* t)
   getTypeSub(t, subst);
   Signature::Symbol* sym = env.signature->getFunction(t->functor());
   TermList result = sym->fnType()->result();
-  ASS(!subst.isEmpty()  || (result.isTerm() && (result.term()->isSuper() || result.term()->ground())));  
+
+  /*
+  either
+  1. the substitution is non-empty
+  2. the result is ground (or $tType)
+  3. t is let-bound: consider the following TFF1
+
+      % polymorphic constant
+      tff(c_type, type, c: !>[A: $tType]: A).
+      % some polymorphic predicate, not important
+      tff(p_type, type, p: !>[A: $tType]: A > $o).
+
+      % let-bind a polymorphic identity function
+      tff(bug, axiom, ![A: $tType]: $let(id: A > A, id(X) := X, p(A, id(c(A))))).
+      % note that type of id is A > A, *not* !>[A: $tType]: A > A.
+  */
+  ASS(
+    !subst.isEmpty() ||
+    (result.isTerm() && (result.term()->isSuper() || result.term()->ground())) ||
+    sym->letBound()
+  )
   return SubstHelper::apply(result, subst);
 }
 

Parse/TPTP.cpp

@@ -2345,18 +2345,18 @@ void TPTP::endLetTypes()
   unsigned arity = type->arity();
   bool isPredicate = type->isPredicateType();
 
-  unsigned symbol = isPredicate
+  unsigned functor = isPredicate
                   ? env.signature->addFreshPredicate(arity, name.c_str())
                   : env.signature->addFreshFunction(arity,  name.c_str());
+  Signature::Symbol *symbol = isPredicate
+    ? env.signature->getPredicate(functor)
+    : env.signature->getFunction(functor);
 
-  if (isPredicate) {
-    env.signature->getPredicate(symbol)->setType(type);
-  } else {
-    env.signature->getFunction(symbol)->setType(type);
-  }
+  symbol->setType(type);
+  symbol->markLetBound();
 
   LetSymbolName symbolName(name, arity);
-  LetSymbolReference symbolReference(symbol, isPredicate);
+  LetSymbolReference symbolReference(functor, isPredicate);
 
   LetSymbols scope = _letTypedSymbols.pop();