1 files changed, 29 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_9294.v b/test-suite/bugs/closed/bug_9294.v
new file mode 100644
index 0000000000..a079d672d3
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9294.v
@@ -0,0 +1,29 @@
+Set Printing Universes.
+
+Inductive Foo@{i} (A:Type@{i}) : Type := foo : (Set:Type@{i}) -> Foo A.
+Arguments foo {_} _.
+Print Universes Subgraph (Foo.i).
+Definition bar : Foo True -> Set := fun '(foo x) => x.
+
+Definition foo_bar (n : Foo True) : foo (bar n) = n.
+Proof. destruct n;reflexivity. Qed.
+
+Definition bar_foo (n : Set) : bar (foo n) = n.
+Proof. reflexivity. Qed.
+
+Require Import Hurkens.
+
+Inductive box (A : Set) : Prop := Box : A -> box A.
+
+Definition Paradox : False.
+Proof.
+Fail unshelve refine (
+  NoRetractFromSmallPropositionToProp.paradox
+  (Foo True)
+  (fun A => foo A)
+  (fun A => box (bar A))
+  _
+  _
+  False
+).
+Abort.