Have implicit arguments with "Asymmetric Patterns"

dev/ci/user-overlays/21947-proux01-asymmetric-patterns-no-implicits.sh

@@ -0,0 +1,15 @@
+overlay aac_tactics https://github.com/rocq-community/aac-tactics rocq21947 21947
+overlay atbr https://github.com/rocq-community/atbr rocq21947 21947
+overlay ext_lib https://github.com/coq-community/coq-ext-lib rocq21947 21947
+overlay equations https://github.com/proux01/Coq-Equations rocq21947 21947
+overlay fiat_crypto https://github.com/proux01/fiat-crypto rocq21947 21947
+overlay fiat_crypto_legacy https://github.com/proux01/fiat-crypto rocq21947-legacy 21947
+overlay fiat_parsers https://github.com/proux01/fiat rocq21947 21947
+overlay hott https://github.com/proux01/HoTT rocq21947 21947
+overlay kami https://github.com/proux01/kami rocq21947 21947
+overlay mathcomp https://github.com/proux01/math-comp rocq21947 21947
+overlay metarocq https://github.com/proux01/metarocq rocq21947 21947
+overlay relation_algebra https://github.com/proux01/relation-algebra rocq21947 21947
+overlay rewriter https://github.com/proux01/rewriter rocq21947 21947
+overlay stdlib https://github.com/proux01/stdlib rocq21947 21947
+overlay vst https://github.com/proux01/vst rocq21947 21947

doc/changelog/08-vernac-commands-and-options/21947-asymmetric-patterns-no-implicits-Changed.rst

@@ -0,0 +1,8 @@
+- **Changed:**
+  the bahavior of the :flag:`Asymmetric Patterns` flag, which no
+  longer disactivates implicit arguments in patterns. Set the
+  compatibility flag :flag:`Asymmetric Patterns No Implicits` to
+  retrieve the previous behavior
+  (`#21947 <https://github.com/rocq-prover/rocq/pull/21947>`_,
+  fixes `#21769 <https://github.com/rocq-prover/rocq/issues/21769>`_,
+  by Pierre Roux).

doc/sphinx/language/extensions/match.rst

@@ -664,6 +664,15 @@ When we use parameters in patterns there is an error message:
      end).
    Unset Asymmetric Patterns.
 
+.. flag:: Asymmetric Patterns No Implicits
+
+   This compatibility :term:`flag` (off by default) disactivates
+   implicit arguments in patterns when :flag:`Asymmetric Patterns` is
+   on, thus recovering the behavior of :flag:`Asymmetric Patterns`
+   before Rocq 9.3.
+
+   .. deprecated:: 9.3
+
 Implicit arguments in patterns
 ------------------------------
 

interp/constrextern.ml

@@ -307,18 +307,23 @@ let rec extern_cases_pattern_in_scope ~flags ((custom,(lev_after:int option)),sc
             | Some l -> CPatRecord l
             | None ->
                   let c = extern_reference vars (GlobRef.ConstructRef cstrsp) in
-                  if Constrintern.get_asymmetric_patterns () then
-                    if pattern_printable_in_both_syntax ~flags cstrsp
-                    then CPatCstr (c, None, args)
-                    else CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), [])
-                  else
-                    let full_args = add_patt_for_params (fst cstrsp) args in
+                  let full_args = add_patt_for_params (fst cstrsp) args in
+                  let drop n =
                     let tags = try Inductiveops.constructor_alltags (Global.env()) cstrsp
                       with _ when !Flags.in_debugger -> []
                     in
-                    match drop_implicits_in_patt ~flags (GlobRef.ConstructRef cstrsp) 0 ~tags full_args with
+                    let tags = List.skipn_at_best n tags in
+                    let args = List.skipn_at_best n full_args in
+                    match drop_implicits_in_patt ~flags (GlobRef.ConstructRef cstrsp) n ~tags args with
                       | Some true_args -> CPatCstr (c, None, true_args)
-                      | None           -> CPatCstr (c, Some full_args, [])
+                      | None           -> CPatCstr (c, Some full_args, []) in
+                  if Constrintern.get_asymmetric_patterns () then
+                    if pattern_printable_in_both_syntax ~flags cstrsp
+                    then CPatCstr (c, None, args)
+                    else if Constrintern.get_asymmetric_patterns_no_implicits ()
+                    then CPatCstr (c, Some full_args, [])
+                    else drop (Inductiveops.inductive_nparamdecls (Global.env()) (fst cstrsp))
+                  else drop 0
           in
           insert_pat_alias ?loc (CAst.make ?loc p) na
       in

interp/constrintern.ml

@@ -1776,6 +1776,13 @@ let { Goptions.get = get_asymmetric_patterns } =
     ~value:false
     ()
 
+let { Goptions.get = get_asymmetric_patterns_no_implicits } =
+  Goptions.declare_bool_option_and_ref
+    ~depr:(Deprecation.make ~since:"9.3" ())
+    ~key:["Asymmetric";"Patterns";"No";"Implicits"]
+    ~value:false
+    ()
+
 type global_reference_test = {
   for_ind : bool;
   test_kind : ?loc:Loc.t -> GlobRef.t -> unit
@@ -1853,7 +1860,7 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat =
     let loc = pt.loc in
     (* The two policies implied by asymmetric pattern mode *)
     let add_par_if_no_ntn_with_par = get_asymmetric_patterns () && not for_ind in
-    let no_impl = get_asymmetric_patterns () && not for_ind in
+    let no_impl = get_asymmetric_patterns_no_implicits () && get_asymmetric_patterns () && not for_ind in
     match pt.v with
     | CPatAlias (p, id) -> DAst.make ?loc @@ RCPatAlias (in_pat test_kind scopes p, id)
     | CPatRecord l ->

interp/constrintern.mli

@@ -251,6 +251,8 @@ val parsing_explicit : bool ref
 (** Placeholder for global option, should be moved to a parameter *)
 val get_asymmetric_patterns : unit -> bool
 
+val get_asymmetric_patterns_no_implicits : unit -> bool
+
 val check_duplicate : ?loc:Loc.t -> (qualid * constr_expr) list -> unit
 (** Check that a list of record field definitions doesn't contain
     duplicates. *)

test-suite/bugs/bug_11576.v

@@ -25,12 +25,11 @@ Existing Class rep.
 Fixpoint translate_func' (pv:=_) {t} (e : @expr ltype t)
   : for_each_lhs_of_arrow ltype t -> @cmd pv :=
   match e with
-  | Abs base d f =>
-    fun (args : _ * for_each_lhs_of_arrow _ d) =>
+  | Abs f =>
+    fun (args : _ * for_each_lhs_of_arrow _ _) =>
       translate_func' (f (fst args)) (snd args)
-  | Var base v =>
+  | Var v =>
     fun _ => translate_cmd (Var v)
-  | _ => fun _ => admit
   end.
 (* Used to be: File "./bug_01.v", line 30, characters 30-31:
 Error: Cannot infer this placeholder of type "parameters" (no type class

test-suite/bugs/bug_3045.v

@@ -19,14 +19,14 @@ Inductive ReifiedMorphism : forall objC (C : SpecializedCategory objC), C -> C -
 
 Fixpoint ReifiedMorphismDenote objC C s d (m : @ReifiedMorphism objC C s d) : Morphism C s d :=
   match m in @ReifiedMorphism objC C s d return Morphism C s d with
-    | ReifiedComposedMorphism _ _ _ _ _ m1 m2 => Compose (@ReifiedMorphismDenote _ _ _ _ m1)
+    | ReifiedComposedMorphism m1 m2 => Compose (@ReifiedMorphismDenote _ _ _ _ m1)
                                                          (@ReifiedMorphismDenote _ _ _ _ m2)
   end.
 
 Fixpoint ReifiedMorphismSimplifyWithProof objC C s d (m : @ReifiedMorphism objC C s d)
 : { m' : ReifiedMorphism C s d | ReifiedMorphismDenote m = ReifiedMorphismDenote m' }.
 refine match m with
-         | ReifiedComposedMorphism _ _ s0 d0 d0' m1 m2 => _
+         | ReifiedComposedMorphism m1 m2 => _
        end; clear m.
 (* This fails with an error rather than an anomaly, but morally
    it should work, if destruct were able to do the good generalization

test-suite/bugs/bug_3262.v

@@ -21,7 +21,7 @@ Section hlist.
                                  | l :: _ => F l
                                end with
       | Hnil => tt
-      | Hcons _ _ x _ => x
+      | Hcons x _ => x
     end.
 
   Definition hlist_tl {a b} (hl : hlist (a :: b)) : hlist b :=
@@ -30,7 +30,7 @@ Section hlist.
                                  | _ :: ls => hlist ls
                                end with
       | Hnil => tt
-      | Hcons _ _ _ x => x
+      | Hcons _ x => x
     end.
 
   Lemma hlist_eta : forall ls (h : hlist ls),

test-suite/bugs/bug_3732.v

@@ -34,8 +34,8 @@ Section machine.
 
   Fixpoint subst G (p : propX G) : (last G -> PropX) -> propX (eatLast G) :=
     match p with
-      | Inj _ P => fun _ => Inj P
-      | ExistsX G A p1 => fun p' =>
+      | Inj P => fun _ => Inj P
+      | @ExistsX G A p1 => fun p' =>
                             match G return propX (A :: G) -> propX (eatLast (A :: G)) -> propX (eatLast G) with
                               | nil => fun p1 _ => ExistsX p1
                               | cons _ _ => fun _ rc => ExistsX rc

test-suite/bugs/bug_4001.v

@@ -14,5 +14,5 @@ Inductive t : list A -> Type :=
 Definition car (x:A) (lx : list A) (s: t (x::lx)) : typ x :=
   match s in t l'  with
   | snil => False
-  | scons _ e _ _ => e
+  | scons e _ => e
   end.

test-suite/bugs/bug_7916.v

@@ -53,7 +53,7 @@ Module MathComp.
    Local Coercion sort : type >-> Sortclass.
    Variables (T : Type) (cT : type).
 
-   Definition class := let: Pack _ c := cT return class_of cT in c.
+   Definition class := let: Pack c := cT return class_of cT in c.
 
    End ClassDef.
    Coercion sort : type >-> Sortclass.

test-suite/output/Cases.out

@@ -231,19 +231,22 @@ File "./output/Cases.v", line 279, characters 33-39:
 The command has indeed failed with message:
 The constructor cons (in type list) is expected to be applied to 2 arguments
 while it is actually applied to 1 argument.
-File "./output/Cases.v", line 281, characters 33-39:
-The command has indeed failed with message:
-The constructor D' (in type J') is expected to be applied to 3 arguments (or
-4 arguments when including variables for local definitions) while it is
-actually applied to 2 arguments.
+fun x : J' ?T ?p => match x with
+                    | D' _ _ _ => 0
+                    end
+     : J' ?T ?p -> nat
+where
+?T : [x : J' ?T ?p |- Type] (x cannot be used)
+?T0 : [x : J' ?T ?p |- Type] (x cannot be used)
+?p : [x : J' ?T ?p |- (?T * ?T0)%type] (x cannot be used)
 File "./output/Cases.v", line 282, characters 33-45:
 The command has indeed failed with message:
-The constructor D' (in type J') is expected to be applied to 3 arguments (or
-4 arguments when including variables for local definitions) while it is
+The constructor D' (in type J') is expected to be applied to 2 arguments (or
+3 arguments when including variables for local definitions) while it is
 actually applied to 5 arguments.
 fun x : J' bool (true, true) =>
 match x with
-| @D' _ _ _ _ _ m _ e => existT (fun x0 : nat => x0 = x0) m e
+| D' m _ e => existT (fun x0 : nat => x0 = x0) m e
 end
      : J' bool (true, true) -> {x : nat & x = x}
 fun x : J' bool (true, true) =>

test-suite/output/Cases.v

@@ -278,10 +278,10 @@ Fail Check fun x => match x with (y,z) w => y+z+w end.
 Fail Check fun x => match x with cons y z w => 0 | nil => 0 end.
 Fail Check fun x => match x with cons y => 0 | nil => 0 end.
 
-Fail Check fun x => match x with D' n _ => 0 end.
+Check fun x => match x with D' n _ => 0 end.
 Fail Check fun x => match x with D' n m p e _ => 0 end.
-Check fun x : J' bool (true,true) => match x with D' n m e => existT (fun x => eq x x) m e end.
-Check fun x : J' bool (true,true) => match x with D' n m p e => (n,p) end.
+Check fun x : J' bool (true,true) => match x with D' n e => existT (fun x => eq x x) _ e end.
+Check fun x : J' bool (true,true) => match x with D' n p e => (n,p) end.
 
 End ConstructorArgumentsNumber.
 

test-suite/output/PrintMatch.out

@@ -41,7 +41,7 @@ Arguments eq_sym [A]%_type_scope [x y] H
 eq_sym =
 fun (A : Type) (x y : A) (H : x = y) =>
 match H in _ = y0 return y0 = x with
-| @eq_refl _ _ => @eq_refl A x
+| eq_refl => @eq_refl A x
 end
      : forall [A : Type] [x y : A], x = y -> y = x
 

test-suite/prerequisite/ssr_mini_mathcomp.v

@@ -35,7 +35,7 @@ Structure type := Pack {sort; _ : class_of sort; _ : Type}.
 Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (cT : type).
 
-Definition class := let: Pack _ c _ := cT return class_of cT in c.
+Definition class := let: Pack c _ := cT return class_of cT in c.
 
 Definition pack c := @Pack T c T.
 Definition clone := fun c & cT -> T & phant_id (pack c) cT => pack c.
@@ -694,9 +694,9 @@ Local Coercion base : class_of >->  Equality.class_of.
 Structure type := Pack {sort; _ : class_of sort; _ : Type}.
 Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
+Definition class := let: Pack c _ as cT' := cT return class_of cT' in c.
 Definition clone c & phant_id class c := @Pack T c T.
-Let xT := let: Pack T _ _ := cT in T.
+Let xT := let: @Pack T _ _ := cT in T.
 Notation xclass := (class : class_of xT).
 
 Definition pack m :=
@@ -797,9 +797,9 @@ Local Coercion base : class_of >-> Choice.class_of.
 Structure type : Type := Pack {sort : Type; _ : class_of sort; _ : Type}.
 Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
+Definition class := let: Pack c _ as cT' := cT return class_of cT' in c.
 Definition clone c & phant_id class c := @Pack T c T.
-Let xT := let: Pack T _ _ := cT in T.
+Let xT := let: @Pack T _ _ := cT in T.
 Notation xclass := (class : class_of xT).
 
 Definition pack m :=
@@ -881,7 +881,7 @@ Structure subCountType : Type :=
   SubCountType {subCount_sort :> subType P; _ : mixin_of subCount_sort}.
 
 Coercion sub_countType (sT : subCountType) :=
-  Eval hnf in pack (let: SubCountType _ m := sT return mixin_of sT in m) id.
+  Eval hnf in pack (let: SubCountType m := sT return mixin_of sT in m) id.
 Canonical sub_countType.
 
 Definition pack_subCountType U :=
@@ -925,7 +925,7 @@ Section Mixins.
 Variable T : countType.
 
 Definition EnumMixin :=
-  let: Countable.Pack _ (Countable.Class _ m) _ as cT := T
+  let: Countable.Pack (Countable.Class _ m) _ as cT := T
     return forall e : seq cT, axiom e -> mixin_of cT in
   @Mixin (EqType _ _) m.
 
@@ -947,9 +947,9 @@ Local Coercion base : class_of >-> Choice.class_of.
 Structure type : Type := Pack {sort; _ : class_of sort; _ : Type}.
 Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
+Definition class := let: Pack c _ as cT' := cT return class_of cT' in c.
 Definition clone c & phant_id class c := @Pack T c T.
-Let xT := let: Pack T _ _ := cT in T.
+Let xT := let: @Pack T _ _ := cT in T.
 Notation xclass := (class : class_of xT).
 
 Definition pack b0 (m0 : mixin_of (EqType T b0)) :=
@@ -1016,7 +1016,7 @@ Definition pack_subFinType U :=
 Implicit Type sT : subFinType.
 
 Definition subFin_mixin sT :=
-  let: SubFinType _ m := sT return mixin_of (sub_eqType sT) in m.
+  let: SubFinType m := sT return mixin_of (sub_eqType sT) in m.
 
 Coercion subFinType_subCountType sT := @SubCountType _ _ sT (subFin_mixin sT).
 Canonical subFinType_subCountType.
@@ -1047,7 +1047,7 @@ Variable n : nat.
 
 Inductive ordinal : predArgType := Ordinal m of m < n.
 
-Coercion nat_of_ord i := let: Ordinal m _ := i in m.
+Coercion nat_of_ord i := let: @Ordinal m _ := i in m.
 
 Canonical ordinal_subType := [subType for nat_of_ord].
 Definition ordinal_eqMixin := Eval hnf in [eqMixin of ordinal by <:].

test-suite/success/Case22.v

@@ -100,5 +100,5 @@ Check fun x : {True}+{False} => match x with left _ => 0 | right _ => 1 end.
 Inductive expr {A} : A -> Type := intro : forall {n:nat} (a:A), n=n -> expr a.
 Check fun (x:expr true) => match x in expr n return n=n with intro _ _ => eq_refl end.
 Set Asymmetric Patterns.
-Check fun (x:expr true) => match x in expr n return n=n with intro _ a _ => eq_refl a end.
+Check fun (x:expr true) => match x in expr n return n=n with intro a _ => eq_refl a end.
 Unset Asymmetric Patterns.

theories/Corelib/Compat/Rocq92.v

@@ -16,3 +16,5 @@
 #[export] Set Warnings "-deprecated-since-9.3".
 
 #[export] Set Inline Abstract Subproof.
+
+#[export] Set Asymmetric Patterns No Implicits.