Trying out herbelin's suggestion in https://github.com/coq/coq/issues/11998#issuecomment-607773624

ring4.v

From mathcomp Require Import ssreflect ssrnat eqtype ssrbool ssrnum ssralg.
Require Import Ring.

Import GRing.Theory.
Open Scope ring_scope.

Section foo.
(* Variant of the same problem. *)
(* Variable R: numFieldType. *)

Variable R: comRingType.
Locate "+".

Lemma check_defeq: GRing.Zmodule.sort R = GRing.ComRing.sort R. done. Qed.

Locate "+%R".
Check +%R.

(* Definition addT : R -> R -> R := +%R.
Local Infix "+" := addT. *)

Definition rt :
  (* @ring_theory (GRing.ComRing.sort R) 0%:R 1%:R addT *%R (fun a b => a - b) -%R eq. *)
  @ring_theory (GRing.Zmodule.sort R) 0%:R 1%:R +%R *%R (fun a b => a - b) -%R eq.
  (* Doesn't work.*)
  (* @ring_theory R 0%:R 1%:R +%R *%R (fun a b => a - b) -%R eq. *)
  (* Works. *)
  (* @ring_theory R 0%:R 1%:R addT *%R (fun a b => a - b) -%R eq. *)
Proof.
  apply mk_rt.
  - apply add0r.
  - apply addrC.
  - apply addrA.
  - apply mul1r.
  - apply mulrC.
  - apply mulrA.
  - apply mulrDl.
  - by [].
  - apply subrr.
Qed.
Add Ring Ringgg : rt.

Lemma tmp2:
    forall x y: R, eq (x + y) (y + x).
Proof. move => x y. ring. Qed.