Fix a bug with default dependencies

JetBrains · May 25, 2024 · 53aa4e6 · 53aa4e6
1 parent adb0744
commit 53aa4e6
Showing 1 changed file with 7 additions and 10 deletions.
diff --git a/base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java b/base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java
@@ -3012,17 +3012,7 @@ protected Void forDependencies(ClassDefinition unit) {
     }
 
     for (ClassDefinition superClass : typedDef.getSuperClasses()) {
-      Set<ClassField> added = new HashSet<>();
-      for (Map.Entry<ClassField, Pair<AbsExpression, Boolean>> entry : superClass.getDefaults()) {
-        Levels levels = typedDef.getSuperLevels().get(superClass);
-        if (typedDef.addDefaultIfAbsent(entry.getKey(), entry.getValue().proj1.subst(new ExprSubstitution(), levels == null ? idLevels.makeSubstitution(superClass) : levels.makeSubstitution(superClass)), entry.getValue().proj2)) {
-          added.add(entry.getKey());
-        }
-      }
       for (Map.Entry<ClassField, Set<ClassField>> entry : superClass.getDefaultDependencies().entrySet()) {
-        if (!added.contains(entry.getKey())) {
-          continue;
-        }
         Set<ClassField> dependencies = entry.getValue();
         if (!typedDef.getDefaults().isEmpty()) {
           Set<ClassField> newDependencies = new HashSet<>();
@@ -3037,6 +3027,13 @@ protected Void forDependencies(ClassDefinition unit) {
         }
         typedDef.addDefaultDependencies(entry.getKey(), dependencies);
       }
+      Set<ClassField> added = new HashSet<>();
+      for (Map.Entry<ClassField, Pair<AbsExpression, Boolean>> entry : superClass.getDefaults()) {
+        Levels levels = typedDef.getSuperLevels().get(superClass);
+        if (typedDef.addDefaultIfAbsent(entry.getKey(), entry.getValue().proj1.subst(new ExprSubstitution(), levels == null ? idLevels.makeSubstitution(superClass) : levels.makeSubstitution(superClass)), entry.getValue().proj2)) {
+          added.add(entry.getKey());
+        }
+      }
       for (Map.Entry<ClassField, Set<ClassField>> entry : superClass.getDefaultImplDependencies().entrySet()) {
         if (added.contains(entry.getKey())) {
           typedDef.addDefaultImplDependencies(entry.getKey(), entry.getValue());