locking definitions to address `integral.v` divergence

Line 426 in `integral.v` diverged to over 40 minutes with the new
`finfun.v`, because matching `mod_Iirr` to `quo_Iirr` goes into
exponential backtracking. This is currently averted by limiting the
repetition of `mod_IirrE` in this `rewrite` line.
Making `finfun` mixing opaque brings this down to 40 seconds, and
locking `cfIirr` to a tractable 0.15 seconds, hopefully improving the
instances. This line also takes 47 seconds to execute in the master
branch, so this is likely an undetected Coq performance regression.

2 files changed, 25 insertions, 22 deletions

diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v
index 783c46f..eda6f5a 100644
--- a/mathcomp/character/character.v
+++ b/mathcomp/character/character.v
@@ -667,11 +667,13 @@ Proof. by rewrite eqr_le ltr_geF ?irr1_gt0. Qed.
 Lemma irr_neq0 i : 'chi_i != 0.
 Proof. by apply: contraNneq (irr1_neq0 i) => ->; rewrite cfunE. Qed.
 
-Definition cfIirr B (chi : 'CF(B)) : Iirr B := inord (index chi (irr B)).
+Local Remark cfIirr_key : unit. Proof. by []. Qed.
+Definition cfIirr : forall B, 'CF(B) -> Iirr B :=
+  locked_with cfIirr_key (fun B chi => inord (index chi (irr B))).
 
 Lemma cfIirrE chi : chi \in irr G -> 'chi_(cfIirr chi) = chi.
 Proof.
-move=> chi_irr; rewrite (tnth_nth 0) inordK ?nth_index //.
+move=> chi_irr; rewrite (tnth_nth 0) [cfIirr]unlock inordK ?nth_index //.
 by rewrite -index_mem size_tuple in chi_irr.
 Qed.
 
diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v
index 9a8c723..db03671 100644
--- a/mathcomp/ssreflect/finfun.v
+++ b/mathcomp/ssreflect/finfun.v
@@ -239,34 +239,35 @@ Notation family F := (family_mem (fmem F)).
 Section InheritedStructures.
 
 Variable aT : finType.
+Notation dffun_aT rT rS := {dffun forall x : aT, rT x : rS}.
 
-Definition finfun_eqMixin (rT : _ -> eqType) :=
-  @PcanEqMixin {dffun finPi aT rT} _ _ _ tfgraphK.
+Local Remark eqMixin rT : Equality.mixin_of (dffun_aT rT eqType).
+Proof. exact: PcanEqMixin tfgraphK. Qed.
 Canonical finfun_eqType (rT : eqType) :=
-  EqType {ffun aT -> rT} (finfun_eqMixin _).
-Canonical dfinfun_eqType (rT : _ -> eqType) :=
-  EqType {dffun finPi aT rT} (finfun_eqMixin _).
+  EqType {ffun aT -> rT} (eqMixin (fun=> rT)).
+Canonical dfinfun_eqType rT :=
+  EqType (dffun_aT rT eqType) (eqMixin rT).
 
-Definition finfun_choiceMixin (rT : _ -> choiceType) :=
-  @PcanChoiceMixin _ {dffun finPi aT rT} _ _ tfgraphK.
+Local Remark choiceMixin rT : Choice.mixin_of (dffun_aT rT choiceType).
+Proof. exact: PcanChoiceMixin tfgraphK. Qed.
 Canonical finfun_choiceType (rT : choiceType) :=
-  ChoiceType {ffun aT -> rT} (finfun_choiceMixin _).
-Canonical dfinfun_choiceType (rT : _ -> choiceType) :=
-  ChoiceType {dffun finPi aT _} (finfun_choiceMixin rT).
+  ChoiceType {ffun aT -> rT} (choiceMixin (fun=> rT)).
+Canonical dfinfun_choiceType rT :=
+  ChoiceType (dffun_aT rT choiceType) (choiceMixin rT).
 
-Definition finfun_countMixin (rT : _ -> countType) :=
-  @PcanCountMixin _ {dffun finPi aT rT} _ _ tfgraphK.
+Local Remark countMixin rT : Countable.mixin_of (dffun_aT rT countType).
+Proof. exact: PcanCountMixin tfgraphK. Qed.
 Canonical finfun_countType (rT : countType) :=
-  CountType {ffun aT -> rT} (finfun_countMixin _).
-Canonical dfinfun_countType (rT : _ -> countType) :=
-  CountType {dffun finPi aT rT} (finfun_countMixin _).
+  CountType {ffun aT -> rT} (countMixin (fun => rT)).
+Canonical dfinfun_countType rT :=
+  CountType (dffun_aT rT countType) (countMixin rT).
 
-Definition finfun_finMixin (rT : _ -> finType) :=
-  @PcanFinMixin (dfinfun_countType rT) _ _ _ tfgraphK.
+Local Definition finMixin rT :=
+  PcanFinMixin (tfgraphK : @pcancel _ (dffun_aT rT finType) _ _).
 Canonical finfun_finType (rT : finType) :=
-  FinType {ffun aT -> rT} (finfun_finMixin _).
-Canonical dfinfun_finType (rT : _ -> finType) :=
-  FinType {dffun finPi aT rT} (finfun_finMixin _).
+  FinType {ffun aT -> rT} (finMixin (fun=> rT)).
+Canonical dfinfun_finType rT :=
+  FinType (dffun_aT rT finType) (finMixin rT).
 
 End InheritedStructures.