From 28ede181e2a39320fb95bb81e8f21ad7b0531ea0 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Sat, 7 Mar 2020 21:03:27 -0500
Subject: [PATCH] Compare with codomain even if it's not pi

---
 .../typechecking/subexpr/CorrespondedSubExprVisitor.java      | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/main/java/org/arend/typechecking/subexpr/CorrespondedSubExprVisitor.java b/src/main/java/org/arend/typechecking/subexpr/CorrespondedSubExprVisitor.java
index 54bf3f6e3..e9ede5f21 100644
--- a/src/main/java/org/arend/typechecking/subexpr/CorrespondedSubExprVisitor.java
+++ b/src/main/java/org/arend/typechecking/subexpr/CorrespondedSubExprVisitor.java
@@ -246,9 +246,9 @@ protected Pair<Expression, Concrete.Expression> visitParameter(Concrete.Paramete
       if (expression != null) return expression;
       Expression corePiCodomain = corePi.getCodomain();
       if (corePiCodomain instanceof PiExpression) corePi = (PiExpression) corePiCodomain;
-      else break;
+      else return codomain.accept(this, corePiCodomain);
     }
-    return codomain.accept(this, corePi);
+    return null;
   }
 
   @Nullable Pair<@NotNull Expression, Concrete.@NotNull Expression>