Coq中是否可以声明依赖类型的可重载Notation记法？

Coq完全支持你需要的基于变量类型的记法重载，官方最推荐的实现方案是记法作用域（Notation Scope），也可以用类型类实现更自动的隐式重载。

方案1：记法作用域（官方推荐） #

这个方案的核心是把相同符号的不同定义绑定到不同的作用域，再将作用域和对应类型做绑定，Coq的类型推断会自动根据项的类型启用对应作用域的记法规则，不会出现符号重定义冲突。
完整实现示例如下：

(* 定义基础类型 *)
Inductive type: Type := 
  | tbase : nat -> type
  | tpair: type -> type -> type.

Inductive expr: Type := 
  | ebase : nat -> expr
  | epair: expr -> expr -> expr.

(* 绑定type类型的记法作用域 *)
Declare Scope type_scope.
Delimit Scope type_scope with T.
Notation "{ t1 , t2 }" := (tpair t1 t2) : type_scope.
Bind Scope type_scope with type. (* 所有type类型的项默认启用该作用域 *)

(* 绑定expr类型的记法作用域 *)
Declare Scope expr_scope.
Delimit Scope expr_scope with E.
Notation "{ e1 , e2 }" := (epair e1 e2) : expr_scope.
Bind Scope expr_scope with expr. (* 所有expr类型的项默认启用该作用域 *)

使用时绝大多数场景可以靠Coq类型推断自动匹配记法规则：

(* 自动识别为tpair构造器 *)
Check fun (A B : type) => {A, B} : type.
(* 自动识别为epair构造器 *)
Check fun (a b : expr) => {a, b} : expr.

遇到类型推断上下文不足的场景，也可以手动加作用域分隔符强制指定：

(* 强制使用type作用域的记法 *)
Check {tbase 1, tbase 2}%T.
(* 强制使用expr作用域的记法 *)
Check {ebase 1, ebase 2}%E.

方案2：类型类实现全自动重载 #

如果你需要完全无标注的自动重载，也可以通过类型类实现：

(* 定义重载的类型类 *)
Class Pair (A : Type) := pair : A -> A -> A.

(* 注册不同类型的实现 *)
Instance pair_type : Pair type := tpair.
Instance pair_expr : Pair expr := epair.

(* 全局定义统一记法 *)
Notation "{ x , y }" := (pair x y).

该方案下Coq会根据参数的类型自动匹配对应的类型类实例，不需要手动标注作用域，更适合重载的操作语义一致的场景。

内容的提问来源于stack exchange，提问作者Damián Ferencz