Ltac2 abbreviations typecheck at declaration time

dev/ci/user-overlays/21617-SkySkimmer-tac2abbrev-up.sh

@@ -0,0 +1 @@
+overlay ltac2_compiler https://github.com/SkySkimmer/coq-ltac2-compiler tac2abbrev-up 21617

doc/changelog/06-Ltac2-language/21617-tac2abbrev-up-Added.rst

@@ -0,0 +1,6 @@
+- **Added:**
+  :cmd:`Ltac2 Abbreviation` typecheck the body at declaration time instead of when they are used.
+  This means incorrect abbreviations produce errors at declaration time, and also means quotations may be used inside abbreviations
+  (e.g. `Ltac2 Abbreviation foo := @foo.`)
+  (`#21617 <https://github.com/rocq-prover/rocq/pull/21617>`_,
+  by Gaëtan Gilbert).

doc/sphinx/proof-engine/ltac2.rst

@@ -1432,8 +1432,10 @@ Abbreviations
 
    :n:`foo 0 ↦ (fun x => x ()) (fun _ => 0)`
 
-   Note that abbreviations are not type checked at all, and may result in typing
-   errors after expansion.
+   Abbreviations are typechecked at declaration time regardless of
+   :flag:`Ltac2 Typed Notations`. Unlike notations, this does not lose
+   any generality because they expand to applications instead of
+   letins.
 
    This command supports the :attr:`deprecated` attribute.
 

plugins/ltac2/tac2entries.ml

@@ -604,29 +604,25 @@ let import_type qid as_id =
 
 (** {5 Parsing} *)
 
-type abbreviation = {
-  abbr_body : raw_tacexpr;
-  abbr_depr : Deprecation.t option;
-}
-
 let perform_abbreviation visibility ((sp, kn), abbr) =
-  let () = Tac2env.push_ltac visibility sp (TacAlias kn) in
-  Tac2env.define_alias ?deprecation:abbr.abbr_depr kn abbr.abbr_body
+  let () = Tac2env.push_ltac visibility sp (TacAbbrev kn) in
+  Tac2env.define_abbrev kn abbr
 
 let load_abbreviation i obj = perform_abbreviation (Until i) obj
 let open_abbreviation i obj = perform_abbreviation (Exactly i) obj
 
 let cache_abbreviation ((sp, kn), abbr) =
-  let () = Tac2env.push_ltac (Until 1) sp (TacAlias kn) in
-  Tac2env.define_alias ?deprecation:abbr.abbr_depr kn abbr.abbr_body
+  let () = Tac2env.push_ltac (Until 1) sp (TacAbbrev kn) in
+  Tac2env.define_abbrev kn abbr
 
 let subst_abbreviation (subst, abbr) =
-  let body' = subst_rawexpr subst abbr.abbr_body in
-  if body' == abbr.abbr_body then abbr
-  else { abbr_body = body'; abbr_depr = abbr.abbr_depr }
+  let open Tac2env in
+  let ty' = subst_type subst abbr.abbrev_ty in
+  let body' = subst_expr subst abbr.abbrev_body in
+  if ty' == abbr.abbrev_ty && body' == abbr.abbrev_body then abbr
+  else { abbr with abbrev_body = body'; abbrev_ty = ty'; }
 
-let inTac2Abbreviation : Id.t -> abbreviation -> Libobject.obj =
-  let open Libobject in
+let inTac2Abbreviation : Id.t -> Tac2env.abbrev_data -> obj =
   declare_named_object {(default_object "TAC2-ABBREVIATION") with
      cache_function  = cache_abbreviation;
      load_function   = load_abbreviation;
@@ -672,8 +668,7 @@ let register_notation atts tkn target body =
 
 let register_notation_interpretation = function
   | Abbreviation (id, deprecation, body) ->
-    let body = Tac2intern.globalize Id.Set.empty body in
-    let abbr = { abbr_body = body; abbr_depr = deprecation } in
+    let abbr = Tac2intern.intern_abbrev deprecation body in
     Lib.add_leaf (inTac2Abbreviation id abbr)
   | Synext data ->
     let data = Tac2syn.intern_notation_interpretation intern_notation_data data in
@@ -753,7 +748,7 @@ let register_redefinition ~local qid old ({loc=eloc} as e) =
   in
   let kn = match kn with
   | TacConstant kn -> kn
-  | TacAlias _ ->
+  | TacAbbrev _ ->
     user_err ?loc:qid.CAst.loc (str "Cannot redefine syntactic abbreviations")
   in
   let data = Tac2env.interp_global kn in
@@ -995,10 +990,10 @@ let print_tacref ~print_def qid = function
     let data = Tac2env.interp_global kn in
     let info = Option.map fst (Tac2env.get_compiled_global kn) in
     print_constant ~print_def qid data ?info
-  | TacAlias kn ->
-    let { Tac2env.alias_body = body } = Tac2env.interp_alias kn in
+  | TacAbbrev kn ->
+    let { Tac2env.abbrev_body = body } = Tac2env.interp_abbrev kn in
     str "Notation" ++ spc() ++ pr_qualid qid ++ str " :=" ++ spc()
-    ++ Tac2print.pr_rawexpr_gen E5 ~avoid:Id.Set.empty body
+    ++ Tac2print.pr_glbexpr_gen E5 ~avoid:Id.Set.empty body
 
 let print_constructor qid kn =
   let cdata = Tac2env.interp_constructor kn in
@@ -1051,7 +1046,7 @@ let () =
     let hdr = match kn with
       | Type _ -> str "Ltac2 Type"
       | TacRef (TacConstant _) -> str "Ltac2"
-      | TacRef (TacAlias _) -> str "Ltac2 Notation"
+      | TacRef (TacAbbrev _) -> str "Ltac2 Notation"
       | Constructor _ -> str "Ltac2 Constructor"
     in
     hdr ++ spc () ++ pr_path (path_of_object kn)

plugins/ltac2/tac2env.ml

@@ -37,25 +37,27 @@ type projection_data = {
   pdata_indx : int;
 }
 
-type alias_data = {
-  alias_body : raw_tacexpr;
-  alias_depr : Deprecation.t option;
+type abbrev_data = {
+  abbrev_prms : int;
+  abbrev_ty : int glb_typexpr;
+  abbrev_body : glb_tacexpr;
+  abbrev_depr : Deprecation.t option;
 }
 
 type ltac_state = {
   ltac_tactics : global_data KerName.Map.t;
   ltac_constructors : constructor_data KerName.Map.t;
   ltac_projections : projection_data KerName.Map.t;
   ltac_types : glb_quant_typedef KerName.Map.t;
-  ltac_aliases : alias_data KerName.Map.t;
+  ltac_abbrevs : abbrev_data KerName.Map.t;
 }
 
 let empty_state = {
   ltac_tactics = KerName.Map.empty;
   ltac_constructors = KerName.Map.empty;
   ltac_projections = KerName.Map.empty;
   ltac_types = KerName.Map.empty;
-  ltac_aliases = KerName.Map.empty;
+  ltac_abbrevs = KerName.Map.empty;
 }
 
 type compile_info = {
@@ -106,12 +108,11 @@ let define_type kn e =
 
 let interp_type kn = KerName.Map.find kn ltac_state.contents.ltac_types
 
-let define_alias ?deprecation kn tac =
+let define_abbrev kn data =
   let state = !ltac_state in
-  let data = { alias_body = tac; alias_depr = deprecation } in
-  ltac_state := { state with ltac_aliases = KerName.Map.add kn data state.ltac_aliases }
+  ltac_state := { state with ltac_abbrevs = KerName.Map.add kn data state.ltac_abbrevs }
 
-let interp_alias kn = KerName.Map.find kn ltac_state.contents.ltac_aliases
+let interp_abbrev kn = KerName.Map.find kn ltac_state.contents.ltac_abbrevs
 
 module ML =
 struct
@@ -138,16 +139,16 @@ let interp_primitive name = MLMap.find name !primitive_map
 
 type tacref = Tac2expr.tacref =
 | TacConstant of ltac_constant
-| TacAlias of ltac_alias
+| TacAbbrev of ltac_abbrev
 
 module TacRef =
 struct
 type t = tacref
 let compare r1 r2 = match r1, r2 with
 | TacConstant c1, TacConstant c2 -> KerName.compare c1 c2
-| TacAlias c1, TacAlias c2 -> KerName.compare c1 c2
-| TacConstant _, TacAlias _ -> -1
-| TacAlias _, TacConstant _ -> 1
+| TacAbbrev c1, TacAbbrev c2 -> KerName.compare c1 c2
+| TacConstant _, TacAbbrev _ -> -1
+| TacAbbrev _, TacConstant _ -> 1
 
 let equal r1 r2 = compare r1 r2 == 0
 end

plugins/ltac2/tac2env.mli

@@ -83,15 +83,17 @@ type projection_data = {
 val define_projection : ltac_projection -> projection_data -> unit
 val interp_projection : ltac_projection -> projection_data
 
-(** {5 Toplevel definition of aliases} *)
+(** {5 Toplevel definition of abbreviations} *)
 
-type alias_data = {
-  alias_body : raw_tacexpr;
-  alias_depr : Deprecation.t option;
+type abbrev_data = {
+  abbrev_prms : int;
+  abbrev_ty : int glb_typexpr;
+  abbrev_body : glb_tacexpr;
+  abbrev_depr : Deprecation.t option;
 }
 
-val define_alias : ?deprecation:Deprecation.t -> ltac_constant -> raw_tacexpr -> unit
-val interp_alias : ltac_constant -> alias_data
+val define_abbrev : ltac_constant -> abbrev_data -> unit
+val interp_abbrev : ltac_constant -> abbrev_data
 
 (** {5 Name management} *)
 

plugins/ltac2/tac2expr.mli

@@ -18,15 +18,15 @@ type lid = Id.t
 type uid = Id.t
 
 type ltac_constant = KerName.t
-type ltac_alias = KerName.t
+type ltac_abbrev = KerName.t
 type ltac_notation = KerName.t
 type ltac_constructor = KerName.t
 type ltac_projection = KerName.t
 type type_constant = KerName.t
 
 type tacref =
 | TacConstant of ltac_constant
-| TacAlias of ltac_alias
+| TacAbbrev of ltac_abbrev
 
 type 'a or_relid =
 | RelId of qualid

plugins/ltac2/tac2intern.ml

@@ -287,19 +287,19 @@ let expand_pattern avoid bnd =
   let nas = List.rev_map (fun (na, _, _) -> na) bnd in
   (nas, expand)
 
-let is_alias env qid = match get_variable env qid with
-| ArgArg (TacAlias _) -> true
+let is_abbrev env qid = match get_variable env qid with
+| ArgArg (TacAbbrev _) -> true
 | ArgVar _ | (ArgArg (TacConstant _)) -> false
 
 let is_user_name qid = match qid with
 | AbsKn _ -> false
 | RelId _ -> true
 
-let deprecated_ltac2_alias =
+let deprecated_ltac2_abbrev =
   Deprecation.create_warning
     ~object_name:"Ltac2 abbreviation"
     ~warning_name_if_no_since:"deprecated-ltac2-abbreviation"
-    (fun kn -> pr_qualid (Tac2env.shortest_qualid_of_ltac Id.Set.empty (TacAlias kn)))
+    (fun kn -> pr_qualid (Tac2env.shortest_qualid_of_ltac Id.Set.empty (TacAbbrev kn)))
 
 let deprecated_ltac2_def =
   Deprecation.create_warning
@@ -309,10 +309,10 @@ let deprecated_ltac2_def =
 
 let check_deprecated_ltac2 ?loc qid def =
   if is_user_name qid then match def with
-  | TacAlias kn ->
-    begin match (Tac2env.interp_alias kn).alias_depr with
+  | TacAbbrev kn ->
+    begin match (Tac2env.interp_abbrev kn).abbrev_depr with
     | None -> ()
-    | Some depr -> deprecated_ltac2_alias ?loc (kn, depr)
+    | Some depr -> deprecated_ltac2_abbrev ?loc (kn, depr)
     end
   | TacConstant kn ->
     begin match (Tac2env.interp_global kn).gdata_deprecation with
@@ -1113,6 +1113,14 @@ 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_abbrev ?loc kn =
+  let e =
+    try Tac2env.interp_abbrev kn
+    with Not_found ->
+      CErrors.anomaly (str "Missing hardwired abbrev " ++ KerName.print kn)
+  in
+  CAst.make ?loc @@ CTacGlb (e.abbrev_prms, [], e.abbrev_body, e.abbrev_ty)
+
 let expand_notation ?loc scopes syn =
   let data, el = Tac2syn.interp_notation ?loc scopes syn in
   match data with
@@ -1179,14 +1187,10 @@ let rec intern_rec env tycon {loc;v=e} =
     in
     let () = check_deprecated_ltac2 ?loc qid (TacConstant kn) in
     check (GTacRef kn, fresh_type_scheme env sch)
-  | ArgArg (TacAlias kn) ->
-    let e =
-      try Tac2env.interp_alias kn
-      with Not_found ->
-        CErrors.anomaly (str "Missing hardwired alias " ++ KerName.print kn)
-    in
-    let () = check_deprecated_ltac2 ?loc qid (TacAlias kn) in
-    intern_rec env tycon e.alias_body
+  | ArgArg (TacAbbrev kn) ->
+    let e = expand_abbrev ?loc kn in
+    let () = check_deprecated_ltac2 ?loc qid (TacAbbrev kn) in
+    intern_rec env tycon e
   end
 | CTacCst qid ->
   let kn = get_constructor env qid in
@@ -1217,22 +1221,22 @@ let rec intern_rec env tycon {loc;v=e} =
 | CTacApp ({loc;v=CTacCst qid}, args) ->
   let kn = get_constructor env qid in
   intern_constructor env loc tycon kn args
-| CTacApp ({v=CTacRef qid; loc=aloc}, args) when is_alias env qid ->
+| CTacApp ({v=CTacRef qid; loc=aloc}, args) when is_abbrev env qid ->
   let kn = match get_variable env qid with
-  | ArgArg (TacAlias kn) -> kn
+  | ArgArg (TacAbbrev kn) -> kn
   | ArgVar _ | (ArgArg (TacConstant _)) -> assert false
   in
-  let e = Tac2env.interp_alias kn in
-  let () = check_deprecated_ltac2 ?loc:aloc qid (TacAlias kn) in
+  let e = expand_abbrev ?loc:aloc kn in
+  let () = check_deprecated_ltac2 ?loc:aloc qid (TacAbbrev kn) in
   let map arg =
-    (* Thunk alias arguments *)
+    (* Thunk abbrev arguments *)
     let loc = arg.loc in
     let t_unit = CAst.make ?loc @@ CTypRef (AbsKn (Tuple 0), []) in
     let var = CAst.make ?loc @@ CPatCnv (CAst.make ?loc @@ CPatVar Anonymous, t_unit) in
     CAst.make ?loc @@ CTacFun ([var], arg)
   in
   let args = List.map map args in
-  intern_rec env tycon (CAst.make ?loc @@ CTacApp (e.alias_body, args))
+  intern_rec env tycon (CAst.make ?loc @@ CTacApp (e, args))
 | CTacApp (f, args) ->
   let loc = f.loc in
   let (f, ft) = intern_rec env None f in
@@ -1797,6 +1801,19 @@ let globalize ids tac =
   in
   globalize_gen ~tacext ids tac
 
+let intern_abbrev depr body =
+  let env = empty_env ~strict:true UnivNames.empty_binders () in
+  let body, ty = intern_rec env None body in
+  let count = ref 0 in
+  let vars = ref TVar.Map.empty in
+  let ty = normalize env (count, vars) ty in
+  let prms = !count in
+  { abbrev_body = body;
+    abbrev_ty = ty;
+    abbrev_prms = prms;
+    abbrev_depr = depr;
+  }
+
 let { Goptions.get = typed_notations } =
   Goptions.declare_bool_option_and_ref
     ~key:["Ltac2";"Typed";"Notations"] ~value:true ()

plugins/ltac2/tac2intern.mli

@@ -17,6 +17,7 @@ val intern : strict:bool -> UnivNames.universe_binders -> context -> raw_tacexpr
 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 -> Tac2syn.notation_data
+val intern_abbrev : Deprecation.t option -> raw_tacexpr -> Tac2env.abbrev_data
 
 val intern_accumulate_errors : strict:bool -> context -> raw_tacexpr ->
   glb_tacexpr * type_scheme * Pp.t Loc.located list
@@ -55,12 +56,6 @@ val check_subtype : type_scheme -> type_scheme -> bool
 (** [check_subtype t1 t2] returns [true] iff all values of instances of type [t1]
     also have type [t2]. *)
 
-(** {5 Notations} *)
-
-val globalize : Id.Set.t -> raw_tacexpr -> raw_tacexpr
-(** Replaces all qualified identifiers by their corresponding kernel name. The
-    set represents bound variables in the context. *)
-
 (** Errors *)
 
 val error_nargs_mismatch : ?loc:Loc.t -> ltac_constructor -> int -> int -> 'a

plugins/ltac2/tac2print.ml

@@ -590,7 +590,7 @@ let pr_rawexpr_gen lvl ~avoid c =
   | CTacAtm a -> pr_atom a
   | CTacRef (RelId qid) -> Libnames.pr_qualid qid
   | CTacRef (AbsKn (TacConstant r)) -> pr_tacref avoid r
-  | CTacRef (AbsKn (TacAlias _ as r)) -> Libnames.pr_qualid (Tac2env.shortest_qualid_of_ltac avoid r)
+  | CTacRef (AbsKn (TacAbbrev _ as r)) -> Libnames.pr_qualid (Tac2env.shortest_qualid_of_ltac avoid r)
   | CTacCst (RelId qid) -> Libnames.pr_qualid qid
   | CTacCst (AbsKn (Tuple 0)) -> str "()"
   | CTacCst (AbsKn (Tuple n)) -> CErrors.anomaly ?loc Pp.(str "Incorrect tuple.")

plugins/ltac2/tac2subst.ml

@@ -161,9 +161,9 @@ let subst_tacref subst ref = match ref with
 | AbsKn (TacConstant kn) ->
   let kn' = subst_kn subst kn in
   if kn' == kn then ref else AbsKn (TacConstant kn')
-| AbsKn (TacAlias kn) ->
+| AbsKn (TacAbbrev kn) ->
   let kn' = subst_kn subst kn in
-  if kn' == kn then ref else AbsKn (TacAlias kn')
+  if kn' == kn then ref else AbsKn (TacAbbrev kn')
 
 let subst_projection subst prj = match prj with
 | RelId _ -> prj

test-suite/output/ltac2_printabout.out

@@ -13,7 +13,7 @@ Inr : 'b -> ('a, 'b) either
 Triple : 'c -> 'b -> 'a -> ('a, 'b, 'c) triple
 Not_found : exn
 Out_of_bounds : message option -> exn
-Ltac2 Notation nota := () ()
+Ltac2 Notation nota := fun thunk => thunk ()
 Ltac2 Type constr
 Ltac2 Type constr := Init.constr
 ('a, 'b) thing := 'b option

test-suite/output/ltac2_printabout.v

@@ -31,7 +31,7 @@ Print Ltac2 Out_of_bounds.
 
 (* alias *)
 
-Ltac2 Abbreviation nota := () ().
+Ltac2 Abbreviation nota := fun thunk => thunk ().
 
 Print nota.