optimizations

[gares]

the first one brings down the last instance in ssralg to 0.4s, slow but tolerable.
the second one is just to avoid being silly and store s.phant_Build crap instead of s.Build less crap, it does not impact performances too much for not.

I believe the root problem is still there:

Set Printing All. Print prod_is_a_Ring.
(*
prod_is_a_Ring = 
@Ring.Pack (prod (Ring.sort R1) (Ring.sort R2))
  (@Ring.Class (prod (Ring.sort R1) (Ring.sort R2))
	 (HB_unnamed_factory_105 (Ring_to_Zmodule R1) (Ring_to_Zmodule R2))
     (prod_eqMixin
        (Choice_to_Equality (Zmodule_to_Choice (Ring_to_Zmodule R1)))
        (Choice_to_Equality (Zmodule_to_Choice (Ring_to_Zmodule R2))))
     (prod_choiceMixin (Zmodule_to_Choice (Ring_to_Zmodule R1))
        (Zmodule_to_Choice (Ring_to_Zmodule R2))) HB_unnamed_factory_107)
     : Ring.type
*)

This instance is where the "coercion chain problem" pops up and is still manageable, hence were we can debug it.
(FTR: before this PR this term was already gigantic and contained phant_Build crap)

CC @CohenCyril @pi8027

[CohenCyril]

LGTM

[gares]

Do you agree that the coercion problem is still there?

[CohenCyril]

I did not check yet... but from the big term you showed, it seems so...

[gares]

in the term above, the small but not optimal one

[CohenCyril]

Maybe we should reverse the list of coercion declaration?

[gares]

IMO it is mixin-src / mterm->term which does things in the wrong order

[gares]

or maybe not, but the coercion order seems OK according to @pi8027

[CohenCyril]

and you saw that thanks to the logger?

[gares]

Print Graph.