Merge PR #11579: Remove ad-hoc treatment of inductive parameters in implicit arguments

Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: herbelin

4 files changed, 38 insertions, 2 deletions

diff --git a/test-suite/bugs/closed/bug_11585.v b/test-suite/bugs/closed/bug_11585.v
new file mode 100644
index 0000000000..6294668323
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11585.v
@@ -0,0 +1,3 @@
+Fail Inductive type {type : Type} : Type := T : type.
+
+Inductive type {type : Type} : Type := T .
diff --git a/test-suite/bugs/closed/bug_5233.v b/test-suite/bugs/closed/bug_5233.v
index 06286c740d..63e33b63f7 100644
--- a/test-suite/bugs/closed/bug_5233.v
+++ b/test-suite/bugs/closed/bug_5233.v
@@ -1,2 +1,5 @@
 (* Implicit arguments on type were missing for recursive records *)
 Inductive foo {A : Type} : Type := { Foo : foo }.
+
+(* Implicit arguments can be overidden *)
+Inductive bar {A : Type} : Type := { Bar : @bar (A*A) }.
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
index ff2556c5dc..e6c2806433 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -1,6 +1,10 @@
 The command has indeed failed with message:
-Last occurrence of "list'" must have "A" as 1st argument in
- "A -> list' A -> list' (A * A)%type".
+In environment
+list' : Set -> Set
+A : Set
+a : A
+l : list' A
+Unable to unify "list' (A * A)%type" with "list' A".
 Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=  Foo : foo A x
 
 Arguments foo _%type_scope
diff --git a/test-suite/success/InductiveVsImplicitsVsTC.v b/test-suite/success/InductiveVsImplicitsVsTC.v
new file mode 100644
index 0000000000..a98de32b70
--- /dev/null
+++ b/test-suite/success/InductiveVsImplicitsVsTC.v
@@ -0,0 +1,26 @@
+Module NoConv.
+  Class C := {}.
+
+  Definition useC {c:C} := nat.
+
+  Inductive foo {a b : C} := CC : useC -> foo.
+  (* If TC search runs before parameter unification it will pick the
+     wrong instance for the first parameter.
+
+     useC makes sure we don't completely skip TC search.
+   *)
+End NoConv.
+
+Module ForConv.
+
+  Class Bla := { bla : Type }.
+
+  Instance bli : Bla := { bla := nat }.
+
+  Inductive vs := C : forall x : bla, x = 2 -> vs.
+  (* here we need to resolve TC to pass the conversion problem if we
+     combined with the previous example it would fail as TC resolution
+     for conversion is unrestricted and so would resolve the
+     conclusion too early. *)
+
+End ForConv.