From 86aaf0dea3d187f3ae58a073a93e299617666e42 Mon Sep 17 00:00:00 2001
From: valis <valery.isaev@gmail.com>
Date: Fri, 4 Oct 2024 17:22:34 +0300
Subject: [PATCH] Refactor metric spaces

---
 .../org/arend/core/expr/visitor/CompareVisitor.java    | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

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
index f3b532d4f..eff9e28a9 100644
--- a/base/src/main/java/org/arend/core/expr/visitor/CompareVisitor.java
+++ b/base/src/main/java/org/arend/core/expr/visitor/CompareVisitor.java
@@ -1142,7 +1142,15 @@ private Boolean checkDefCallAndApp(Expression expr1, Expression expr2, boolean c
       TypeClassInferenceVariable variable;
       FieldCallExpression fieldCall = funNorm.cast(FieldCallExpression.class);
       if (fieldCall != null) {
-        InferenceVariable infVar = fieldCall.getArgument().getInferenceVariable();
+        while (true) {
+          funNorm = myNormalCompare ? fieldCall.getArgument().normalize(NormalizationMode.WHNF) : fieldCall.getArgument();
+          if (funNorm instanceof FieldCallExpression) {
+            fieldCall = (FieldCallExpression) funNorm;
+          } else {
+            break;
+          }
+        }
+        InferenceVariable infVar = funNorm.getInferenceVariable();
         variable = infVar instanceof TypeClassInferenceVariable ? (TypeClassInferenceVariable) infVar : null;
       } else {
         variable = null;