From d96bf8a633ab684773407f603ebac93d258d96e6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 1 Sep 2022 06:06:03 -0700
Subject: [PATCH] chore: restore accidentally deleted test

https://github.com/leanprover/lean4/commit/25447af13cd069a39cf75cd0390122a41df20d4d
---
 tests/lean/run/1547.lean | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 tests/lean/run/1547.lean

diff --git a/tests/lean/run/1547.lean b/tests/lean/run/1547.lean
new file mode 100644
index 0000000000..1f784d4793
--- /dev/null
+++ b/tests/lean/run/1547.lean
@@ -0,0 +1,4 @@
+def foo (x : {_ : Unit} → StateM Nat Nat) : Nat :=
+  (@x () 0).1
+
+def bar := foo (return 42)