Fix a bug with \case \elim

JetBrains · Nov 11, 2024 · fc01f9e · fc01f9e
1 parent 86aaf0d
commit fc01f9e
Show file tree

Hide file tree

Showing 4 changed files with 166 additions and 137 deletions.
diff --git a/base/src/main/java/org/arend/typechecking/error/local/IdpPatternError.java b/base/src/main/java/org/arend/typechecking/error/local/IdpPatternError.java
@@ -37,7 +37,7 @@ public static String subst(String substVar, String paramVar, String freeVar) {
   }
 
   public static String noParameter() {
-    return "One of the sides in the expected type should be a variable";
+    return "One of the sides in the expected type should be a parameter";
   }
 
   @Override

diff --git a/base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java b/base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java
@@ -4016,11 +4016,8 @@ public TypecheckingResult visitCase(Concrete.CaseExpression expr, Expression exp
         list.append(link);
         if (caseArg.isElim) {
           if (argTypeExpr != null) {
-            Expression actualArgType = exprResult.type.subst(substitution);
-            if (!CompareVisitor.compare(myEquations, CMP.EQ, actualArgType, argTypeExpr, Type.OMEGA, caseArg.type)) {
-              errorReporter.report(new TypeMismatchError(actualArgType, argTypeExpr, caseArg.expression));
-              return null;
-            }
+            errorReporter.report(new TypecheckingError("Explicit type annotation is not allowed with \\elim", caseArg.expression));
+            return null;
           }
           Binding origBinding = ((ReferenceExpression) exprResult.expression).getBinding();
           origElimBindings.put(asRef, origBinding);

diff --git a/src/test/java/org/arend/typechecking/constructions/ArrayTest.java b/src/test/java/org/arend/typechecking/constructions/ArrayTest.java
@@ -425,7 +425,7 @@ public void casePatternMatchingTest5() {
   public void casePatternMatchingTest6() {
     typeCheckModule("""
       \\func test {A : \\Set} {n : Nat} (l : Array A n) : Nat
-        => \\case \\elim n, \\elim l : Array A n \\with {
+        => \\case \\elim n, l : Array A n \\with {
           | 0, nil => 0
           | suc n, a :: l => 1
         }