Support strict casts in the SimpleSub inferencer (#3870)

Part of #3848. 

- Add support for strict casts in the SimpleSub-based sort inference
algorithm
- Improve the error message for `CHECKED` mode
- Add missing constraints when handling anywhere rules
- Not strictly required at this point, but ensures that every parameter
is inferred as will be needed for #3849.

kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java

@@ -445,7 +445,7 @@ private Tuple2<Either<Set<KEMException>, Term>, Set<KEMException>> parseStringTe
           boolean equalRight =
               rez.isRight() && z3Rez.isRight() && rez.right().get().equals(z3Rez.right().get());
           if (!(bothLeft || equalRight)) {
-            throw KEMException.criticalError("Z3 and SimpleSub algorithms differ!");
+            throw typeInferenceCheckError(rez3, z3Rez, rez);
           }
         } else {
           rez = z3Rez;
@@ -495,6 +495,32 @@ private Tuple2<Either<Set<KEMException>, Term>, Set<KEMException>> parseStringTe
     }
   }
 
+  private static KEMException typeInferenceCheckError(
+      Term term, Either<Set<KEMException>, Term> z3, Either<Set<KEMException>, Term> simple) {
+    StringBuilder msg = new StringBuilder("Z3 and SimpleSub sort inference algorithms differ!\n");
+    msg.append(term.source().isPresent() ? term.source().get().toString() : "").append("\n");
+    msg.append(term.location().isPresent() ? term.location().get().toString() : "").append("\n");
+    msg.append("\nZ3:\n");
+    if (z3.isLeft()) {
+      msg.append(
+          z3.left().get().stream().map(KEMException::getMessage).collect(Collectors.joining("\n")));
+    } else {
+      msg.append(z3.right().get());
+    }
+    msg.append("\n");
+    msg.append("\nSimpleSub:\n");
+    if (simple.isLeft()) {
+      msg.append(
+          simple.left().get().stream()
+              .map(KEMException::getMessage)
+              .collect(Collectors.joining("\n")));
+    } else {
+      msg.append(simple.right().get());
+    }
+    msg.append("\n");
+    return KEMException.criticalError(msg.toString());
+  }
+
   private boolean isDebug(Source source, int startLine) {
     if (typeInferenceDebug == null) {
       return false;

kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/InferenceDriver.java

@@ -75,6 +75,12 @@ public BoundedSort sortToBoundedSort(Sort sort, ProductionReference prOrNull) {
     return new BoundedSort.Constructor(sort.head());
   }
 
+  public BoundedSort returnSort(ProductionReference pr) throws ConstraintError {
+    BoundedSort resSort = new BoundedSort.Variable();
+    constrain(sortToBoundedSort(pr.production().sort(), pr), resSort, pr);
+    return resSort;
+  }
+
   /**
    * Update sub-/super-type constraints to record the fact that lhs <: rhs.
    *

kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/SortInferencer.java

@@ -19,7 +19,6 @@
 import org.kframework.definition.Module;
 import org.kframework.definition.NonTerminal;
 import org.kframework.definition.Production;
-import org.kframework.kore.KLabel;
 import org.kframework.kore.Sort;
 import org.kframework.kore.SortHead;
 import org.kframework.parser.Ambiguity;
@@ -88,10 +87,10 @@ public SortInferencer(Module mod) {
 
   /**
    * Determine whether a Term is supported by the current SortInferencer algorithm. Supported terms
-   * can contain neither ambiguities, strict casts, nor parametric sorts.
+   * can contain neither ambiguities nor parametric sorts.
    */
   public static boolean isSupported(Term t) {
-    return !hasAmbiguity(t) && !hasStrictCast(t) && !hasParametricSorts(t);
+    return !hasAmbiguity(t) && !hasParametricSorts(t);
   }
 
   private static boolean hasAmbiguity(Term t) {
@@ -104,24 +103,6 @@ private static boolean hasAmbiguity(Term t) {
     return ((TermCons) t).items().stream().anyMatch(SortInferencer::hasAmbiguity);
   }
 
-  private static boolean hasStrictCast(Term t) {
-    if (t instanceof Ambiguity amb) {
-      return amb.items().stream().anyMatch(SortInferencer::hasStrictCast);
-    }
-    ProductionReference pr = (ProductionReference) t;
-    if (pr.production().klabel().isDefined()) {
-      KLabel klabel = pr.production().klabel().get();
-      String label = klabel.name();
-      if (label.equals("#SyntacticCast") || label.equals("#SyntacticCastBraced")) {
-        return true;
-      }
-    }
-    if (t instanceof Constant) {
-      return false;
-    }
-    return ((TermCons) t).items().stream().anyMatch(SortInferencer::hasStrictCast);
-  }
-
   private static boolean hasParametricSorts(Term t) {
     if (t instanceof Ambiguity amb) {
       return amb.items().stream().anyMatch(SortInferencer::hasParametricSorts);
@@ -259,26 +240,42 @@ private BoundedSort infer(Term t, boolean isAnywhereRule, InferenceDriver driver
       // Note that we do actually need the LHS's declared sort. The LHS's inferred sort
       // is a variable X with a bound L <: X, and constraining against X would just add a
       // new lower bound aka permit widening.
+      //
+      // It's also safe to assume the LHS is not an Ambiguity due to PushTopAmbiguitiesUp
       ProductionReference lhsDeclaredPr = (ProductionReference) stripBrackets(tc.get(0));
       BoundedSort lhsDeclaredSort =
           driver.sortToBoundedSort(lhsDeclaredPr.production().sort(), lhsDeclaredPr);
       BoundedSort rhsSort = infer(tc.get(1), false, driver);
       driver.constrain(rhsSort, lhsDeclaredSort, (ProductionReference) tc.get(1));
-      return lhsSort;
+
+      // Handle usual production constraints
+      BoundedSort rewriteParam = driver.sortToBoundedSort(tc.production().sort(), tc);
+      driver.constrain(lhsSort, rewriteParam, tc);
+      driver.constrain(rhsSort, rewriteParam, tc);
+      return driver.returnSort(tc);
+    }
+
+    if (tc.production()
+        .klabel()
+        .filter(k -> k.name().equals("#SyntacticCast") || k.name().equals("#SyntacticCastBraced"))
+        .isDefined()) {
+      BoundedSort castedSort = driver.sortToBoundedSort(tc.production().sort(), tc);
+      BoundedSort childSort = infer(tc.get(0), isAnywhereRule, driver);
+      driver.constrain(castedSort, childSort, tc);
+      driver.constrain(childSort, castedSort, tc);
+      return driver.returnSort(tc);
     }
 
     for (int prodI = 0, tcI = 0; prodI < tc.production().items().size(); prodI++) {
       if (!(tc.production().items().apply(prodI) instanceof NonTerminal nt)) {
         continue;
       }
-      BoundedSort expectedSort = driver.sortToBoundedSort(nt.sort(), pr);
+      BoundedSort expectedSort = driver.sortToBoundedSort(nt.sort(), tc);
       BoundedSort childSort = infer(tc.get(tcI), isAnywhereRule, driver);
-      driver.constrain(childSort, expectedSort, pr);
+      driver.constrain(childSort, expectedSort, tc);
       tcI++;
     }
-    BoundedSort resSort = new BoundedSort.Variable();
-    driver.constrain(driver.sortToBoundedSort(tc.production().sort(), pr), resSort, pr);
-    return resSort;
+    return driver.returnSort(tc);
   }
 
   /**