diff --git a/base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java b/base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java index 9b81ce7d4..3eb5594b8 100644 --- a/base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java +++ b/base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java @@ -1333,20 +1333,25 @@ private TypecheckingResult typecheckClassExt(List(definition,classFieldImpl)); + boolean ok = true; if (definition instanceof ClassField) { if (baseClass.getFields().contains(definition)) { defined.add((ClassField) definition); } else { errorReporter.report(new IncorrectImplementationError((ClassField) definition, baseClass, classFieldImpl)); + ok = false; } } else if (definition instanceof ClassDefinition) { if (baseClass.isSubClassOf((ClassDefinition) definition)) { defined.addAll(((ClassDefinition) definition).getFields()); } else { errorReporter.report(new IncorrectImplementationError((ClassDefinition) definition, baseClass, classFieldImpl)); + ok = false; } } + if (ok) { + implementations.add(new Pair<>(definition, classFieldImpl)); + } } }