perf: compact normal form of CommAlgebra baseChange

[plt-amy]

The module ….FreeCommAlgebra.OnCoproduct spends almost 10s conversion-checking the reduct of R[I][J], incl. 7s doing this in the definition of from' alone. My surgical {-# INLINE #-} pragma placement cuts the total runtime of checking OnCoproduct to less than a second.

Before:

Checking Cubical.Algebra.CommAlgebra.AsModule.FreeCommAlgebra.OnCoproduct (...).
Total                                  12,522ms           
Miscellaneous                              14ms           
Typing                                      0ms (11,565ms)
Typing.CheckRHS                        10,325ms           
Typing.TypeSig                            934ms           
Typing.Generalize                         199ms           
Deserialization                           787ms           

After:

Checking Cubical.Algebra.CommAlgebra.AsModule.FreeCommAlgebra.OnCoproduct (...).
Total                                  1,569ms        
Miscellaneous                             14ms        
Deserialization                          783ms        
Typing                                     0ms (687ms)
Typing.CheckRHS                          562ms        
Typing.TypeSig                            53ms        
Typing.Generalize                         18ms        

[plt-amy]

I just remembered that I had copy-pasted the old normal form into a gist but forgot to actually share. I recommend safety glasses