[ #5584 ] test case

closes #5584 which was a the same problem as #5544
agda · Nov 18, 2021 · 058e350 · 058e350
1 parent 4173fd6
commit 058e350
Showing 1 changed file with 19 additions and 0 deletions.
diff --git a/test/Succeed/Issue5584.agda b/test/Succeed/Issue5584.agda
@@ -0,0 +1,19 @@
+
+open import Agda.Builtin.Sigma
+
+dup : ∀ {A : Set} → A → Σ A λ _ → A
+dup x = x , x
+
+postulate
+  A : Set
+
+module M {x : A} where
+  y = x
+
+data X : Set where
+  mkX : ∀ {x : A}
+    → let
+        (_ , _) = dup x
+        open M {x}
+      in
+      X