From fb4978ce2cf0a2d4fc871d5d739eda8618a5184b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 30 Oct 2018 00:10:50 +0100
Subject: Fix #8364: making univ algebraic when already equal to another.

When making a universe a variable we iterate through the universes
we're equal to and if we find one we update the substitution
accordingly.

NB: The bug called make_flexible_variable on Top.15 and
~~~
   {Top.15 Top.14} |= Top.11 < Top.6
                      Top.14 < Top.5
                      Top.11 = Top.15

  ALGEBRAIC UNIVERSES:{Top.17 Top.16}
  UNDEFINED UNIVERSES:Top.17 := Top.14+1
                      Top.16 := Top.14+1
  WEAK CONSTRAINTS:
~~~
so now we would add [Top.15 := Top.11].
---
 test-suite/bugs/closed/bug_8364.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_8364.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_8364.v b/test-suite/bugs/closed/bug_8364.v
new file mode 100644
index 0000000000..10f955b41f
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8364.v
@@ -0,0 +1,17 @@
+Unset Primitive Projections.
+
+Record Box (A:Type) := box { unbox : A }.
+Arguments box {_} _. Arguments unbox {_} _.
+
+Definition map {A B} (f:A -> B) x :=
+  match x with box x => box (f x) end.
+
+Definition tuple (l : Box Type) : Type :=
+  match l with
+  | box x => x
+  end.
+
+Fail Inductive stack : Type -> Type :=
+| Stack T foos :
+  tuple (map stack foos) ->
+  stack T.
-- 
cgit v1.2.3