From 18880888d56b3f5f1e69ddadb7aadf02b0c56401 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Tue, 12 Jun 2018 11:35:08 +0200
Subject: Test file for #7723

---
 test-suite/bugs/closed/7723.v | 58 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 58 insertions(+)
 create mode 100644 test-suite/bugs/closed/7723.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/7723.v b/test-suite/bugs/closed/7723.v
new file mode 100644
index 000000000..216290123
--- /dev/null
+++ b/test-suite/bugs/closed/7723.v
@@ -0,0 +1,58 @@
+Set Universe Polymorphism.
+
+Module Segfault.
+
+Inductive decision_tree : Type := .
+
+Fixpoint first_satisfying_helper {A B} (f : A -> option B) (ls : list A) : option B
+  := match ls with
+     | nil => None
+     | cons x xs
+       => match f x with
+          | Some v => Some v
+          | None => first_satisfying_helper f xs
+          end
+     end.
+
+Axiom admit : forall {T}, T.
+Definition dtree4 : option decision_tree :=
+  match first_satisfying_helper (fun pat : nat => Some pat) (cons 0 nil)
+  with
+  | Some _ => admit
+  | None => admit
+  end
+.
+Definition dtree'' := Eval vm_compute in dtree4. (* segfault *)
+
+End Segfault.
+
+Module OtherExample.
+
+Definition bar@{i} := Type@{i}.
+Definition foo@{i j} (x y z : nat) :=
+  @id Type@{j} bar@{i}.
+Eval vm_compute in foo.
+
+End OtherExample.
+
+Module LocalClosure.
+
+Definition bar@{i} := Type@{i}.
+
+Definition foo@{i j} (x y z : nat) :=
+  @id (nat -> Type@{j}) (fun _ => Type@{i}).
+Eval vm_compute in foo.
+
+End LocalClosure.
+
+Require Import Hurkens.
+Polymorphic Inductive unit := tt.
+
+Polymorphic Definition foo :=
+  let x := id tt in (x, x, Type).
+
+Lemma bad : False.
+  refine (TypeNeqSmallType.paradox (snd foo) _).
+  vm_compute.
+  Fail reflexivity.
+Abort.
-- 
cgit v1.2.3