From 95c511a8a380a3a9229a654abd1565baaacead93 Mon Sep 17 00:00:00 2001 From: valis Date: Thu, 21 Mar 2024 11:00:51 +0300 Subject: [PATCH] Fix a bug with coelim in lemmas --- .../typechecking/visitor/DefinitionTypechecker.java | 5 ++++- src/test/java/org/arend/classes/RecordsTest.java | 10 ++++++++++ 2 files changed, 14 insertions(+), 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 index d53dca550..502d11bde 100644 --- 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 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 pseudoImplemented = new HashSet<>(); diff --git a/src/test/java/org/arend/classes/RecordsTest.java b/src/test/java/org/arend/classes/RecordsTest.java index b977ed764..f5c82cb17 100644 --- 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")))); + } }