Fix a bug with coelim in lemmas

JetBrains · Mar 21, 2024 · 95c511a · 95c511a
1 parent da10a8b
commit 95c511a
Show file tree

Hide file tree

Showing 2 changed files with 14 additions 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
@@ -1235,7 +1235,10 @@ private Pair<Expression,ClassCallExpression> typecheckCoClauses(FunctionDefiniti
     Concrete.Expression resultType = def.getResultType();
     if (typedDef.isSFunc() || kind == FunctionKind.CONS) {
       TypecheckingResult typeResult = typechecker.finalCheckExpr(resultType, Type.OMEGA);
-      if (typeResult == null || !(typeResult.expression instanceof ClassCallExpression type)) {
+      if (typeResult == null) return null;
+      ClassCallExpression type = typeResult.expression.normalize(NormalizationMode.WHNF).cast(ClassCallExpression.class);
+      if (type == null) {
+        errorReporter.report(new TypeMismatchError(DocFactory.text("a classCall"), typeResult.expression, def.getResultType()));
         return null;
       }
       Set<ClassField> pseudoImplemented = new HashSet<>();

diff --git a/src/test/java/org/arend/classes/RecordsTest.java b/src/test/java/org/arend/classes/RecordsTest.java
@@ -429,4 +429,14 @@ public void comparisonTest() {
     assertFalse(CompareVisitor.compare(DummyEquations.getInstance(), CMP.EQ, expr1, expr2, Type.OMEGA, null));
     assertFalse(CompareVisitor.compare(DummyEquations.getInstance(), CMP.EQ, expr2, expr1, Type.OMEGA, null));
   }
+
+  @Test
+  public void lemmaCowithTest() {
+    typeCheckModule("""
+      \\record R (x : Nat) (p : x = x)
+      \\func S (n : Nat) => R n
+      \\lemma test : S 0 \\cowith
+      """, 1);
+    assertThatErrorsAre(Matchers.fieldsImplementation(false, Collections.singletonList(get("R.p"))));
+  }
 }