Merge PR coq#18432: Ltac2 typed notations

Reviewed-by: ppedrot
Ack-by: rlepigre
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

doc/changelog/06-Ltac2-language/18432-ltac2-typed-notation.rst

@@ -0,0 +1,10 @@
+- **Changed:**
+  Ltac2 are typechecked at declaration time by default.
+  This should produce better errors when a notation argument does not have the expected type
+  (e.g. wrong branch type in `match! goal`).
+  The previous behaviour of typechecking only the expansion result can be
+  recovered using :flag:`Ltac2 Typed Notations`. We believe there are no real
+  use cases for this, please report if you have any
+  (`#18432 <https://github.com/coq/coq/pull/18432>`_,
+  fixes `#17477 <https://github.com/coq/coq/issues/17477>`_,
+  by Gaëtan Gilbert).

doc/sphinx/proof-engine/ltac2.rst

@@ -1220,11 +1220,22 @@ Notations
    side (before the `:=`) defines the syntax to recognize and gives formal parameter
    names for the syntactic values.  :n:`@integer` is the level of the notation.
    When the notation is used, the values are substituted
-   into the right-hand side.  The right-hand side is typechecked when the notation is used,
-   not when it is defined.  In the following example, `x` is the formal parameter name and
+   into the right-hand side.  In the following example, `x` is the formal parameter name and
    `constr` is its :ref:`syntactic class<syntactic_classes>`.  `print` and `of_constr` are
    functions provided by Coq through `Message.v`.
 
+   .. flag:: Ltac2 Typed Notations
+
+      By default Ltac2 notations are typechecked at declaration time.
+      This assigns an expected type to notation arguments.
+
+      When a notation is declared with this flag unset, it is not
+      typechecked at declaration time and its expansion is typechecked
+      when it is used. This may allow slightly more flexible use of
+      the notation arguments at the cost of worse error messages when
+      incorrectly using the notation. It is not believed to be useful
+      in practice, please report any real use cases you find.
+
    .. todo "print" doesn't seem to pay attention to "Set Printing All"
 
    .. example:: Printing a :n:`@term`

doc/stdlib/index-list.html.template

@@ -717,6 +717,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Compat/Coq818.v
     theories/Compat/Coq819.v
     user-contrib/Ltac2/Compat/Coq818.v
+    user-contrib/Ltac2/Compat/Coq819.v
   </dd>
 
   <dt> <b>Array</b>:

plugins/ltac2/tac2entries.ml

@@ -674,7 +674,7 @@ let perform_notation syn st =
     | Some depr -> deprecated_ltac2_notation ~loc (syn.synext_tok, depr)
     in
     let map (na, e) =
-      ((CAst.make ?loc:e.loc @@ CPatVar na), e)
+      ((CAst.make ?loc:e.loc na), e)
     in
     let bnd = List.map map args in
     CAst.make ~loc @@ CTacSyn (bnd, syn.synext_kn)
@@ -721,16 +721,27 @@ let cache_synext_interp (local,kn,tac) =
 let open_synext_interp i o =
   if Int.equal i 1 then cache_synext_interp o
 
+let subst_notation_data subst = function
+  | Tac2env.UntypedNota body as n ->
+    let body' = Tac2intern.subst_rawexpr subst body in
+    if body' == body then n else UntypedNota body'
+  | TypedNota { nota_prms=prms; nota_argtys=argtys; nota_ty=ty; nota_body=body } as n ->
+    let body' = Tac2intern.subst_expr subst body in
+    let argtys' = Id.Map.Smart.map (subst_type subst) argtys in
+    let ty' = subst_type subst ty in
+    if body' == body && argtys' == argtys && ty' == ty then n
+    else TypedNota {nota_body=body'; nota_argtys=argtys'; nota_ty=ty'; nota_prms=prms}
+
 let subst_synext_interp (subst, (local,kn,tac as o)) =
-  let tac' = Tac2intern.subst_rawexpr subst tac in
+  let tac' = subst_notation_data subst tac in
   let kn' = Mod_subst.subst_kn subst kn in
   if kn' == kn && tac' == tac then o else
   (local, kn', tac')
 
 let classify_synext_interp (local,_,_) =
   if local then Dispose else Substitute
 
-let inTac2NotationInterp : (bool*KerName.t*raw_tacexpr) -> obj =
+let inTac2NotationInterp : (bool*KerName.t*Tac2env.notation_data) -> obj =
   declare_object {(default_object "TAC2-NOTATION-INTERP") with
      cache_function  = cache_synext_interp;
      open_function   = simple_open ~cat:ltac2_notation_cat open_synext_interp;
@@ -837,8 +848,8 @@ let register_notation_interpretation = function
     let abbr = { abbr_body = body; abbr_depr = deprecation } in
     Lib.add_leaf (inTac2Abbreviation id abbr)
   | Synext (local,kn,ids,body) ->
-    let body = Tac2intern.globalize ids body in
-    Lib.add_leaf (inTac2NotationInterp (local,kn,body))
+    let data = intern_notation_data ids body in
+    Lib.add_leaf (inTac2NotationInterp (local,kn,data))
 
 type redefinition = {
   redef_kn : ltac_constant;

plugins/ltac2/tac2env.ml

@@ -65,6 +65,15 @@ let ltac_state = Summary.ref empty_state ~name:"ltac2-state"
 
 let compiled_tacs = Summary.ref ~local:true ~name:"ltac2-compiled-state" KNmap.empty
 
+type notation_data =
+  | UntypedNota of raw_tacexpr
+  | TypedNota of {
+      nota_prms : int;
+      nota_argtys : int glb_typexpr Id.Map.t;
+      nota_ty : int glb_typexpr;
+      nota_body : glb_tacexpr;
+    }
+
 let ltac_notations = Summary.ref KNmap.empty ~stage:Summary.Stage.Synterp ~name:"ltac2-notations"
 
 let define_global kn e =

plugins/ltac2/tac2env.mli

@@ -95,8 +95,18 @@ val interp_alias : ltac_constant -> alias_data
 
 (** {5 Toplevel definition of notations} *)
 
-val define_notation : ltac_notation -> raw_tacexpr -> unit
-val interp_notation : ltac_notation -> raw_tacexpr
+(* no deprecation info: deprecation warning is emitted by the parser *)
+type notation_data =
+  | UntypedNota of raw_tacexpr
+  | TypedNota of {
+      nota_prms : int;
+      nota_argtys : int glb_typexpr Id.Map.t;
+      nota_ty : int glb_typexpr;
+      nota_body : glb_tacexpr;
+    }
+
+val define_notation : ltac_notation -> notation_data -> unit
+val interp_notation : ltac_notation -> notation_data
 
 (** {5 Name management} *)
 

plugins/ltac2/tac2expr.mli

@@ -89,41 +89,6 @@ type atom =
 | AtmInt of int
 | AtmStr of string
 
-(** Tactic expressions *)
-type raw_patexpr_r =
-| CPatVar of Name.t
-| CPatAtm of atom
-| CPatRef of ltac_constructor or_tuple or_relid * raw_patexpr list
-| CPatRecord of (ltac_projection or_relid * raw_patexpr) list
-| CPatCnv of raw_patexpr * raw_typexpr
-| CPatOr of raw_patexpr list
-| CPatAs of raw_patexpr * lident
-
-and raw_patexpr = raw_patexpr_r CAst.t
-
-type raw_tacexpr_r =
-| CTacAtm of atom
-| CTacRef of tacref or_relid
-| CTacCst of ltac_constructor or_tuple or_relid
-| CTacFun of raw_patexpr list * raw_tacexpr
-| CTacApp of raw_tacexpr * raw_tacexpr list
-| CTacSyn of (raw_patexpr * raw_tacexpr) list * KerName.t
-| CTacLet of rec_flag * (raw_patexpr * raw_tacexpr) list * raw_tacexpr
-| CTacCnv of raw_tacexpr * raw_typexpr
-| CTacSeq of raw_tacexpr * raw_tacexpr
-| CTacIft of raw_tacexpr * raw_tacexpr * raw_tacexpr
-| CTacCse of raw_tacexpr * raw_taccase list
-| CTacRec of raw_tacexpr option * raw_recexpr
-| CTacPrj of raw_tacexpr * ltac_projection or_relid
-| CTacSet of raw_tacexpr * ltac_projection or_relid * raw_tacexpr
-| CTacExt : ('a, _) Tac2dyn.Arg.tag * 'a -> raw_tacexpr_r
-
-and raw_tacexpr = raw_tacexpr_r CAst.t
-
-and raw_taccase = raw_patexpr * raw_tacexpr
-
-and raw_recexpr = (ltac_projection or_relid * raw_tacexpr) list
-
 (* We want to generate these easily in the Closed case, otherwise we
    could have the kn in the ctor_data_for_patterns type. Maybe still worth doing?? *)
 type ctor_indx =
@@ -180,6 +145,44 @@ type glb_tacexpr =
 | GTacExt : (_, 'a) Tac2dyn.Arg.tag * 'a -> glb_tacexpr
 | GTacPrm of ml_tactic_name
 
+(** Tactic expressions *)
+type raw_patexpr_r =
+| CPatVar of Name.t
+| CPatAtm of atom
+| CPatRef of ltac_constructor or_tuple or_relid * raw_patexpr list
+| CPatRecord of (ltac_projection or_relid * raw_patexpr) list
+| CPatCnv of raw_patexpr * raw_typexpr
+| CPatOr of raw_patexpr list
+| CPatAs of raw_patexpr * lident
+
+and raw_patexpr = raw_patexpr_r CAst.t
+
+type raw_tacexpr_r =
+| CTacAtm of atom
+| CTacRef of tacref or_relid
+| CTacCst of ltac_constructor or_tuple or_relid
+| CTacFun of raw_patexpr list * raw_tacexpr
+| CTacApp of raw_tacexpr * raw_tacexpr list
+| CTacSyn of (lname * raw_tacexpr) list * KerName.t
+| CTacLet of rec_flag * (raw_patexpr * raw_tacexpr) list * raw_tacexpr
+| CTacCnv of raw_tacexpr * raw_typexpr
+| CTacSeq of raw_tacexpr * raw_tacexpr
+| CTacIft of raw_tacexpr * raw_tacexpr * raw_tacexpr
+| CTacCse of raw_tacexpr * raw_taccase list
+| CTacRec of raw_tacexpr option * raw_recexpr
+| CTacPrj of raw_tacexpr * ltac_projection or_relid
+| CTacSet of raw_tacexpr * ltac_projection or_relid * raw_tacexpr
+| CTacExt : ('a, _) Tac2dyn.Arg.tag * 'a -> raw_tacexpr_r
+| CTacGlb of int * (lname * raw_tacexpr * int glb_typexpr option) list * glb_tacexpr * int glb_typexpr
+(** CTacGlb is essentially an expanded typed notation.
+    Arguments bound with Anonymous have no type constraint. *)
+
+and raw_tacexpr = raw_tacexpr_r CAst.t
+
+and raw_taccase = raw_patexpr * raw_tacexpr
+
+and raw_recexpr = (ltac_projection or_relid * raw_tacexpr) list
+
 (** {5 Parsing & Printing} *)
 
 type exp_level =

plugins/ltac2/tac2intern.ml

@@ -1079,6 +1079,25 @@ let warn_useless_record_with = CWarnings.create ~name:"ltac2-useless-record-with
         str "All the fields are explicitly listed in this record:" ++
         spc() ++ str "the 'with' clause is useless.")
 
+let expand_notation ?loc el kn =
+  match Tac2env.interp_notation kn with
+  | UntypedNota body ->
+    let el = List.map (fun (pat, e) -> CAst.map (fun na -> CPatVar na) pat, e) el in
+    let v = if CList.is_empty el then body else CAst.make ?loc @@ CTacLet(false, el, body) in
+    v
+  | TypedNota {nota_prms=prms; nota_argtys=argtys; nota_ty=ty; nota_body=body} ->
+    let argtys, el = List.fold_left_map (fun argtys (na,arg) ->
+        let argty, argtys = match na.CAst.v with
+          | Anonymous -> None, argtys
+          | Name id -> Some (Id.Map.get id argtys), Id.Map.remove id argtys
+        in
+        argtys ,(na, arg, argty))
+        argtys
+        el
+    in
+    assert (Id.Map.is_empty argtys);
+    CAst.make ?loc @@ CTacGlb (prms, el, body, ty)
+
 let rec intern_rec env tycon {loc;v=e} =
   let check et = check ?loc env tycon et in
   match e with
@@ -1175,8 +1194,7 @@ let rec intern_rec env tycon {loc;v=e} =
   if is_rec then intern_let_rec env el tycon e
   else intern_let env loc ids el tycon e
 | CTacSyn (el, kn) ->
-  let body = Tac2env.interp_notation kn in
-  let v = if CList.is_empty el then body else CAst.make ?loc @@ CTacLet(false, el, body) in
+  let v = expand_notation ?loc el kn in
   intern_rec env tycon v
 | CTacCnv (e, tc) ->
   let tc = intern_type env tc in
@@ -1306,6 +1324,28 @@ let rec intern_rec env tycon {loc;v=e} =
   | GlbTacexpr e -> e
   in
   check (e, tpe)
+| CTacGlb (prms, args, body, ty) ->
+  let tysubst = Array.init prms (fun _ -> fresh_id env) in
+  let tysubst i = GTypVar tysubst.(i) in
+  let ty = subst_type tysubst ty in
+  let ty = match tycon with
+    | None -> ty
+    | Some tycon ->
+      let () = unify ?loc env ty tycon in
+      tycon
+  in
+  let args = List.map (fun (na, arg, ty) ->
+      let ty = Option.map (subst_type tysubst) ty in
+      let () = match na.CAst.v, ty with
+        | Anonymous, None | Name _, Some _ -> ()
+        | Anonymous, Some _ | Name _, None -> assert false
+      in
+      let e, _ = intern_rec env ty arg in
+      na.CAst.v, e)
+      args
+  in
+  if CList.is_empty args then body, ty
+  else GTacLet (false, args, body), ty
 
 and intern_rec_with_constraint env e exp =
   let (er, t) = intern_rec env (Some exp) e in
@@ -1592,8 +1632,7 @@ let globalize_gen ~tacext ids tac =
       let bnd = List.map map bnd in
       CAst.make ?loc @@ CTacLet (isrec, bnd, e)
     | CTacSyn (el, kn) ->
-      let body = Tac2env.interp_notation kn in
-      let v = if CList.is_empty el then body else CAst.make ?loc @@ CTacLet(false, el, body) in
+      let v = expand_notation ?loc el kn in
       globalize ids v
     | CTacCnv (e, t) ->
       let e = globalize ids e in
@@ -1629,6 +1668,9 @@ let globalize_gen ~tacext ids tac =
       let e' = globalize ids e' in
       CAst.make ?loc @@ CTacSet (e, AbsKn p, e')
     | CTacExt (tag, arg) -> tacext ?loc (RawExt (tag, arg))
+    | CTacGlb (prms, args, body, ty) ->
+      let args = List.map (fun (na, arg, ty) -> na, globalize ids arg, ty) args in
+      CAst.make ?loc @@ CTacGlb (prms, args, body, ty)
 
   and globalize_case ids (p, e) =
     (globalize_pattern ids p, globalize ids e)
@@ -1670,6 +1712,35 @@ let debug_globalize_allow_ext ids tac =
   let tacext ?loc (RawExt (tag,arg)) = CAst.make ?loc @@ CTacExt (tag,arg) in
   globalize_gen ~tacext ids tac
 
+let { Goptions.get = typed_notations } =
+  Goptions.declare_bool_option_and_ref
+    ~key:["Ltac2";"Typed";"Notations"] ~value:true ()
+
+let intern_notation_data ids body =
+  if typed_notations () then
+    let env = empty_env ~strict:true () in
+    let fold id (env,argtys) =
+      let ty = GTypVar (fresh_id env) in
+      let env = push_name (Name id) (monomorphic ty) env in
+      env, Id.Map.add id ty argtys
+    in
+    let env, argtys = Id.Set.fold fold ids (env,Id.Map.empty) in
+    let body, ty = intern_rec env None body in
+    let count = ref 0 in
+    let vars = ref TVar.Map.empty in
+    let argtys = Id.Map.map (fun ty -> normalize env (count, vars) ty) argtys in
+    let ty = normalize env (count, vars) ty in
+    let prms = !count in
+    Tac2env.TypedNota {
+      nota_prms = prms;
+      nota_argtys = argtys;
+      nota_ty = ty;
+      nota_body = body;
+    }
+  else
+    let body = globalize ids body in
+    Tac2env.UntypedNota body
+
 (** Kernel substitution *)
 
 open Mod_subst
@@ -1924,6 +1995,18 @@ let rec subst_rawexpr subst ({loc;v=tr} as t) = match tr with
     let e' = subst_rawexpr subst e in
     let r' = subst_rawexpr subst r in
     if prj' == prj && e' == e && r' == r then t else CAst.make ?loc @@ CTacSet (e', prj', r')
+| CTacGlb (prms, args, body, ty) ->
+  let args' = List.Smart.map (fun (na, arg, ty as o) ->
+      let arg' = subst_rawexpr subst arg in
+      let ty' = Option.Smart.map (subst_type subst) ty in
+      if arg' == arg && ty' == ty then o
+      else (na, arg', ty'))
+      args
+  in
+  let body' = subst_expr subst body in
+  let ty' = subst_type subst ty in
+  if args' == args && body' == body && ty' == ty then t
+  else CAst.make ?loc @@ CTacGlb (prms, args', body', ty')
 | CTacSyn _ | CTacExt _ -> assert false (** Should not be generated by globalization *)
 
 (** Registering *)

plugins/ltac2/tac2intern.mli

@@ -17,6 +17,7 @@ type context = (Id.t * type_scheme) list
 val intern : strict:bool -> context -> raw_tacexpr -> glb_tacexpr * type_scheme
 val intern_typedef : (KerName.t * int) Id.Map.t -> raw_quant_typedef -> glb_quant_typedef
 val intern_open_type : raw_typexpr -> type_scheme
+val intern_notation_data : Id.Set.t -> raw_tacexpr -> Tac2env.notation_data
 
 (** Check that a term is a value. Only values are safe to marshall between
     processes. *)