Merge pull request #242 from anton-trunov/remove-canonical-for-mixins

Document and review the usage of canonical Equality mixins

1 files changed, 6 insertions, 1 deletions

diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v
index 64585f6..38e3dbe 100644
--- a/mathcomp/ssreflect/tuple.v
+++ b/mathcomp/ssreflect/tuple.v
@@ -360,7 +360,12 @@ Section UseFinTuple.
 
 Variables (n : nat) (T : finType).
 
-Canonical tuple_finMixin := Eval hnf in FinMixin (@FinTuple.enumP n T).
+(* tuple_finMixin could, in principle, be made Canonical to allow for folding *)
+(* Finite.enum of a finite tuple type (see comments around eqE in eqtype.v),  *)
+(* but in practice it will not work because the mixin_enum projector          *)
+(* has been burried under an opaque alias, to avoid some performance issues   *)
+(* during type inference.                                                     *)
+Definition tuple_finMixin := Eval hnf in FinMixin (@FinTuple.enumP n T).
 Canonical tuple_finType := Eval hnf in FinType (n.-tuple T) tuple_finMixin.
 Canonical tuple_subFinType := Eval hnf in [subFinType of n.-tuple T].