Fix a bug with lambda expressions

JetBrains · Sep 20, 2023 · 335f82d · 335f82d
1 parent 3e4a000
commit 335f82d
Showing 1 changed file with 16 additions and 0 deletions.
diff --git a/base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java b/base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java
@@ -2457,6 +2457,22 @@ private TypecheckingResult visitLam(List<? extends Concrete.Parameter> parameter
                 prevLink = prevLink.getNext();
               }
               prevLink.setNext(EmptyDependentLink.getInstance());
+              prevLink = link;
+              while (prevLink.getNext().hasNext()) {
+                prevLink = prevLink.getNext();
+              }
+              if (prevLink instanceof UntypedDependentLink) {
+                TypedSingleDependentLink lastLink = new TypedSingleDependentLink(prevLink.isExplicit(), prevLink.getName(), actualLink.getType(), prevLink.isHidden());
+                if (prevLink == link) {
+                  link = lastLink;
+                } else {
+                  DependentLink prevPrevLink = link;
+                  while (prevPrevLink.getNext() != prevLink) {
+                    prevPrevLink = prevPrevLink.getNext();
+                  }
+                  prevPrevLink.setNext(lastLink);
+                }
+              }
               return new Pair<>(new TypecheckingResult(new LamExpression(sort, link, result.expression), new PiExpression(sort, link, result.type)), true);
             }
           }