From 01f21bdbd6175131393f47b1f60b2996e94b6698 Mon Sep 17 00:00:00 2001
From: valis <valery.isaev@gmail.com>
Date: Thu, 31 Aug 2023 17:28:14 +0200
Subject: [PATCH] Fix a bug with scopes in patterns

---
 .../org/arend/naming/scope/ScopeFactory.java   | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/base/src/main/java/org/arend/naming/scope/ScopeFactory.java b/base/src/main/java/org/arend/naming/scope/ScopeFactory.java
index 975a4c704..156b37c98 100644
--- a/base/src/main/java/org/arend/naming/scope/ScopeFactory.java
+++ b/base/src/main/java/org/arend/naming/scope/ScopeFactory.java
@@ -349,6 +349,24 @@ public static Scope forSourceNode(Scope parentScope, Abstract.SourceNode sourceN
       return new PatternScope(parentScope, ((Abstract.Clause) parentSourceNode).getPatterns());
     }
 
+    // Extend the scope with previous patterns for the type in a pattern
+   if (sourceNode instanceof Abstract.Expression && parentSourceNode instanceof Abstract.Pattern) {
+     Abstract.SourceNode parentParentSourceNode = parentSourceNode.getParentSourceNode();
+     List<? extends Abstract.Pattern> patterns = parentParentSourceNode instanceof Abstract.Clause clause ? clause.getPatterns() : parentParentSourceNode instanceof Abstract.Pattern pattern ? pattern.getSequence() : Collections.emptyList();
+     if (!patterns.isEmpty()) {
+       List<Abstract.Pattern> newPatterns = new ArrayList<>(patterns.size());
+       for (Abstract.Pattern pattern : patterns) {
+         if (pattern == parentSourceNode) {
+           break;
+         }
+         newPatterns.add(pattern);
+       }
+       if (!newPatterns.isEmpty()) {
+         return new PatternScope(parentScope, newPatterns);
+       }
+     }
+   }
+
     return parentScope;
   }
 }