Fix an issue with comparison of inference variables

JetBrains · Apr 18, 2024 · 5d1df89 · 5d1df89
1 parent 1236058
commit 5d1df89
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 7 deletions.
diff --git a/base/src/main/java/org/arend/core/expr/Expression.java b/base/src/main/java/org/arend/core/expr/Expression.java
@@ -694,24 +694,31 @@ public InferenceVariable getStuckInferenceVariable() {
     return stuck instanceof InferenceReferenceExpression && ((InferenceReferenceExpression) stuck).getVariable() != null ? ((InferenceReferenceExpression) stuck).getVariable() : null;
   }
 
-  public InferenceVariable getInferenceVariable() {
+  public InferenceVariable getInferenceVariable(boolean allowSubst) {
     Expression expr = this;
     while (true) {
-      expr = expr.cast(InferenceReferenceExpression.class);
-      if (expr == null) {
+      expr = expr.getUnderlyingExpression();
+      if (allowSubst && expr instanceof SubstExpression substExpr) {
+        expr = substExpr.getExpression().getUnderlyingExpression();
+      }
+      if (!(expr instanceof InferenceReferenceExpression refExpr)) {
         return null;
       }
-      InferenceVariable var = ((InferenceReferenceExpression) expr).getVariable();
+      InferenceVariable var = refExpr.getVariable();
       if (var != null) {
         return var;
       }
-      expr = ((InferenceReferenceExpression) expr).getSubstExpression();
+      expr = refExpr.getSubstExpression();
       if (expr == null) {
         return null;
       }
     }
   }
 
+  public InferenceVariable getInferenceVariable() {
+    return getInferenceVariable(false);
+  }
+
   @Override
   public boolean computeMatchedConstructorsWithDataArguments(List<? super ConstructorWithDataArguments> result) {
     return false;

diff --git a/base/src/main/java/org/arend/core/expr/visitor/CompareVisitor.java b/base/src/main/java/org/arend/core/expr/visitor/CompareVisitor.java
@@ -253,8 +253,8 @@ public boolean normalizedCompare(Expression expr1, Expression expr2, Expression
       }
     }
 
-    InferenceVariable stuckVar1 = expr1.getInferenceVariable();
-    InferenceVariable stuckVar2 = expr2.getInferenceVariable();
+    InferenceVariable stuckVar1 = expr1.getInferenceVariable(true);
+    InferenceVariable stuckVar2 = expr2.getInferenceVariable(true);
     if (stuckVar1 != null || stuckVar2 != null) {
       if (!(myNormalCompare && myEquations.addEquation(expr1, substitute(expr2), type, myCMP, stuckVar1 != null ? stuckVar1.getSourceNode() : stuckVar2.getSourceNode(), stuckVar1, stuckVar2))) {
         initResult(expr1, expr2);