From a9399d9b498025b27fc381c3a21aa748cf510b1d Mon Sep 17 00:00:00 2001
From: valis <valery.isaev@gmail.com>
Date: Thu, 18 Apr 2024 19:24:28 +0300
Subject: [PATCH] Fix a bug in ClassCallExpression

---
 .../arend/core/expr/ClassCallExpression.java  |  9 ++++++--
 .../visitor/DefinitionTypechecker.java        | 21 +++++++++++++++++--
 2 files changed, 26 insertions(+), 4 deletions(-)

diff --git a/base/src/main/java/org/arend/core/expr/ClassCallExpression.java b/base/src/main/java/org/arend/core/expr/ClassCallExpression.java
index 443c1f6ba..e6f0b015e 100644
--- a/base/src/main/java/org/arend/core/expr/ClassCallExpression.java
+++ b/base/src/main/java/org/arend/core/expr/ClassCallExpression.java
@@ -387,9 +387,14 @@ public Expression visitFieldCall(FieldCallExpression expr, Void params) {
             }
           }
 
-          // TODO: This is a workaround for ClassParametersTest.classFieldParametersTest
           Expression arg = expr.getArgument().getUnderlyingExpression();
-          return arg instanceof ReferenceExpression && ((ReferenceExpression) arg).getBinding() == thisBinding && !newExpr.getClassCall().isImplemented(expr.getDefinition()) ? expr : FieldCallExpression.make(expr.getDefinition(), expr.getArgument().accept(this, null));
+          if (arg instanceof ReferenceExpression && ((ReferenceExpression) arg).getBinding() == thisBinding) {
+            Expression fieldImpl = newExpr.getClassCall().myImplementations.get(field);
+            if (fieldImpl != null) {
+              return expr.subst(myThisBinding, newExpr).accept(this, null);
+            }
+          }
+          return super.visitFieldCall(expr, null);
         }
 
         @Override
diff --git a/base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java b/base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java
index 68b5cf015..3150b14d9 100644
--- a/base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java
+++ b/base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java
@@ -3386,8 +3386,25 @@ private ClassField typecheckClassField(Concrete.BaseClassField def, ClassDefinit
           ok = false;
         }
       }
-      if (newDef) {
-        overrideField(typedDef, ok ? piType : new PiExpression(piType.getResultSort(), piType.getParameters(), new ErrorExpression()), parentClass, def);
+      if (ok) {
+        Set<ClassField> allowedFields = new HashSet<>();
+        for (ClassField field : parentClass.getNotImplementedFields()) {
+          if (field == typedDef) {
+            break;
+          }
+          allowedFields.add(field);
+        }
+        if (piType.accept(new SearchVisitor<Void>() {
+          @Override
+          protected CoreExpression.FindAction processDefCall(DefCallExpression expression, Void param) {
+            return expression.getDefinition() instanceof ClassField field && parentClass.isSubClassOf(field.getParentClass()) && !allowedFields.contains(field) && !parentClass.isImplemented(field) ? CoreExpression.FindAction.STOP : CoreExpression.FindAction.CONTINUE;
+          }
+        }, null)) {
+          ok = false;
+        }
+      }
+      if (newDef && ok) {
+        overrideField(typedDef, piType, parentClass, def);
       }
       if (!ok) {
         return null;