Fix tests

JetBrains · Jun 24, 2024 · ef50df8 · ef50df8
1 parent 3540f92
commit ef50df8
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java b/base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java
@@ -1950,7 +1950,7 @@ private List<ExtElimClause> typecheckFunctionBody(FunctionDefinition typedDef, C
           }
           index++;
         }
-      } else {
+      } else if (!expectedType.isError()) {
         errorReporter.report(new CertainTypecheckingError(CertainTypecheckingError.Kind.INSTANCE_TYPE, def));
       }
     } else if (kind == FunctionKind.TYPE) {