From fafc731885f84656ec884d40b843aa62a5991025 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 30 Mar 2020 13:34:17 +0200 Subject: Include review suggestions --- .../11579-inductive-params.rst | 11 +++++--- pretyping/pretyping.mli | 7 +++++ test-suite/success/InductiveVsImplicitsVsTC.v | 30 +++++++++++++++++----- 3 files changed, 37 insertions(+), 11 deletions(-) diff --git a/doc/changelog/02-specification-language/11579-inductive-params.rst b/doc/changelog/02-specification-language/11579-inductive-params.rst index 75358ab4ad..28bc8e9592 100644 --- a/doc/changelog/02-specification-language/11579-inductive-params.rst +++ b/doc/changelog/02-specification-language/11579-inductive-params.rst @@ -1,4 +1,7 @@ -- **Changed:** - Treatment of implicit inductive parameters in inductive declarations is less adhoc. - (`#11579 `_, - by Maxime Dénès, Gaëtan Gilbert and Jasper Hugunin). +- **Fixed:** + More robust and expressive treatment of implicit inductive + parameters in inductive declarations (`#11579 + `_, by Maxime Dénès, Gaëtan + Gilbert and Jasper Hugunin; fixes `#7253 + `_ and `#11585 + `_) diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 3396c5a0e7..8be7b1477b 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -45,6 +45,13 @@ type typing_constraint = | WithoutTypeConstraint (** A term of unknown expected type *) type use_typeclasses = NoUseTC | UseTCForConv | UseTC +(** Typeclasses are used in 2 ways: + +- through the "Typeclass Resolution For Conversion" option, if a + conversion problem fails we try again after resolving typeclasses + (UseTCForConv and UseTC) +- after pretyping we resolve typeclasses (UseTC) (in [solve_remaining_evars]) +*) type inference_flags = { use_typeclasses : use_typeclasses; diff --git a/test-suite/success/InductiveVsImplicitsVsTC.v b/test-suite/success/InductiveVsImplicitsVsTC.v index 9b787867fc..a98de32b70 100644 --- a/test-suite/success/InductiveVsImplicitsVsTC.v +++ b/test-suite/success/InductiveVsImplicitsVsTC.v @@ -1,10 +1,26 @@ -Class C := {}. +Module NoConv. + Class C := {}. -Definition useC {c:C} := nat. + 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. + 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. -*) + 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. -- cgit v1.2.3